diff --git a/shared/sx/components.py b/shared/sx/components.py index 92421bb..1535fa2 100644 --- a/shared/sx/components.py +++ b/shared/sx/components.py @@ -9,11 +9,27 @@ from __future__ import annotations import os -from .jinja_bridge import load_sx_dir, watch_sx_dir +from .jinja_bridge import load_sx_dir, register_reload_callback, watch_sx_dir def load_shared_components() -> None: """Register all shared s-expression components.""" + # Load SX libraries first — reader macros (#z3 etc.) must resolve + # before any .sx file that uses them is parsed + _load_sx_libraries() + register_reload_callback(_load_sx_libraries) + templates_dir = os.path.join(os.path.dirname(__file__), "templates") load_sx_dir(templates_dir) watch_sx_dir(templates_dir) + + +def _load_sx_libraries() -> None: + """Load self-hosted SX libraries from the ref directory.""" + from .jinja_bridge import register_components + ref_dir = os.path.join(os.path.dirname(__file__), "ref") + for name in ("z3.sx",): + path = os.path.join(ref_dir, name) + if os.path.exists(path): + with open(path, encoding="utf-8") as f: + register_components(f.read()) diff --git a/shared/sx/evaluator.py b/shared/sx/evaluator.py index 683fb6f..746c2f3 100644 --- a/shared/sx/evaluator.py +++ b/shared/sx/evaluator.py @@ -233,13 +233,20 @@ def _sf_cond(expr: list, env: dict) -> Any: clauses = expr[1:] if not clauses: return NIL - # Detect scheme-style: first clause is a 2-element list that isn't a comparison + # Detect scheme-style: first clause is a 2-element list that isn't a + # comparison or predicate call (predicates end in ?) + def _is_clojure_test(clause): + if not isinstance(clause, list) or len(clause) != 2: + return False + head = clause[0] + if not isinstance(head, Symbol): + return False + return (head.name in ("=", "<", ">", "<=", ">=", "!=", "and", "or") + or head.name.endswith("?")) if ( isinstance(clauses[0], list) and len(clauses[0]) == 2 - and not (isinstance(clauses[0][0], Symbol) and clauses[0][0].name in ( - "=", "<", ">", "<=", ">=", "!=", "and", "or", - )) + and not _is_clojure_test(clauses[0]) ): for clause in clauses: if not isinstance(clause, list) or len(clause) < 2: diff --git a/shared/sx/jinja_bridge.py b/shared/sx/jinja_bridge.py index 2648c8f..c64c8d3 100644 --- a/shared/sx/jinja_bridge.py +++ b/shared/sx/jinja_bridge.py @@ -98,7 +98,7 @@ def load_sx_dir(directory: str) -> None: Skips boundary.sx — those are parsed separately by the boundary validator. """ for filepath in sorted( - glob.glob(os.path.join(directory, "*.sx")) + glob.glob(os.path.join(directory, "**", "*.sx"), recursive=True) ): if os.path.basename(filepath) == "boundary.sx": continue @@ -112,6 +112,12 @@ def load_sx_dir(directory: str) -> None: _watched_dirs: list[str] = [] _file_mtimes: dict[str, float] = {} +_reload_callbacks: list[Any] = [] + + +def register_reload_callback(fn: Any) -> None: + """Register a function to call after hot-reload clears and reloads components.""" + _reload_callbacks.append(fn) def watch_sx_dir(directory: str) -> None: @@ -119,7 +125,7 @@ def watch_sx_dir(directory: str) -> None: _watched_dirs.append(directory) # Seed mtimes for fp in sorted( - glob.glob(os.path.join(directory, "*.sx")) + glob.glob(os.path.join(directory, "**", "*.sx"), recursive=True) ): _file_mtimes[fp] = os.path.getmtime(fp) @@ -129,7 +135,7 @@ def reload_if_changed() -> None: changed = False for directory in _watched_dirs: for fp in sorted( - glob.glob(os.path.join(directory, "*.sx")) + glob.glob(os.path.join(directory, "**", "*.sx"), recursive=True) ): mtime = os.path.getmtime(fp) if fp not in _file_mtimes or _file_mtimes[fp] != mtime: @@ -137,6 +143,9 @@ def reload_if_changed() -> None: changed = True if changed: _COMPONENT_ENV.clear() + # Reload SX libraries first (e.g. z3.sx) so reader macros resolve + for cb in _reload_callbacks: + cb() for directory in _watched_dirs: load_sx_dir(directory) diff --git a/shared/sx/parser.py b/shared/sx/parser.py index 2a6bdea..6f9eb77 100644 --- a/shared/sx/parser.py +++ b/shared/sx/parser.py @@ -32,6 +32,29 @@ def register_reader_macro(name: str, handler: Any) -> None: _READER_MACROS[name] = handler +def _resolve_sx_reader_macro(name: str): + """Auto-resolve a reader macro from the component env. + + If a file like z3.sx defines (define z3-translate ...), then #z3 is + automatically available as a reader macro without any Python registration. + Looks for {name}-translate as a Lambda in the component env. + """ + try: + from .jinja_bridge import get_component_env + from .evaluator import _trampoline, _call_lambda + from .types import Lambda + except ImportError: + return None + env = get_component_env() + fn = env.get(f"{name}-translate") + if fn is None or not isinstance(fn, Lambda): + return None + # Return a Python callable that invokes the SX lambda + def _sx_handler(expr): + return _trampoline(_call_lambda(fn, [expr], env)) + return _sx_handler + + # --------------------------------------------------------------------------- # SxExpr — pre-built sx source marker # --------------------------------------------------------------------------- @@ -114,8 +137,8 @@ class Tokenizer: NUMBER = re.compile(r"-?(?:\d+\.?\d*|\.\d+)(?:[eE][+-]?\d+)?") KEYWORD = re.compile(r":[a-zA-Z_~*+\-><=/!?&\[]{1}[a-zA-Z0-9_~*+\-><=/!?.:&/\[\]#,]*") # Symbols may start with alpha, _, or common operator chars, plus ~ for components, - # <> for the fragment symbol, and & for &key/&rest. - SYMBOL = re.compile(r"[a-zA-Z_~*+\-><=/!?&][a-zA-Z0-9_~*+\-><=/!?.:&]*") + # <> for the fragment symbol, & for &key/&rest, and unicode letters (é, ñ, em-dash…). + SYMBOL = re.compile(r"[a-zA-Z_~*+\-><=/!?&\u0080-\uFFFF][a-zA-Z0-9_~*+\-><=/!?.:&\u0080-\uFFFF]*") def __init__(self, text: str): self.text = text @@ -321,6 +344,9 @@ def _parse_expr(tok: Tokenizer) -> Any: if dispatch.isalpha() or dispatch in "_~": macro_name = tok._read_ident() handler = _READER_MACROS.get(macro_name) + if handler is None: + # Auto-resolve: look for {name}-translate in component env + handler = _resolve_sx_reader_macro(macro_name) if handler is None: raise ParseError(f"Unknown reader macro: #{macro_name}", tok.pos, tok.line, tok.col) diff --git a/shared/sx/primitives.py b/shared/sx/primitives.py index 5f74c42..27269d4 100644 --- a/shared/sx/primitives.py +++ b/shared/sx/primitives.py @@ -10,7 +10,7 @@ from __future__ import annotations import math from typing import Any, Callable -from .types import Keyword, NIL +from .types import Component, Island, Keyword, Lambda, Macro, NIL, Symbol # --------------------------------------------------------------------------- @@ -494,6 +494,56 @@ def prim_dict_set_mut(d: Any, key: Any, val: Any) -> Any: d[key] = val return val + +# --------------------------------------------------------------------------- +# Type introspection — platform primitives declared in eval.sx +# --------------------------------------------------------------------------- + +@register_primitive("type-of") +def prim_type_of(x: Any) -> str: + if isinstance(x, bool): + return "boolean" + if isinstance(x, (int, float)): + return "number" + if isinstance(x, str): + return "string" + if x is None or x is NIL: + return "nil" + if isinstance(x, Symbol): + return "symbol" + if isinstance(x, Keyword): + return "keyword" + if isinstance(x, list): + return "list" + if isinstance(x, dict): + return "dict" + if isinstance(x, Lambda): + return "lambda" + if isinstance(x, Component): + return "component" + if isinstance(x, Island): + return "island" + if isinstance(x, Macro): + return "macro" + return "unknown" + + +@register_primitive("symbol-name") +def prim_symbol_name(s: Any) -> str: + return s.name if isinstance(s, Symbol) else str(s) + + +@register_primitive("keyword-name") +def prim_keyword_name(k: Any) -> str: + return k.name if isinstance(k, Keyword) else str(k) + + +@register_primitive("sx-parse") +def prim_sx_parse(source: str) -> list: + from .parser import parse_all + return parse_all(source) + + @register_primitive("into") def prim_into(target: Any, coll: Any) -> Any: if isinstance(target, list): diff --git a/shared/sx/ref/primitives.sx b/shared/sx/ref/primitives.sx index 507a3b8..21fd182 100644 --- a/shared/sx/ref/primitives.sx +++ b/shared/sx/ref/primitives.sx @@ -553,3 +553,30 @@ :params (condition &rest message) :returns "boolean" :doc "Assert condition is truthy; raise error with message if not.") + + +;; -------------------------------------------------------------------------- +;; Type introspection — platform primitives +;; -------------------------------------------------------------------------- + +(define-module :stdlib.types) + +(define-primitive "type-of" + :params (x) + :returns "string" + :doc "Return type name: number, string, boolean, nil, symbol, keyword, list, dict, lambda, component, island, macro.") + +(define-primitive "symbol-name" + :params (sym) + :returns "string" + :doc "Return the name string of a symbol.") + +(define-primitive "keyword-name" + :params (kw) + :returns "string" + :doc "Return the name string of a keyword.") + +(define-primitive "sx-parse" + :params (source) + :returns "list" + :doc "Parse SX source string into a list of AST expressions.") diff --git a/shared/sx/ref/prove.sx b/shared/sx/ref/prove.sx new file mode 100644 index 0000000..57b6ca5 --- /dev/null +++ b/shared/sx/ref/prove.sx @@ -0,0 +1,404 @@ +;; ========================================================================== +;; prove.sx — SMT-LIB satisfiability checker, written in SX +;; +;; Verifies the SMT-LIB output from z3.sx. For the class of assertions +;; z3.sx produces (definitional equalities), satisfiability is provable +;; by construction: the definition IS the model. +;; +;; This closes the loop: +;; primitives.sx → z3.sx → SMT-LIB → prove.sx → sat +;; SX spec → SX translator → s-expressions → SX prover → proof +;; +;; The prover also evaluates each definition with concrete test values +;; to demonstrate consistency. +;; +;; Usage: +;; (prove-check smtlib-string) — verify a single check-sat block +;; (prove-translate expr) — translate + verify a define-* form +;; (prove-file exprs) — verify all define-* forms +;; ========================================================================== + + +;; -------------------------------------------------------------------------- +;; SMT-LIB expression evaluator +;; -------------------------------------------------------------------------- + +;; Evaluate an SMT-LIB expression in a variable environment +(define smt-eval + (fn (expr env) + (cond + ;; Numbers + (number? expr) expr + + ;; String literals + (string? expr) + (cond + (= expr "true") true + (= expr "false") false + :else expr) + + ;; Booleans + (= expr true) true + (= expr false) false + + ;; Symbols — look up in env + (= (type-of expr) "symbol") + (let ((name (symbol-name expr))) + (cond + (= name "true") true + (= name "false") false + :else (get env name expr))) + + ;; Lists — function application + (list? expr) + (if (empty? expr) nil + (let ((head (first expr)) + (args (rest expr))) + (if (not (= (type-of head) "symbol")) + expr + (let ((op (symbol-name head))) + (cond + ;; Arithmetic + (= op "+") + (reduce (fn (a b) (+ a b)) 0 + (map (fn (a) (smt-eval a env)) args)) + (= op "-") + (if (= (len args) 1) + (- 0 (smt-eval (first args) env)) + (- (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env))) + (= op "*") + (reduce (fn (a b) (* a b)) 1 + (map (fn (a) (smt-eval a env)) args)) + (= op "/") + (let ((a (smt-eval (nth args 0) env)) + (b (smt-eval (nth args 1) env))) + (if (= b 0) 0 (/ a b))) + (= op "div") + (let ((a (smt-eval (nth args 0) env)) + (b (smt-eval (nth args 1) env))) + (if (= b 0) 0 (/ a b))) + (= op "mod") + (let ((a (smt-eval (nth args 0) env)) + (b (smt-eval (nth args 1) env))) + (if (= b 0) 0 (mod a b))) + + ;; Comparison + (= op "=") + (= (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env)) + (= op "<") + (< (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env)) + (= op ">") + (> (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env)) + (= op "<=") + (<= (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env)) + (= op ">=") + (>= (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env)) + + ;; Logic + (= op "and") + (every? (fn (a) (smt-eval a env)) args) + (= op "or") + (some (fn (a) (smt-eval a env)) args) + (= op "not") + (not (smt-eval (first args) env)) + + ;; ite (if-then-else) + (= op "ite") + (if (smt-eval (nth args 0) env) + (smt-eval (nth args 1) env) + (smt-eval (nth args 2) env)) + + ;; Function call — look up in env + :else + (let ((fn-def (get env op nil))) + (if (nil? fn-def) + (list op (map (fn (a) (smt-eval a env)) args)) + ;; fn-def is {:params [...] :body expr} + (let ((params (get fn-def "params" (list))) + (body (get fn-def "body" nil)) + (evals (map (fn (a) (smt-eval a env)) args))) + (if (nil? body) + ;; Uninterpreted — return symbolic + (list op evals) + ;; Evaluate body with params bound + (smt-eval body + (merge env + (smt-bind-params params evals)))))))))))) + + :else expr))) + + +;; Bind parameter names to values +(define smt-bind-params + (fn (params vals) + (smt-bind-loop params vals {}))) + +(define smt-bind-loop + (fn (params vals acc) + (if (or (empty? params) (empty? vals)) + acc + (smt-bind-loop (rest params) (rest vals) + (assoc acc (first params) (first vals)))))) + + +;; -------------------------------------------------------------------------- +;; SMT-LIB statement parser +;; -------------------------------------------------------------------------- + +;; Extract declarations and assertions from parsed SMT-LIB +(define smt-extract-statements + (fn (exprs) + (smt-extract-loop exprs {} (list)))) + +(define smt-extract-loop + (fn (exprs decls assertions) + (if (empty? exprs) + {:decls decls :assertions assertions} + (let ((expr (first exprs)) + (rest-e (rest exprs))) + (if (not (list? expr)) + (smt-extract-loop rest-e decls assertions) + (if (empty? expr) + (smt-extract-loop rest-e decls assertions) + (let ((head (symbol-name (first expr)))) + (cond + ;; (declare-fun name (sorts) sort) + (= head "declare-fun") + (let ((name (nth expr 1)) + (param-sorts (nth expr 2)) + (ret-sort (nth expr 3))) + (smt-extract-loop rest-e + (assoc decls (if (= (type-of name) "symbol") + (symbol-name name) name) + {:params (if (list? param-sorts) + (map (fn (s) (if (= (type-of s) "symbol") + (symbol-name s) (str s))) + param-sorts) + (list)) + :ret (if (= (type-of ret-sort) "symbol") + (symbol-name ret-sort) (str ret-sort))}) + assertions)) + + ;; (assert ...) + (= head "assert") + (smt-extract-loop rest-e decls + (append assertions (list (nth expr 1)))) + + ;; (check-sat) — skip + (= head "check-sat") + (smt-extract-loop rest-e decls assertions) + + ;; comments (strings starting with ;) — skip + :else + (smt-extract-loop rest-e decls assertions))))))))) + + +;; -------------------------------------------------------------------------- +;; Assertion classifier +;; -------------------------------------------------------------------------- + +;; Check if an assertion is definitional: (forall (...) (= (f ...) body)) +;; or (= (f) body) for nullary +(define smt-definitional? + (fn (assertion) + (if (not (list? assertion)) false + (let ((head (symbol-name (first assertion)))) + (cond + ;; (forall ((bindings)) (= (f ...) body)) + (= head "forall") + (let ((body (nth assertion 2))) + (and (list? body) + (= (symbol-name (first body)) "="))) + ;; (= (f ...) body) + (= head "=") + true + :else false))))) + + +;; Extract the function name, parameters, and body from a definitional assertion +(define smt-extract-definition + (fn (assertion) + (let ((head (symbol-name (first assertion)))) + (cond + ;; (forall (((x Int) (y Int))) (= (f x y) body)) + (= head "forall") + (let ((bindings (first (nth assertion 1))) + (eq-expr (nth assertion 2)) + (call (nth eq-expr 1)) + (body (nth eq-expr 2))) + {:name (if (= (type-of (first call)) "symbol") + (symbol-name (first call)) (str (first call))) + :params (map (fn (b) + (if (list? b) + (if (= (type-of (first b)) "symbol") + (symbol-name (first b)) (str (first b))) + (if (= (type-of b) "symbol") + (symbol-name b) (str b)))) + (if (list? bindings) bindings (list bindings))) + :body body}) + + ;; (= (f) body) + (= head "=") + (let ((call (nth assertion 1)) + (body (nth assertion 2))) + {:name (if (list? call) + (if (= (type-of (first call)) "symbol") + (symbol-name (first call)) (str (first call))) + (str call)) + :params (list) + :body body}) + + :else nil)))) + + +;; -------------------------------------------------------------------------- +;; Test value generation +;; -------------------------------------------------------------------------- + +(define smt-test-values + (list + (list 0) + (list 1) + (list -1) + (list 5) + (list 42) + (list 1 2) + (list -3 7) + (list 5 5) + (list 100 -50) + (list 3 1) + (list 1 1 10) + (list 5 1 3) + (list -5 1 10) + (list 3 3 3) + (list 7 2 9))) + + +;; -------------------------------------------------------------------------- +;; Proof engine +;; -------------------------------------------------------------------------- + +;; Verify a single definitional assertion by construction + evaluation +(define smt-verify-definition + (fn (def-info decls) + (let ((name (get def-info "name")) + (params (get def-info "params")) + (body (get def-info "body")) + (n-params (len params))) + + ;; Build the model: define f = λparams.body + (let ((model (assoc decls name {:params params :body body})) + ;; Select test values matching arity + (tests (filter (fn (tv) (= (len tv) n-params)) smt-test-values)) + ;; Run tests + (results (map + (fn (test-vals) + (let ((env (merge model (smt-bind-params params test-vals))) + ;; Evaluate body directly + (body-result (smt-eval body env)) + ;; Evaluate via function call + (call-expr (cons (first (sx-parse name)) test-vals)) + (call-result (smt-eval call-expr env))) + {:vals test-vals + :body-result body-result + :call-result call-result + :equal (= body-result call-result)})) + tests))) + {:name name + :status (if (every? (fn (r) (get r "equal")) results) "sat" "FAIL") + :proof "by construction (definition is the model)" + :tests-passed (len (filter (fn (r) (get r "equal")) results)) + :tests-total (len results) + :sample (if (empty? results) nil (first results))})))) + + +;; -------------------------------------------------------------------------- +;; Public API +;; -------------------------------------------------------------------------- + +;; Strip SMT-LIB comment lines (starting with ;) and return only actual forms. +;; Handles comments that contain ( characters. +(define smt-strip-comments + (fn (s) + (let ((lines (split s "\n")) + (non-comment (filter + (fn (line) (not (starts-with? (trim line) ";"))) + lines))) + (join "\n" non-comment)))) + +;; Verify SMT-LIB output (string) — parse, classify, prove +(define prove-check + (fn (smtlib-str) + (let ((parsed (sx-parse (smt-strip-comments smtlib-str))) + (stmts (smt-extract-statements parsed)) + (decls (get stmts "decls")) + (assertions (get stmts "assertions"))) + (if (empty? assertions) + {:status "sat" :reason "no assertions (declaration only)"} + (let ((results (map + (fn (assertion) + (if (smt-definitional? assertion) + (let ((def-info (smt-extract-definition assertion))) + (if (nil? def-info) + {:status "unknown" :reason "could not parse definition"} + (smt-verify-definition def-info decls))) + {:status "unknown" + :reason "non-definitional assertion (needs full SMT solver)"})) + assertions))) + {:status (if (every? (fn (r) (= (get r "status") "sat")) results) + "sat" "unknown") + :assertions (len assertions) + :results results}))))) + + +;; Translate a define-* form AND verify it — the full pipeline +(define prove-translate + (fn (expr) + (let ((smtlib (z3-translate expr)) + (proof (prove-check smtlib)) + (status (get proof "status")) + (results (get proof "results" (list)))) + (str smtlib "\n" + ";; ─── prove.sx ───\n" + ";; status: " status "\n" + (if (empty? results) "" + (let ((r (first results))) + (str ";; proof: " (get r "proof" "") "\n" + ";; tested: " (str (get r "tests-passed" 0)) + "/" (str (get r "tests-total" 0)) + " ground instances\n"))))))) + + +;; Batch verify: translate and prove all define-* forms +(define prove-file + (fn (exprs) + (let ((translatable + (filter + (fn (expr) + (and (list? expr) + (>= (len expr) 2) + (= (type-of (first expr)) "symbol") + (let ((name (symbol-name (first expr)))) + (or (= name "define-primitive") + (= name "define-io-primitive") + (= name "define-special-form"))))) + exprs)) + (results (map + (fn (expr) + (let ((smtlib (z3-translate expr)) + (proof (prove-check smtlib)) + (name (nth expr 1))) + (assoc proof "name" name))) + translatable)) + (sat-count (len (filter (fn (r) (= (get r "status") "sat")) results))) + (total (len results))) + {:total total + :sat sat-count + :all-sat (= sat-count total) + :results results}))) diff --git a/shared/sx/ref/reader_z3.py b/shared/sx/ref/reader_z3.py index 3fcd62b..f5c7623 100644 --- a/shared/sx/ref/reader_z3.py +++ b/shared/sx/ref/reader_z3.py @@ -1,8 +1,9 @@ """ #z3 reader macro — translates SX spec declarations to SMT-LIB format. -Demonstrates extensible reader macros by converting define-primitive -declarations from primitives.sx into Z3 SMT-LIB verification conditions. +Self-hosted: loads z3.sx (the translator written in SX) and executes it +via the SX evaluator. The Python code here is pure host infrastructure — +all translation logic lives in z3.sx. Usage: from shared.sx.ref.reader_z3 import z3_translate, register_z3_macro @@ -15,284 +16,67 @@ Usage: """ from __future__ import annotations +import os from typing import Any -from shared.sx.types import Symbol, Keyword + +# --------------------------------------------------------------------------- +# Load z3.sx into an evaluator environment (cached) +# --------------------------------------------------------------------------- + +_z3_env: dict[str, Any] | None = None + + +def _get_z3_env() -> dict[str, Any]: + """Load and evaluate z3.sx, returning the environment with all z3-* functions. + + Platform primitives (type-of, symbol-name, keyword-name) are registered + in primitives.py. z3.sx uses canonical primitive names (get, assoc) so + no additional bindings are needed. + """ + global _z3_env + if _z3_env is not None: + return _z3_env + + from shared.sx.parser import parse_all + from shared.sx.evaluator import make_env, _eval, _trampoline + + env = make_env() + z3_path = os.path.join(os.path.dirname(__file__), "z3.sx") + with open(z3_path, encoding="utf-8") as f: + for expr in parse_all(f.read()): + _trampoline(_eval(expr, env)) + + _z3_env = env + return env # --------------------------------------------------------------------------- -# Type mapping +# Public API # --------------------------------------------------------------------------- -_SX_TO_SORT = { - "number": "Int", - "boolean": "Bool", - "string": "String", - "any": "Value", - "list": "(List Value)", - "dict": "(Array String Value)", -} - - -def _sort(sx_type: str) -> str: - return _SX_TO_SORT.get(sx_type, "Value") - - -# --------------------------------------------------------------------------- -# Expression translation: SX → SMT-LIB -# --------------------------------------------------------------------------- - -# SX operators that map directly to SMT-LIB -_IDENTITY_OPS = {"+", "-", "*", "/", "=", "!=", "<", ">", "<=", ">=", - "and", "or", "not", "mod"} - -# SX operators with SMT-LIB equivalents -_RENAME_OPS = { - "if": "ite", - "str": "str.++", -} - - -def _translate_expr(expr: Any) -> str: - """Translate an SX expression to SMT-LIB s-expression string.""" - if isinstance(expr, (int, float)): - if isinstance(expr, float): - return f"(to_real {int(expr)})" if expr == int(expr) else str(expr) - return str(expr) - - if isinstance(expr, str): - return f'"{expr}"' - - if isinstance(expr, bool): - return "true" if expr else "false" - - if expr is None: - return "nil_val" - - if isinstance(expr, Symbol): - name = expr.name - # Translate SX predicate names to SMT-LIB - if name.endswith("?"): - return "is_" + name[:-1].replace("-", "_") - return name.replace("-", "_").replace("!", "_bang") - - if isinstance(expr, list) and len(expr) > 0: - head = expr[0] - if isinstance(head, Symbol): - op = head.name - args = expr[1:] - - # Direct identity ops - if op in _IDENTITY_OPS: - smt_args = " ".join(_translate_expr(a) for a in args) - return f"({op} {smt_args})" - - # Renamed ops - if op in _RENAME_OPS: - smt_op = _RENAME_OPS[op] - smt_args = " ".join(_translate_expr(a) for a in args) - return f"({smt_op} {smt_args})" - - # max/min → ite - if op == "max" and len(args) == 2: - a, b = _translate_expr(args[0]), _translate_expr(args[1]) - return f"(ite (>= {a} {b}) {a} {b})" - if op == "min" and len(args) == 2: - a, b = _translate_expr(args[0]), _translate_expr(args[1]) - return f"(ite (<= {a} {b}) {a} {b})" - - # empty? → length check - if op == "empty?": - a = _translate_expr(args[0]) - return f"(= (len {a}) 0)" - - # first/rest → list ops - if op == "first": - return f"(head {_translate_expr(args[0])})" - if op == "rest": - return f"(tail {_translate_expr(args[0])})" - - # reduce with initial value - if op == "reduce" and len(args) >= 3: - return f"(reduce {_translate_expr(args[0])} {_translate_expr(args[2])} {_translate_expr(args[1])})" - - # fn (lambda) → unnamed function - if op == "fn": - params = args[0] if isinstance(args[0], list) else [args[0]] - param_str = " ".join(f"({_translate_expr(p)} Int)" for p in params) - body = _translate_expr(args[1]) - return f"(lambda (({param_str})) {body})" - - # native-* → bare op - if op.startswith("native-"): - bare = op[7:] # strip "native-" - smt_args = " ".join(_translate_expr(a) for a in args) - return f"({bare} {smt_args})" - - # Generic function call - smt_name = op.replace("-", "_").replace("?", "_p").replace("!", "_bang") - smt_args = " ".join(_translate_expr(a) for a in args) - return f"({smt_name} {smt_args})" - - return str(expr) - - -# --------------------------------------------------------------------------- -# Define-primitive → SMT-LIB -# --------------------------------------------------------------------------- - -def _extract_kwargs(expr: list) -> dict[str, Any]: - """Extract keyword arguments from a define-primitive form.""" - kwargs: dict[str, Any] = {} - i = 2 # skip head and name - while i < len(expr): - item = expr[i] - if isinstance(item, Keyword) and i + 1 < len(expr): - kwargs[item.name] = expr[i + 1] - i += 2 - else: - i += 1 - return kwargs - - -def _params_to_sorts(params: list) -> list[tuple[str, str]]: - """Convert SX param list to (name, sort) pairs, skipping &rest/&key.""" - result = [] - skip_next = False - for p in params: - if isinstance(p, Symbol) and p.name in ("&rest", "&key"): - skip_next = True - continue - if skip_next: - skip_next = False - continue - if isinstance(p, Symbol): - result.append((p.name, "Int")) - return result - - def z3_translate(expr: Any) -> str: - """Translate an SX define-primitive to SMT-LIB verification conditions. + """Translate an SX define-* form to SMT-LIB. - Input: parsed (define-primitive "name" :params (...) :returns "type" ...) - Output: SMT-LIB string with declare-fun and assert/check-sat. + Delegates to z3-translate defined in z3.sx. """ - if not isinstance(expr, list) or len(expr) < 2: - return f"; Cannot translate: not a list form" + from shared.sx.evaluator import _trampoline, _call_lambda - head = expr[0] - if not isinstance(head, Symbol): - return f"; Cannot translate: head is not a symbol" + env = _get_z3_env() + return _trampoline(_call_lambda(env["z3-translate"], [expr], env)) - form = head.name - - if form == "define-primitive": - return _translate_primitive(expr) - elif form == "define-io-primitive": - return _translate_io(expr) - elif form == "define-special-form": - return _translate_special_form(expr) - else: - # Generic expression translation - return _translate_expr(expr) - - -def _translate_primitive(expr: list) -> str: - """Translate define-primitive to SMT-LIB.""" - name = expr[1] if len(expr) > 1 else "?" - kwargs = _extract_kwargs(expr) - - params = kwargs.get("params", []) - returns = kwargs.get("returns", "any") - doc = kwargs.get("doc", "") - body = kwargs.get("body") - - # Build param sorts - param_pairs = _params_to_sorts(params if isinstance(params, list) else []) - has_rest = any(isinstance(p, Symbol) and p.name == "&rest" - for p in (params if isinstance(params, list) else [])) - - # SMT-LIB function name - if name == "!=": - smt_name = "neq" - elif name in ("+", "-", "*", "/", "=", "<", ">", "<=", ">="): - smt_name = name # keep arithmetic ops as-is - else: - smt_name = name.replace("-", "_").replace("?", "_p").replace("!", "_bang") - - lines = [f"; {name} — {doc}"] - - if has_rest: - # Variadic — declare as uninterpreted - lines.append(f"; (variadic — modeled as uninterpreted)") - lines.append(f"(declare-fun {smt_name} (Int Int) {_sort(returns)})") - else: - param_sorts = " ".join(s for _, s in param_pairs) - lines.append(f"(declare-fun {smt_name} ({param_sorts}) {_sort(returns)})") - - if body is not None and not has_rest: - # Generate forall assertion from body - if param_pairs: - bindings = " ".join(f"({p} Int)" for p, _ in param_pairs) - call_args = " ".join(p for p, _ in param_pairs) - smt_body = _translate_expr(body) - lines.append(f"(assert (forall (({bindings}))") - lines.append(f" (= ({smt_name} {call_args}) {smt_body})))") - else: - smt_body = _translate_expr(body) - lines.append(f"(assert (= ({smt_name}) {smt_body}))") - - lines.append("(check-sat)") - return "\n".join(lines) - - -def _translate_io(expr: list) -> str: - """Translate define-io-primitive — uninterpreted (cannot verify statically).""" - name = expr[1] if len(expr) > 1 else "?" - kwargs = _extract_kwargs(expr) - doc = kwargs.get("doc", "") - smt_name = name.replace("-", "_").replace("?", "_p") - return (f"; IO primitive: {name} — {doc}\n" - f"; (uninterpreted — IO cannot be verified statically)\n" - f"(declare-fun {smt_name} () Value)") - - -def _translate_special_form(expr: list) -> str: - """Translate define-special-form to SMT-LIB.""" - name = expr[1] if len(expr) > 1 else "?" - kwargs = _extract_kwargs(expr) - doc = kwargs.get("doc", "") - - if name == "if": - return (f"; Special form: if — {doc}\n" - f"(assert (forall ((c Bool) (t Value) (e Value))\n" - f" (= (sx_if c t e) (ite c t e))))\n" - f"(check-sat)") - elif name == "when": - return (f"; Special form: when — {doc}\n" - f"(assert (forall ((c Bool) (body Value))\n" - f" (= (sx_when c body) (ite c body nil_val))))\n" - f"(check-sat)") - - return f"; Special form: {name} — {doc}\n; (not directly expressible in SMT-LIB)" - - -# --------------------------------------------------------------------------- -# Batch translation: process an entire spec file -# --------------------------------------------------------------------------- def z3_translate_file(source: str) -> str: - """Parse an SX spec file and translate all define-primitive forms.""" + """Parse an SX spec file and translate all define-* forms to SMT-LIB. + + Delegates to z3-translate-file defined in z3.sx. + """ from shared.sx.parser import parse_all + from shared.sx.evaluator import _trampoline, _call_lambda + + env = _get_z3_env() exprs = parse_all(source) - results = [] - for expr in exprs: - if (isinstance(expr, list) and len(expr) >= 2 - and isinstance(expr[0], Symbol) - and expr[0].name in ("define-primitive", "define-io-primitive", - "define-special-form")): - results.append(z3_translate(expr)) - return "\n\n".join(results) + return _trampoline(_call_lambda(env["z3-translate-file"], [exprs], env)) # --------------------------------------------------------------------------- diff --git a/shared/sx/ref/z3.sx b/shared/sx/ref/z3.sx new file mode 100644 index 0000000..74717e8 --- /dev/null +++ b/shared/sx/ref/z3.sx @@ -0,0 +1,358 @@ +;; ========================================================================== +;; z3.sx — SX spec to SMT-LIB translator, written in SX +;; +;; Translates define-primitive, define-io-primitive, and define-special-form +;; declarations from the SX spec into SMT-LIB verification conditions for +;; Z3 and other theorem provers. +;; +;; This is the first self-hosted bootstrapper: the SX evaluator (itself +;; bootstrapped from eval.sx) executes this file against the spec to +;; produce output in a different language. Same pattern as bootstrap_js.py +;; and bootstrap_py.py, but written in SX instead of Python. +;; +;; Usage (from SX): +;; (z3-translate expr) — translate one define-* form +;; (z3-translate-file exprs) — translate a list of parsed expressions +;; +;; Usage (as reader macro): +;; #z3(define-primitive "inc" :params (n) :returns "number" :body (+ n 1)) +;; → "; inc — ...\n(declare-fun inc (Int) Int)\n..." +;; ========================================================================== + + +;; -------------------------------------------------------------------------- +;; Type mapping: SX type names → SMT-LIB sorts +;; -------------------------------------------------------------------------- + +(define z3-sort + (fn (sx-type) + (case sx-type + "number" "Int" + "boolean" "Bool" + "string" "String" + "list" "(List Value)" + "dict" "(Array String Value)" + :else "Value"))) + + +;; -------------------------------------------------------------------------- +;; Name translation: SX identifiers → SMT-LIB identifiers +;; -------------------------------------------------------------------------- + +(define z3-name + (fn (name) + (cond + (= name "!=") "neq" + (= name "+") "+" + (= name "-") "-" + (= name "*") "*" + (= name "/") "/" + (= name "=") "=" + (= name "<") "<" + (= name ">") ">" + (= name "<=") "<=" + (= name ">=") ">=" + :else (replace (replace (replace name "-" "_") "?" "_p") "!" "_bang")))) + +(define z3-sym + (fn (sym) + (let ((name (symbol-name sym))) + (cond + (ends-with? name "?") + (str "is_" (replace (slice name 0 (- (string-length name) 1)) "-" "_")) + :else + (replace (replace name "-" "_") "!" "_bang"))))) + + +;; -------------------------------------------------------------------------- +;; Expression translation: SX body expressions → SMT-LIB s-expressions +;; -------------------------------------------------------------------------- + +;; Operators that pass through unchanged +(define z3-identity-ops + (list "+" "-" "*" "/" "=" "!=" "<" ">" "<=" ">=" "and" "or" "not" "mod")) + +;; Operators that get renamed +(define z3-rename-op + (fn (op) + (case op + "if" "ite" + "str" "str.++" + :else nil))) + +(define z3-expr + (fn (expr) + (cond + ;; Numbers + (number? expr) + (str expr) + + ;; Strings + (string? expr) + (str "\"" expr "\"") + + ;; Booleans + (= expr true) "true" + (= expr false) "false" + + ;; Nil + (nil? expr) + "nil_val" + + ;; Symbols + (= (type-of expr) "symbol") + (z3-sym expr) + + ;; Lists (function calls / special forms) + (list? expr) + (if (empty? expr) + "()" + (let ((head (first expr)) + (args (rest expr))) + (if (not (= (type-of head) "symbol")) + (str expr) + (let ((op (symbol-name head))) + (cond + ;; Identity ops: same syntax in both languages + (some (fn (x) (= x op)) z3-identity-ops) + (str "(" op " " (join " " (map z3-expr args)) ")") + + ;; Renamed ops + (not (nil? (z3-rename-op op))) + (str "(" (z3-rename-op op) " " (join " " (map z3-expr args)) ")") + + ;; max → ite + (and (= op "max") (= (len args) 2)) + (let ((a (z3-expr (nth args 0))) + (b (z3-expr (nth args 1)))) + (str "(ite (>= " a " " b ") " a " " b ")")) + + ;; min → ite + (and (= op "min") (= (len args) 2)) + (let ((a (z3-expr (nth args 0))) + (b (z3-expr (nth args 1)))) + (str "(ite (<= " a " " b ") " a " " b ")")) + + ;; empty? → length check + (= op "empty?") + (str "(= (len " (z3-expr (first args)) ") 0)") + + ;; first/rest → list ops + (= op "first") + (str "(head " (z3-expr (first args)) ")") + (= op "rest") + (str "(tail " (z3-expr (first args)) ")") + + ;; reduce with initial value + (and (= op "reduce") (>= (len args) 3)) + (str "(reduce " (z3-expr (nth args 0)) " " + (z3-expr (nth args 2)) " " + (z3-expr (nth args 1)) ")") + + ;; fn (lambda) + (= op "fn") + (let ((params (first args)) + (body (nth args 1))) + (str "(lambda ((" + (join " " (map (fn (p) (str "(" (z3-sym p) " Int)")) params)) + ")) " (z3-expr body) ")")) + + ;; native-* → strip prefix + (starts-with? op "native-") + (str "(" (slice op 7 (string-length op)) " " + (join " " (map z3-expr args)) ")") + + ;; Generic function call + :else + (str "(" (z3-name op) " " + (join " " (map z3-expr args)) ")")))))) + + ;; Fallback + :else (str expr)))) + + +;; -------------------------------------------------------------------------- +;; Keyword argument extraction from define-* forms +;; -------------------------------------------------------------------------- + +(define z3-extract-kwargs + (fn (expr) + ;; Returns a dict of keyword args from a define-* form + ;; (define-primitive "name" :params (...) :returns "type" ...) → {:params ... :returns ...} + (let ((result {}) + (items (rest (rest expr)))) ;; skip head and name + (z3-extract-kwargs-loop items result)))) + +(define z3-extract-kwargs-loop + (fn (items result) + (if (or (empty? items) (< (len items) 2)) + result + (if (= (type-of (first items)) "keyword") + (z3-extract-kwargs-loop + (rest (rest items)) + (assoc result (keyword-name (first items)) (nth items 1))) + (z3-extract-kwargs-loop (rest items) result))))) + + +;; -------------------------------------------------------------------------- +;; Parameter processing +;; -------------------------------------------------------------------------- + +(define z3-params-to-sorts + (fn (params) + ;; Convert SX param list to list of (name sort) pairs, skipping &rest/&key + (z3-params-loop params false (list)))) + +(define z3-params-loop + (fn (params skip-next acc) + (if (empty? params) + acc + (let ((p (first params)) + (rest-p (rest params))) + (cond + ;; &rest or &key marker — skip it and the next param + (and (= (type-of p) "symbol") + (or (= (symbol-name p) "&rest") + (= (symbol-name p) "&key"))) + (z3-params-loop rest-p true acc) + ;; Skipping the param after &rest/&key + skip-next + (z3-params-loop rest-p false acc) + ;; Normal parameter + (= (type-of p) "symbol") + (z3-params-loop rest-p false + (append acc (list (list (symbol-name p) "Int")))) + ;; Something else — skip + :else + (z3-params-loop rest-p false acc)))))) + +(define z3-has-rest? + (fn (params) + (some (fn (p) (and (= (type-of p) "symbol") (= (symbol-name p) "&rest"))) + params))) + + +;; -------------------------------------------------------------------------- +;; define-primitive → SMT-LIB +;; -------------------------------------------------------------------------- + +(define z3-translate-primitive + (fn (expr) + (let ((name (nth expr 1)) + (kwargs (z3-extract-kwargs expr)) + (params (or (get kwargs "params") (list))) + (returns (or (get kwargs "returns") "any")) + (doc (or (get kwargs "doc") "")) + (body (get kwargs "body")) + (pairs (z3-params-to-sorts params)) + (has-rest (z3-has-rest? params)) + (smt-name (z3-name name))) + + (str + ;; Comment header + "; " name " — " doc "\n" + + ;; Declaration + (if has-rest + (str "; (variadic — modeled as uninterpreted)\n" + "(declare-fun " smt-name " (Int Int) " (z3-sort returns) ")") + (str "(declare-fun " smt-name " (" + (join " " (map (fn (pair) (nth pair 1)) pairs)) + ") " (z3-sort returns) ")")) + "\n" + + ;; Assertion (if body exists and not variadic) + (if (and (not (nil? body)) (not has-rest)) + (if (empty? pairs) + ;; No params — simple assertion + (str "(assert (= (" smt-name ") " (z3-expr body) "))\n") + ;; With params — forall + (let ((bindings (join " " (map (fn (pair) (str "(" (nth pair 0) " Int)")) pairs))) + (call-args (join " " (map (fn (pair) (nth pair 0)) pairs)))) + (str "(assert (forall ((" bindings "))\n" + " (= (" smt-name " " call-args ") " (z3-expr body) ")))\n"))) + "") + + ;; Check satisfiability + "(check-sat)")))) + + +;; -------------------------------------------------------------------------- +;; define-io-primitive → SMT-LIB +;; -------------------------------------------------------------------------- + +(define z3-translate-io + (fn (expr) + (let ((name (nth expr 1)) + (kwargs (z3-extract-kwargs expr)) + (doc (or (get kwargs "doc") "")) + (smt-name (replace (replace name "-" "_") "?" "_p"))) + (str "; IO primitive: " name " — " doc "\n" + "; (uninterpreted — IO cannot be verified statically)\n" + "(declare-fun " smt-name " () Value)")))) + + +;; -------------------------------------------------------------------------- +;; define-special-form → SMT-LIB +;; -------------------------------------------------------------------------- + +(define z3-translate-special-form + (fn (expr) + (let ((name (nth expr 1)) + (kwargs (z3-extract-kwargs expr)) + (doc (or (get kwargs "doc") ""))) + (case name + "if" + (str "; Special form: if — " doc "\n" + "(assert (forall ((c Bool) (t Value) (e Value))\n" + " (= (sx_if c t e) (ite c t e))))\n" + "(check-sat)") + "when" + (str "; Special form: when — " doc "\n" + "(assert (forall ((c Bool) (body Value))\n" + " (= (sx_when c body) (ite c body nil_val))))\n" + "(check-sat)") + :else + (str "; Special form: " name " — " doc "\n" + "; (not directly expressible in SMT-LIB)"))))) + + +;; -------------------------------------------------------------------------- +;; Top-level dispatch +;; -------------------------------------------------------------------------- + +(define z3-translate + (fn (expr) + (if (not (list? expr)) + "; Cannot translate: not a list form" + (if (< (len expr) 2) + "; Cannot translate: too short" + (let ((head (first expr))) + (if (not (= (type-of head) "symbol")) + "; Cannot translate: head is not a symbol" + (case (symbol-name head) + "define-primitive" (z3-translate-primitive expr) + "define-io-primitive" (z3-translate-io expr) + "define-special-form" (z3-translate-special-form expr) + :else (z3-expr expr)))))))) + + +;; -------------------------------------------------------------------------- +;; Batch translation: process a list of parsed expressions +;; -------------------------------------------------------------------------- + +(define z3-translate-file + (fn (exprs) + ;; Filter to translatable forms and translate each + (let ((translatable + (filter + (fn (expr) + (and (list? expr) + (>= (len expr) 2) + (= (type-of (first expr)) "symbol") + (let ((name (symbol-name (first expr)))) + (or (= name "define-primitive") + (= name "define-io-primitive") + (= name "define-special-form"))))) + exprs))) + (join "\n\n" (map z3-translate translatable))))) diff --git a/sx/sx/essays.sx b/sx/sx/essays.sx deleted file mode 100644 index c8362d6..0000000 --- a/sx/sx/essays.sx +++ /dev/null @@ -1,1232 +0,0 @@ -;; Essay content — static content extracted from essays.py - -;; --------------------------------------------------------------------------- -;; Philosophy section content -;; --------------------------------------------------------------------------- - -(defcomp ~philosophy-index-content () - (~doc-page :title "Philosophy" - (div :class "space-y-4" - (p :class "text-lg text-stone-600 mb-4" - "The deeper ideas behind SX — manifestos, self-reference, and the philosophical traditions that shaped the language.") - (div :class "space-y-3" - (map (fn (item) - (a :href (get item "href") - :sx-get (get item "href") :sx-target "#main-panel" :sx-select "#main-panel" - :sx-swap "outerHTML" :sx-push-url "true" - :class "block rounded border border-stone-200 p-4 hover:border-violet-300 hover:bg-violet-50 transition-colors" - (div :class "font-semibold text-stone-800" (get item "label")) - (when (get item "summary") - (p :class "text-sm text-stone-500 mt-1" (get item "summary"))))) - philosophy-nav-items))))) - -(defcomp ~essay-sx-and-wittgenstein () - (~doc-page :title "SX and Wittgenstein" - (p :class "text-stone-500 text-sm italic mb-8" - "The limits of my language are the limits of my world.") - (~doc-section :title "I. Language games" :id "language-games" - (p :class "text-stone-600" - "In 1953, Ludwig " (a :href "https://en.wikipedia.org/wiki/Ludwig_Wittgenstein" :class "text-violet-600 hover:underline" "Wittgenstein") " published " (a :href "https://en.wikipedia.org/wiki/Philosophical_Investigations" :class "text-violet-600 hover:underline" "Philosophical Investigations") " — a book that dismantled the theory of language he had built in his own earlier work. The " (a :href "https://en.wikipedia.org/wiki/Tractatus_Logico-Philosophicus" :class "text-violet-600 hover:underline" "Tractatus") " had argued that language pictures the world: propositions mirror facts, and the structure of a sentence corresponds to the structure of reality. The Investigations abandoned this. Language does not picture anything. Language is " (em "used") ".") - (p :class "text-stone-600" - "Wittgenstein replaced the picture theory with " (a :href "https://en.wikipedia.org/wiki/Language_game_(philosophy)" :class "text-violet-600 hover:underline" "language games") " — activities in which words get their meaning from how they are employed, not from what they refer to. \"Slab!\" on a building site means \"bring me a slab.\" The same word in a dictionary means nothing until it enters a game. Meaning is use.") - (p :class "text-stone-600" - "Web development is a proliferation of language games. HTML is one game — a markup game where tags denote structure. CSS is another — a declaration game where selectors denote style. JavaScript is a third — an imperative game where statements denote behaviour. JSX is a fourth game layered on top of the third, pretending to be the first. TypeScript is a fifth game that annotates the third. Each has its own grammar, its own rules, its own way of meaning.") - (p :class "text-stone-600" - "SX collapses these into a single game. " (code "(div :class \"p-4\" (h2 title))") " is simultaneously structure (a div containing an h2), style (the class attribute), and behaviour (the symbol " (code "title") " is evaluated). There is one syntax, one set of rules, one way of meaning. Not because the distinctions between structure, style, and behaviour have been erased — they haven't — but because they are all expressed in the same language game.")) - (~doc-section :title "II. The limits of my language" :id "limits" - (p :class "text-stone-600" - "\"" (a :href "https://en.wikipedia.org/wiki/Tractatus_Logico-Philosophicus" :class "text-violet-600 hover:underline" "Die Grenzen meiner Sprache bedeuten die Grenzen meiner Welt") "\" — the limits of my language mean the limits of my world. This is proposition 5.6 of the Tractatus, and it is the most important sentence Wittgenstein ever wrote.") - (p :class "text-stone-600" - "If your language is HTML, your world is documents. You can link documents. You can nest elements inside documents. You cannot compose documents from smaller documents without a server-side include, an iframe, or JavaScript. The language does not have composition, so your world does not have composition.") - (p :class "text-stone-600" - "If your language is React, your world is components that re-render. You can compose components. You can pass props. You cannot inspect a component's structure at runtime without React DevTools. You cannot serialize a component tree to a format another framework can consume. You cannot send a component over HTTP and have it work on the other side without the same React runtime. The language has composition but not portability, so your world has composition but not portability.") - (p :class "text-stone-600" - "If your language is s-expressions, your world is " (em "expressions") ". An expression can represent a DOM node, a function call, a style declaration, a macro transformation, a component definition, a wire-format payload, or a specification of the evaluator itself. The language has no built-in limits on what can be expressed, because the syntax — the list — can represent anything. The limits of the language are only the limits of what you choose to evaluate.") - (~doc-code :lang "lisp" :code - ";; The same syntax expresses everything:\n(div :class \"card\" (h2 \"Title\")) ;; structure\n(css :flex :gap-4 :p-2) ;; style\n(defcomp ~card (&key title) (div title)) ;; abstraction\n(defmacro ~log (x) `(console.log ,x)) ;; metaprogramming\n(quote (div :class \"card\" (h2 \"Title\"))) ;; data about structure") - (p :class "text-stone-600" - "Wittgenstein's proposition cuts both ways. A language that limits you to documents limits your world to documents. A language that can express anything — because its syntax is the minimal recursive structure — limits your world to " (em "everything") ".")) - (~doc-section :title "III. Whereof one cannot speak" :id "silence" - (p :class "text-stone-600" - "The Tractatus ends: \"" (a :href "https://en.wikipedia.org/wiki/Tractatus_Logico-Philosophicus#Proposition_7" :class "text-violet-600 hover:underline" "Whereof one cannot speak, thereof one must be silent") ".\" Proposition 7. The things that cannot be said in a language simply do not exist within that language's world.") - (p :class "text-stone-600" - "HTML cannot speak of composition. It is silent on components. You cannot define " (code "~card") " in HTML. You can define " (code "