Delete sx_ref.py — OCaml is the sole SX evaluator
Removes the 5993-line bootstrapped Python evaluator (sx_ref.py) and all
code that depended on it exclusively. Both bootstrappers (JS + OCaml)
now use a new synchronous OCaml bridge (ocaml_sync.py) to run the
transpiler. JS build produces identical output; OCaml bootstrap produces
byte-identical sx_ref.ml.
Key changes:
- New shared/sx/ocaml_sync.py: sync subprocess bridge to sx_server.exe
- hosts/javascript/bootstrap.py: serialize defines → temp file → OCaml eval
- hosts/ocaml/bootstrap.py: same pattern for OCaml transpiler
- shared/sx/{html,async_eval,resolver,jinja_bridge,handlers,pages,deps,helpers}:
stub or remove sx_ref imports; runtime uses OCaml bridge (SX_USE_OCAML=1)
- sx/sxc/pages: parse defpage/defhandler from AST instead of Python eval
- hosts/ocaml/lib/sx_primitives.ml: append handles non-list 2nd arg per spec
- Deleted: sx_ref.py, async_eval_ref.py, 6 Python test runners, misc ref/ files
Test results: JS 1078/1078, OCaml 1114/1114.
sx_docs SSR has pre-existing rendering issues to investigate separately.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -1,22 +0,0 @@
|
||||
"""Async evaluation — thin re-export from bootstrapped sx_ref.py.
|
||||
|
||||
The async adapter (adapter-async.sx) is now bootstrapped directly into
|
||||
sx_ref.py alongside the sync evaluator. This file re-exports the public
|
||||
API so existing imports keep working.
|
||||
|
||||
All async rendering, serialization, and evaluation logic lives in the spec:
|
||||
- shared/sx/ref/adapter-async.sx (canonical SX source)
|
||||
- shared/sx/ref/sx_ref.py (bootstrapped Python)
|
||||
|
||||
Platform async primitives (I/O dispatch, context vars, RequestContext)
|
||||
are in shared/sx/ref/platform_py.py → PLATFORM_ASYNC_PY.
|
||||
"""
|
||||
|
||||
from . import sx_ref
|
||||
|
||||
# Re-export the public API used by handlers.py, helpers.py, pages.py, etc.
|
||||
EvalError = sx_ref.EvalError
|
||||
async_eval = sx_ref.async_eval
|
||||
async_render = sx_ref.async_render
|
||||
async_eval_to_sx = sx_ref.async_eval_to_sx
|
||||
async_eval_slot_to_sx = sx_ref.async_eval_slot_to_sx
|
||||
@@ -1,245 +0,0 @@
|
||||
#!/usr/bin/env python3
|
||||
"""
|
||||
Bootstrap compiler: test.sx -> pytest test module.
|
||||
|
||||
Reads test.sx and emits a Python test file that runs each deftest
|
||||
as a pytest test case, grouped into classes by defsuite.
|
||||
|
||||
The emitted tests use the SX evaluator to run SX test bodies,
|
||||
verifying that the Python implementation matches the spec.
|
||||
|
||||
Usage:
|
||||
python bootstrap_test.py --output shared/sx/tests/test_sx_spec.py
|
||||
pytest shared/sx/tests/test_sx_spec.py -v
|
||||
"""
|
||||
from __future__ import annotations
|
||||
|
||||
import os
|
||||
import re
|
||||
import sys
|
||||
import argparse
|
||||
|
||||
_HERE = os.path.dirname(os.path.abspath(__file__))
|
||||
_PROJECT = os.path.abspath(os.path.join(_HERE, "..", "..", ".."))
|
||||
sys.path.insert(0, _PROJECT)
|
||||
|
||||
from shared.sx.parser import parse_all
|
||||
from shared.sx.types import Symbol, Keyword, NIL as SX_NIL
|
||||
|
||||
|
||||
def _slugify(name: str) -> str:
|
||||
"""Convert a test/suite name to a valid Python identifier."""
|
||||
s = name.lower().strip()
|
||||
s = re.sub(r'[^a-z0-9]+', '_', s)
|
||||
s = s.strip('_')
|
||||
return s
|
||||
|
||||
|
||||
def _sx_to_source(expr) -> str:
|
||||
"""Convert an SX AST node back to SX source string."""
|
||||
if isinstance(expr, bool):
|
||||
return "true" if expr else "false"
|
||||
if isinstance(expr, (int, float)):
|
||||
return str(expr)
|
||||
if isinstance(expr, str):
|
||||
escaped = expr.replace('\\', '\\\\').replace('"', '\\"')
|
||||
return f'"{escaped}"'
|
||||
if expr is None or expr is SX_NIL:
|
||||
return "nil"
|
||||
if isinstance(expr, Symbol):
|
||||
return expr.name
|
||||
if isinstance(expr, Keyword):
|
||||
return f":{expr.name}"
|
||||
if isinstance(expr, dict):
|
||||
pairs = []
|
||||
for k, v in expr.items():
|
||||
pairs.append(f":{k} {_sx_to_source(v)}")
|
||||
return "{" + " ".join(pairs) + "}"
|
||||
if isinstance(expr, list):
|
||||
if not expr:
|
||||
return "()"
|
||||
return "(" + " ".join(_sx_to_source(e) for e in expr) + ")"
|
||||
return str(expr)
|
||||
|
||||
|
||||
def _parse_test_sx(path: str) -> tuple[list[dict], list]:
|
||||
"""Parse test.sx and return (suites, preamble_exprs).
|
||||
|
||||
Preamble exprs are define forms (assertion helpers) that must be
|
||||
evaluated before tests run. Suites contain the actual test cases.
|
||||
"""
|
||||
with open(path) as f:
|
||||
content = f.read()
|
||||
|
||||
exprs = parse_all(content)
|
||||
suites = []
|
||||
preamble = []
|
||||
|
||||
for expr in exprs:
|
||||
if not isinstance(expr, list) or not expr:
|
||||
continue
|
||||
head = expr[0]
|
||||
if isinstance(head, Symbol) and head.name == "defsuite":
|
||||
suite = _parse_suite(expr)
|
||||
if suite:
|
||||
suites.append(suite)
|
||||
elif isinstance(head, Symbol) and head.name == "define":
|
||||
preamble.append(expr)
|
||||
|
||||
return suites, preamble
|
||||
|
||||
|
||||
def _parse_suite(expr: list) -> dict | None:
|
||||
"""Parse a (defsuite "name" ...) form."""
|
||||
if len(expr) < 2:
|
||||
return None
|
||||
|
||||
name = expr[1]
|
||||
if not isinstance(name, str):
|
||||
return None
|
||||
|
||||
tests = []
|
||||
for child in expr[2:]:
|
||||
if not isinstance(child, list) or not child:
|
||||
continue
|
||||
head = child[0]
|
||||
if isinstance(head, Symbol):
|
||||
if head.name == "deftest":
|
||||
test = _parse_test(child)
|
||||
if test:
|
||||
tests.append(test)
|
||||
elif head.name == "defsuite":
|
||||
sub = _parse_suite(child)
|
||||
if sub:
|
||||
tests.append(sub)
|
||||
|
||||
return {"type": "suite", "name": name, "tests": tests}
|
||||
|
||||
|
||||
def _parse_test(expr: list) -> dict | None:
|
||||
"""Parse a (deftest "name" body ...) form."""
|
||||
if len(expr) < 3:
|
||||
return None
|
||||
name = expr[1]
|
||||
if not isinstance(name, str):
|
||||
return None
|
||||
body = expr[2:]
|
||||
return {"type": "test", "name": name, "body": body}
|
||||
|
||||
|
||||
def _emit_py(suites: list[dict], preamble: list) -> str:
|
||||
"""Emit a pytest module from parsed suites."""
|
||||
# Serialize preamble (assertion helpers) as SX source
|
||||
preamble_sx = "\n".join(_sx_to_source(expr) for expr in preamble)
|
||||
preamble_escaped = preamble_sx.replace('\\', '\\\\').replace("'", "\\'")
|
||||
|
||||
lines = []
|
||||
lines.append('"""Auto-generated from test.sx — SX spec self-tests.')
|
||||
lines.append('')
|
||||
lines.append('DO NOT EDIT. Regenerate with:')
|
||||
lines.append(' python shared/sx/ref/bootstrap_test.py --output shared/sx/tests/test_sx_spec.py')
|
||||
lines.append('"""')
|
||||
lines.append('from __future__ import annotations')
|
||||
lines.append('')
|
||||
lines.append('import pytest')
|
||||
lines.append('from shared.sx.parser import parse_all')
|
||||
lines.append('from shared.sx.ref.sx_ref import eval_expr as _eval, trampoline as _trampoline')
|
||||
lines.append('')
|
||||
lines.append('')
|
||||
lines.append(f"_PREAMBLE = '''{preamble_escaped}'''")
|
||||
lines.append('')
|
||||
lines.append('')
|
||||
lines.append('def _make_env() -> dict:')
|
||||
lines.append(' """Create a fresh env with assertion helpers loaded."""')
|
||||
lines.append(' env = {}')
|
||||
lines.append(' for expr in parse_all(_PREAMBLE):')
|
||||
lines.append(' _trampoline(_eval(expr, env))')
|
||||
lines.append(' return env')
|
||||
lines.append('')
|
||||
lines.append('')
|
||||
lines.append('def _run(sx_source: str, env: dict | None = None) -> object:')
|
||||
lines.append(' """Evaluate SX source and return the result."""')
|
||||
lines.append(' if env is None:')
|
||||
lines.append(' env = _make_env()')
|
||||
lines.append(' exprs = parse_all(sx_source)')
|
||||
lines.append(' result = None')
|
||||
lines.append(' for expr in exprs:')
|
||||
lines.append(' result = _trampoline(_eval(expr, env))')
|
||||
lines.append(' return result')
|
||||
lines.append('')
|
||||
|
||||
for suite in suites:
|
||||
_emit_suite(suite, lines, indent=0)
|
||||
|
||||
return "\n".join(lines)
|
||||
|
||||
|
||||
def _emit_suite(suite: dict, lines: list[str], indent: int):
|
||||
"""Emit a pytest class for a suite."""
|
||||
class_name = f"TestSpec{_slugify(suite['name']).title().replace('_', '')}"
|
||||
pad = " " * indent
|
||||
lines.append(f'{pad}class {class_name}:')
|
||||
lines.append(f'{pad} """test.sx suite: {suite["name"]}"""')
|
||||
lines.append('')
|
||||
|
||||
for item in suite["tests"]:
|
||||
if item["type"] == "test":
|
||||
_emit_test(item, lines, indent + 1)
|
||||
elif item["type"] == "suite":
|
||||
_emit_suite(item, lines, indent + 1)
|
||||
|
||||
lines.append('')
|
||||
|
||||
|
||||
def _emit_test(test: dict, lines: list[str], indent: int):
|
||||
"""Emit a pytest test method."""
|
||||
method_name = f"test_{_slugify(test['name'])}"
|
||||
pad = " " * indent
|
||||
|
||||
# Convert body expressions to SX source
|
||||
body_parts = []
|
||||
for expr in test["body"]:
|
||||
body_parts.append(_sx_to_source(expr))
|
||||
|
||||
# Wrap in (do ...) if multiple expressions, or use single
|
||||
if len(body_parts) == 1:
|
||||
sx_source = body_parts[0]
|
||||
else:
|
||||
sx_source = "(do " + " ".join(body_parts) + ")"
|
||||
|
||||
# Escape for Python string
|
||||
sx_escaped = sx_source.replace('\\', '\\\\').replace("'", "\\'")
|
||||
|
||||
lines.append(f"{pad}def {method_name}(self):")
|
||||
lines.append(f"{pad} _run('{sx_escaped}')")
|
||||
lines.append('')
|
||||
|
||||
|
||||
def main():
|
||||
parser = argparse.ArgumentParser(description="Bootstrap test.sx to pytest")
|
||||
parser.add_argument("--output", "-o", help="Output file path")
|
||||
parser.add_argument("--dry-run", action="store_true", help="Print to stdout")
|
||||
args = parser.parse_args()
|
||||
|
||||
test_sx = os.path.join(_HERE, "test.sx")
|
||||
suites, preamble = _parse_test_sx(test_sx)
|
||||
|
||||
print(f"Parsed {len(suites)} suites, {len(preamble)} preamble defines from test.sx", file=sys.stderr)
|
||||
total_tests = sum(
|
||||
sum(1 for t in s["tests"] if t["type"] == "test")
|
||||
for s in suites
|
||||
)
|
||||
print(f"Total test cases: {total_tests}", file=sys.stderr)
|
||||
|
||||
output = _emit_py(suites, preamble)
|
||||
|
||||
if args.output and not args.dry_run:
|
||||
with open(args.output, "w") as f:
|
||||
f.write(output)
|
||||
print(f"Wrote {args.output}", file=sys.stderr)
|
||||
else:
|
||||
print(output)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
@@ -1,182 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
<title>SX Reactive Islands Demo</title>
|
||||
<style>
|
||||
* { box-sizing: border-box; margin: 0; padding: 0; }
|
||||
body { font-family: system-ui, sans-serif; max-width: 640px; margin: 40px auto; padding: 0 20px; color: #1a1a2e; background: #f8f8fc; }
|
||||
h1 { margin-bottom: 8px; font-size: 1.5rem; }
|
||||
.subtitle { color: #666; margin-bottom: 32px; font-size: 0.9rem; }
|
||||
.demo { background: white; border: 1px solid #e2e2ea; border-radius: 8px; padding: 20px; margin-bottom: 20px; }
|
||||
.demo h2 { font-size: 1.1rem; margin-bottom: 12px; color: #2d2d4e; }
|
||||
.demo-row { display: flex; align-items: center; gap: 12px; margin-bottom: 8px; }
|
||||
button { background: #4a3f8a; color: white; border: none; border-radius: 4px; padding: 6px 16px; cursor: pointer; font-size: 0.9rem; }
|
||||
button:hover { background: #5b4fa0; }
|
||||
button:active { background: #3a2f7a; }
|
||||
.value { font-size: 1.4rem; font-weight: 600; min-width: 3ch; text-align: center; }
|
||||
.derived { color: #666; font-size: 0.85rem; }
|
||||
.effect-log { background: #f0f0f8; border-radius: 4px; padding: 8px 12px; font-family: monospace; font-size: 0.8rem; max-height: 120px; overflow-y: auto; white-space: pre-wrap; }
|
||||
.batch-indicator { display: inline-block; background: #e8f5e9; color: #2e7d32; padding: 2px 8px; border-radius: 3px; font-size: 0.8rem; }
|
||||
code { background: #f0f0f8; padding: 2px 6px; border-radius: 3px; font-size: 0.85rem; }
|
||||
.note { color: #888; font-size: 0.8rem; margin-top: 8px; }
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<h1>SX Reactive Islands</h1>
|
||||
<p class="subtitle">Signals transpiled from <code>signals.sx</code> spec via <code>bootstrap_js.py</code></p>
|
||||
|
||||
<!-- Demo 1: Basic signal -->
|
||||
<div class="demo" id="demo-counter">
|
||||
<h2>1. Signal: Counter</h2>
|
||||
<div class="demo-row">
|
||||
<button onclick="decr()">-</button>
|
||||
<span class="value" id="count-display">0</span>
|
||||
<button onclick="incr()">+</button>
|
||||
</div>
|
||||
<div class="derived" id="doubled-display"></div>
|
||||
<p class="note"><code>signal</code> + <code>computed</code> + <code>effect</code></p>
|
||||
</div>
|
||||
|
||||
<!-- Demo 2: Batch -->
|
||||
<div class="demo" id="demo-batch">
|
||||
<h2>2. Batch: Two signals, one notification</h2>
|
||||
<div class="demo-row">
|
||||
<span>first: <strong id="first-display">0</strong></span>
|
||||
<span>second: <strong id="second-display">0</strong></span>
|
||||
<span class="batch-indicator" id="render-count"></span>
|
||||
</div>
|
||||
<div class="demo-row">
|
||||
<button onclick="batchBoth()">Batch increment both</button>
|
||||
<button onclick="noBatchBoth()">No-batch increment both</button>
|
||||
</div>
|
||||
<p class="note"><code>batch</code> coalesces writes: 2 updates, 1 re-render</p>
|
||||
</div>
|
||||
|
||||
<!-- Demo 3: Effect with cleanup -->
|
||||
<div class="demo" id="demo-effect">
|
||||
<h2>3. Effect: Auto-tracking + Cleanup</h2>
|
||||
<div class="demo-row">
|
||||
<button onclick="togglePolling()">Toggle polling</button>
|
||||
<span id="poll-status"></span>
|
||||
</div>
|
||||
<div class="effect-log" id="effect-log"></div>
|
||||
<p class="note"><code>effect</code> returns cleanup fn; dispose stops tracking</p>
|
||||
</div>
|
||||
|
||||
<!-- Demo 4: Computed chains -->
|
||||
<div class="demo" id="demo-chain">
|
||||
<h2>4. Computed chain: base → doubled → quadrupled</h2>
|
||||
<div class="demo-row">
|
||||
<button onclick="chainDecr()">-</button>
|
||||
<span>base: <strong id="chain-base">1</strong></span>
|
||||
<button onclick="chainIncr()">+</button>
|
||||
</div>
|
||||
<div class="derived">
|
||||
doubled: <strong id="chain-doubled"></strong>
|
||||
quadrupled: <strong id="chain-quad"></strong>
|
||||
</div>
|
||||
<p class="note">Three-level computed dependency graph, auto-propagation</p>
|
||||
</div>
|
||||
|
||||
<script src="sx-ref.js"></script>
|
||||
<script>
|
||||
// Grab signal primitives from transpiled runtime
|
||||
var S = window.Sx;
|
||||
var signal = S.signal;
|
||||
var deref = S.deref;
|
||||
var reset = S.reset;
|
||||
var swap = S.swap;
|
||||
var computed = S.computed;
|
||||
var effect = S.effect;
|
||||
var batch = S.batch;
|
||||
|
||||
// ---- Demo 1: Counter ----
|
||||
var count = signal(0);
|
||||
var doubled = computed(function() { return deref(count) * 2; });
|
||||
|
||||
effect(function() {
|
||||
document.getElementById("count-display").textContent = deref(count);
|
||||
});
|
||||
effect(function() {
|
||||
document.getElementById("doubled-display").textContent = "doubled: " + deref(doubled);
|
||||
});
|
||||
|
||||
function incr() { swap(count, function(n) { return n + 1; }); }
|
||||
function decr() { swap(count, function(n) { return n - 1; }); }
|
||||
|
||||
// ---- Demo 2: Batch ----
|
||||
var first = signal(0);
|
||||
var second = signal(0);
|
||||
var renders = signal(0);
|
||||
|
||||
effect(function() {
|
||||
document.getElementById("first-display").textContent = deref(first);
|
||||
document.getElementById("second-display").textContent = deref(second);
|
||||
swap(renders, function(n) { return n + 1; });
|
||||
});
|
||||
effect(function() {
|
||||
document.getElementById("render-count").textContent = "renders: " + deref(renders);
|
||||
});
|
||||
|
||||
function batchBoth() {
|
||||
batch(function() {
|
||||
swap(first, function(n) { return n + 1; });
|
||||
swap(second, function(n) { return n + 1; });
|
||||
});
|
||||
}
|
||||
function noBatchBoth() {
|
||||
swap(first, function(n) { return n + 1; });
|
||||
swap(second, function(n) { return n + 1; });
|
||||
}
|
||||
|
||||
// ---- Demo 3: Effect with cleanup ----
|
||||
var polling = signal(false);
|
||||
var pollDispose = null;
|
||||
var logEl = document.getElementById("effect-log");
|
||||
|
||||
function log(msg) {
|
||||
logEl.textContent += msg + "\n";
|
||||
logEl.scrollTop = logEl.scrollHeight;
|
||||
}
|
||||
|
||||
effect(function() {
|
||||
var active = deref(polling);
|
||||
document.getElementById("poll-status").textContent = active ? "polling..." : "stopped";
|
||||
if (active) {
|
||||
var n = 0;
|
||||
var id = setInterval(function() {
|
||||
n++;
|
||||
log("poll #" + n);
|
||||
}, 500);
|
||||
log("effect: started interval");
|
||||
// Return cleanup function
|
||||
return function() {
|
||||
clearInterval(id);
|
||||
log("cleanup: cleared interval");
|
||||
};
|
||||
}
|
||||
});
|
||||
|
||||
function togglePolling() { swap(polling, function(v) { return !v; }); }
|
||||
|
||||
// ---- Demo 4: Computed chain ----
|
||||
var base = signal(1);
|
||||
var chainDoubled = computed(function() { return deref(base) * 2; });
|
||||
var quadrupled = computed(function() { return deref(chainDoubled) * 2; });
|
||||
|
||||
effect(function() {
|
||||
document.getElementById("chain-base").textContent = deref(base);
|
||||
});
|
||||
effect(function() {
|
||||
document.getElementById("chain-doubled").textContent = deref(chainDoubled);
|
||||
});
|
||||
effect(function() {
|
||||
document.getElementById("chain-quad").textContent = deref(quadrupled);
|
||||
});
|
||||
|
||||
function chainIncr() { swap(base, function(n) { return n + 1; }); }
|
||||
function chainDecr() { swap(base, function(n) { return n - 1; }); }
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,782 +0,0 @@
|
||||
;; ==========================================================================
|
||||
;; 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 :as dict))
|
||||
(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 :as list) (vals :as list))
|
||||
(smt-bind-loop params vals {})))
|
||||
|
||||
(define smt-bind-loop
|
||||
(fn ((params :as list) (vals :as list) (acc :as dict))
|
||||
(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 :as list))
|
||||
(smt-extract-loop exprs {} (list))))
|
||||
|
||||
(define smt-extract-loop
|
||||
(fn ((exprs :as list) (decls :as dict) (assertions :as list))
|
||||
(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 :as dict) (decls :as dict))
|
||||
(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 :as list)) (= (len tv) n-params)) smt-test-values))
|
||||
;; Run tests
|
||||
(results (map
|
||||
(fn ((test-vals :as list))
|
||||
(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 :as dict)) (get r "equal")) results) "sat" "FAIL")
|
||||
:proof "by construction (definition is the model)"
|
||||
:tests-passed (len (filter (fn ((r :as dict)) (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 :as string))
|
||||
(let ((lines (split s "\n"))
|
||||
(non-comment (filter
|
||||
(fn ((line :as string)) (not (starts-with? (trim line) ";")))
|
||||
lines)))
|
||||
(join "\n" non-comment))))
|
||||
|
||||
;; Verify SMT-LIB output (string) — parse, classify, prove
|
||||
(define prove-check
|
||||
(fn ((smtlib-str :as string))
|
||||
(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 :as dict)) (= (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 :as list))
|
||||
(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 :as dict)) (= (get r "status") "sat")) results)))
|
||||
(total (len results)))
|
||||
{:total total
|
||||
:sat sat-count
|
||||
:all-sat (= sat-count total)
|
||||
:results results})))
|
||||
|
||||
|
||||
;; ==========================================================================
|
||||
;; Phase 2: Property-based constraint solving
|
||||
;; ==========================================================================
|
||||
;;
|
||||
;; Properties are dicts:
|
||||
;; {:name "+-commutative"
|
||||
;; :vars ("a" "b")
|
||||
;; :test (fn (a b) (= (+ a b) (+ b a))) — for bounded checking
|
||||
;; :holds (= (+ a b) (+ b a)) — quoted AST for SMT-LIB
|
||||
;; :given (fn (lo hi) (<= lo hi)) — optional precondition
|
||||
;; :given-expr (<= lo hi) — quoted AST of precondition
|
||||
;; :domain (-20 21)} — optional custom range
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Domain generation
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Default domain bounds by arity — balance coverage vs. combinatorics
|
||||
(define prove-domain-for
|
||||
(fn ((arity :as number))
|
||||
(cond
|
||||
(<= arity 1) (range -50 51) ;; 101 values
|
||||
(= arity 2) (range -20 21) ;; 41^2 = 1,681 pairs
|
||||
(= arity 3) (range -8 9) ;; 17^3 = 4,913 triples
|
||||
:else (range -5 6)))) ;; 11^n for n >= 4
|
||||
|
||||
;; Cartesian product: all n-tuples from a domain
|
||||
(define prove-tuples
|
||||
(fn ((domain :as list) (arity :as number))
|
||||
(if (<= arity 0) (list (list))
|
||||
(if (= arity 1)
|
||||
(map (fn (x) (list x)) domain)
|
||||
(let ((sub (prove-tuples domain (- arity 1))))
|
||||
(prove-tuples-expand domain sub (list)))))))
|
||||
|
||||
(define prove-tuples-expand
|
||||
(fn ((domain :as list) (sub :as list) (acc :as list))
|
||||
(if (empty? domain) acc
|
||||
(prove-tuples-expand
|
||||
(rest domain) sub
|
||||
(append acc
|
||||
(map (fn ((t :as list)) (cons (first domain) t)) sub))))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Function application by arity (no apply primitive available)
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
(define prove-call
|
||||
(fn ((f :as lambda) (vals :as list))
|
||||
(let ((n (len vals)))
|
||||
(cond
|
||||
(= n 0) (f)
|
||||
(= n 1) (f (nth vals 0))
|
||||
(= n 2) (f (nth vals 0) (nth vals 1))
|
||||
(= n 3) (f (nth vals 0) (nth vals 1) (nth vals 2))
|
||||
(= n 4) (f (nth vals 0) (nth vals 1) (nth vals 2) (nth vals 3))
|
||||
:else nil))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Bounded model checker
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Search for a counterexample. Returns nil if property holds for all tested
|
||||
;; values, or the first counterexample found.
|
||||
(define prove-search
|
||||
(fn ((test-fn :as lambda) given-fn (domain :as list) (vars :as list))
|
||||
(let ((arity (len vars))
|
||||
(tuples (prove-tuples domain arity)))
|
||||
(prove-search-loop test-fn given-fn tuples 0 0))))
|
||||
|
||||
(define prove-search-loop
|
||||
(fn ((test-fn :as lambda) given-fn (tuples :as list) (tested :as number) (skipped :as number))
|
||||
(if (empty? tuples)
|
||||
{:status "verified" :tested tested :skipped skipped}
|
||||
(let ((vals (first tuples))
|
||||
(rest-t (rest tuples)))
|
||||
;; Check precondition (if any)
|
||||
(if (and (not (nil? given-fn))
|
||||
(not (prove-call given-fn vals)))
|
||||
;; Precondition not met — skip this combination
|
||||
(prove-search-loop test-fn given-fn rest-t tested (+ skipped 1))
|
||||
;; Evaluate the property
|
||||
(if (prove-call test-fn vals)
|
||||
;; Passed — continue
|
||||
(prove-search-loop test-fn given-fn rest-t (+ tested 1) skipped)
|
||||
;; Failed — counterexample found
|
||||
{:status "falsified"
|
||||
:tested tested
|
||||
:skipped skipped
|
||||
:counterexample vals}))))))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Property verification (public API)
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Verify a single property via bounded model checking
|
||||
(define prove-property
|
||||
(fn ((prop :as dict))
|
||||
(let ((name (get prop "name"))
|
||||
(vars (get prop "vars"))
|
||||
(test-fn (get prop "test"))
|
||||
(given-fn (get prop "given" nil))
|
||||
(custom (get prop "domain" nil))
|
||||
(domain (if (nil? custom)
|
||||
(prove-domain-for (len vars))
|
||||
(range (nth custom 0) (nth custom 1)))))
|
||||
(let ((result (prove-search test-fn given-fn domain vars)))
|
||||
(assoc result "name" name)))))
|
||||
|
||||
;; Batch verify a list of properties
|
||||
(define prove-properties
|
||||
(fn ((props :as list))
|
||||
(let ((results (map prove-property props))
|
||||
(verified (filter (fn ((r :as dict)) (= (get r "status") "verified")) results))
|
||||
(falsified (filter (fn ((r :as dict)) (= (get r "status") "falsified")) results)))
|
||||
{:total (len results)
|
||||
:verified (len verified)
|
||||
:falsified (len falsified)
|
||||
:all-verified (= (len falsified) 0)
|
||||
:results results})))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; SMT-LIB generation for properties
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
;; Generate SMT-LIB for a property — asserts (not (forall ...)) so that
|
||||
;; Z3 returning "unsat" proves the property holds universally.
|
||||
(define prove-property-smtlib
|
||||
(fn ((prop :as dict))
|
||||
(let ((name (get prop "name"))
|
||||
(vars (get prop "vars"))
|
||||
(holds (get prop "holds"))
|
||||
(given-e (get prop "given-expr" nil))
|
||||
(bindings (join " "
|
||||
(map (fn ((v :as string)) (str "(" v " Int)")) vars)))
|
||||
(holds-smt (z3-expr holds))
|
||||
(body (if (nil? given-e)
|
||||
holds-smt
|
||||
(str "(=> " (z3-expr given-e) " " holds-smt ")"))))
|
||||
(str "; Property: " name "\n"
|
||||
"; Strategy: assert negation, check for unsat\n"
|
||||
"(assert (not (forall ((" bindings "))\n"
|
||||
" " body ")))\n"
|
||||
"(check-sat) ; expect unsat\n"))))
|
||||
|
||||
;; Generate SMT-LIB for all properties, including necessary definitions
|
||||
(define prove-properties-smtlib
|
||||
(fn ((props :as list) (primitives-exprs :as list))
|
||||
(let ((defs (z3-translate-file primitives-exprs))
|
||||
(prop-smts (map prove-property-smtlib props)))
|
||||
(str ";; ================================================================\n"
|
||||
";; Auto-generated by prove.sx — property verification conditions\n"
|
||||
";; Feed to Z3 for unbounded proofs\n"
|
||||
";; ================================================================\n\n"
|
||||
";; --- Primitive definitions ---\n"
|
||||
defs "\n\n"
|
||||
";; --- Properties ---\n"
|
||||
(join "\n" prop-smts)))))
|
||||
|
||||
|
||||
;; ==========================================================================
|
||||
;; Property library: algebraic laws of SX primitives
|
||||
;; ==========================================================================
|
||||
|
||||
(define sx-properties
|
||||
(list
|
||||
|
||||
;; ----- Arithmetic identities -----
|
||||
|
||||
{:name "+-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (+ a b) (+ b a)))
|
||||
:holds '(= (+ a b) (+ b a))}
|
||||
|
||||
{:name "+-associative"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (+ (+ a b) c) (+ a (+ b c))))
|
||||
:holds '(= (+ (+ a b) c) (+ a (+ b c)))}
|
||||
|
||||
{:name "+-identity"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (+ a 0) a))
|
||||
:holds '(= (+ a 0) a)}
|
||||
|
||||
{:name "*-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (* a b) (* b a)))
|
||||
:holds '(= (* a b) (* b a))}
|
||||
|
||||
{:name "*-associative"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (* (* a b) c) (* a (* b c))))
|
||||
:holds '(= (* (* a b) c) (* a (* b c)))}
|
||||
|
||||
{:name "*-identity"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (* a 1) a))
|
||||
:holds '(= (* a 1) a)}
|
||||
|
||||
{:name "*-zero"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (* a 0) 0))
|
||||
:holds '(= (* a 0) 0)}
|
||||
|
||||
{:name "distributive"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (= (* a (+ b c)) (+ (* a b) (* a c))))
|
||||
:holds '(= (* a (+ b c)) (+ (* a b) (* a c)))}
|
||||
|
||||
{:name "--inverse"
|
||||
:vars (list "a")
|
||||
:test (fn (a) (= (- a a) 0))
|
||||
:holds '(= (- a a) 0)}
|
||||
|
||||
;; ----- inc / dec -----
|
||||
|
||||
{:name "inc-is-plus-1"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (inc n) (+ n 1)))
|
||||
:holds '(= (inc n) (+ n 1))}
|
||||
|
||||
{:name "dec-is-minus-1"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (dec n) (- n 1)))
|
||||
:holds '(= (dec n) (- n 1))}
|
||||
|
||||
{:name "inc-dec-inverse"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (dec (inc n)) n))
|
||||
:holds '(= (dec (inc n)) n)}
|
||||
|
||||
{:name "dec-inc-inverse"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (inc (dec n)) n))
|
||||
:holds '(= (inc (dec n)) n)}
|
||||
|
||||
;; ----- abs -----
|
||||
|
||||
{:name "abs-non-negative"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (>= (abs n) 0))
|
||||
:holds '(>= (abs n) 0)}
|
||||
|
||||
{:name "abs-idempotent"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (abs (abs n)) (abs n)))
|
||||
:holds '(= (abs (abs n)) (abs n))}
|
||||
|
||||
{:name "abs-symmetric"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (abs n) (abs (- 0 n))))
|
||||
:holds '(= (abs n) (abs (- 0 n)))}
|
||||
|
||||
;; ----- Predicates -----
|
||||
|
||||
{:name "odd-not-even"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (odd? n) (not (even? n))))
|
||||
:holds '(= (odd? n) (not (even? n)))}
|
||||
|
||||
{:name "even-mod-2"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (even? n) (= (mod n 2) 0)))
|
||||
:holds '(= (even? n) (= (mod n 2) 0))}
|
||||
|
||||
{:name "zero-is-zero"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (zero? n) (= n 0)))
|
||||
:holds '(= (zero? n) (= n 0))}
|
||||
|
||||
{:name "not-involution"
|
||||
:vars (list "n")
|
||||
:test (fn (n) (= (not (not (zero? n))) (zero? n)))
|
||||
:holds '(= (not (not (zero? n))) (zero? n))}
|
||||
|
||||
;; ----- min / max -----
|
||||
|
||||
{:name "min-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (min a b) (min b a)))
|
||||
:holds '(= (min a b) (min b a))}
|
||||
|
||||
{:name "max-commutative"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (max a b) (max b a)))
|
||||
:holds '(= (max a b) (max b a))}
|
||||
|
||||
{:name "min-le-both"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (and (<= (min a b) a) (<= (min a b) b)))
|
||||
:holds '(and (<= (min a b) a) (<= (min a b) b))}
|
||||
|
||||
{:name "max-ge-both"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (and (>= (max a b) a) (>= (max a b) b)))
|
||||
:holds '(and (>= (max a b) a) (>= (max a b) b))}
|
||||
|
||||
{:name "min-max-identity"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (+ (min a b) (max a b)) (+ a b)))
|
||||
:holds '(= (+ (min a b) (max a b)) (+ a b))}
|
||||
|
||||
;; ----- clamp -----
|
||||
|
||||
{:name "clamp-in-range"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (and (<= lo (clamp x lo hi))
|
||||
(<= (clamp x lo hi) hi)))
|
||||
:given (fn (x lo hi) (<= lo hi))
|
||||
:holds '(and (<= lo (clamp x lo hi)) (<= (clamp x lo hi) hi))
|
||||
:given-expr '(<= lo hi)}
|
||||
|
||||
{:name "clamp-identity-in-range"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (= (clamp x lo hi) x))
|
||||
:given (fn (x lo hi) (and (<= lo hi) (<= lo x) (<= x hi)))
|
||||
:holds '(= (clamp x lo hi) x)
|
||||
:given-expr '(and (<= lo hi) (<= lo x) (<= x hi))}
|
||||
|
||||
{:name "clamp-idempotent"
|
||||
:vars (list "x" "lo" "hi")
|
||||
:test (fn (x lo hi) (= (clamp (clamp x lo hi) lo hi)
|
||||
(clamp x lo hi)))
|
||||
:given (fn (x lo hi) (<= lo hi))
|
||||
:holds '(= (clamp (clamp x lo hi) lo hi) (clamp x lo hi))
|
||||
:given-expr '(<= lo hi)}
|
||||
|
||||
;; ----- Comparison -----
|
||||
|
||||
{:name "lt-gt-flip"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (< a b) (> b a)))
|
||||
:holds '(= (< a b) (> b a))}
|
||||
|
||||
{:name "le-not-gt"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (<= a b) (not (> a b))))
|
||||
:holds '(= (<= a b) (not (> a b)))}
|
||||
|
||||
{:name "ge-not-lt"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (>= a b) (not (< a b))))
|
||||
:holds '(= (>= a b) (not (< a b)))}
|
||||
|
||||
{:name "trichotomy"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (or (< a b) (= a b) (> a b)))
|
||||
:holds '(or (< a b) (= a b) (> a b))}
|
||||
|
||||
{:name "lt-transitive"
|
||||
:vars (list "a" "b" "c")
|
||||
:test (fn (a b c) (if (and (< a b) (< b c)) (< a c) true))
|
||||
:given (fn (a b c) (and (< a b) (< b c)))
|
||||
:holds '(< a c)
|
||||
:given-expr '(and (< a b) (< b c))}
|
||||
|
||||
;; ----- Inequality -----
|
||||
|
||||
{:name "neq-is-not-eq"
|
||||
:vars (list "a" "b")
|
||||
:test (fn (a b) (= (!= a b) (not (= a b))))
|
||||
:holds '(= (!= a b) (not (= a b)))}))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; Run all built-in properties
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
(define prove-all-properties
|
||||
(fn ()
|
||||
(prove-properties sx-properties)))
|
||||
@@ -1,89 +0,0 @@
|
||||
"""
|
||||
#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)
|
||||
@@ -1,122 +0,0 @@
|
||||
#!/usr/bin/env python3
|
||||
"""
|
||||
Bootstrap runner: execute py.sx against spec files to produce sx_ref.py.
|
||||
|
||||
This is the G1 bootstrapper — py.sx (SX-to-Python translator written in SX)
|
||||
is loaded into the Python evaluator, which then uses it to translate the
|
||||
spec .sx files into Python.
|
||||
|
||||
The output should be identical to: python bootstrap_py.py
|
||||
|
||||
Usage:
|
||||
python run_py_sx.py > sx_ref_g1.py
|
||||
"""
|
||||
from __future__ import annotations
|
||||
|
||||
import os
|
||||
import sys
|
||||
|
||||
_HERE = os.path.dirname(os.path.abspath(__file__))
|
||||
_PROJECT = os.path.abspath(os.path.join(_HERE, "..", "..", ".."))
|
||||
sys.path.insert(0, _PROJECT)
|
||||
|
||||
from shared.sx.parser import parse_all
|
||||
from shared.sx.types import Symbol
|
||||
from shared.sx.ref.platform_py import (
|
||||
PREAMBLE, PLATFORM_PY, PRIMITIVES_PY_PRE, PRIMITIVES_PY_POST,
|
||||
PLATFORM_DEPS_PY, FIXUPS_PY, CONTINUATIONS_PY,
|
||||
_assemble_primitives_py, public_api_py,
|
||||
)
|
||||
|
||||
|
||||
def load_py_sx(evaluator_env: dict) -> dict:
|
||||
"""Load py.sx into an evaluator environment and return it."""
|
||||
py_sx_path = os.path.join(_HERE, "py.sx")
|
||||
with open(py_sx_path) as f:
|
||||
source = f.read()
|
||||
|
||||
exprs = parse_all(source)
|
||||
|
||||
# Import the evaluator
|
||||
from shared.sx.ref.sx_ref import evaluate, make_env
|
||||
|
||||
env = make_env()
|
||||
for expr in exprs:
|
||||
evaluate(expr, env)
|
||||
|
||||
return env
|
||||
|
||||
|
||||
def extract_defines(source: str) -> list[tuple[str, list]]:
|
||||
"""Parse .sx source, return list of (name, define-expr) for top-level defines."""
|
||||
exprs = parse_all(source)
|
||||
defines = []
|
||||
for expr in exprs:
|
||||
if isinstance(expr, list) and expr and isinstance(expr[0], Symbol):
|
||||
if expr[0].name == "define":
|
||||
name = expr[1].name if isinstance(expr[1], Symbol) else str(expr[1])
|
||||
defines.append((name, expr))
|
||||
return defines
|
||||
|
||||
|
||||
def main():
|
||||
from shared.sx.ref.sx_ref import evaluate
|
||||
|
||||
# Load py.sx into evaluator
|
||||
env = load_py_sx({})
|
||||
|
||||
# Get the py-translate-file function
|
||||
py_translate_file = env.get("py-translate-file")
|
||||
if py_translate_file is None:
|
||||
print("ERROR: py-translate-file not found in py.sx environment", file=sys.stderr)
|
||||
sys.exit(1)
|
||||
|
||||
# Same file list and order as bootstrap_py.py compile_ref_to_py()
|
||||
sx_files = [
|
||||
("eval.sx", "eval"),
|
||||
("forms.sx", "forms (server definition forms)"),
|
||||
("render.sx", "render (core)"),
|
||||
("adapter-html.sx", "adapter-html"),
|
||||
("adapter-sx.sx", "adapter-sx"),
|
||||
("deps.sx", "deps (component dependency analysis)"),
|
||||
("signals.sx", "signals (reactive signal runtime)"),
|
||||
]
|
||||
|
||||
# Build output — static sections are identical
|
||||
parts = []
|
||||
parts.append(PREAMBLE)
|
||||
parts.append(PLATFORM_PY)
|
||||
parts.append(PRIMITIVES_PY_PRE)
|
||||
parts.append(_assemble_primitives_py(None))
|
||||
parts.append(PRIMITIVES_PY_POST)
|
||||
parts.append(PLATFORM_DEPS_PY)
|
||||
|
||||
# Translate each spec file using py.sx
|
||||
for filename, label in sx_files:
|
||||
filepath = os.path.join(_HERE, filename)
|
||||
if not os.path.exists(filepath):
|
||||
continue
|
||||
with open(filepath) as f:
|
||||
src = f.read()
|
||||
defines = extract_defines(src)
|
||||
|
||||
# Convert defines to SX-compatible format: list of [name, expr] pairs
|
||||
sx_defines = [[name, expr] for name, expr in defines]
|
||||
|
||||
parts.append(f"\n# === Transpiled from {label} ===\n")
|
||||
# Bind defines as data in env to avoid evaluator trying to execute AST
|
||||
env["_defines"] = sx_defines
|
||||
result = evaluate(
|
||||
[Symbol("py-translate-file"), Symbol("_defines")],
|
||||
env,
|
||||
)
|
||||
parts.append(result)
|
||||
|
||||
parts.append(FIXUPS_PY)
|
||||
parts.append(public_api_py(True, True, True))
|
||||
|
||||
print("\n".join(parts))
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,358 +0,0 @@
|
||||
;; ==========================================================================
|
||||
;; 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 :as string))
|
||||
(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 :as string))
|
||||
(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 :as string))
|
||||
(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 :as list))
|
||||
;; 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 :as list) (result :as dict))
|
||||
(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 :as list))
|
||||
;; 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 :as list) (skip-next :as boolean) (acc :as list))
|
||||
(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 :as list))
|
||||
(some (fn (p) (and (= (type-of p) "symbol") (= (symbol-name p) "&rest")))
|
||||
params)))
|
||||
|
||||
|
||||
;; --------------------------------------------------------------------------
|
||||
;; define-primitive → SMT-LIB
|
||||
;; --------------------------------------------------------------------------
|
||||
|
||||
(define z3-translate-primitive
|
||||
(fn ((expr :as list))
|
||||
(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 :as list))
|
||||
(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 :as list))
|
||||
(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 :as list))
|
||||
;; 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)))))
|
||||
Reference in New Issue
Block a user