coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Compare commits

base: coop:c0ced8a40f37a4bc12fe7f7960f9f8182ae68f85
Branches Tags
coop:main coop:architecture coop:wasm coop:macros coop:sx coop:exorcism coop:cssx coop:decoupling coop:sexpression coop:relations
...
compare: coop:e4e8b45cb4261630b2f474391c1d60ffedd395dc
Branches Tags
coop:architecture coop:main coop:wasm coop:macros coop:sx coop:exorcism coop:cssx coop:decoupling coop:sexpression coop:relations

3 Commits
c0ced8a40f ... e4e8b45cb4

Author SHA1 Message Date
giles
e4e8b45cb4 Update py.sx scope: general SX-to-Python translator, not spec-only
All checks were successful
Build and Deploy / build-and-deploy (push) Successful in 1m37s
Details 
The translation rules are mechanical and apply to all SX forms — HTML tags,
components, macros, islands, page forms. Bootstrapping the spec is the first
test case (fixed-point proof); phases 6-9 extend to full SX compilation.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
 2026-03-09 00:54:20 +00:00
giles
db1691d8f5 Add JS bootstrapper plan: js.sx design document 
js.sx — SX-to-JavaScript translator + ahead-of-time component compiler.
Two modes: spec bootstrapper (replacing bootstrap_js.py) and component
compiler (server-evaluated SX trees → standalone JS DOM construction).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
 2026-03-09 00:52:35 +00:00
giles
192d48d0e3 Add self-hosting bootstrapper plan: py.sx design document 
Plan for py.sx — an SX-to-Python translator written in SX that
replaces bootstrap_py.py. Covers translation rules, statement vs
expression modes, mutation/cell variables, five implementation
phases, fixed-point verification, and implications for multi-host
bootstrapping.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
 2026-03-09 00:45:07 +00:00
4 changed files with 919 additions and 0 deletions
Expand all files Collapse all files

4
sx/sx/nav-data.sx
View File

@@ -159,6 +159,10 @@
:summary "Live demo: #z3 translates SX spec declarations to SMT-LIB verification conditions.")
(dict :label "Theorem Prover" :href "/plans/theorem-prover"
:summary "prove.sx — constraint solver and property prover for SX primitives, written in SX.")
(dict :label "Self-Hosting Bootstrapper" :href "/plans/self-hosting-bootstrapper"
:summary "py.sx — an SX-to-Python translator written in SX. The bootstrapper bootstraps itself.")
(dict :label "JS Bootstrapper" :href "/plans/js-bootstrapper"
:summary "js.sx — SX-to-JavaScript translator + ahead-of-time component compiler. Zero-runtime static sites.")
(dict :label "SX-Activity" :href "/plans/sx-activity"
:summary "A new web built on SX — executable content, shared components, parsers, and logic on IPFS, provenance on Bitcoin, all running within your own security context.")
(dict :label "Predictive Prefetching" :href "/plans/predictive-prefetch"

511
sx/sx/plans/js-bootstrapper.sx Normal file
View File

@@ -0,0 +1,511 @@
;; ---------------------------------------------------------------------------
;; js.sx — Self-Hosting JavaScript Bootstrapper
;; ---------------------------------------------------------------------------
(defcomp ~plan-js-bootstrapper-content ()
(~doc-page :title "js.sx — JavaScript Bootstrapper"
;; -----------------------------------------------------------------------
;; Overview
;; -----------------------------------------------------------------------
(~doc-section :title "Overview" :id "overview"
(p (code "bootstrap_js.py") " is a 4,361-line Python program that reads the "
(code ".sx") " spec files and emits " (code "sx-ref.js") " — the entire "
"browser runtime. Parser, evaluator, three rendering adapters (HTML, SX wire, DOM), "
"the engine (fetch/swap/trigger), orchestration, boot, signals, router, component "
"dependency analysis — all transpiled from " (code ".sx") " spec files into JavaScript.")
(p (code "js.sx") " replaces that Python program with an SX program. "
"Like " (code "py.sx") " for Python, " (code "js.sx") " is an SX-to-JavaScript "
"translator written in SX. But it goes further.")
(p "Because the JS bootstrapper produces " (em "browser code") ", " (code "js.sx")
" can also compile " (em "any") " SX component tree into a standalone JavaScript "
"program. The server evaluates an " (code ".sx") " page definition, calls "
(code "#js") " on the result, and gets a self-contained JS bundle that renders "
"the same output in the browser — no SX runtime needed."))
;; -----------------------------------------------------------------------
;; Two Modes
;; -----------------------------------------------------------------------
(~doc-section :title "Two Compilation Modes" :id "modes"
(~doc-subsection :title "Mode 1: Spec Bootstrapper"
(p "Same job as " (code "bootstrap_js.py") ". Read spec " (code ".sx") " files, "
"emit " (code "sx-ref.js") ".")
(~doc-code :code (highlight ";; Translate eval.sx to JavaScript
(js-translate-file (parse-file \"eval.sx\"))
;; → \"function evalExpr(expr, env) { ... }\"
;; Full bootstrap: all spec modules → sx-ref.js
(js-bootstrap
:adapters (list \"html\" \"sx\" \"dom\" \"engine\" \"boot\")
:modules (list \"deps\" \"router\" \"signals\"))" "lisp"))
(p "The output is identical to " (code "python bootstrap_js.py") ". "
"Verification: " (code "diff <(python bootstrap_js.py) <(python run_js_sx.py)") "."))
(~doc-subsection :title "Mode 2: Component Compiler"
(p "Server-side SX evaluation + " (code "js.sx") " translation = static JS output. "
"Given a component tree that the server has already evaluated (data fetched, "
"conditionals resolved, loops expanded), " (code "js.sx") " compiles the "
"resulting DOM description into a JavaScript program that builds the same DOM.")
(~doc-code :code (highlight ";; Server evaluates the page (fetches data, expands components)
;; Result is a resolved SX tree: (div :class \"...\" (h1 \"Hello\") ...)
;; js.sx compiles that tree to standalone JS
(js-compile-component evaluated-tree)
;; → \"(function(){
;; var el = document.createElement('div');
;; el.className = '...';
;; var h1 = document.createElement('h1');
;; h1.textContent = 'Hello';
;; el.appendChild(h1);
;; return el;
;; })()\"" "lisp"))
(p "This is ahead-of-time compilation. The browser receives JavaScript, "
"not s-expressions. No parser, no evaluator, no runtime. "
"Just DOM construction code.")))
;; -----------------------------------------------------------------------
;; Architecture
;; -----------------------------------------------------------------------
(~doc-section :title "Architecture" :id "architecture"
(p "The JS bootstrapper has more moving parts than the Python one because "
"JavaScript is the " (em "client") " host. The browser runtime includes "
"things Python never needs:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Spec Module")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Purpose")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Python?")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Browser?")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "eval.sx")
(td :class "px-4 py-2" "Core evaluator, special forms, TCO")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "render.sx")
(td :class "px-4 py-2" "Tag registry, void elements, boolean attrs")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "parser.sx")
(td :class "px-4 py-2" "Tokenizer, parser, serializer")
(td :class "px-4 py-2 text-center" "—") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "adapter-html.sx")
(td :class "px-4 py-2" "Render to HTML string")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "adapter-sx.sx")
(td :class "px-4 py-2" "Serialize to SX wire format")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100 bg-blue-50"
(td :class "px-4 py-2 font-mono" "adapter-dom.sx")
(td :class "px-4 py-2" "Render to live DOM nodes")
(td :class "px-4 py-2 text-center" "—") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100 bg-blue-50"
(td :class "px-4 py-2 font-mono" "engine.sx")
(td :class "px-4 py-2" "Fetch, swap, trigger, history")
(td :class "px-4 py-2 text-center" "—") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100 bg-blue-50"
(td :class "px-4 py-2 font-mono" "orchestration.sx")
(td :class "px-4 py-2" "Element scanning, attribute processing")
(td :class "px-4 py-2 text-center" "—") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100 bg-blue-50"
(td :class "px-4 py-2 font-mono" "boot.sx")
(td :class "px-4 py-2" "Script processing, mount, hydration")
(td :class "px-4 py-2 text-center" "—") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "signals.sx")
(td :class "px-4 py-2" "Reactive signal runtime")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "deps.sx")
(td :class "px-4 py-2" "Component dependency analysis")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "router.sx")
(td :class "px-4 py-2" "Client-side route matching")
(td :class "px-4 py-2 text-center" "Yes") (td :class "px-4 py-2 text-center" "Yes")))))
(p "Blue rows are browser-only modules. " (code "js.sx") " must handle all of them. "
"The platform interface is also larger: DOM primitives (" (code "dom-create-element")
", " (code "dom-append") ", " (code "dom-set-attr") ", ...), "
"browser APIs (" (code "fetch") ", " (code "history") ", " (code "localStorage")
"), and event handling."))
;; -----------------------------------------------------------------------
;; Translation Rules
;; -----------------------------------------------------------------------
(~doc-section :title "Translation Rules" :id "translation"
(p (code "js.sx") " shares the same pattern as " (code "py.sx") " — expression translator, "
"statement translator, name mangling — but with JavaScript-specific mappings:")
(~doc-subsection :title "Name Mangling"
(p "SX uses kebab-case. JavaScript uses camelCase.")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "JavaScript")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Rule")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "eval-expr")
(td :class "px-4 py-2 font-mono" "evalExpr")
(td :class "px-4 py-2" "kebab → camelCase"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "nil?")
(td :class "px-4 py-2 font-mono" "isNil")
(td :class "px-4 py-2" "predicate → is-prefix"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "empty?")
(td :class "px-4 py-2 font-mono" "isEmpty")
(td :class "px-4 py-2" "? → is-prefix (general)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "set!")
(td :class "px-4 py-2 font-mono" "—")
(td :class "px-4 py-2" "assignment (no rename)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "dom-create-element")
(td :class "px-4 py-2 font-mono" "domCreateElement")
(td :class "px-4 py-2" "platform function rename"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "delete")
(td :class "px-4 py-2 font-mono" "delete_")
(td :class "px-4 py-2" "JS reserved word escape"))))))
(~doc-subsection :title "Special Forms → JavaScript"
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "JavaScript")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(if c t e)")
(td :class "px-4 py-2 font-mono" "(sxTruthy(c) ? t : e)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(when c body)")
(td :class "px-4 py-2 font-mono" "(sxTruthy(c) ? body : NIL)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(let ((a 1)) body)")
(td :class "px-4 py-2 font-mono" "(function(a) { return body; })(1)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(fn (x) body)")
(td :class "px-4 py-2 font-mono" "function(x) { return body; }"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(define name val)")
(td :class "px-4 py-2 font-mono" "var name = val;"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(and a b c)")
(td :class "px-4 py-2 font-mono" "(sxTruthy(a) ? (sxTruthy(b) ? c : b) : a)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(case x \"a\" 1 ...)")
(td :class "px-4 py-2 font-mono" "sxCase(x, [[\"a\", () => 1], ...])"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(str a b c)")
(td :class "px-4 py-2 font-mono" "sxStr(a, b, c)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "&rest args")
(td :class "px-4 py-2 font-mono" "...args (rest params)"))))))
(~doc-subsection :title "JavaScript Advantages"
(p "JavaScript is easier to target than Python in two key ways:")
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
(li (strong "No mutation problem. ")
"JavaScript closures capture by reference, not by value. "
(code "set!") " from a nested function Just Works — no cell variable "
"hack needed. This eliminates the hardest part of " (code "py.sx") ".")
(li (strong "Expression-oriented. ")
"JavaScript's comma operator, ternary, and IIFEs make "
"almost everything expressible as an expression. "
"The statement/expression duality is less painful than Python."))))
;; -----------------------------------------------------------------------
;; Component Compilation
;; -----------------------------------------------------------------------
(~doc-section :title "Component Compilation" :id "component-compiler"
(p "Mode 2 is the interesting one. The server already evaluates SX page "
"definitions — it fetches data, resolves conditionals, expands components, "
"and produces a complete DOM description as an SX tree. Currently this tree "
"is either:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li "Rendered to HTML server-side (" (code "render-to-html") ")")
(li "Serialized as SX wire format for the client to render (" (code "aser") ")"))
(p "A third option: " (strong "compile it to JavaScript") ". "
"The SX tree is already fully resolved — no data to fetch, no conditionals "
"to evaluate. It's just a description of DOM nodes. " (code "js.sx")
" walks this tree and emits imperative JavaScript that constructs the same DOM.")
(~doc-subsection :title "What Gets Compiled"
(p "A resolved SX tree like:")
(~doc-code :code (highlight "(div :class \"container\"
(h1 \"Hello\")
(ul (map (fn (item)
(li :class \"item\" (get item \"name\")))
items)))" "lisp"))
(p "After server-side evaluation (with " (code "items") " = "
(code "[{\"name\": \"Alice\"}, {\"name\": \"Bob\"}]") "):")
(~doc-code :code (highlight "(div :class \"container\"
(h1 \"Hello\")
(ul
(li :class \"item\" \"Alice\")
(li :class \"item\" \"Bob\")))" "lisp"))
(p "Compiles to:")
(~doc-code :code (highlight "var _0 = document.createElement('div');
_0.className = 'container';
var _1 = document.createElement('h1');
_1.textContent = 'Hello';
_0.appendChild(_1);
var _2 = document.createElement('ul');
var _3 = document.createElement('li');
_3.className = 'item';
_3.textContent = 'Alice';
_2.appendChild(_3);
var _4 = document.createElement('li');
_4.className = 'item';
_4.textContent = 'Bob';
_2.appendChild(_4);
_0.appendChild(_2);" "javascript")))
(~doc-subsection :title "Why Not Just Use HTML?"
(p "HTML already does this — " (code "innerHTML") " parses and builds DOM. "
"Why compile to JS instead?")
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
(li (strong "Event handlers. ")
"HTML can't express " (code ":on-click") " or " (code ":sx-get")
" — those need JavaScript. The compiled JS can wire up event "
"listeners inline during construction.")
(li (strong "Reactive islands. ")
"Signal bindings (" (code "deref") "), reactive text nodes, and "
"reactive attributes need to register subscriptions during construction. "
"Compiled JS can create signals and wire subscriptions as it builds the DOM.")
(li (strong "No parse overhead. ")
"The browser doesn't need to parse HTML or SX source. "
"The JavaScript engine JIT-compiles the DOM construction code. "
"For large pages, this can be faster than " (code "innerHTML") ".")
(li (strong "Tree-shakeable. ")
"The compiled output only contains what the page uses. "
"No SX parser, no evaluator, no rendering runtime. "
"A static page compiles to pure DOM API calls — zero framework overhead.")
(li (strong "Portable. ")
"The output is a JavaScript module. It works in any JS environment: "
"browser, Node, Deno, Bun. Server-side rendered pages become "
"testable JavaScript programs.")))
(~doc-subsection :title "Hybrid Mode"
(p "Not every page is fully static. Some parts are server-rendered, "
"some are interactive. " (code "js.sx") " handles this with a hybrid approach:")
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
(li (strong "Static subtrees") " → compiled to DOM construction code (no runtime)")
(li (strong "Reactive islands") " → compiled with signal creation + subscriptions "
"(needs signal runtime, ~2KB)")
(li (strong "Hypermedia attributes") " (" (code "sx-get") ", " (code "sx-post")
") → compiled with event listeners + fetch calls "
"(needs engine, ~5KB)")
(li (strong "Client-routed pages") " → full SX runtime included"))
(p "The compiler analyzes the tree and includes only the runtime slices needed. "
"A purely static page ships zero SX runtime. "
"A page with one reactive counter ships just the signal runtime.")))
;; -----------------------------------------------------------------------
;; The Bootstrap Chain
;; -----------------------------------------------------------------------
(~doc-section :title "The Bootstrap Chain" :id "chain"
(p "With both " (code "py.sx") " and " (code "js.sx") ", the full picture:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Translator")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Written in")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Outputs")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Replaces")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "z3.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "SMT-LIB")
(td :class "px-4 py-2 text-stone-400 italic" "(none — new capability)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "prove.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "Constraint proofs")
(td :class "px-4 py-2 text-stone-400 italic" "(none — new capability)"))
(tr :class "border-t border-stone-100 bg-violet-50"
(td :class "px-4 py-2 font-mono text-violet-700" "py.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "Python")
(td :class "px-4 py-2 font-mono" "bootstrap_py.py"))
(tr :class "border-t border-stone-100 bg-blue-50"
(td :class "px-4 py-2 font-mono text-blue-700" "js.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "JavaScript")
(td :class "px-4 py-2 font-mono" "bootstrap_js.py"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono text-stone-400" "go.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "Go")
(td :class "px-4 py-2 text-stone-400 italic" "(future host)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono text-stone-400" "rs.sx")
(td :class "px-4 py-2" "SX")
(td :class "px-4 py-2" "Rust")
(td :class "px-4 py-2 text-stone-400 italic" "(future host)")))))
(p "Every translator is an SX program. The only Python left is the platform "
"interface (types, DOM primitives, runtime support functions) and the thin "
"runner script that loads " (code "py.sx") " or " (code "js.sx")
" and feeds it the spec files."))
;; -----------------------------------------------------------------------
;; Implementation Plan
;; -----------------------------------------------------------------------
(~doc-section :title "Implementation" :id "implementation"
(~doc-subsection :title "Phase 1: Expression Translator"
(p "Core SX-to-JavaScript expression translation.")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "js-mangle") " — SX name → JavaScript identifier (RENAMES + kebab→camelCase)")
(li (code "js-literal") " — atoms: numbers, strings, booleans, nil, symbols, keywords")
(li (code "js-expr") " — recursive expression translator")
(li "Ternary: " (code "if") ", " (code "when") ", " (code "cond") ", " (code "and") ", " (code "or"))
(li (code "let") " → IIFE: " (code "(function(a) { return body; })(val)"))
(li (code "fn") " → " (code "function(x) { return body; }"))
(li (code "str") " → " (code "sxStr(...)"))
(li "Infix: " (code "+") ", " (code "-") ", " (code "*") ", " (code "/") ", "
(code "===") ", " (code "!==") ", " (code "%"))
(li (code "&rest") " → " (code "...args") " (rest parameters)")))
(~doc-subsection :title "Phase 2: Statement Translator"
(p "Top-level and function body statement emission.")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "js-statement") " — emit as JavaScript statement")
(li (code "define") " → " (code "var name = expr;"))
(li (code "set!") " → direct assignment (closures capture by reference)")
(li (code "for-each") " → " (code "for (var i = 0; i < arr.length; i++)") " loop")
(li (code "do") "/" (code "begin") " → comma expression or block")
(li "Function bodies with multiple expressions → explicit " (code "return"))))
(~doc-subsection :title "Phase 3: Spec Bootstrapper"
(p "Process spec files identically to " (code "bootstrap_js.py") ".")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "js-extract-defines") " — parse .sx source, collect top-level defines")
(li (code "js-translate-file") " — translate a list of define expressions")
(li "Adapter selection: parser, html, sx, dom, engine, orchestration, boot")
(li "Dependency resolution: engine requires dom, boot requires engine + parser")
(li "Static sections (IIFE wrapper, platform interface) stay as string templates")))
(~doc-subsection :title "Phase 4: Component Compiler"
(p "Ahead-of-time compilation of evaluated SX trees to JavaScript.")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "js-compile-element") " — emit " (code "createElement") " + attribute setting")
(li (code "js-compile-text") " — emit " (code "textContent") " or " (code "createTextNode"))
(li (code "js-compile-component") " — inline-expand or emit component call")
(li (code "js-compile-island") " — emit signal creation + reactive DOM subscriptions")
(li (code "js-compile-fragment") " — emit " (code "DocumentFragment") " construction")
(li "Runtime slicing: analyze tree → include only necessary runtime modules")))
(~doc-subsection :title "Phase 5: Verification"
(~doc-code :code (highlight "# Mode 1: spec bootstrapper parity
python bootstrap_js.py > sx-ref-g0.js
python run_js_sx.py > sx-ref-g1.js
diff sx-ref-g0.js sx-ref-g1.js # must be empty
# Mode 2: component compilation correctness
# Server renders page → SX tree → compile to JS
# Compare DOM output: runtime-rendered vs compiled
python test_js_compile.py # renders both, diffs DOM" "bash")))
;; -----------------------------------------------------------------------
;; Comparison with py.sx
;; -----------------------------------------------------------------------
(~doc-section :title "Comparison with py.sx" :id "comparison"
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Concern")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "py.sx"))
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "js.sx"))))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Naming convention")
(td :class "px-4 py-2" "snake_case")
(td :class "px-4 py-2" "camelCase"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Closures & mutation")
(td :class "px-4 py-2" "Cell variable hack")
(td :class "px-4 py-2" "Direct (reference capture)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Spec modules")
(td :class "px-4 py-2" "eval, render, html, sx, deps, signals")
(td :class "px-4 py-2" "All 12 modules"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Platform interface")
(td :class "px-4 py-2" "~300 lines")
(td :class "px-4 py-2" "~1500 lines (DOM, browser APIs)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "RENAMES table")
(td :class "px-4 py-2" "~200 entries")
(td :class "px-4 py-2" "~350 entries"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Component compilation")
(td :class "px-4 py-2 text-stone-400" "N/A")
(td :class "px-4 py-2" "Ahead-of-time DOM compiler"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Estimated size")
(td :class "px-4 py-2" "~800-1000 lines")
(td :class "px-4 py-2" "~1200-1500 lines"))))))
;; -----------------------------------------------------------------------
;; Implications
;; -----------------------------------------------------------------------
(~doc-section :title "Implications" :id "implications"
(~doc-subsection :title "Zero-Runtime Static Sites"
(p "A static page written in SX compiles to a JavaScript program with "
"no SX runtime dependency. The output is just DOM API calls — "
(code "createElement") ", " (code "appendChild") ", " (code "textContent")
". This gives SX a compilation target competitive with Svelte's "
"approach: components compile away, the framework disappears.")
(p "Combined with the " (a :href "/plans/content-addressed-components" "content-addressed components")
" plan, a page's compiled JS could be stored on IPFS by its content hash. "
"The server returns a CID. The browser fetches and executes pre-compiled JavaScript. "
"No parser, no evaluator, no network round-trip for component definitions."))
(~doc-subsection :title "Progressive Enhancement Layers"
(p "The component compiler naturally supports progressive enhancement:")
(ol :class "list-decimal pl-6 space-y-1 text-stone-700"
(li (strong "HTML") " — server renders to HTML string. No JS needed. Works everywhere.")
(li (strong "Compiled JS") " — server compiles to DOM construction code. "
"Event handlers work. No SX runtime. Kilobytes, not megabytes.")
(li (strong "SX runtime") " — full evaluator + engine. Client-side routing, "
"component caching, reactive islands. The current architecture.")
(li (strong "SX + signals") " — full reactive islands. Fine-grained DOM updates."))
(p "Each layer adds capability and weight. The right layer depends on the page. "
"A blog post needs layer 1. An interactive form needs layer 2. "
"A single-page app needs layer 3. A real-time dashboard needs layer 4. "
(code "js.sx") " makes layer 2 possible — it didn't exist before."))
(~doc-subsection :title "The Bootstrap Completion"
(p "With " (code "py.sx") " and " (code "js.sx") " both written in SX:")
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
(li "The " (em "spec") " defines SX semantics (" (code "eval.sx") ", " (code "render.sx") ", ...)")
(li "The " (em "translators") " convert the spec to host languages (" (code "py.sx") ", " (code "js.sx") ")")
(li "The " (em "prover") " verifies the spec's properties (" (code "z3.sx") ", " (code "prove.sx") ")")
(li "All four are written " (em "in") " SX, executable " (em "by") " any SX evaluator"))
(p "The language defines itself, verifies itself, and compiles itself. "
"The Python and JavaScript \"bootstrappers\" are not programs that produce SX — "
"they are SX programs that produce Python and JavaScript. "
"The arrow points the other way."))))))

402
sx/sx/plans/self-hosting-bootstrapper.sx Normal file
View File

@@ -0,0 +1,402 @@
;; ---------------------------------------------------------------------------
;; Self-Hosting Bootstrapper — py.sx
;; ---------------------------------------------------------------------------
(defcomp ~plan-self-hosting-bootstrapper-content ()
(~doc-page :title "Self-Hosting Bootstrapper"
;; -----------------------------------------------------------------------
;; The Idea
;; -----------------------------------------------------------------------
(~doc-section :title "The Idea" :id "idea"
(p "We have " (code "bootstrap_py.py") " — a Python program that reads "
(code ".sx") " spec files and emits " (code "sx_ref.py")
", a standalone Python evaluator. It's a compiler written in the host language.")
(p "We also have " (code "z3.sx") " — a translator written in SX itself that "
"converts SX spec declarations into SMT-LIB for Z3. It's proof that "
"SX can generate code in another language.")
(p "The next step: " (strong "py.sx") " — an SX-to-Python translator written in SX. "
"Feed it through the existing Python evaluator against the spec files and it produces "
(code "sx_ref.py") ". The bootstrapper bootstraps itself.")
(p "If " (code "py.sx") " produces output identical to " (code "bootstrap_py.py")
", the Python bootstrapper becomes redundant. "
"The spec defines itself."))
;; -----------------------------------------------------------------------
;; Architecture
;; -----------------------------------------------------------------------
(~doc-section :title "Architecture" :id "architecture"
(p "Three bootstrapper generations:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Gen")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Source")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Runs on")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Reads")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Produces")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono text-stone-600" "G0")
(td :class "px-4 py-2" (code "bootstrap_py.py"))
(td :class "px-4 py-2" "Python (manual)")
(td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...")
(td :class "px-4 py-2" (code "sx_ref.py")))
(tr :class "border-t border-stone-100 bg-violet-50"
(td :class "px-4 py-2 font-mono text-violet-700" "G1")
(td :class "px-4 py-2" (code "py.sx"))
(td :class "px-4 py-2" "Python evaluator + SX")
(td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...")
(td :class "px-4 py-2" (code "sx_ref.py") " (identical)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono text-stone-600" "G2")
(td :class "px-4 py-2" (code "py.sx"))
(td :class "px-4 py-2" (code "sx_ref.py") " from G1 + SX")
(td :class "px-4 py-2" (code "eval.sx") ", " (code "render.sx") ", ...")
(td :class "px-4 py-2" (code "sx_ref.py") " (fixed-point)")))))
(p "G0 is the hand-written compiler. G1 replaces it with SX. "
"G2 proves the fixed-point: " (code "py.sx") " compiled by its own output "
"produces the same output. That's the definition of self-hosting."))
;; -----------------------------------------------------------------------
;; Translation Rules
;; -----------------------------------------------------------------------
(~doc-section :title "Translation Rules" :id "translation"
(~doc-subsection :title "Name Mangling"
(p "SX identifiers become valid Python identifiers:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Python")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Rule")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "eval-expr")
(td :class "px-4 py-2 font-mono" "eval_expr")
(td :class "px-4 py-2" "kebab → snake"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "nil?")
(td :class "px-4 py-2 font-mono" "is_nil")
(td :class "px-4 py-2" "predicate rename"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "empty?")
(td :class "px-4 py-2 font-mono" "empty_p")
(td :class "px-4 py-2" "? → _p (general)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "set!")
(td :class "px-4 py-2 font-mono" "set_b")
(td :class "px-4 py-2" "! → _b"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "make-lambda")
(td :class "px-4 py-2 font-mono" "make_lambda")
(td :class "px-4 py-2" "platform function rename"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "type")
(td :class "px-4 py-2 font-mono" "type_")
(td :class "px-4 py-2" "Python reserved word escape"))))))
(~doc-subsection :title "Literals"
(~doc-code :code (highlight "(define py-literal
(fn (expr)
(cond
;; Bool before number (Python: bool subclass of int)
(= expr true) \"True\"
(= expr false) \"False\"
(nil? expr) \"NIL\"
(number? expr) (str expr)
(string? expr) (py-quote-string expr)
(= (type-of expr) \"keyword\") (py-quote-string (keyword-name expr))
(= (type-of expr) \"symbol\") (py-mangle (symbol-name expr))
:else (str expr))))" "lisp")))
(~doc-subsection :title "Special Forms"
(p "Each SX special form maps to a Python expression pattern:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "SX")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Python")))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(if c t e)")
(td :class "px-4 py-2 font-mono" "(t if sx_truthy(c) else e)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(when c body)")
(td :class "px-4 py-2 font-mono" "(body if sx_truthy(c) else NIL)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(let ((a 1)) body)")
(td :class "px-4 py-2 font-mono" "(lambda a: body)(1)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(fn (x) body)")
(td :class "px-4 py-2 font-mono" "lambda x: body"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(define name val)")
(td :class "px-4 py-2 font-mono" "name = val"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(and a b c)")
(td :class "px-4 py-2 font-mono" "(a if not sx_truthy(a) else (b if ... else c))"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(or a b c)")
(td :class "px-4 py-2 font-mono" "(a if sx_truthy(a) else (b if ... else c))"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(case x \"a\" 1 \"b\" 2)")
(td :class "px-4 py-2 font-mono" "_sx_case(x, [(\"a\", lambda: 1), ...])"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(str a b c)")
(td :class "px-4 py-2 font-mono" "sx_str(a, b, c)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(+ a b)")
(td :class "px-4 py-2 font-mono" "(a + b)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "(= a b)")
(td :class "px-4 py-2 font-mono" "(a == b)"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2 font-mono" "&rest args")
(td :class "px-4 py-2 font-mono" "*args"))))))
(~doc-subsection :title "Mutation: set! and Cell Variables"
(p "Python closures can read but not rebind outer variables. "
"SX " (code "set!") " from nested lambdas requires a cell indirection pattern:")
(~doc-code :code (highlight ";; SX
(define counter
(fn ()
(let ((n 0))
(fn () (set! n (+ n 1)) n))))
;; Python (impossible with plain lambda)
;; → uses _cells dict for mutable bindings
def counter():
_cells = {}
_cells['n'] = 0
return lambda: _sx_begin(
_sx_cell_set(_cells, 'n', (_cells['n'] + 1)),
_cells['n'])" "python"))
(p (code "py.sx") " must detect " (code "set!") " targets that cross lambda boundaries "
"and route them through the cell dictionary. "
"This is the hardest translation rule — the existing bootstrapper's "
(code "_find_nested_set_vars") " and " (code "_emit_define_as_def") " handle it.")))
;; -----------------------------------------------------------------------
;; Statement vs Expression
;; -----------------------------------------------------------------------
(~doc-section :title "Statement vs Expression Mode" :id "modes"
(p "The fundamental tension: SX is expression-oriented (everything returns a value). "
"Python has both expressions and statements. " (code "define") " must be a statement. "
(code "for-each") " with side effects wants a " (code "for") " loop.")
(p "The existing bootstrapper handles this with two methods:")
(ul :class "list-disc pl-6 space-y-2 text-stone-700"
(li (code "emit(expr)") " → Python expression (used inside other expressions)")
(li (code "emit_statement(expr, indent)") " → Python statement (used at top level and in def bodies)"))
(p (code "py.sx") " needs the same dual-mode emission. Top-level " (code "define") " forms "
"emit as statements. Everything else emits as expressions. Functions with "
(code "set!") " emit as " (code "def") " with proper statements instead of lambda expressions."))
;; -----------------------------------------------------------------------
;; Implementation Plan
;; -----------------------------------------------------------------------
(~doc-section :title "Implementation" :id "implementation"
(p "Build " (code "py.sx") " incrementally:")
(~doc-subsection :title "Phase 1: Core Expression Translator"
(p "Translate the SX subset used in the spec to Python expressions.")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "py-mangle") " — SX name → Python identifier (RENAMES table + general rules)")
(li (code "py-literal") " — atoms: numbers, strings, booleans, nil, symbols, keywords")
(li (code "py-expr") " — recursive expression translator")
(li "Infix operators: " (code "+") ", " (code "-") ", " (code "*") ", "
(code "/") ", " (code "=") "→" (code "==") ", " (code "!=") ", "
(code "<") ", " (code ">") ", " (code "<=") ", " (code ">=") ", " (code "mod") "→" (code "%"))
(li "Special forms: " (code "if") ", " (code "when") ", " (code "cond") ", "
(code "case") ", " (code "and") ", " (code "or") ", " (code "not"))
(li (code "let") " → nested IIFE lambdas")
(li (code "fn") "/" (code "lambda") " → Python " (code "lambda"))
(li (code "str") " → " (code "sx_str()"))
(li (code "list") " → " (code "[...]") " literal")
(li (code "dict") " → " (code "{...}") " literal")
(li (code "quote") " → AST constructor literals")))
(~doc-subsection :title "Phase 2: Statement Translator"
(p "Top-level forms and function bodies need statement mode:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "py-statement") " — emit as Python statement with indentation")
(li (code "define") " → " (code "name = expr") " or " (code "def name(): ..."))
(li (code "set!") " → assignment (direct or via _cells)")
(li (code "for-each") " → " (code "for") " loop")
(li (code "do") "/" (code "begin") " → sequential statements")
(li (code "when") " → " (code "if:") " block")
(li "Mutation detection: scan for " (code "set!") " across lambda boundaries")))
(~doc-subsection :title "Phase 3: File Translator"
(p "Process spec files the same way " (code "bootstrap_py.py") " does:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "py-extract-defines") " — parse .sx source, collect top-level defines")
(li (code "py-translate-file") " — translate a list of define expressions")
(li (code "py-translate-module") " — read a .sx file and produce Python source")
(li "Section labels: " (code "# === Transpiled from eval ===") " etc.")))
(~doc-subsection :title "Phase 4: Bootstrap Runner"
(p "A thin Python script that:")
(ol :class "list-decimal pl-6 space-y-1 text-stone-700"
(li "Loads " (code "py.sx") " into the SX evaluator")
(li "Parses each spec file (" (code "eval.sx") ", " (code "render.sx") ", etc.)")
(li "Calls " (code "py-translate-file") " on the parsed expressions")
(li "Emits the static preamble (types, platform interface)")
(li "Concatenates translated sections")
(li "Emits the static postamble (fixups, public API)"))
(p "The static sections (preamble, platform, primitives) stay in Python — "
"they're host-specific by definition. Only the transpilation of "
(code ".sx") " spec logic moves to SX."))
(~doc-subsection :title "Phase 5: Verification"
(p "Prove correctness by comparing outputs:")
(~doc-code :code (highlight "# Generate with hand-written bootstrapper
python bootstrap_py.py > sx_ref_g0.py
# Generate with py.sx (G1)
python run_py_sx.py > sx_ref_g1.py
# They must be identical
diff sx_ref_g0.py sx_ref_g1.py
# Generate with G1 output running py.sx (G2)
python run_py_sx_with_ref.py > sx_ref_g2.py
# Fixed-point: G1 == G2
diff sx_ref_g1.py sx_ref_g2.py" "bash"))
(p "When all three diffs are empty, the bootstrapper is self-hosting.")))
;; -----------------------------------------------------------------------
;; What py.sx is NOT
;; -----------------------------------------------------------------------
(~doc-section :title "Scope" :id "scope"
(p (code "py.sx") " is a general-purpose SX-to-Python translator. "
"The translation rules are mechanical and apply to " (em "all") " SX, "
"not just the spec subset.")
(~doc-subsection :title "Why General?"
(p "Every SX form has a straightforward Python equivalent:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "(div :class \"foo\" ...)") " → " (code "render_element(\"div\", {\"class\": \"foo\"}, ...)"))
(li (code "(~card :title \"hi\")") " → component function call with keyword args")
(li (code "defcomp") " → function definition with " (code "&key") " / " (code "&rest") " argument parsing")
(li (code "defmacro") " → function that returns AST (macros expand before translation)")
(li (code "defpage") " → route registration + handler function")
(li (code "defisland") " → island registration (same shape as " (code "defcomp") ")")
(li "I/O primitives → calls to host-provided functions"))
(p "The spec files are the " (em "first test case") " — because we can verify correctness "
"by diffing G0 and G1 output. But the translator itself is target-agnostic: "
"it translates SX syntax, not SX semantics."))
(~doc-subsection :title "Bootstrapping First, Then Everything"
(p "The implementation plan above starts with the spec subset (Phases 1-5) because "
"that's where the fixed-point proof lives. Once G1 == G0, extend to full SX:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (strong "Phase 6") ": Component and macro forms — " (code "defcomp") ", "
(code "defmacro") ", " (code "defisland") ", component calling convention")
(li (strong "Phase 7") ": HTML/DOM tags — translate " (code "(div ...)") " to render calls")
(li (strong "Phase 8") ": Page forms — " (code "defpage") ", " (code "defhandler") ", route wiring")
(li (strong "Phase 9") ": Full application files — translate any " (code ".sx") " file to a Python module"))
(p "At that point, " (code "py.sx") " can compile " (em "itself") " — and any SX application — "
"into Python. The bootstrapper is just the proof that the translation is correct. "
"The translator is the real product."))
(p "The full RENAMES table from " (code "bootstrap_py.py") " (200+ entries) moves into "
(code "py.sx") " as a dict literal. This is the largest single piece — "
"a mapping from SX names to their exact Python equivalents."))
;; -----------------------------------------------------------------------
;; Implications
;; -----------------------------------------------------------------------
(~doc-section :title "Implications" :id "implications"
(~doc-subsection :title "Level 1: Practical"
(p "One less Python file to maintain. Changes to the transpilation logic "
"are written in SX and tested with the SX test harness. The spec and its "
"compiler live in the same language."))
(~doc-subsection :title "Level 2: Architectural"
(p "With " (code "z3.sx") " (SMT-LIB), " (code "py.sx") " (Python), and "
(code "bootstrap_js.py") " → future " (code "js.sx") " (JavaScript), "
"the pattern is clear: SX translators are SX programs. "
"Adding a new target language means writing one " (code ".sx") " file, "
"not a new Python compiler.")
(p "The roadmap:")
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
(li (code "py.sx") " → Python (this plan)")
(li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")")
(li (code "go.sx") " → Go (new host)")
(li (code "rs.sx") " → Rust (new host)")
(li (code "hs.sx") " → Haskell (new host)"))
(p "Each new host only needs: (1) a minimal evaluator to run " (code "py.sx") " / "
(code "{host}.sx") " once, and (2) the platform interface in the target language."))
(~doc-subsection :title "Level 3: Philosophical"
(p "A self-hosting bootstrapper is a fixed point. The spec defines behavior. "
"The translator is itself defined in terms of that behavior. Running the "
"translator on the spec produces a program that can run the translator on "
"the spec and get the same program.")
(p "This is the same structure as a quine — a program that outputs itself. "
"But instead of textual self-reproduction, it's " (em "semantic") " "
"self-reproduction: the spec's meaning is preserved across the translation, "
"and the translation process is defined within the spec's language.")
(p "Gödel showed that any sufficiently powerful formal system can encode statements "
"about itself. A self-hosting bootstrapper is the constructive version: "
"the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself.")))
;; -----------------------------------------------------------------------
;; Existing Patterns
;; -----------------------------------------------------------------------
(~doc-section :title "Existing Patterns" :id "patterns"
(p "The " (code "z3.sx") " translator establishes the pattern " (code "py.sx") " follows:")
(div :class "overflow-x-auto rounded border border-stone-200 my-4"
(table :class "w-full text-sm"
(thead :class "bg-stone-50"
(tr
(th :class "px-4 py-2 text-left font-semibold text-stone-700" "Concern")
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "z3.sx"))
(th :class "px-4 py-2 text-left font-semibold text-stone-700" (code "py.sx"))))
(tbody
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Name mapping")
(td :class "px-4 py-2 font-mono" "z3-name, z3-sym")
(td :class "px-4 py-2 font-mono" "py-mangle"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Type mapping")
(td :class "px-4 py-2 font-mono" "z3-sort")
(td :class "px-4 py-2 font-mono" "—"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Expression emission")
(td :class "px-4 py-2 font-mono" "z3-expr")
(td :class "px-4 py-2 font-mono" "py-expr"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Keyword extraction")
(td :class "px-4 py-2 font-mono" "z3-extract-kwargs")
(td :class "px-4 py-2 font-mono" "py-extract-defines"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "File translation")
(td :class "px-4 py-2 font-mono" "z3-translate-file")
(td :class "px-4 py-2 font-mono" "py-translate-file"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Reader macro")
(td :class "px-4 py-2 font-mono" "#z3 expr")
(td :class "px-4 py-2 font-mono" "#py expr"))
(tr :class "border-t border-stone-100"
(td :class "px-4 py-2" "Complexity")
(td :class "px-4 py-2" "~360 lines")
(td :class "px-4 py-2" "~800-1000 lines (set!, statements)")))))
(p (code "py.sx") " is larger because Python's statement/expression duality "
"and closure mutation rules demand more translation machinery. "
"SMT-LIB is expression-only, so " (code "z3.sx") " never needs statement mode."))))

2
sx/sxc/pages/docs.sx
View File

@@ -634,6 +634,8 @@
"reader-macros" (~plan-reader-macros-content)
"reader-macro-demo" (~plan-reader-macro-demo-content)
"theorem-prover" (~plan-theorem-prover-content)
"self-hosting-bootstrapper" (~plan-self-hosting-bootstrapper-content)
"js-bootstrapper" (~plan-js-bootstrapper-content)
"sx-activity" (~plan-sx-activity-content)
"predictive-prefetch" (~plan-predictive-prefetch-content)
"content-addressed-components" (~plan-content-addressed-components-content)