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