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>
This commit is contained in:
@@ -159,6 +159,8 @@
|
||||
: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 "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"
|
||||
|
||||
378
sx/sx/plans/self-hosting-bootstrapper.sx
Normal file
378
sx/sx/plans/self-hosting-bootstrapper.sx
Normal file
@@ -0,0 +1,378 @@
|
||||
;; ---------------------------------------------------------------------------
|
||||
;; 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 and Non-Goals" :id "scope"
|
||||
(p (code "py.sx") " is " (em "not") " a general-purpose SX-to-Python compiler. "
|
||||
"It only needs to translate the restricted SX subset used in the spec files:")
|
||||
(ul :class "list-disc pl-6 space-y-1 text-stone-700"
|
||||
(li "No " (code "defcomp") " / " (code "defmacro") " emission — those are runtime constructs that " (code "eval.sx") " itself handles")
|
||||
(li "No HTML rendering — that's inside the spec, not the translation")
|
||||
(li "No I/O — the spec is pure functions")
|
||||
(li "No " (code "defpage") " / " (code "defhandler") " — those are app-level forms"))
|
||||
(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."))))
|
||||
@@ -634,6 +634,7 @@
|
||||
"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)
|
||||
"sx-activity" (~plan-sx-activity-content)
|
||||
"predictive-prefetch" (~plan-predictive-prefetch-content)
|
||||
"content-addressed-components" (~plan-content-addressed-components-content)
|
||||
|
||||
Reference in New Issue
Block a user