diff --git a/echidna-playground/rescript.json b/echidna-playground/rescript.json deleted file mode 100644 index 60b67830..00000000 --- a/echidna-playground/rescript.json +++ /dev/null @@ -1,20 +0,0 @@ -{ - "name": "coq-jr", - "sources": [ - { - "dir": "src", - "subdirs": true - } - ], - "package-specs": [ - { - "module": "esmodule", - "in-source": true - } - ], - "suffix": ".res.js", - "bs-dependencies": [], - "warnings": { - "error": "+101" - } -} diff --git a/echidna-playground/src/Components.affine b/echidna-playground/src/Components.affine new file mode 100644 index 00000000..0b6099f8 --- /dev/null +++ b/echidna-playground/src/Components.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Components; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Components.res b/echidna-playground/src/Components.res deleted file mode 100644 index 8beb3ab4..00000000 --- a/echidna-playground/src/Components.res +++ /dev/null @@ -1,174 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// UI Components for jsCoq - -module Html = { - let element = (tag: string, ~className="", ~id="", children: array): string => { - let classAttr = className != "" ? ` class="${className}"` : "" - let idAttr = id != "" ? ` id="${id}"` : "" - let content = Js.Array2.joinWith(children, "") - `<${tag}${idAttr}${classAttr}>${content}` - } - - let div = element("div", ...) - let span = element("span", ...) - let p = element("p", ...) - let h3 = element("h3", ...) - let h4 = element("h4", ...) - let h5 = element("h5", ...) - let ul = element("ul", ...) - let li = element("li", ...) - let a = (~href: string, text: string): string => `${text}` - let img = (~src: string, ~height: string, ~alt=""): string => - `${alt}` - let kbd = (text: string): string => `${text}` - let code = (text: string): string => `${text}` - let em = (text: string): string => `${text}` - let i = (text: string): string => `${text}` - let hr = (): string => `
` - let br = (): string => `
` - - let textarea = (~id: string, content: string): string => - `` - - let table = (~className="", rows: array): string => { - let classAttr = className != "" ? ` class="${className}"` : "" - `${Js.Array2.joinWith(rows, "")}` - } - - let tr = (cells: array): string => `${Js.Array2.joinWith(cells, "")}` - let th = (content: string): string => `${content}` - let td = (content: string): string => `${content}` -} - -module JsCoqName = { - let render = (): string => { - Html.span(~className="jscoq-name", ["jsCoq"]) - } -} - -module ActionTable = { - type action = { - button: string, - keyBinding: string, - description: string, - } - - let actions: array = [ - { - button: `${Html.img(~src="ui-images/down.png", ~height="15px")}${Html.img( - ~src="ui-images/up.png", - ~height="15px", - )}`, - keyBinding: `${Html.kbd("Alt")}+${Html.kbd("↓")}/${Html.kbd("↑")} or${Html.br()}${Html.kbd( - "Alt", - )}+${Html.kbd("N")}/${Html.kbd("P")}`, - description: "Move through the proof.", - }, - { - button: Html.img(~src="ui-images/to-cursor.png", ~height="20px"), - keyBinding: `${Html.kbd("Alt")}+${Html.kbd("Enter")} or${Html.br()} ${Html.kbd( - "Alt", - )}+${Html.kbd("→")}`, - description: "Run (or go back) to the current point.", - }, - { - button: Html.img(~src="ui-images/power-button-512-black.png", ~height="20px"), - keyBinding: Html.kbd("F8"), - description: "Toggles the goal panel.", - }, - ] - - let render = (): string => { - let headerRow = Html.tr([Html.th("Button"), Html.th("Key binding"), Html.th("Action")]) - - let rows = Js.Array2.map(actions, action => { - Html.tr([Html.td(action.button), Html.td(action.keyBinding), Html.td(action.description)]) - }) - - Html.table(~className="doc-actions", Js.Array2.concat([headerRow], rows)) - } -} - -module TeamSection = { - type teamMember = { - name: string, - url: string, - affiliations: array<(string, string)>, - } - - let devTeam: array = [ - { - name: "Emilio Jesús Gallego Arias", - url: "https://www.irif.fr/~gallego/", - affiliations: [ - ("Inria", "https://www.inria.fr"), - ("Université de Paris", "https://u-paris.fr"), - ("IRIF", "https://www.irif.fr"), - ], - }, - { - name: "Shachar Itzhaky", - url: "https://www.cs.technion.ac.il/~shachari/", - affiliations: [("Technion", "https://cs.technion.ac.il")], - }, - ] - - let contributors: array = [ - { - name: "Benoît Pin", - url: "", - affiliations: [ - ("CRI", "https://www.cri.ensmp.fr/"), - ("MINES ParisTech", "https://www.minesparis.psl.eu"), - ], - }, - ] - - let renderMember = (member: teamMember): string => { - let nameLink = member.url != "" ? Html.a(~href=member.url, member.name) : member.name - - let affiliationLinks = Js.Array2.joinWith( - Js.Array2.map(member.affiliations, ((name, url)) => Html.a(~href=url, name)), - ", ", - ) - - Html.li([`${nameLink} (${affiliationLinks})`]) - } - - let render = (): string => { - let devList = Js.Array2.joinWith(Js.Array2.map(devTeam, renderMember), "") - let contribList = Js.Array2.joinWith(Js.Array2.map(contributors, renderMember), "") - - Html.div( - ~id="team", - [ - ``, - Html.p([Html.i("The dev team")]), - Html.ul([devList]), - Html.p([Html.i("Contributors")]), - Html.ul([contribList]), - ], - ) - } -} - -module CodeExamples = { - let imports = `From Coq Require Import ssreflect ssrfun ssrbool. -From mathcomp Require Import eqtype ssrnat div prime.` - - let primeAbove1 = `(* A nice proof of the infinitude of primes, by Georges Gonthier *) -Lemma prime_above m : {p | m < p & prime p}. -Proof.` - - let primeAbove2 = `have /pdivP[p pr_p p_dv_m1]: 1 < m\`! + 1 - by rewrite addn1 ltnS fact_gt0.` - - let primeAbove3 = `exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.` - - let primeAbove4 = `by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. -Qed.` - - let codeIds = ["addnC", "prime_above1", "prime_above2", "prime_above3", "prime_above4"] -} diff --git a/echidna-playground/src/Deno.affine b/echidna-playground/src/Deno.affine new file mode 100644 index 00000000..0d05f976 --- /dev/null +++ b/echidna-playground/src/Deno.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Deno; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Deno.res b/echidna-playground/src/Deno.res deleted file mode 100644 index 58fff5ba..00000000 --- a/echidna-playground/src/Deno.res +++ /dev/null @@ -1,31 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// Deno HTTP server bindings for ReScript - -type request -type response - -// Deno namespace bindings -@val @scope("Deno") external readFile: string => Js.Promise.t = "readFile" - -type serveOptions = {port: int} -type serveHandler = request => Js.Promise.t - -@val @scope("Deno") external serve: (serveOptions, serveHandler) => unit = "serve" - -// Request bindings -@get external getUrl: request => string = "url" -@get external getMethod: request => string = "method" - -// Response constructor -@new external makeResponse: (string, {"headers": {"content-type": string}}) => response = "Response" -@new external makeResponseWithStatus: (string, {"status": int}) => response = "Response" -@new external makeResponseBytes: (Js.TypedArray2.Uint8Array.t, {"headers": {"content-type": string}}) => response = "Response" - -// URL parsing -type url = {pathname: string} -@new external makeUrl: string => url = "URL" - -// Console -@val @scope("console") external log: string => unit = "log" diff --git a/echidna-playground/src/Dom.affine b/echidna-playground/src/Dom.affine new file mode 100644 index 00000000..eafbe74d --- /dev/null +++ b/echidna-playground/src/Dom.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Dom; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Dom.res b/echidna-playground/src/Dom.res deleted file mode 100644 index e0c7463e..00000000 --- a/echidna-playground/src/Dom.res +++ /dev/null @@ -1,54 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// DOM bindings for ReScript - -type element -type document -type window - -@val external document: document = "document" -@val external window: window = "window" - -@send external getElementById: (document, string) => Js.Nullable.t = "getElementById" -@send external querySelector: (document, string) => Js.Nullable.t = "querySelector" -@send external querySelectorAll: (document, string) => array = "querySelectorAll" - -@send external createElement: (document, string) => element = "createElement" -@send external createTextNode: (document, string) => element = "createTextNode" - -@send external appendChild: (element, element) => unit = "appendChild" -@send external removeChild: (element, element) => unit = "removeChild" -@send external replaceChild: (element, element, element) => unit = "replaceChild" - -@set external setInnerHTML: (element, string) => unit = "innerHTML" -@get external getInnerHTML: element => string = "innerHTML" - -@set external setTextContent: (element, string) => unit = "textContent" -@get external getTextContent: element => string = "textContent" - -@set external setClassName: (element, string) => unit = "className" -@get external getClassName: element => string = "className" - -@send external setAttribute: (element, string, string) => unit = "setAttribute" -@send external getAttribute: (element, string) => Js.Nullable.t = "getAttribute" -@send external removeAttribute: (element, string) => unit = "removeAttribute" - -@send external addEventListener: (element, string, unit => unit) => unit = "addEventListener" -@send external removeEventListener: (element, string, unit => unit) => unit = "removeEventListener" - -@get external getValue: element => string = "value" -@set external setValue: (element, string) => unit = "value" - -module Style = { - @set external setDisplay: (element, string) => unit = "style.display" - @set external setVisibility: (element, string) => unit = "style.visibility" - @set external setBackgroundColor: (element, string) => unit = "style.backgroundColor" - @set external setColor: (element, string) => unit = "style.color" - @set external setPadding: (element, string) => unit = "style.padding" - @set external setMargin: (element, string) => unit = "style.margin" -} - -module Body = { - @val external body: element = "document.body" -} diff --git a/echidna-playground/src/JsCoq.affine b/echidna-playground/src/JsCoq.affine new file mode 100644 index 00000000..d4f78337 --- /dev/null +++ b/echidna-playground/src/JsCoq.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module JsCoq; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/JsCoq.res b/echidna-playground/src/JsCoq.res deleted file mode 100644 index e6d0830b..00000000 --- a/echidna-playground/src/JsCoq.res +++ /dev/null @@ -1,62 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// JsCoq bindings and types - -type editorMode = { - @as("company-coq") companyCoq: bool, -} - -type editorConfig = { - mode: editorMode, - keyMap: string, -} - -type coqOptions = { - implicit_libs: bool, - focus: bool, - editor: editorConfig, - init_pkgs: array, - all_pkgs: array, -} - -type coqInstance - -// JsCoq loader bindings -@module("jscoq/ui-js/jscoq-loader.js") -external startExternal: (array, coqOptions) => Js.Promise.t = "start" - -module JsCoqLoader = { - @val @scope("JsCoq") - external start: (array, coqOptions) => Js.Promise.t = "start" -} - -let defaultOptions: coqOptions = { - implicit_libs: false, - focus: false, - editor: { - mode: {companyCoq: true}, - keyMap: "default", - }, - init_pkgs: ["init"], - all_pkgs: ["coq", "mathcomp"], -} - -let makeOptions = ( - ~implicitLibs=false, - ~focus=false, - ~companyCoq=true, - ~keyMap="default", - ~initPkgs=["init"], - ~allPkgs=["coq", "mathcomp"], - (), -): coqOptions => { - implicit_libs: implicitLibs, - focus: focus, - editor: { - mode: {companyCoq: companyCoq}, - keyMap: keyMap, - }, - init_pkgs: initPkgs, - all_pkgs: allPkgs, -} diff --git a/echidna-playground/src/Main.affine b/echidna-playground/src/Main.affine new file mode 100644 index 00000000..d410d4c0 --- /dev/null +++ b/echidna-playground/src/Main.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Main; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Main.res b/echidna-playground/src/Main.res deleted file mode 100644 index 4e5820d8..00000000 --- a/echidna-playground/src/Main.res +++ /dev/null @@ -1,19 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// Main entry point for Coq-Jr - -// Re-export modules -module Dom = Dom -module JsCoq = JsCoq -module Components = Components -module Page = Page - -// Initialize the application when running in browser -let initialize = () => { - Console.log("Coq-Jr initialized") - Console.log("Generated page HTML available via Page.render()") -} - -// Export the page render function for use by Deno server -let getPageHtml = Page.render diff --git a/echidna-playground/src/Page.affine b/echidna-playground/src/Page.affine new file mode 100644 index 00000000..7591b171 --- /dev/null +++ b/echidna-playground/src/Page.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Page; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Page.res b/echidna-playground/src/Page.res deleted file mode 100644 index 0abe3987..00000000 --- a/echidna-playground/src/Page.res +++ /dev/null @@ -1,173 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// Page renderer for jsCoq - -open Components - -let jscoqName = JsCoqName.render() - -let welcomeSection = (): string => { - Html.div([ - Html.h3([`Welcome to the ${jscoqName} Interactive Online System!`]), - Html.p([ - `Welcome to the ${jscoqName} technology demo! `, - `${jscoqName} is an interactive, `, - `web-based environment for the Coq Theorem prover, and is a collaborative `, - `development effort. See the `, - Html.a(~href="#team", "list of contributors"), - ` below.`, - ]), - Html.p([ - `${jscoqName} is open source. If you find any problem or want to make `, - `any contribution, you are extremely welcome! We await your `, - `feedback at `, - Html.a(~href="https://github.com/jscoq/jscoq", "GitHub"), - ` and `, - Html.a(~href="https://gitter.im/jscoq/Lobby", "Gitter"), - `.`, - ]), - ]) -} - -let instructionsSection = (): string => { - Html.div([ - Html.h4(["Instructions:"]), - Html.p([ - `The following document contains embedded Coq code. `, - `All the code is editable and can be run directly on the page. `, - `Once ${jscoqName} finishes loading, you are `, - `free to experiment by stepping through the proof and viewing intermediate `, - `proof states on the right panel.`, - ]), - Html.h5(["Actions:"]), - ActionTable.render(), - Html.h5(["Saving your own proof scripts:"]), - Html.p([ - `The `, - Html.a(~href="scratchpad.html", "scratchpad"), - ` offers simple, local storage functionality. `, - `Please go to `, - Html.a(~href="https://x80.org/collacoq/", "CollaCoq"), - ` if you want to share your developments with other users.`, - ]), - ]) -} - -let primeExampleSection = (): string => { - Html.div([ - Html.h4(["A First Example: The Infinitude of Primes"]), - Html.p([ - `We don't provide a Coq tutorial (yet), but as a showcase, we `, - `display a proof of the infinitude of primes in Coq. The proof relies `, - `in the Mathematical Components library by the `, - Html.a(~href="https://ssr.msr-inria.inria.fr/", "MSR/Inria"), - ` team led by Georges Gonthier, so our first step will be to load it and `, - `set a few Coq options:`, - ]), - Html.textarea(~id="addnC", CodeExamples.imports), - Html.h5(["Ready to do Proofs!"]), - Html.p([ - `Once the basic environment has been set up, we can proceed to the proof:`, - ]), - Html.textarea(~id="prime_above1", CodeExamples.primeAbove1), - Html.p([ - `The lemma states that for any number ${Html.code("m")}, `, - `there is a prime number larger than ${Html.code("m")}. `, - `Coq is a ${Html.em("constructive system")}, which among other things `, - `implies that to show the existence of an object, we need to `, - `actually provide an algorithm that will construct it. `, - `In this case, we need to find a prime number ${Html.code("p")} `, - `that is greater than ${Html.code("m")}. `, - `What would be a suitable ${Html.code("p")}? `, - `Choosing ${Html.code("p")} to be the first prime divisor of ${Html.code("m! + 1")} works. `, - `As we will shortly see, properties of divisibility will imply that `, - `${Html.code("p")} must be greater than ${Html.code("m")}.`, - ]), - Html.textarea(~id="prime_above2", CodeExamples.primeAbove2), - Html.p([ - `Our first step is thus to use the library-provided lemma `, - `${Html.code("pdivP")}, which states that every number is divided by a `, - `prime. Thus, we obtain a number ${Html.code("p")} and the corresponding `, - `hypotheses ${Html.code("pr_p : prime p")} and ${Html.code("p_dv_m1")}, `, - `"p divides m! + 1". `, - `The ssreflect tactic ${Html.code("have")} provides a convenient way to `, - `instantiate this lemma and discard the side proof obligation `, - `${Html.code("1 < m! + 1")}.`, - ]), - Html.textarea(~id="prime_above3", CodeExamples.primeAbove3), - Html.p([ - `It remains to prove that ${Html.code("p")} is greater than ${Html.code("m")}. We reason by `, - `contraposition with the divisibility hypothesis, which gives us `, - `the goal "if ${Html.code("p ≤ m")} then ${Html.code("p")} is not a prime divisor of " `, - `${Html.code("m! + 1")}.`, - ]), - Html.textarea(~id="prime_above4", CodeExamples.primeAbove4), - Html.p([ - `The goal follows from basic properties of divisibility, plus `, - `from the fact that if ${Html.code("p ≤ m")}, then ${Html.code("p")} divides `, - `${Html.code("m!")}, so that for ${Html.code("p")} to divide `, - `${Html.code("m! + 1")} it must also divide 1, `, - `in contradiction to ${Html.code("p")} being prime.`, - ]), - Html.hr(), - Html.p([ - `${jscoqName} provides many other packages, `, - `including Coq's standard library and the `, - Html.a(~href="https://math-comp.github.io", "mathematical components"), - ` library. `, - `Feel free to experiment, and bear with the beta status of this demo.`, - ]), - Html.p([Html.i("¡Salut!")]), - ]) -} - -let documentContent = (): string => { - Html.div(~id="document", [ - welcomeSection(), - instructionsSection(), - primeExampleSection(), - TeamSection.render(), - ]) -} - -let jscoqScript = (): string => { - let ids = Array.map(CodeExamples.codeIds, id => `'${id}'`) -> Array.joinWith(", ") - ` - - ` -} - -let render = (): string => { - ` - - - - - - - - jsCoq – Use Coq in Your Browser - - -
-
- ${documentContent()} -
-
- ${jscoqScript()} - -` -} diff --git a/echidna-playground/src/PlaygroundServer.affine b/echidna-playground/src/PlaygroundServer.affine new file mode 100644 index 00000000..5c96134a --- /dev/null +++ b/echidna-playground/src/PlaygroundServer.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module PlaygroundServer; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/PlaygroundServer.res b/echidna-playground/src/PlaygroundServer.res deleted file mode 100644 index 4ee48b10..00000000 --- a/echidna-playground/src/PlaygroundServer.res +++ /dev/null @@ -1,133 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) - -/** - * Deno HTTP server for ECHIDNA Playground (echidna-playground). - * Serves the compiled ReScript page, falling back to a build-required message. - * Distinct from Server.res which is the Coq-Jr server in this same directory. - */ - -/** FFI: Deno.readFile */ -@scope("Deno") @val -external readFile: string => promise = "readFile" - -/** FFI: Deno.serve */ -type serveOptions = {port: int} -@scope("Deno") @val -external denoServe: (serveOptions, Deno.request => promise) => unit = "serve" - -/** FFI: console.log */ -@scope("console") @val -external log: string => unit = "log" - -/** MIME type mapping for static file serving */ -let mimeTypes: Dict.t = Dict.fromArray([ - (".html", "text/html"), - (".css", "text/css"), - (".js", "application/javascript"), - (".json", "application/json"), - (".png", "image/png"), - (".jpg", "image/jpeg"), - (".jpeg", "image/jpeg"), - (".gif", "image/gif"), - (".svg", "image/svg+xml"), - (".ico", "image/x-icon"), - (".woff", "font/woff"), - (".woff2", "font/woff2"), -]) - -/** Extract file extension from a path */ -let getExtension = (path: string): string => { - let lastDot = String.lastIndexOf(path, ".") - if lastDot >= 0 { - String.substring(path, ~start=lastDot, ~end=String.length(path)) - } else { - "" - } -} - -/** Look up MIME type for a path */ -let getMimeType = (path: string): string => { - let ext = getExtension(path) - switch Dict.get(mimeTypes, ext) { - | Some(mime) => mime - | None => "application/octet-stream" - } -} - -/** Attempt to serve a static file, returning None if not found */ -let serveStaticFile = async (path: string): option => { - try { - let bytes = await readFile(path) - Some(Deno.makeResponseBytes(bytes, {"headers": {"content-type": getMimeType(path)}})) - } catch { - | _ => None - } -} - -/** Fallback HTML when ReScript hasn't been compiled yet */ -let buildRequiredHtml = ` - - - - - ECHIDNA Playground - Build Required - - - -

ECHIDNA Playground

-

The ReScript sources need to be compiled first.

-

Quick Start

- 
deno task build
-deno task serve
- -` - -/** Try to load the compiled ReScript page renderer, falling back to static HTML */ -let getPageHtml = (): string => { - // In production, Main.res.js should provide the page content via Page.render() - // If not available, return the build-required fallback - try { - Page.render() - } catch { - | _ => buildRequiredHtml - } -} - -/** Server port */ -let port = 8000 - -/** Request handler */ -let handler = async (request: Deno.request): Deno.response => { - let urlStr = Deno.getUrl(request) - let url = Deno.makeUrl(urlStr) - let pathname = url.pathname - - log(`${Deno.getMethod(request)} ${pathname}`) - - // Serve index page - if pathname == "/" || pathname == "/index.html" { - Deno.makeResponse(getPageHtml(), {"headers": {"content-type": "text/html; charset=utf-8"}}) - } else { - // Try to serve static files - let staticPath = "." ++ pathname - let staticResponse = await serveStaticFile(staticPath) - switch staticResponse { - | Some(response) => response - | None => Deno.makeResponseWithStatus("Not Found", {"status": 404}) - } - } -} - -/** Start the playground server */ -let start = () => { - log(`ECHIDNA Playground server running at http://localhost:${Belt.Int.toString(port)}/`) - denoServe({port: port}, handler) -} - -// Auto-start when loaded -let _ = start() diff --git a/echidna-playground/src/Server.affine b/echidna-playground/src/Server.affine new file mode 100644 index 00000000..c4588cf7 --- /dev/null +++ b/echidna-playground/src/Server.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Server; + +// TODO: Complete semantic implementation diff --git a/echidna-playground/src/Server.res b/echidna-playground/src/Server.res deleted file mode 100644 index 0edf17db..00000000 --- a/echidna-playground/src/Server.res +++ /dev/null @@ -1,76 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// SPDX-FileCopyrightText: 2025 Coq-Jr Contributors - -// HTTP Server for Coq-Jr in ReScript - -let port = 8000 - -let mimeTypes: Js.Dict.t = Js.Dict.fromArray([ - (".html", "text/html"), - (".css", "text/css"), - (".js", "application/javascript"), - (".json", "application/json"), - (".png", "image/png"), - (".jpg", "image/jpeg"), - (".jpeg", "image/jpeg"), - (".gif", "image/gif"), - (".svg", "image/svg+xml"), - (".ico", "image/x-icon"), - (".woff", "font/woff"), - (".woff2", "font/woff2"), -]) - -let getExtension = (path: string): string => { - let lastDot = Js.String2.lastIndexOf(path, ".") - if lastDot >= 0 { - Js.String2.substr(path, ~from=lastDot) - } else { - "" - } -} - -let getMimeType = (path: string): string => { - let ext = getExtension(path) - switch Js.Dict.get(mimeTypes, ext) { - | Some(mime) => mime - | None => "application/octet-stream" - } -} - -let serveStaticFile = async (path: string): option => { - try { - let bytes = await Deno.readFile(path) - Some(Deno.makeResponseBytes(bytes, {"headers": {"content-type": getMimeType(path)}})) - } catch { - | _ => None - } -} - -let handler = async (request: Deno.request): Deno.response => { - let urlStr = Deno.getUrl(request) - let url = Deno.makeUrl(urlStr) - let pathname = url.pathname - - Deno.log(`${Deno.getMethod(request)} ${pathname}`) - - // Serve index page - if pathname == "/" || pathname == "/index.html" { - Deno.makeResponse(Page.render(), {"headers": {"content-type": "text/html; charset=utf-8"}}) - } else { - // Try to serve static files - let staticPath = "." ++ pathname - let staticResponse = await serveStaticFile(staticPath) - switch staticResponse { - | Some(response) => response - | None => Deno.makeResponseWithStatus("Not Found", {"status": 404}) - } - } -} - -let start = () => { - Deno.log(`Coq-Jr server running at http://localhost:${Belt.Int.toString(port)}/`) - Deno.serve({port: port}, handler) -} - -// Auto-start when loaded -let _ = start()