From 1819156d1e29eabf90b739e46c4bcd37f3fe0757 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Sat, 25 Apr 2026 18:32:36 +0000
Subject: [PATCH] prolog: cross-validate compiler vs interpreter (+17)

---
 lib/prolog/compiler.sx             | 19 +++++++
 lib/prolog/conformance.sh          |  1 +
 lib/prolog/tests/cross_validate.sx | 86 ++++++++++++++++++++++++++++++
 3 files changed, 106 insertions(+)
 create mode 100644 lib/prolog/tests/cross_validate.sx

diff --git a/lib/prolog/compiler.sx b/lib/prolog/compiler.sx
index c3c80a5f..725f8cdf 100644
--- a/lib/prolog/compiler.sx
+++ b/lib/prolog/compiler.sx
@@ -155,3 +155,22 @@
         (keys src-table))
       (dict-set! db :compiled compiled-table)
       db)))
+
+;; Cross-validate: load src into both a plain and a compiled DB,
+;; run goal-str through each, return true iff solution counts match.
+;; Use this to keep the interpreter as the reference implementation.
+(define
+  pl-compiled-matches-interp?
+  (fn
+    (src goal-str)
+    (let
+      ((db-interp (pl-mk-db)) (db-comp (pl-mk-db)))
+      (pl-db-load! db-interp (pl-parse src))
+      (pl-db-load! db-comp (pl-parse src))
+      (pl-compile-db! db-comp)
+      (let
+        ((gi (pl-instantiate (pl-parse-goal goal-str) {}))
+          (gc (pl-instantiate (pl-parse-goal goal-str) {})))
+        (=
+          (pl-solve-count! db-interp gi (pl-mk-trail))
+          (pl-solve-count! db-comp gc (pl-mk-trail)))))))
diff --git a/lib/prolog/conformance.sh b/lib/prolog/conformance.sh
index da9da278..4376638c 100755
--- a/lib/prolog/conformance.sh
+++ b/lib/prolog/conformance.sh
@@ -42,6 +42,7 @@ SUITES=(
   "string_agg:lib/prolog/tests/string_agg.sx:pl-string-agg-tests-run!"
   "advanced:lib/prolog/tests/advanced.sx:pl-advanced-tests-run!"
   "compiler:lib/prolog/tests/compiler.sx:pl-compiler-tests-run!"
+  "cross_validate:lib/prolog/tests/cross_validate.sx:pl-cross-validate-tests-run!"
 )
 
 SCRIPT='(epoch 1)
diff --git a/lib/prolog/tests/cross_validate.sx b/lib/prolog/tests/cross_validate.sx
new file mode 100644
index 00000000..1a365b11
--- /dev/null
+++ b/lib/prolog/tests/cross_validate.sx
@@ -0,0 +1,86 @@
+;; lib/prolog/tests/cross_validate.sx
+;; Verifies that the compiled solver produces the same solution counts as the
+;; interpreter for each classic program + built-in exercise.
+;; Interpreter is the reference: if they disagree, the compiler is wrong.
+
+(define pl-xv-test-count 0)
+(define pl-xv-test-pass 0)
+(define pl-xv-test-fail 0)
+(define pl-xv-test-failures (list))
+
+(define
+  pl-xv-test!
+  (fn
+    (name got expected)
+    (set! pl-xv-test-count (+ pl-xv-test-count 1))
+    (if
+      (= got expected)
+      (set! pl-xv-test-pass (+ pl-xv-test-pass 1))
+      (begin
+        (set! pl-xv-test-fail (+ pl-xv-test-fail 1))
+        (append! pl-xv-test-failures name)))))
+
+;; Shorthand: assert compiled result matches interpreter.
+(define
+  pl-xv-match!
+  (fn
+    (name src goal)
+    (pl-xv-test! name (pl-compiled-matches-interp? src goal) true)))
+
+;; ── 1. append/3 ─────────────────────────────────────────────────
+
+(define
+  pl-xv-append
+  "append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R).")
+
+(pl-xv-match! "append build 2+2" pl-xv-append "append([1,2],[3,4],X)")
+(pl-xv-match! "append split [a,b,c]" pl-xv-append "append(X, Y, [a,b,c])")
+(pl-xv-match! "append member-mode" pl-xv-append "append(_, [3], [1,2,3])")
+
+;; ── 2. member/2 ─────────────────────────────────────────────────
+
+(define pl-xv-member "member(X, [X|_]). member(X, [_|T]) :- member(X, T).")
+
+(pl-xv-match! "member check hit" pl-xv-member "member(b, [a,b,c])")
+(pl-xv-match! "member count" pl-xv-member "member(X, [a,b,c])")
+(pl-xv-match! "member empty" pl-xv-member "member(X, [])")
+
+;; ── 3. facts + transitive rules ─────────────────────────────────
+
+(define
+  pl-xv-ancestor
+  (str
+    "parent(a,b). parent(b,c). parent(c,d). parent(a,c)."
+    "ancestor(X,Y) :- parent(X,Y)."
+    "ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y)."))
+
+(pl-xv-match! "ancestor direct" pl-xv-ancestor "ancestor(a,b)")
+(pl-xv-match! "ancestor transitive" pl-xv-ancestor "ancestor(a,d)")
+(pl-xv-match! "ancestor all from a" pl-xv-ancestor "ancestor(a,Y)")
+
+;; ── 4. cut semantics ────────────────────────────────────────────
+
+(define pl-xv-cut "first(X,[X|_]) :- !. first(X,[_|T]) :- first(X,T).")
+
+(pl-xv-match! "cut one solution" pl-xv-cut "first(X,[a,b,c])")
+(pl-xv-match! "cut empty list" pl-xv-cut "first(X,[])")
+
+;; ── 5. arithmetic ───────────────────────────────────────────────
+
+(define pl-xv-arith "sq(X,Y) :- Y is X * X. even(X) :- 0 is X mod 2.")
+
+(pl-xv-match! "sq(3,Y) count" pl-xv-arith "sq(3,Y)")
+(pl-xv-match! "sq(3,9) check" pl-xv-arith "sq(3,9)")
+(pl-xv-match! "even(4) check" pl-xv-arith "even(4)")
+(pl-xv-match! "even(3) check" pl-xv-arith "even(3)")
+
+;; ── 6. if-then-else ─────────────────────────────────────────────
+
+(define pl-xv-ite "classify(X, pos) :- X > 0, !. classify(_, nonpos).")
+
+(pl-xv-match! "classify positive" pl-xv-ite "classify(5, C)")
+(pl-xv-match! "classify zero" pl-xv-ite "classify(0, C)")
+
+;; ── Runner ───────────────────────────────────────────────────────
+
+(define pl-cross-validate-tests-run! (fn () {:failed pl-xv-test-fail :passed pl-xv-test-pass :total pl-xv-test-count :failures pl-xv-test-failures}))