"""
#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)