Skip to content

Commit 5b58598

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: migrate all 15 TypeScript files to ReScript — zero TS remaining
Complete TS→ReScript migration for echidna prover subsystem: - Prover clients (LeanTool, Metamath, SystemOnTptp, Unified, Wolfram, Z3Wasm) - Prover types and tests (Prover, ProverTest) - HTTP utilities (Http) - Runners (Cli, Daemon) - Module barrel (Mod) - UI servers (Server, PlaygroundServer) - All 15 .ts files deleted, 33 .res files now in repo Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 637e39e commit 5b58598

30 files changed

Lines changed: 3362 additions & 3010 deletions

‎echidna-playground/server.ts‎

Lines changed: 0 additions & 96 deletions
This file was deleted.

‎echidna-playground/src/PlaygroundServer.res‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
4+
/**
5+
* Deno HTTP server for ECHIDNA Playground (echidna-playground).
6+
* Serves the compiled ReScript page, falling back to a build-required message.
7+
* Distinct from Server.res which is the Coq-Jr server in this same directory.
8+
*/
9+
10+
/** FFI: Deno.readFile */
11+
@scope("Deno") @val
12+
external readFile: string => promise<Js.TypedArray2.Uint8Array.t> = "readFile"
13+
14+
/** FFI: Deno.serve */
15+
type serveOptions = {port: int}
16+
@scope("Deno") @val
17+
external denoServe: (serveOptions, Deno.request => promise<Deno.response>) => unit = "serve"
18+
19+
/** FFI: console.log */
20+
@scope("console") @val
21+
external log: string => unit = "log"
22+
23+
/** MIME type mapping for static file serving */
24+
let mimeTypes: Js.Dict.t<string> = Js.Dict.fromArray([
25+
(".html", "text/html"),
26+
(".css", "text/css"),
27+
(".js", "application/javascript"),
28+
(".json", "application/json"),
29+
(".png", "image/png"),
30+
(".jpg", "image/jpeg"),
31+
(".jpeg", "image/jpeg"),
32+
(".gif", "image/gif"),
33+
(".svg", "image/svg+xml"),
34+
(".ico", "image/x-icon"),
35+
(".woff", "font/woff"),
36+
(".woff2", "font/woff2"),
37+
])
38+
39+
/** Extract file extension from a path */
40+
let getExtension = (path: string): string => {
41+
let lastDot = Js.String2.lastIndexOf(path, ".")
42+
if lastDot >= 0 {
43+
Js.String2.substr(path, ~from=lastDot)
44+
} else {
45+
""
46+
}
47+
}
48+
49+
/** Look up MIME type for a path */
50+
let getMimeType = (path: string): string => {
51+
let ext = getExtension(path)
52+
switch Js.Dict.get(mimeTypes, ext) {
53+
| Some(mime) => mime
54+
| None => "application/octet-stream"
55+
}
56+
}
57+
58+
/** Attempt to serve a static file, returning None if not found */
59+
let serveStaticFile = async (path: string): option<Deno.response> => {
60+
try {
61+
let bytes = await readFile(path)
62+
Some(Deno.makeResponseBytes(bytes, {"headers": {"content-type": getMimeType(path)}}))
63+
} catch {
64+
| _ => None
65+
}
66+
}
67+
68+
/** Fallback HTML when ReScript hasn't been compiled yet */
69+
let buildRequiredHtml = `
70+
<!DOCTYPE html>
71+
<html>
72+
<head>
73+
<meta charset="utf-8">
74+
<title>ECHIDNA Playground - Build Required</title>
75+
<style>
76+
body { font-family: system-ui, sans-serif; max-width: 800px; margin: 50px auto; padding: 20px; }
77+
code { background: #f4f4f4; padding: 2px 6px; border-radius: 3px; }
78+
pre { background: #f4f4f4; padding: 15px; border-radius: 5px; overflow-x: auto; }
79+
</style>
80+
</head>
81+
<body>
82+
<h1>ECHIDNA Playground</h1>
83+
<p>The ReScript sources need to be compiled first.</p>
84+
<h2>Quick Start</h2>
85+
<pre><code>deno task build
86+
deno task serve</code></pre>
87+
</body>
88+
</html>`
89+
90+
/** Try to load the compiled ReScript page renderer, falling back to static HTML */
91+
let getPageHtml = (): string => {
92+
// In production, Main.res.js should provide the page content via Page.render()
93+
// If not available, return the build-required fallback
94+
try {
95+
Page.render()
96+
} catch {
97+
| _ => buildRequiredHtml
98+
}
99+
}
100+
101+
/** Server port */
102+
let port = 8000
103+
104+
/** Request handler */
105+
let handler = async (request: Deno.request): Deno.response => {
106+
let urlStr = Deno.getUrl(request)
107+
let url = Deno.makeUrl(urlStr)
108+
let pathname = url.pathname
109+
110+
log(`${Deno.getMethod(request)} ${pathname}`)
111+
112+
// Serve index page
113+
if pathname == "/" || pathname == "/index.html" {
114+
Deno.makeResponse(getPageHtml(), {"headers": {"content-type": "text/html; charset=utf-8"}})
115+
} else {
116+
// Try to serve static files
117+
let staticPath = "." ++ pathname
118+
let staticResponse = await serveStaticFile(staticPath)
119+
switch staticResponse {
120+
| Some(response) => response
121+
| None => Deno.makeResponseWithStatus("Not Found", {"status": 404})
122+
}
123+
}
124+
}
125+
126+
/** Start the playground server */
127+
let start = () => {
128+
log(`ECHIDNA Playground server running at http://localhost:${Belt.Int.toString(port)}/`)
129+
denoServe({port: port}, handler)
130+
}
131+
132+
// Auto-start when loaded
133+
let _ = start()

‎src/provers/Mod.res‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
4+
/**
5+
* ECHIDNA Prover Integration Module
6+
* Barrel re-export of all prover types, clients, runners, and utilities.
7+
* Deno-native theorem prover integration (NO NPM).
8+
*
9+
* Types: Prover, ProverResult, Problem, QueueItem, ProverConfig, etc.
10+
* Clients: SystemOnTPTP, Metamath, Z3Wasm, Wolfram, LeanTool, Unified
11+
* Runners: ProofRunnerDaemon
12+
* Utilities: HTTP helpers with retry logic
13+
*/
14+
15+
// NOTE: ReScript does not have barrel re-exports like TypeScript.
16+
// Each module (Prover.res, LeanTool.res, Metamath.res, etc.) is
17+
// automatically available by name. This file documents the public API
18+
// surface for the prover subsystem.
19+
//
20+
// Module Map:
21+
// Types: Prover (types, DEFAULT_CONFIG, PROVER_REGISTRY)
22+
// Clients: SystemOnTptp, Metamath, Z3Wasm, Wolfram, LeanTool, Unified
23+
// Runners: Daemon (ProofRunnerDaemon, DaemonConfig, DaemonStats, DaemonEvent)
24+
// Utils: Http (fetchWithRetry, postForm, postJSON, getText, sleep, backoffDelay)
25+
26+
/** Re-export key type aliases for convenience */
27+
type inputFormat = Prover.inputFormat
28+
type proverStatus = Prover.proverStatus
29+
type prover = Prover.prover
30+
type proverResult = Prover.proverResult
31+
type problem = Prover.problem
32+
type queueItem = Prover.queueItem
33+
type proverConfig = Prover.proverConfig

0 commit comments

Comments
 (0)