prolog: cross-validate compiler vs interpreter (+17)

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

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)

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}))