giles
29c90a625b
EvalError moved to types.py. All 27 files updated to import eval_expr, trampoline, call_lambda, etc. directly from shared.sx.ref.sx_ref instead of through the evaluator.py indirection layer. 320/320 spec tests pass. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
90 lines
2.9 KiB
Python
90 lines
2.9 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.ref.sx_ref import make_env, eval_expr as _eval, trampoline as _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.ref.sx_ref import trampoline as _trampoline, call_lambda as _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.ref.sx_ref import trampoline as _trampoline, call_lambda as _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)
|