giles
3ca89ef765
- z3.sx: SX-to-SMT-LIB translator written in SX (359 lines), replaces Python translation logic - prove.sx: SMT-LIB satisfiability checker in SX — proves all 91 primitives sat by construction - Parser: support unicode characters (em-dash, accented letters) in symbols - Auto-resolve reader macros: #name finds name-translate in component env, no Python registration - Platform primitives: type-of, symbol-name, keyword-name, sx-parse registered in primitives.py - Cond heuristic: predicates ending in ? recognized as Clojure-style tests - Library loading: z3.sx loaded at startup with reload callbacks for hot-reload ordering - reader_z3.py: rewritten as thin shell delegating to z3.sx - Split monolithic .sx files: essays (22), plans (13), reactive-islands (6) into separate files Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
90 lines
2.8 KiB
Python
90 lines
2.8 KiB
Python
"""
|
|
#z3 reader macro — translates SX spec declarations to SMT-LIB format.
|
|
|
|
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
|
|
|
|
# Register as reader macro (enables #z3 in parser)
|
|
register_z3_macro()
|
|
|
|
# Or call directly
|
|
smtlib = z3_translate(parse('(define-primitive "inc" :params (n) ...)'))
|
|
"""
|
|
from __future__ import annotations
|
|
|
|
import os
|
|
from typing import Any
|
|
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# 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
|
|
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# Public API
|
|
# ---------------------------------------------------------------------------
|
|
|
|
def z3_translate(expr: Any) -> str:
|
|
"""Translate an SX define-* form to SMT-LIB.
|
|
|
|
Delegates to z3-translate defined in z3.sx.
|
|
"""
|
|
from shared.sx.evaluator import _trampoline, _call_lambda
|
|
|
|
env = _get_z3_env()
|
|
return _trampoline(_call_lambda(env["z3-translate"], [expr], env))
|
|
|
|
|
|
def z3_translate_file(source: str) -> str:
|
|
"""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)
|
|
return _trampoline(_call_lambda(env["z3-translate-file"], [exprs], env))
|
|
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# Reader macro registration
|
|
# ---------------------------------------------------------------------------
|
|
|
|
def register_z3_macro():
|
|
"""Register #z3 as a reader macro in the SX parser."""
|
|
from shared.sx.parser import register_reader_macro
|
|
register_reader_macro("z3", z3_translate)
|