giles
00e7ba4650
Some checks failed
Build and Deploy / build-and-deploy (push) Has been cancelled
- prove.sx Phase 2: bounded model checking with 34 algebraic properties (commutativity, associativity, distributivity, inverses, bounds, transitivity) - prove.sx generates SMT-LIB for unbounded Z3 verification via z3-expr - New docs page /plans/theorem-prover with live results (91/91 sat, 34/34 verified) - Page helper runs both proof phases and returns structured data - Parser: re-add ' quote syntax (removed by prior edit) - Load prove.sx alongside z3.sx at startup Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
36 lines
1.1 KiB
Python
36 lines
1.1 KiB
Python
"""
|
|
Shared s-expression component definitions.
|
|
|
|
Loaded at app startup via ``load_shared_components()``. Each component
|
|
is defined in an external ``.sx`` file under ``templates/``.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import os
|
|
|
|
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", "prove.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())
|