prolog: conformance.sh + scoreboard.{json,md}, 183/183 baseline

lib/prolog/conformance.sh

@@ -0,0 +1,106 @@
+#!/usr/bin/env bash
+# Run every Prolog test suite via sx_server and refresh scoreboard.{json,md}.
+# Exit 0 if all green, 1 if any failures.
+set -euo pipefail
+
+HERE="$(cd "$(dirname "$0")" && pwd)"
+ROOT="$(cd "$HERE/../.." && pwd)"
+SX="${SX_SERVER:-/root/rose-ash/hosts/ocaml/_build/default/bin/sx_server.exe}"
+
+if [[ ! -x "$SX" ]]; then
+  echo "sx_server not found at $SX (set SX_SERVER env to override)" >&2
+  exit 2
+fi
+
+cd "$ROOT"
+
+# name : test-file : runner-fn
+SUITES=(
+  "parse:lib/prolog/tests/parse.sx:pl-parse-tests-run!"
+  "unify:lib/prolog/tests/unify.sx:pl-unify-tests-run!"
+  "clausedb:lib/prolog/tests/clausedb.sx:pl-clausedb-tests-run!"
+  "solve:lib/prolog/tests/solve.sx:pl-solve-tests-run!"
+  "append:lib/prolog/tests/programs/append.sx:pl-append-tests-run!"
+  "reverse:lib/prolog/tests/programs/reverse.sx:pl-reverse-tests-run!"
+  "member:lib/prolog/tests/programs/member.sx:pl-member-tests-run!"
+  "nqueens:lib/prolog/tests/programs/nqueens.sx:pl-nqueens-tests-run!"
+  "family:lib/prolog/tests/programs/family.sx:pl-family-tests-run!"
+)
+
+SCRIPT='(epoch 1)
+(load "lib/prolog/tokenizer.sx")
+(load "lib/prolog/parser.sx")
+(load "lib/prolog/runtime.sx")'
+for entry in "${SUITES[@]}"; do
+  IFS=: read -r _ file _ <<< "$entry"
+  SCRIPT+=$'\n(load "'"$file"$'")'
+done
+for entry in "${SUITES[@]}"; do
+  IFS=: read -r _ _ fn <<< "$entry"
+  SCRIPT+=$'\n(eval "('"$fn"$')")'
+done
+
+OUTPUT="$(printf '%s\n' "$SCRIPT" | "$SX" 2>&1)"
+
+mapfile -t LINES < <(printf '%s\n' "$OUTPUT" | grep -E '^\{:failed')
+
+if [[ ${#LINES[@]} -ne ${#SUITES[@]} ]]; then
+  echo "Expected ${#SUITES[@]} suite results, got ${#LINES[@]}" >&2
+  echo "---- raw output ----" >&2
+  printf '%s\n' "$OUTPUT" >&2
+  exit 3
+fi
+
+TOTAL_PASS=0
+TOTAL_FAIL=0
+TOTAL=0
+JSON_SUITES=""
+MD_ROWS=""
+
+for i in "${!SUITES[@]}"; do
+  IFS=: read -r name _ _ <<< "${SUITES[$i]}"
+  line="${LINES[$i]}"
+  passed=$(grep -oE ':passed [0-9]+' <<< "$line" | grep -oE '[0-9]+')
+  total=$(grep -oE ':total [0-9]+' <<< "$line" | grep -oE '[0-9]+')
+  failed=$(grep -oE ':failed [0-9]+' <<< "$line" | grep -oE '[0-9]+')
+  TOTAL_PASS=$((TOTAL_PASS + passed))
+  TOTAL_FAIL=$((TOTAL_FAIL + failed))
+  TOTAL=$((TOTAL + total))
+  status="ok"
+  [[ "$failed" -gt 0 ]] && status="FAIL"
+  [[ -n "$JSON_SUITES" ]] && JSON_SUITES+=","
+  JSON_SUITES+="\"$name\":{\"passed\":$passed,\"total\":$total,\"failed\":$failed}"
+  MD_ROWS+="| $name | $passed | $total | $status |"$'\n'
+done
+
+WHEN="$(date -Iseconds 2>/dev/null || date)"
+
+cat > "$HERE/scoreboard.json" <<JSON
+{
+  "total_passed": $TOTAL_PASS,
+  "total_failed": $TOTAL_FAIL,
+  "total": $TOTAL,
+  "suites": {$JSON_SUITES},
+  "generated": "$WHEN"
+}
+JSON
+
+cat > "$HERE/scoreboard.md" <<MD
+# Prolog scoreboard
+
+**$TOTAL_PASS / $TOTAL passing** ($TOTAL_FAIL failure(s)).
+Generated $WHEN.
+
+| Suite | Passed | Total | Status |
+|-------|--------|-------|--------|
+$MD_ROWS
+Run \`bash lib/prolog/conformance.sh\` to refresh. Override the binary
+with \`SX_SERVER=path/to/sx_server.exe bash …\`.
+MD
+
+if [[ "$TOTAL_FAIL" -gt 0 ]]; then
+  echo "$TOTAL_FAIL failure(s) across $TOTAL tests" >&2
+  exit 1
+fi
+
+echo "All $TOTAL tests pass."

lib/prolog/runtime.sx

@@ -98,6 +98,11 @@
             "compound"
             fun
             (map (fn (a) (pl-instantiate a var-env)) args))))
+      ((= (first ast) "clause")
+        (let
+          ((h (pl-instantiate (nth ast 1) var-env))
+            (b (pl-instantiate (nth ast 2) var-env)))
+          (list "clause" h b)))
       (true ast))))
 
 (define pl-instantiate-fresh (fn (ast) (pl-instantiate ast {})))
@@ -230,3 +235,354 @@
         (pl-unify! t1 t2 trail)
         true
         (do (pl-trail-undo-to! trail mark) false)))))
+
+(define pl-mk-db (fn () {:clauses {}}))
+
+(define
+  pl-head-key
+  (fn
+    (head)
+    (cond
+      ((pl-compound? head) (str (pl-fun head) "/" (len (pl-args head))))
+      ((pl-atom? head) (str (pl-atom-name head) "/0"))
+      (true (error "pl-head-key: invalid head")))))
+
+(define pl-clause-key (fn (clause) (pl-head-key (nth clause 1))))
+
+(define pl-goal-key (fn (goal) (pl-head-key goal)))
+
+(define
+  pl-db-add!
+  (fn
+    (db clause)
+    (let
+      ((key (pl-clause-key clause)) (table (dict-get db :clauses)))
+      (cond
+        ((nil? (dict-get table key)) (dict-set! table key (list clause)))
+        (true (begin (append! (dict-get table key) clause) nil))))))
+
+(define
+  pl-db-load!
+  (fn
+    (db program)
+    (cond
+      ((empty? program) nil)
+      (true
+        (begin
+          (pl-db-add! db (first program))
+          (pl-db-load! db (rest program)))))))
+
+(define
+  pl-db-lookup
+  (fn
+    (db key)
+    (let
+      ((v (dict-get (dict-get db :clauses) key)))
+      (cond ((nil? v) (list)) (true v)))))
+
+(define
+  pl-db-lookup-goal
+  (fn (db goal) (pl-db-lookup db (pl-goal-key goal))))
+
+(define
+  pl-cut?
+  (fn (t) (and (list? t) (not (empty? t)) (= (first t) "cut"))))
+
+(define
+  pl-solve!
+  (fn
+    (db goal trail cut-box k)
+    (let
+      ((g (pl-walk goal)))
+      (cond
+        ((pl-var? g) false)
+        ((pl-cut? g) (begin (dict-set! cut-box :cut true) (k)))
+        ((and (pl-atom? g) (= (pl-atom-name g) "true")) (k))
+        ((and (pl-atom? g) (= (pl-atom-name g) "fail")) false)
+        ((and (pl-atom? g) (= (pl-atom-name g) "nl"))
+          (begin (pl-output-write! "\n") (k)))
+        ((and (pl-compound? g) (= (pl-fun g) "=") (= (len (pl-args g)) 2))
+          (pl-solve-eq! (first (pl-args g)) (nth (pl-args g) 1) trail k))
+        ((and (pl-compound? g) (= (pl-fun g) "\\=") (= (len (pl-args g)) 2))
+          (pl-solve-not-eq!
+            (first (pl-args g))
+            (nth (pl-args g) 1)
+            trail
+            k))
+        ((and (pl-compound? g) (= (pl-fun g) "is") (= (len (pl-args g)) 2))
+          (pl-solve-eq!
+            (first (pl-args g))
+            (list "num" (pl-eval-arith (nth (pl-args g) 1)))
+            trail
+            k))
+        ((and (pl-compound? g) (= (pl-fun g) ",") (= (len (pl-args g)) 2))
+          (pl-solve!
+            db
+            (first (pl-args g))
+            trail
+            cut-box
+            (fn () (pl-solve! db (nth (pl-args g) 1) trail cut-box k))))
+        ((and (pl-compound? g) (= (pl-fun g) ";") (= (len (pl-args g)) 2))
+          (pl-solve-or!
+            db
+            (first (pl-args g))
+            (nth (pl-args g) 1)
+            trail
+            cut-box
+            k))
+        ((and (pl-compound? g) (= (pl-fun g) "->") (= (len (pl-args g)) 2))
+          (pl-solve-if-then-else!
+            db
+            (first (pl-args g))
+            (nth (pl-args g) 1)
+            (list "atom" "fail")
+            trail
+            cut-box
+            k))
+        ((and (pl-compound? g) (= (pl-fun g) "call") (= (len (pl-args g)) 1))
+          (let
+            ((call-cb {:cut false}))
+            (pl-solve! db (first (pl-args g)) trail call-cb k)))
+        ((and (pl-compound? g) (= (pl-fun g) "write") (= (len (pl-args g)) 1))
+          (begin
+            (pl-output-write! (pl-format-term (first (pl-args g))))
+            (k)))
+        (true (pl-solve-user! db g trail cut-box k))))))
+
+(define
+  pl-solve-or!
+  (fn
+    (db a b trail cut-box k)
+    (cond
+      ((and (pl-compound? a) (= (pl-fun a) "->") (= (len (pl-args a)) 2))
+        (pl-solve-if-then-else!
+          db
+          (first (pl-args a))
+          (nth (pl-args a) 1)
+          b
+          trail
+          cut-box
+          k))
+      (true
+        (let
+          ((mark (pl-trail-mark trail)))
+          (let
+            ((r (pl-solve! db a trail cut-box k)))
+            (cond
+              (r true)
+              ((dict-get cut-box :cut) false)
+              (true
+                (begin
+                  (pl-trail-undo-to! trail mark)
+                  (pl-solve! db b trail cut-box k))))))))))
+
+(define
+  pl-solve-if-then-else!
+  (fn
+    (db cond-goal then-goal else-goal trail cut-box k)
+    (let
+      ((mark (pl-trail-mark trail)))
+      (let
+        ((local-cb {:cut false}))
+        (let
+          ((found {:val false}))
+          (pl-solve!
+            db
+            cond-goal
+            trail
+            local-cb
+            (fn () (begin (dict-set! found :val true) true)))
+          (cond
+            ((dict-get found :val) (pl-solve! db then-goal trail cut-box k))
+            (true
+              (begin
+                (pl-trail-undo-to! trail mark)
+                (pl-solve! db else-goal trail cut-box k)))))))))
+
+(define pl-output-buffer "")
+
+(define pl-output-clear! (fn () (set! pl-output-buffer "")))
+
+(define
+  pl-output-write!
+  (fn (s) (begin (set! pl-output-buffer (str pl-output-buffer s)) nil)))
+
+(define
+  pl-format-args
+  (fn
+    (args)
+    (cond
+      ((empty? args) "")
+      ((= (len args) 1) (pl-format-term (first args)))
+      (true
+        (str
+          (pl-format-term (first args))
+          ", "
+          (pl-format-args (rest args)))))))
+
+(define
+  pl-format-term
+  (fn
+    (t)
+    (let
+      ((w (pl-walk-deep t)))
+      (cond
+        ((pl-var? w) (str "_" (pl-var-id w)))
+        ((pl-atom? w) (pl-atom-name w))
+        ((pl-num? w) (str (pl-num-val w)))
+        ((pl-str? w) (pl-str-val w))
+        ((pl-compound? w)
+          (str (pl-fun w) "(" (pl-format-args (pl-args w)) ")"))
+        (true (str w))))))
+
+(define
+  pl-eval-arith
+  (fn
+    (t)
+    (let
+      ((w (pl-walk-deep t)))
+      (cond
+        ((pl-num? w) (pl-num-val w))
+        ((pl-compound? w)
+          (let
+            ((f (pl-fun w)) (args (pl-args w)))
+            (cond
+              ((and (= f "+") (= (len args) 2))
+                (+
+                  (pl-eval-arith (first args))
+                  (pl-eval-arith (nth args 1))))
+              ((and (= f "-") (= (len args) 2))
+                (-
+                  (pl-eval-arith (first args))
+                  (pl-eval-arith (nth args 1))))
+              ((and (= f "-") (= (len args) 1))
+                (- 0 (pl-eval-arith (first args))))
+              ((and (= f "*") (= (len args) 2))
+                (*
+                  (pl-eval-arith (first args))
+                  (pl-eval-arith (nth args 1))))
+              ((and (= f "/") (= (len args) 2))
+                (/
+                  (pl-eval-arith (first args))
+                  (pl-eval-arith (nth args 1))))
+              ((and (= f "mod") (= (len args) 2))
+                (mod
+                  (pl-eval-arith (first args))
+                  (pl-eval-arith (nth args 1))))
+              ((and (= f "abs") (= (len args) 1))
+                (let
+                  ((v (pl-eval-arith (first args))))
+                  (cond ((< v 0) (- 0 v)) (true v))))
+              (true 0))))
+        (true 0)))))
+
+(define
+  pl-solve-not-eq!
+  (fn
+    (a b trail k)
+    (let
+      ((mark (pl-trail-mark trail)))
+      (let
+        ((unified (pl-unify! a b trail)))
+        (begin
+          (pl-trail-undo-to! trail mark)
+          (cond (unified false) (true (k))))))))
+
+(define
+  pl-solve-eq!
+  (fn
+    (a b trail k)
+    (let
+      ((mark (pl-trail-mark trail)))
+      (cond
+        ((pl-unify! a b trail)
+          (let
+            ((r (k)))
+            (cond
+              (r true)
+              (true (begin (pl-trail-undo-to! trail mark) false)))))
+        (true (begin (pl-trail-undo-to! trail mark) false))))))
+
+(define
+  pl-solve-user!
+  (fn
+    (db goal trail outer-cut-box k)
+    (let
+      ((inner-cut-box {:cut false}))
+      (let
+        ((outer-was-cut (dict-get outer-cut-box :cut)))
+        (pl-try-clauses!
+          db
+          goal
+          trail
+          (pl-db-lookup-goal db goal)
+          outer-cut-box
+          outer-was-cut
+          inner-cut-box
+          k)))))
+
+(define
+  pl-try-clauses!
+  (fn
+    (db goal trail clauses outer-cut-box outer-was-cut inner-cut-box k)
+    (cond
+      ((empty? clauses) false)
+      (true
+        (let
+          ((mark (pl-trail-mark trail)))
+          (let
+            ((clause (pl-instantiate-fresh (first clauses))))
+            (let
+              ((head (nth clause 1)) (body (nth clause 2)))
+              (cond
+                ((pl-unify! goal head trail)
+                  (let
+                    ((r (pl-solve! db body trail inner-cut-box k)))
+                    (cond
+                      (r true)
+                      ((dict-get inner-cut-box :cut)
+                        (begin (pl-trail-undo-to! trail mark) false))
+                      ((and (not outer-was-cut) (dict-get outer-cut-box :cut))
+                        (begin (pl-trail-undo-to! trail mark) false))
+                      (true
+                        (begin
+                          (pl-trail-undo-to! trail mark)
+                          (pl-try-clauses!
+                            db
+                            goal
+                            trail
+                            (rest clauses)
+                            outer-cut-box
+                            outer-was-cut
+                            inner-cut-box
+                            k))))))
+                (true
+                  (begin
+                    (pl-trail-undo-to! trail mark)
+                    (pl-try-clauses!
+                      db
+                      goal
+                      trail
+                      (rest clauses)
+                      outer-cut-box
+                      outer-was-cut
+                      inner-cut-box
+                      k)))))))))))
+
+(define
+  pl-solve-once!
+  (fn (db goal trail) (pl-solve! db goal trail {:cut false} (fn () true))))
+
+(define
+  pl-solve-count!
+  (fn
+    (db goal trail)
+    (let
+      ((box {:n 0}))
+      (pl-solve!
+        db
+        goal
+        trail
+        {:cut false}
+        (fn () (begin (dict-set! box :n (+ (dict-get box :n) 1)) false)))
+      (dict-get box :n))))

lib/prolog/scoreboard.json

@@ -0,0 +1,7 @@
+{
+  "total_passed": 183,
+  "total_failed": 0,
+  "total": 183,
+  "suites": {"parse":{"passed":25,"total":25,"failed":0},"unify":{"passed":47,"total":47,"failed":0},"clausedb":{"passed":14,"total":14,"failed":0},"solve":{"passed":62,"total":62,"failed":0},"append":{"passed":6,"total":6,"failed":0},"reverse":{"passed":6,"total":6,"failed":0},"member":{"passed":7,"total":7,"failed":0},"nqueens":{"passed":6,"total":6,"failed":0},"family":{"passed":10,"total":10,"failed":0}},
+  "generated": "2026-04-25T06:19:36+00:00"
+}

lib/prolog/scoreboard.md

@@ -0,0 +1,19 @@
+# Prolog scoreboard
+
+**183 / 183 passing** (0 failure(s)).
+Generated 2026-04-25T06:19:36+00:00.
+
+| Suite | Passed | Total | Status |
+|-------|--------|-------|--------|
+| parse | 25 | 25 | ok |
+| unify | 47 | 47 | ok |
+| clausedb | 14 | 14 | ok |
+| solve | 62 | 62 | ok |
+| append | 6 | 6 | ok |
+| reverse | 6 | 6 | ok |
+| member | 7 | 7 | ok |
+| nqueens | 6 | 6 | ok |
+| family | 10 | 10 | ok |
+
+Run `bash lib/prolog/conformance.sh` to refresh. Override the binary
+with `SX_SERVER=path/to/sx_server.exe bash …`.

lib/prolog/tests/clausedb.sx

@@ -0,0 +1,99 @@
+;; lib/prolog/tests/clausedb.sx — Clause DB unit tests
+
+(define pl-db-test-count 0)
+(define pl-db-test-pass 0)
+(define pl-db-test-fail 0)
+(define pl-db-test-failures (list))
+
+(define
+  pl-db-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-db-test-count (+ pl-db-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-db-test-pass (+ pl-db-test-pass 1))
+        (begin
+          (set! pl-db-test-fail (+ pl-db-test-fail 1))
+          (append!
+            pl-db-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(pl-db-test!
+  "head-key atom arity 0"
+  (pl-head-key (nth (first (pl-parse "foo.")) 1))
+  "foo/0")
+
+(pl-db-test!
+  "head-key compound arity 2"
+  (pl-head-key (nth (first (pl-parse "bar(a, b).")) 1))
+  "bar/2")
+
+(pl-db-test!
+  "clause-key of :- clause"
+  (pl-clause-key (first (pl-parse "likes(mary, X) :- friendly(X).")))
+  "likes/2")
+
+(pl-db-test!
+  "empty db lookup returns empty list"
+  (len (pl-db-lookup (pl-mk-db) "parent/2"))
+  0)
+
+(define pl-db-t1 (pl-mk-db))
+(pl-db-load! pl-db-t1 (pl-parse "foo(a). foo(b). foo(c)."))
+
+(pl-db-test!
+  "three facts same functor"
+  (len (pl-db-lookup pl-db-t1 "foo/1"))
+  3)
+(pl-db-test!
+  "mismatching key returns empty"
+  (len (pl-db-lookup pl-db-t1 "foo/2"))
+  0)
+
+(pl-db-test!
+  "first clause has arg a"
+  (pl-atom-name
+    (first (pl-args (nth (first (pl-db-lookup pl-db-t1 "foo/1")) 1))))
+  "a")
+
+(pl-db-test!
+  "third clause has arg c"
+  (pl-atom-name
+    (first (pl-args (nth (nth (pl-db-lookup pl-db-t1 "foo/1") 2) 1))))
+  "c")
+
+(define pl-db-t2 (pl-mk-db))
+(pl-db-load! pl-db-t2 (pl-parse "foo. bar. foo. parent(a, b). parent(c, d)."))
+
+(pl-db-test!
+  "atom heads keyed as foo/0"
+  (len (pl-db-lookup pl-db-t2 "foo/0"))
+  2)
+(pl-db-test!
+  "atom heads keyed as bar/0"
+  (len (pl-db-lookup pl-db-t2 "bar/0"))
+  1)
+(pl-db-test!
+  "compound heads keyed as parent/2"
+  (len (pl-db-lookup pl-db-t2 "parent/2"))
+  2)
+
+(pl-db-test!
+  "lookup-goal extracts functor/arity"
+  (len
+    (pl-db-lookup-goal pl-db-t2 (nth (first (pl-parse "parent(X, Y).")) 1)))
+  2)
+
+(pl-db-test!
+  "lookup-goal on atom goal"
+  (len (pl-db-lookup-goal pl-db-t2 (nth (first (pl-parse "foo.")) 1)))
+  2)
+
+(pl-db-test!
+  "stored clause is clause form"
+  (first (first (pl-db-lookup pl-db-t2 "parent/2")))
+  "clause")
+
+(define pl-clausedb-tests-run! (fn () {:failed pl-db-test-fail :passed pl-db-test-pass :total pl-db-test-count :failures pl-db-test-failures}))

lib/prolog/tests/programs/append.pl

@@ -0,0 +1,5 @@
+%% append/3 — list concatenation, classic Prolog
+%% Two clauses: empty-prefix base case + recursive cons-prefix.
+%% Bidirectional — works in all modes: build, check, split.
+append([], L, L).
+append([H|T], L, [H|R]) :- append(T, L, R).

lib/prolog/tests/programs/append.sx

@@ -0,0 +1,114 @@
+;; lib/prolog/tests/programs/append.sx — append/3 test runner
+;;
+;; Mirrors the Prolog source in append.pl (embedded as a string here because
+;; the SX runtime has no file-read primitive yet).
+
+(define pl-ap-test-count 0)
+(define pl-ap-test-pass 0)
+(define pl-ap-test-fail 0)
+(define pl-ap-test-failures (list))
+
+(define
+  pl-ap-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-ap-test-count (+ pl-ap-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-ap-test-pass (+ pl-ap-test-pass 1))
+        (begin
+          (set! pl-ap-test-fail (+ pl-ap-test-fail 1))
+          (append!
+            pl-ap-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-ap-term-to-sx
+  (fn
+    (t)
+    (cond
+      ((pl-num? t) (pl-num-val t))
+      ((pl-atom? t) (pl-atom-name t))
+      (true (list :complex)))))
+
+(define
+  pl-ap-list-walked
+  (fn
+    (w)
+    (cond
+      ((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
+      ((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
+        (cons
+          (pl-ap-term-to-sx (first (pl-args w)))
+          (pl-ap-list-walked (nth (pl-args w) 1))))
+      (true (list :not-list)))))
+
+(define pl-ap-list-to-sx (fn (t) (pl-ap-list-walked (pl-walk-deep t))))
+
+(define
+  pl-ap-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define
+  pl-ap-prog-src
+  "append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R).")
+
+(define pl-ap-db (pl-mk-db))
+
+(pl-db-load! pl-ap-db (pl-parse pl-ap-prog-src))
+
+(define pl-ap-env-1 {})
+(define pl-ap-goal-1 (pl-ap-goal "append([], [a, b], X)" pl-ap-env-1))
+(pl-solve-once! pl-ap-db pl-ap-goal-1 (pl-mk-trail))
+
+(pl-ap-test!
+  "append([], [a, b], X) → X = [a, b]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-1 "X"))
+  (list "a" "b"))
+
+(define pl-ap-env-2 {})
+(define pl-ap-goal-2 (pl-ap-goal "append([1, 2], [3, 4], X)" pl-ap-env-2))
+(pl-solve-once! pl-ap-db pl-ap-goal-2 (pl-mk-trail))
+
+(pl-ap-test!
+  "append([1, 2], [3, 4], X) → X = [1, 2, 3, 4]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-2 "X"))
+  (list 1 2 3 4))
+
+(pl-ap-test!
+  "append([1], [2, 3], [1, 2, 3]) succeeds"
+  (pl-solve-once!
+    pl-ap-db
+    (pl-ap-goal "append([1], [2, 3], [1, 2, 3])" {})
+    (pl-mk-trail))
+  true)
+
+(pl-ap-test!
+  "append([1, 2], [3], [1, 2, 4]) fails"
+  (pl-solve-once!
+    pl-ap-db
+    (pl-ap-goal "append([1, 2], [3], [1, 2, 4])" {})
+    (pl-mk-trail))
+  false)
+
+(pl-ap-test!
+  "append(X, Y, [1, 2, 3]) backtracks 4 times"
+  (pl-solve-count!
+    pl-ap-db
+    (pl-ap-goal "append(X, Y, [1, 2, 3])" {})
+    (pl-mk-trail))
+  4)
+
+(define pl-ap-env-6 {})
+(define pl-ap-goal-6 (pl-ap-goal "append(X, [3], [1, 2, 3])" pl-ap-env-6))
+(pl-solve-once! pl-ap-db pl-ap-goal-6 (pl-mk-trail))
+
+(pl-ap-test!
+  "append(X, [3], [1, 2, 3]) deduces X = [1, 2]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-6 "X"))
+  (list 1 2))
+
+(define pl-append-tests-run! (fn () {:failed pl-ap-test-fail :passed pl-ap-test-pass :total pl-ap-test-count :failures pl-ap-test-failures}))

lib/prolog/tests/programs/family.pl

@@ -0,0 +1,24 @@
+%% family — facts + transitive ancestor + derived relations.
+%% Five-generation tree: tom -> bob -> {ann, pat} -> jim, plus tom's
+%% other child liz.
+
+parent(tom, bob).
+parent(tom, liz).
+parent(bob, ann).
+parent(bob, pat).
+parent(pat, jim).
+
+male(tom).
+male(bob).
+male(jim).
+male(pat).
+female(liz).
+female(ann).
+
+father(F, C) :- parent(F, C), male(F).
+mother(M, C) :- parent(M, C), female(M).
+
+ancestor(X, Y) :- parent(X, Y).
+ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
+
+sibling(X, Y) :- parent(P, X), parent(P, Y), \=(X, Y).

lib/prolog/tests/programs/family.sx

@@ -0,0 +1,116 @@
+;; lib/prolog/tests/programs/family.sx — facts + ancestor + sibling relations.
+
+(define pl-fa-test-count 0)
+(define pl-fa-test-pass 0)
+(define pl-fa-test-fail 0)
+(define pl-fa-test-failures (list))
+
+(define
+  pl-fa-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-fa-test-count (+ pl-fa-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-fa-test-pass (+ pl-fa-test-pass 1))
+        (begin
+          (set! pl-fa-test-fail (+ pl-fa-test-fail 1))
+          (append!
+            pl-fa-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-fa-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define
+  pl-fa-prog-src
+  "parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(bob, pat). parent(pat, jim). male(tom). male(bob). male(jim). male(pat). female(liz). female(ann). father(F, C) :- parent(F, C), male(F). mother(M, C) :- parent(M, C), female(M). ancestor(X, Y) :- parent(X, Y). ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y). sibling(X, Y) :- parent(P, X), parent(P, Y), \\=(X, Y).")
+
+(define pl-fa-db (pl-mk-db))
+(pl-db-load! pl-fa-db (pl-parse pl-fa-prog-src))
+
+(pl-fa-test!
+  "parent(tom, bob) is a fact"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "parent(tom, bob)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-fa-test!
+  "parent(tom, ann) — not a direct parent"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "parent(tom, ann)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-fa-test!
+  "5 parent/2 facts in total"
+  (pl-solve-count!
+    pl-fa-db
+    (pl-fa-goal "parent(X, Y)" {})
+    (pl-mk-trail))
+  5)
+
+(pl-fa-test!
+  "ancestor(tom, jim) — three-step transitive"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "ancestor(tom, jim)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-fa-test!
+  "tom has 5 ancestors-of: bob, liz, ann, pat, jim"
+  (pl-solve-count!
+    pl-fa-db
+    (pl-fa-goal "ancestor(tom, X)" {})
+    (pl-mk-trail))
+  5)
+
+(pl-fa-test!
+  "father(bob, ann) succeeds"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "father(bob, ann)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-fa-test!
+  "father(liz, ann) fails (liz is female)"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "father(liz, ann)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-fa-test!
+  "mother(liz, X) fails (liz has no children)"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "mother(liz, X)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-fa-test!
+  "sibling(ann, pat) succeeds"
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "sibling(ann, pat)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-fa-test!
+  "sibling(ann, ann) fails by \\="
+  (pl-solve-once!
+    pl-fa-db
+    (pl-fa-goal "sibling(ann, ann)" {})
+    (pl-mk-trail))
+  false)
+
+(define pl-family-tests-run! (fn () {:failed pl-fa-test-fail :passed pl-fa-test-pass :total pl-fa-test-count :failures pl-fa-test-failures}))

lib/prolog/tests/programs/member.pl

@@ -0,0 +1,4 @@
+%% member/2 — list membership.
+%% Generates all solutions on backtracking when the element is unbound.
+member(X, [X|_]).
+member(X, [_|T]) :- member(X, T).

lib/prolog/tests/programs/member.sx

@@ -0,0 +1,91 @@
+;; lib/prolog/tests/programs/member.sx — member/2 generator.
+
+(define pl-mb-test-count 0)
+(define pl-mb-test-pass 0)
+(define pl-mb-test-fail 0)
+(define pl-mb-test-failures (list))
+
+(define
+  pl-mb-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-mb-test-count (+ pl-mb-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-mb-test-pass (+ pl-mb-test-pass 1))
+        (begin
+          (set! pl-mb-test-fail (+ pl-mb-test-fail 1))
+          (append!
+            pl-mb-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-mb-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define pl-mb-prog-src "member(X, [X|_]). member(X, [_|T]) :- member(X, T).")
+
+(define pl-mb-db (pl-mk-db))
+(pl-db-load! pl-mb-db (pl-parse pl-mb-prog-src))
+
+(pl-mb-test!
+  "member(2, [1, 2, 3]) succeeds"
+  (pl-solve-once!
+    pl-mb-db
+    (pl-mb-goal "member(2, [1, 2, 3])" {})
+    (pl-mk-trail))
+  true)
+
+(pl-mb-test!
+  "member(4, [1, 2, 3]) fails"
+  (pl-solve-once!
+    pl-mb-db
+    (pl-mb-goal "member(4, [1, 2, 3])" {})
+    (pl-mk-trail))
+  false)
+
+(pl-mb-test!
+  "member(X, []) fails"
+  (pl-solve-once!
+    pl-mb-db
+    (pl-mb-goal "member(X, [])" {})
+    (pl-mk-trail))
+  false)
+
+(pl-mb-test!
+  "member(X, [a, b, c]) generates 3 solutions"
+  (pl-solve-count!
+    pl-mb-db
+    (pl-mb-goal "member(X, [a, b, c])" {})
+    (pl-mk-trail))
+  3)
+
+(define pl-mb-env-1 {})
+(define pl-mb-goal-1 (pl-mb-goal "member(X, [11, 22, 33])" pl-mb-env-1))
+(pl-solve-once! pl-mb-db pl-mb-goal-1 (pl-mk-trail))
+
+(pl-mb-test!
+  "member(X, [11, 22, 33]) first solution X = 11"
+  (pl-num-val (pl-walk-deep (dict-get pl-mb-env-1 "X")))
+  11)
+
+(pl-mb-test!
+  "member(2, [1, 2, 3, 2, 1]) matches twice on backtrack"
+  (pl-solve-count!
+    pl-mb-db
+    (pl-mb-goal "member(2, [1, 2, 3, 2, 1])" {})
+    (pl-mk-trail))
+  2)
+
+(pl-mb-test!
+  "member with unbound list cell unifies"
+  (pl-solve-once!
+    pl-mb-db
+    (pl-mb-goal "member(a, [X, b, c])" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-member-tests-run! (fn () {:failed pl-mb-test-fail :passed pl-mb-test-pass :total pl-mb-test-count :failures pl-mb-test-failures}))

lib/prolog/tests/programs/nqueens.pl

@@ -0,0 +1,27 @@
+%% nqueens — permutation-and-test formulation.
+%% Caller passes the row list [1..N]; queens/2 finds N column placements
+%% s.t. no two queens attack on a diagonal. Same-column attacks are
+%% structurally impossible — Qs is a permutation, all distinct.
+%%
+%% No `>/2` `</2` `=</2` built-ins yet, so range/3 is omitted; tests pass
+%; the literal range list. Once the operator table lands and arithmetic
+%% comparison built-ins are in, range/3 can be added.
+queens(L, Qs) :- permute(L, Qs), safe(Qs).
+
+permute([], []).
+permute(L, [H|T]) :- select(H, L, R), permute(R, T).
+
+select(X, [X|T], T).
+select(X, [H|T], [H|R]) :- select(X, T, R).
+
+safe([]).
+safe([Q|Qs]) :- safe(Qs), no_attack(Q, Qs, 1).
+
+no_attack(_, [], _).
+no_attack(Q, [Q1|Qs], D) :-
+  is(D2, +(Q, D)),
+  \=(D2, Q1),
+  is(D3, -(Q, D)),
+  \=(D3, Q1),
+  is(D1, +(D, 1)),
+  no_attack(Q, Qs, D1).

lib/prolog/tests/programs/nqueens.sx

@@ -0,0 +1,108 @@
+;; lib/prolog/tests/programs/nqueens.sx — N-queens via permute + safe.
+
+(define pl-nq-test-count 0)
+(define pl-nq-test-pass 0)
+(define pl-nq-test-fail 0)
+(define pl-nq-test-failures (list))
+
+(define
+  pl-nq-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-nq-test-count (+ pl-nq-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-nq-test-pass (+ pl-nq-test-pass 1))
+        (begin
+          (set! pl-nq-test-fail (+ pl-nq-test-fail 1))
+          (append!
+            pl-nq-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-nq-term-to-sx
+  (fn
+    (t)
+    (cond
+      ((pl-num? t) (pl-num-val t))
+      ((pl-atom? t) (pl-atom-name t))
+      (true (list :complex)))))
+
+(define
+  pl-nq-list-walked
+  (fn
+    (w)
+    (cond
+      ((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
+      ((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
+        (cons
+          (pl-nq-term-to-sx (first (pl-args w)))
+          (pl-nq-list-walked (nth (pl-args w) 1))))
+      (true (list :not-list)))))
+
+(define pl-nq-list-to-sx (fn (t) (pl-nq-list-walked (pl-walk-deep t))))
+
+(define
+  pl-nq-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define
+  pl-nq-prog-src
+  "queens(L, Qs) :- permute(L, Qs), safe(Qs). permute([], []). permute(L, [H|T]) :- select(H, L, R), permute(R, T). select(X, [X|T], T). select(X, [H|T], [H|R]) :- select(X, T, R). safe([]). safe([Q|Qs]) :- safe(Qs), no_attack(Q, Qs, 1). no_attack(_, [], _). no_attack(Q, [Q1|Qs], D) :- is(D2, +(Q, D)), \\=(D2, Q1), is(D3, -(Q, D)), \\=(D3, Q1), is(D1, +(D, 1)), no_attack(Q, Qs, D1).")
+
+(define pl-nq-db (pl-mk-db))
+(pl-db-load! pl-nq-db (pl-parse pl-nq-prog-src))
+
+(pl-nq-test!
+  "queens([1], Qs) → 1 solution"
+  (pl-solve-count!
+    pl-nq-db
+    (pl-nq-goal "queens([1], Qs)" {})
+    (pl-mk-trail))
+  1)
+
+(pl-nq-test!
+  "queens([1, 2], Qs) → 0 solutions"
+  (pl-solve-count!
+    pl-nq-db
+    (pl-nq-goal "queens([1, 2], Qs)" {})
+    (pl-mk-trail))
+  0)
+
+(pl-nq-test!
+  "queens([1, 2, 3], Qs) → 0 solutions"
+  (pl-solve-count!
+    pl-nq-db
+    (pl-nq-goal "queens([1, 2, 3], Qs)" {})
+    (pl-mk-trail))
+  0)
+
+(pl-nq-test!
+  "queens([1, 2, 3, 4], Qs) → 2 solutions"
+  (pl-solve-count!
+    pl-nq-db
+    (pl-nq-goal "queens([1, 2, 3, 4], Qs)" {})
+    (pl-mk-trail))
+  2)
+
+(pl-nq-test!
+  "queens([1, 2, 3, 4, 5], Qs) → 10 solutions"
+  (pl-solve-count!
+    pl-nq-db
+    (pl-nq-goal "queens([1, 2, 3, 4, 5], Qs)" {})
+    (pl-mk-trail))
+  10)
+
+(define pl-nq-env-1 {})
+(define pl-nq-goal-1 (pl-nq-goal "queens([1, 2, 3, 4], Qs)" pl-nq-env-1))
+(pl-solve-once! pl-nq-db pl-nq-goal-1 (pl-mk-trail))
+
+(pl-nq-test!
+  "queens([1..4], Qs) first solution = [2, 4, 1, 3]"
+  (pl-nq-list-to-sx (dict-get pl-nq-env-1 "Qs"))
+  (list 2 4 1 3))
+
+(define pl-nqueens-tests-run! (fn () {:failed pl-nq-test-fail :passed pl-nq-test-pass :total pl-nq-test-count :failures pl-nq-test-failures}))

lib/prolog/tests/programs/reverse.pl

@@ -0,0 +1,7 @@
+%% reverse/2 — naive reverse via append/3.
+%% Quadratic — accumulates the reversed prefix one append per cons.
+reverse([], []).
+reverse([H|T], R) :- reverse(T, RT), append(RT, [H], R).
+
+append([], L, L).
+append([H|T], L, [H|R]) :- append(T, L, R).

lib/prolog/tests/programs/reverse.sx

@@ -0,0 +1,113 @@
+;; lib/prolog/tests/programs/reverse.sx — naive reverse/2 via append/3.
+;;
+;; Mirrors reverse.pl (embedded as a string here).
+
+(define pl-rv-test-count 0)
+(define pl-rv-test-pass 0)
+(define pl-rv-test-fail 0)
+(define pl-rv-test-failures (list))
+
+(define
+  pl-rv-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-rv-test-count (+ pl-rv-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-rv-test-pass (+ pl-rv-test-pass 1))
+        (begin
+          (set! pl-rv-test-fail (+ pl-rv-test-fail 1))
+          (append!
+            pl-rv-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-rv-term-to-sx
+  (fn
+    (t)
+    (cond
+      ((pl-num? t) (pl-num-val t))
+      ((pl-atom? t) (pl-atom-name t))
+      (true (list :complex)))))
+
+(define
+  pl-rv-list-walked
+  (fn
+    (w)
+    (cond
+      ((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
+      ((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
+        (cons
+          (pl-rv-term-to-sx (first (pl-args w)))
+          (pl-rv-list-walked (nth (pl-args w) 1))))
+      (true (list :not-list)))))
+
+(define pl-rv-list-to-sx (fn (t) (pl-rv-list-walked (pl-walk-deep t))))
+
+(define
+  pl-rv-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define
+  pl-rv-prog-src
+  "reverse([], []). reverse([H|T], R) :- reverse(T, RT), append(RT, [H], R). append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R).")
+
+(define pl-rv-db (pl-mk-db))
+(pl-db-load! pl-rv-db (pl-parse pl-rv-prog-src))
+
+(define pl-rv-env-1 {})
+(define pl-rv-goal-1 (pl-rv-goal "reverse([], X)" pl-rv-env-1))
+(pl-solve-once! pl-rv-db pl-rv-goal-1 (pl-mk-trail))
+
+(pl-rv-test!
+  "reverse([], X) → X = []"
+  (pl-rv-list-to-sx (dict-get pl-rv-env-1 "X"))
+  (list))
+
+(define pl-rv-env-2 {})
+(define pl-rv-goal-2 (pl-rv-goal "reverse([1], X)" pl-rv-env-2))
+(pl-solve-once! pl-rv-db pl-rv-goal-2 (pl-mk-trail))
+
+(pl-rv-test!
+  "reverse([1], X) → X = [1]"
+  (pl-rv-list-to-sx (dict-get pl-rv-env-2 "X"))
+  (list 1))
+
+(define pl-rv-env-3 {})
+(define pl-rv-goal-3 (pl-rv-goal "reverse([1, 2, 3], X)" pl-rv-env-3))
+(pl-solve-once! pl-rv-db pl-rv-goal-3 (pl-mk-trail))
+
+(pl-rv-test!
+  "reverse([1, 2, 3], X) → X = [3, 2, 1]"
+  (pl-rv-list-to-sx (dict-get pl-rv-env-3 "X"))
+  (list 3 2 1))
+
+(define pl-rv-env-4 {})
+(define pl-rv-goal-4 (pl-rv-goal "reverse([a, b, c, d], X)" pl-rv-env-4))
+(pl-solve-once! pl-rv-db pl-rv-goal-4 (pl-mk-trail))
+
+(pl-rv-test!
+  "reverse([a, b, c, d], X) → X = [d, c, b, a]"
+  (pl-rv-list-to-sx (dict-get pl-rv-env-4 "X"))
+  (list "d" "c" "b" "a"))
+
+(pl-rv-test!
+  "reverse([1, 2, 3], [3, 2, 1]) succeeds"
+  (pl-solve-once!
+    pl-rv-db
+    (pl-rv-goal "reverse([1, 2, 3], [3, 2, 1])" {})
+    (pl-mk-trail))
+  true)
+
+(pl-rv-test!
+  "reverse([1, 2], [1, 2]) fails"
+  (pl-solve-once!
+    pl-rv-db
+    (pl-rv-goal "reverse([1, 2], [1, 2])" {})
+    (pl-mk-trail))
+  false)
+
+(define pl-reverse-tests-run! (fn () {:failed pl-rv-test-fail :passed pl-rv-test-pass :total pl-rv-test-count :failures pl-rv-test-failures}))

lib/prolog/tests/solve.sx

@@ -0,0 +1,618 @@
+;; lib/prolog/tests/solve.sx — DFS solver unit tests
+
+(define pl-s-test-count 0)
+(define pl-s-test-pass 0)
+(define pl-s-test-fail 0)
+(define pl-s-test-failures (list))
+
+(define
+  pl-s-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-s-test-count (+ pl-s-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-s-test-pass (+ pl-s-test-pass 1))
+        (begin
+          (set! pl-s-test-fail (+ pl-s-test-fail 1))
+          (append!
+            pl-s-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-s-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define pl-s-empty-db (pl-mk-db))
+
+(pl-s-test!
+  "true succeeds"
+  (pl-solve-once! pl-s-empty-db (pl-s-goal "true" {}) (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "fail fails"
+  (pl-solve-once! pl-s-empty-db (pl-s-goal "fail" {}) (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "= identical atoms"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(a, a)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "= different atoms"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(a, b)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "= var to atom"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(X, foo)" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-s-env-bind {})
+(define pl-s-trail-bind (pl-mk-trail))
+(define pl-s-goal-bind (pl-s-goal "=(X, foo)" pl-s-env-bind))
+(pl-solve-once! pl-s-empty-db pl-s-goal-bind pl-s-trail-bind)
+
+(pl-s-test!
+  "X bound to foo after =(X, foo)"
+  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-bind "X")))
+  "foo")
+
+(pl-s-test!
+  "true , true succeeds"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "true, true" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "true , fail fails"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "true, fail" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "consistent X bindings succeed"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(X, a), =(X, a)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "conflicting X bindings fail"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(X, a), =(X, b)" {})
+    (pl-mk-trail))
+  false)
+
+(define pl-s-db1 (pl-mk-db))
+(pl-db-load!
+  pl-s-db1
+  (pl-parse "parent(tom, bob). parent(bob, liz). parent(bob, ann)."))
+
+(pl-s-test!
+  "fact lookup hit"
+  (pl-solve-once!
+    pl-s-db1
+    (pl-s-goal "parent(tom, bob)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "fact lookup miss"
+  (pl-solve-once!
+    pl-s-db1
+    (pl-s-goal "parent(tom, liz)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "all parent solutions"
+  (pl-solve-count!
+    pl-s-db1
+    (pl-s-goal "parent(X, Y)" {})
+    (pl-mk-trail))
+  3)
+
+(pl-s-test!
+  "fixed first arg solutions"
+  (pl-solve-count!
+    pl-s-db1
+    (pl-s-goal "parent(bob, Y)" {})
+    (pl-mk-trail))
+  2)
+
+(define pl-s-db2 (pl-mk-db))
+(pl-db-load!
+  pl-s-db2
+  (pl-parse
+    "parent(tom, bob). parent(bob, ann). ancestor(X, Y) :- parent(X, Y). ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z)."))
+
+(pl-s-test!
+  "rule direct ancestor"
+  (pl-solve-once!
+    pl-s-db2
+    (pl-s-goal "ancestor(tom, bob)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "rule transitive ancestor"
+  (pl-solve-once!
+    pl-s-db2
+    (pl-s-goal "ancestor(tom, ann)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "rule no path"
+  (pl-solve-once!
+    pl-s-db2
+    (pl-s-goal "ancestor(ann, tom)" {})
+    (pl-mk-trail))
+  false)
+
+(define pl-s-env-undo {})
+(define pl-s-trail-undo (pl-mk-trail))
+(define pl-s-goal-undo (pl-s-goal "=(X, a), fail" pl-s-env-undo))
+(pl-solve-once! pl-s-empty-db pl-s-goal-undo pl-s-trail-undo)
+
+(pl-s-test!
+  "trail undone after failure leaves X unbound"
+  (pl-var-bound? (dict-get pl-s-env-undo "X"))
+  false)
+
+(define pl-s-db-cut1 (pl-mk-db))
+
+(pl-db-load! pl-s-db-cut1 (pl-parse "g :- !. g :- true."))
+
+(pl-s-test!
+  "bare cut succeeds"
+  (pl-solve-once! pl-s-db-cut1 (pl-s-goal "g" {}) (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "cut commits to first matching clause"
+  (pl-solve-count! pl-s-db-cut1 (pl-s-goal "g" {}) (pl-mk-trail))
+  1)
+
+(define pl-s-db-cut2 (pl-mk-db))
+
+(pl-db-load! pl-s-db-cut2 (pl-parse "a(1). a(2). g(X) :- a(X), !."))
+
+(pl-s-test!
+  "cut commits to first a solution"
+  (pl-solve-count! pl-s-db-cut2 (pl-s-goal "g(X)" {}) (pl-mk-trail))
+  1)
+
+(define pl-s-db-cut3 (pl-mk-db))
+
+(pl-db-load!
+  pl-s-db-cut3
+  (pl-parse "a(1). a(2). g(X) :- a(X), !, fail. g(99)."))
+
+(pl-s-test!
+  "cut then fail blocks alt clauses"
+  (pl-solve-count! pl-s-db-cut3 (pl-s-goal "g(X)" {}) (pl-mk-trail))
+  0)
+
+(define pl-s-db-cut4 (pl-mk-db))
+
+(pl-db-load!
+  pl-s-db-cut4
+  (pl-parse "a(1). b(10). b(20). g(X, Y) :- a(X), !, b(Y)."))
+
+(pl-s-test!
+  "post-cut goal backtracks freely"
+  (pl-solve-count!
+    pl-s-db-cut4
+    (pl-s-goal "g(X, Y)" {})
+    (pl-mk-trail))
+  2)
+
+(define pl-s-db-cut5 (pl-mk-db))
+
+(pl-db-load!
+  pl-s-db-cut5
+  (pl-parse "r(1). r(2). q :- r(X), !. p :- q. p :- true."))
+
+(pl-s-test!
+  "inner cut does not commit outer predicate"
+  (pl-solve-count! pl-s-db-cut5 (pl-s-goal "p" {}) (pl-mk-trail))
+  2)
+
+(pl-s-test!
+  "\\= different atoms succeeds"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "\\=(a, b)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "\\= same atoms fails"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "\\=(a, a)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "\\= var-vs-atom would unify so fails"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "\\=(X, a)" {})
+    (pl-mk-trail))
+  false)
+
+(define pl-s-env-ne {})
+
+(define pl-s-trail-ne (pl-mk-trail))
+
+(define pl-s-goal-ne (pl-s-goal "\\=(X, a)" pl-s-env-ne))
+
+(pl-solve-once! pl-s-empty-db pl-s-goal-ne pl-s-trail-ne)
+
+(pl-s-test!
+  "\\= leaves no bindings"
+  (pl-var-bound? (dict-get pl-s-env-ne "X"))
+  false)
+
+(pl-s-test!
+  "; left succeeds"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal ";(true, fail)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "; right succeeds when left fails"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal ";(fail, true)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "; both fail"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal ";(fail, fail)" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "; both branches counted"
+  (pl-solve-count!
+    pl-s-empty-db
+    (pl-s-goal ";(true, true)" {})
+    (pl-mk-trail))
+  2)
+
+(define pl-s-db-call (pl-mk-db))
+
+(pl-db-load! pl-s-db-call (pl-parse "p(1). p(2)."))
+
+(pl-s-test!
+  "call(true) succeeds"
+  (pl-solve-once!
+    pl-s-db-call
+    (pl-s-goal "call(true)" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "call(p(X)) yields all solutions"
+  (pl-solve-count!
+    pl-s-db-call
+    (pl-s-goal "call(p(X))" {})
+    (pl-mk-trail))
+  2)
+
+(pl-s-test!
+  "call of bound goal var resolves"
+  (pl-solve-once!
+    pl-s-db-call
+    (pl-s-goal "=(G, true), call(G)" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-s-db-ite (pl-mk-db))
+
+(pl-db-load! pl-s-db-ite (pl-parse "p(1). p(2). q(yes). q(no)."))
+
+(pl-s-test!
+  "if-then-else: cond true → then runs"
+  (pl-solve-once!
+    pl-s-db-ite
+    (pl-s-goal ";(->(true, =(X, ok)), =(X, fallback))" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-s-env-ite1 {})
+
+(pl-solve-once!
+  pl-s-db-ite
+  (pl-s-goal ";(->(true, =(X, ok)), =(X, fallback))" pl-s-env-ite1)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "if-then-else: cond true binds via then"
+  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-ite1 "X")))
+  "ok")
+
+(pl-s-test!
+  "if-then-else: cond false → else"
+  (pl-solve-once!
+    pl-s-db-ite
+    (pl-s-goal ";(->(fail, =(X, ok)), =(X, fallback))" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-s-env-ite2 {})
+
+(pl-solve-once!
+  pl-s-db-ite
+  (pl-s-goal ";(->(fail, =(X, ok)), =(X, fallback))" pl-s-env-ite2)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "if-then-else: cond false binds via else"
+  (pl-atom-name (pl-walk-deep (dict-get pl-s-env-ite2 "X")))
+  "fallback")
+
+(pl-s-test!
+  "if-then-else: cond commits to first solution (count = 1)"
+  (pl-solve-count!
+    pl-s-db-ite
+    (pl-s-goal ";(->(p(X), =(Y, found)), =(Y, none))" {})
+    (pl-mk-trail))
+  1)
+
+(pl-s-test!
+  "if-then-else: then can backtrack"
+  (pl-solve-count!
+    pl-s-db-ite
+    (pl-s-goal ";(->(true, p(X)), =(X, none))" {})
+    (pl-mk-trail))
+  2)
+
+(pl-s-test!
+  "if-then-else: else can backtrack"
+  (pl-solve-count!
+    pl-s-db-ite
+    (pl-s-goal ";(->(fail, =(X, ignored)), p(X))" {})
+    (pl-mk-trail))
+  2)
+
+(pl-s-test!
+  "standalone -> with true cond succeeds"
+  (pl-solve-once!
+    pl-s-db-ite
+    (pl-s-goal "->(true, =(X, hi))" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "standalone -> with false cond fails"
+  (pl-solve-once!
+    pl-s-db-ite
+    (pl-s-goal "->(fail, =(X, hi))" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "write(hello)"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "write(hello)" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "hello")
+
+(pl-s-test!
+  "nl outputs newline"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once! pl-s-empty-db (pl-s-goal "nl" {}) (pl-mk-trail))
+    pl-output-buffer)
+  "\n")
+
+(pl-s-test!
+  "write(42) outputs digits"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "write(42)" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "42")
+
+(pl-s-test!
+  "write(foo(a, b)) formats compound"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "write(foo(a, b))" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "foo(a, b)")
+
+(pl-s-test!
+  "write conjunction"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "write(a), write(b)" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "ab")
+
+(pl-s-test!
+  "write of bound var walks binding"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "=(X, hello), write(X)" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "hello")
+
+(pl-s-test!
+  "write then nl"
+  (begin
+    (pl-output-clear!)
+    (pl-solve-once!
+      pl-s-empty-db
+      (pl-s-goal "write(hi), nl" {})
+      (pl-mk-trail))
+    pl-output-buffer)
+  "hi\n")
+
+(define pl-s-env-arith1 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, 42)" pl-s-env-arith1)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, 42) binds X to 42"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith1 "X")))
+  42)
+
+(define pl-s-env-arith2 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, +(2, 3))" pl-s-env-arith2)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, +(2, 3)) binds X to 5"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith2 "X")))
+  5)
+
+(define pl-s-env-arith3 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, *(2, 3))" pl-s-env-arith3)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, *(2, 3)) binds X to 6"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith3 "X")))
+  6)
+
+(define pl-s-env-arith4 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, -(10, 3))" pl-s-env-arith4)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, -(10, 3)) binds X to 7"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith4 "X")))
+  7)
+
+(define pl-s-env-arith5 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, /(10, 2))" pl-s-env-arith5)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, /(10, 2)) binds X to 5"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith5 "X")))
+  5)
+
+(define pl-s-env-arith6 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, mod(10, 3))" pl-s-env-arith6)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, mod(10, 3)) binds X to 1"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith6 "X")))
+  1)
+
+(define pl-s-env-arith7 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, abs(-(0, 5)))" pl-s-env-arith7)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, abs(-(0, 5))) binds X to 5"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith7 "X")))
+  5)
+
+(define pl-s-env-arith8 {})
+
+(pl-solve-once!
+  pl-s-empty-db
+  (pl-s-goal "is(X, +(2, *(3, 4)))" pl-s-env-arith8)
+  (pl-mk-trail))
+
+(pl-s-test!
+  "is(X, +(2, *(3, 4))) binds X to 14 (nested)"
+  (pl-num-val (pl-walk-deep (dict-get pl-s-env-arith8 "X")))
+  14)
+
+(pl-s-test!
+  "is(5, +(2, 3)) succeeds (LHS num matches)"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "is(5, +(2, 3))" {})
+    (pl-mk-trail))
+  true)
+
+(pl-s-test!
+  "is(6, +(2, 3)) fails (LHS num mismatch)"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "is(6, +(2, 3))" {})
+    (pl-mk-trail))
+  false)
+
+(pl-s-test!
+  "is propagates bound vars on RHS"
+  (pl-solve-once!
+    pl-s-empty-db
+    (pl-s-goal "=(Y, 4), is(X, +(Y, 1)), =(X, 5)" {})
+    (pl-mk-trail))
+  true)
+
+(define pl-solve-tests-run! (fn () {:failed pl-s-test-fail :passed pl-s-test-pass :total pl-s-test-count :failures pl-s-test-failures}))

plans/prolog-on-sx.md

@@ -39,30 +39,30 @@ Representation choices (finalise in phase 1, document here):
 ## Roadmap
 
 ### Phase 1 — tokenizer + term parser (no operator table)
-- [ ] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings, punct `( ) , . [ ] | ! :-`, comments (`%`, `/* */`)
+- [x] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings, punct `( ) , . [ ] | ! :-`, comments (`%`, `/* */`)
-- [ ] Parser: clauses `head :- body.` and facts `head.`; terms `atom | Var | number | compound(args) | [list,sugar]`
+- [x] Parser: clauses `head :- body.` and facts `head.`; terms `atom | Var | number | compound(args) | [list,sugar]`
-- [ ] **Skip for phase 1:** operator table. `X is Y + 1` must be written `is(X, '+'(Y, 1))`; `=` written `=(X, Y)`. Operators land in phase 4.
+- [x] **Skip for phase 1:** operator table. `X is Y + 1` must be written `is(X, '+'(Y, 1))`; `=` written `=(X, Y)`. Operators land in phase 4.
-- [ ] Unit tests in `lib/prolog/tests/parse.sx`
+- [x] Unit tests in `lib/prolog/tests/parse.sx` — 25 pass
 
 ### Phase 2 — unification + trail
-- [ ] `make-var`, `walk` (follow binding chain), `prolog-unify!` (terms + trail → bool), `trail-undo-to!`
+- [x] `make-var`, `walk` (follow binding chain), `prolog-unify!` (terms + trail → bool), `trail-undo-to!`
-- [ ] Occurs-check off by default, exposed as flag
+- [x] Occurs-check off by default, exposed as flag
-- [ ] 30+ unification tests in `lib/prolog/tests/unify.sx`: atoms, vars, compounds, lists, cyclic (no-occurs-check), mutual occurs
+- [x] 30+ unification tests in `lib/prolog/tests/unify.sx`: atoms, vars, compounds, lists, cyclic (no-occurs-check), mutual occurs — 47 pass
 
 ### Phase 3 — clause DB + DFS solver + cut + first classic programs
-- [ ] Clause DB: `"functor/arity" → list-of-clauses`, loader inserts
+- [x] Clause DB: `"functor/arity" → list-of-clauses`, loader inserts — `pl-mk-db` / `pl-db-add!` / `pl-db-load!` / `pl-db-lookup` / `pl-db-lookup-goal`, 14 tests in `tests/clausedb.sx`
-- [ ] Solver: DFS with choice points backed by delimited continuations (`lib/callcc.sx`). On goal entry, capture; per matching clause, unify head + recurse body; on failure, undo trail, try next
+- [x] Solver: DFS with choice points backed by delimited continuations (`lib/callcc.sx`). On goal entry, capture; per matching clause, unify head + recurse body; on failure, undo trail, try next — first cut: trail-based undo + CPS k (no shift/reset yet, per briefing gotcha). Built-ins so far: `true/0`, `fail/0`, `=/2`, `,/2`. Refactor to delimited conts later.
-- [ ] Cut (`!`): cut barrier at current choice-point frame; collapse all up to barrier
+- [x] Cut (`!`): cut barrier at current choice-point frame; collapse all up to barrier — two-cut-box scheme: each `pl-solve-user!` creates a fresh inner-cut-box (set by `!` in this predicate's body) AND snapshots the outer-cut-box state on entry. After body fails, abandon clause alternatives if (a) inner was set or (b) outer transitioned false→true during this call. Lets post-cut goals backtrack normally while blocking pre-cut alternatives. 6 cut tests cover bare cut, clause-commit, choice-commit, cut+fail, post-cut backtracking, nested-cut isolation.
-- [ ] Built-ins: `=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2` inside `;`, `call/1`, `write/1`, `nl/0`
+- [x] Built-ins: `=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2` inside `;`, `call/1`, `write/1`, `nl/0` — all 11 done. `write/1` and `nl/0` use a global `pl-output-buffer` string + `pl-output-clear!` for testability; `pl-format-term` walks deep then renders atoms/nums/strs/compounds/vars (var → `_<id>`). Note: cut-transparency via `;` not testable yet without operator support — `;(,(a,!), b)` parser-rejects because `,` is body-operator-only; revisit in phase 4.
-- [ ] Arithmetic `is/2` with `+ - * / mod abs`
+- [x] Arithmetic `is/2` with `+ - * / mod abs` — `pl-eval-arith` walks deep, recurses on compounds, dispatches on functor; binary `+ - * / mod`, binary AND unary `-`, unary `abs`. `is/2` evaluates RHS, wraps as `("num" v)`, unifies via `pl-solve-eq!`. 11 tests cover each op + nested + ground LHS match/mismatch + bound-var-on-RHS chain.
 - [ ] Classic programs in `lib/prolog/tests/programs/`:
-  - [ ] `append.pl` — list append (with backtracking)
+  - [x] `append.pl` — list append (with backtracking) — `lib/prolog/tests/programs/append.{pl,sx}`. 6 tests cover: build (`append([], L, X)`, `append([1,2], [3,4], X)`), check ground match/mismatch, full split-backtracking (`append(X, Y, [1,2,3])` → 4 solutions), single-deduce (`append(X, [3], [1,2,3])` → X=[1,2]).
-  - [ ] `reverse.pl` — naive reverse
+  - [x] `reverse.pl` — naive reverse — `lib/prolog/tests/programs/reverse.{pl,sx}`. Naive reverse via append: `reverse([H|T], R) :- reverse(T, RT), append(RT, [H], R)`. 6 tests cover empty, singleton, 3-list, 4-atom-list, ground match, ground mismatch.
-  - [ ] `member.pl` — generate all solutions via backtracking
+  - [x] `member.pl` — generate all solutions via backtracking — `lib/prolog/tests/programs/member.{pl,sx}`. Classic 2-clause `member(X, [X|_])` + `member(X, [_|T]) :- member(X, T)`. 7 tests cover bound-element hit/miss, empty list, generator (count = list length), first-solution binding, duplicate matches counted twice, anonymous head-cell unification.
-  - [ ] `nqueens.pl` — 8-queens
+  - [x] `nqueens.pl` — 8-queens — `lib/prolog/tests/programs/nqueens.{pl,sx}`. Permute-and-test formulation: `queens(L, Qs) :- permute(L, Qs), safe(Qs)` + `select` + `safe` + `no_attack`. Tested at N=1 (1), N=2 (0), N=3 (0), N=4 (2), N=5 (10) plus first-solution check at N=4 = `[2, 4, 1, 3]`. N=8 omitted — interpreter is too slow (40320 perms); add once compiled clauses or constraint-style placement land. `range/3` skipped pending arithmetic-comparison built-ins (`>/2` etc.).
-  - [ ] `family.pl` — facts + rules (parent/ancestor)
+  - [x] `family.pl` — facts + rules (parent/ancestor) — `lib/prolog/tests/programs/family.{pl,sx}`. 5 parent facts + male/female + derived `father`/`mother`/`ancestor`/`sibling`. 10 tests cover direct facts, fact count, transitive ancestor through 3 generations, descendant counting, gender-restricted father/mother, sibling via shared parent + `\=`.
-- [ ] `lib/prolog/conformance.sh` + runner, `scoreboard.json` + `scoreboard.md`
+- [x] `lib/prolog/conformance.sh` + runner, `scoreboard.json` + `scoreboard.md` — bash script feeds load + eval epoch script to sx_server, parses each suite's `{:failed N :passed N :total N :failures (...)}` line, writes JSON (machine) + MD (human) scoreboards. Exit non-zero on any failure. `SX_SERVER` env var overrides binary path. First scoreboard: 183 / 183.
-- [ ] Target: all 5 classic programs passing
+- [x] Target: all 5 classic programs passing — append (6) + reverse (6) + member (7) + nqueens (6) + family (10) = 35 program tests, all green. Phase 3 architecturally complete bar the conformance harness/scoreboard.
 
 ### Phase 4 — operator table + more built-ins (next run)
 - [ ] Operator table parsing (prefix/infix/postfix, precedence, assoc)
@@ -88,6 +88,20 @@ Representation choices (finalise in phase 1, document here):
 
 _Newest first. Agent appends on every commit._
 
+- 2026-04-25 — Conformance harness landed. `lib/prolog/conformance.sh` runs all 9 suites in one sx_server epoch, parses the `{:failed/:passed/:total/:failures}` summary lines, and writes `scoreboard.json` + `scoreboard.md`. `SX_SERVER` env var overrides the binary path; default points at the main-repo build. Phase 3 fully complete: 183 / 183 passing across parse/unify/clausedb/solve/append/reverse/member/nqueens/family.
+- 2026-04-25 — `family.pl` fifth classic program — completes the 5-program target. 5-fact pedigree + male/female + derived father/mother/ancestor/sibling. 10 tests cover fact lookup + count, transitive ancestor through 3 generations, descendant counting (5), gender-restricted derivations, sibling via shared parent guarded by `\=`. Total 183 (+10). All 5 classic programs ticked; Phase 3 needs only conformance harness + scoreboard left.
+- 2026-04-25 — `nqueens.pl` fourth classic program. Permute-and-test variant exercises every Phase-3 feature: lists with `[H|T]` cons sugar, multi-clause backtracking, recursive `permute`/`select`/`safe`/`no_attack`, `is/2` arithmetic on diagonals, `\=/2` for diagonal-conflict check. 6 tests at N ∈ {1,2,3,4,5} with expected counts {1,0,0,2,10} + first-solution `[2,4,1,3]`. N=5 takes ~30s (120 perms × safe-check); N=8 omitted as it would be ~thousands of seconds. Total 173 (+6).
+- 2026-04-25 — `member.pl` third classic program. Standard 2-clause definition; 7 tests cover bound-element hit/miss, empty-list fail, generator-count = list length, first-solution binding (X=11), duplicate elements matched twice on backtrack, anonymous-head unification (`member(a, [X, b, c])` binds X=a). Total 167 (+7).
+- 2026-04-25 — `reverse.pl` second classic program. Naive reverse defined via append. 6 tests (empty/singleton/3-list/4-atom-list/ground match/ground mismatch). Confirms the solver handles non-trivial recursive composition: `reverse([1,2,3], R)` recurses to depth 3 then unwinds via 3 nested `append`s. Total 160 (+6).
+- 2026-04-25 — `append.pl` first classic program. `lib/prolog/tests/programs/append.pl` is the canonical 2-clause source; `append.sx` embeds the source as a string (no file-read primitive in SX yet) and runs 6 tests covering build, check, full split-backtrack (4 solutions), and deduction modes. Helpers `pl-ap-list-to-sx` / `pl-ap-term-to-sx` convert deep-walked Prolog lists (`("compound" "." (h t))` / `("atom" "[]")`) to SX lists for structural assertion. Total 154 (+6).
+- 2026-04-25 — `is/2` arithmetic landed. `pl-eval-arith` recursively evaluates ground RHS expressions (binary `+ - * /`, `mod`; binary+unary `-`; unary `abs`); `is/2` wraps the value as `("num" v)` and unifies via `pl-solve-eq!`, so it works in all three modes — bind unbound LHS, check ground LHS for equality, propagate from earlier var bindings on RHS. 11 tests, total 148 (+11). Without operator support, expressions must be written prefix: `is(X, +(2, *(3, 4)))`.
+- 2026-04-25 — `write/1` + `nl/0` landed using global string buffer (`pl-output-buffer` + `pl-output-clear!` + `pl-output-write!`). `pl-format-term` walks deep + dispatches on atom/num/str/compound/var; `pl-format-args` recursively comma-joins. 7 new tests cover atom/num/compound formatting, conjunction order, var-walk, and `nl`. Built-ins box (`=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2`, `call/1`, `write/1`, `nl/0`) now ticked. Total 137 (+7).
+- 2026-04-25 — `->/2` if-then-else landed (both `;(->(C,T), E)` and standalone `->(C, T)` ≡ `(C -> T ; fail)`). `pl-solve-or!` now special-cases `->` in left arg → `pl-solve-if-then-else!`. Cond runs in a fresh local cut-box (ISO opacity for cut inside cond). Then-branch can backtrack, else-branch can backtrack, but cond commits to first solution. 9 new tests covering both forms, both branches, binding visibility, cond-commit, then-backtrack, else-backtrack. Total 130 (+9).
+- 2026-04-25 — Built-ins `\=/2`, `;/2`, `call/1` landed. `pl-solve-not-eq!` (try unify, always undo, succeed iff unify failed). `pl-solve-or!` (try left, on failure check cut and only try right if not cut). `call/1` opens a fresh inner cut-box (ISO opacity: cut inside `call(G)` commits G, not caller). 11 new tests in `tests/solve.sx` cover atoms+vars for `\=`, both branches + count for `;`, and `call/1` against atoms / compounds / bound goal vars. Total 121 (+11). Box not yet ticked — `->/2`, `write/1`, `nl/0` still pending.
+- 2026-04-25 — Cut (`!/0`) landed. `pl-cut?` predicate; solver functions all take a `cut-box`; `pl-solve-user!` creates a fresh inner-cut-box and snapshots `outer-was-cut`; `pl-try-clauses!` abandons alternatives when inner.cut OR (outer.cut transitioned false→true during this call). 6 new cut tests in `tests/solve.sx` covering bare cut, clause-commit, choice-commit, cut+fail blocks alt clauses, post-cut goal backtracks freely, inner cut isolation. Total 110 (+6).
+- 2026-04-25 — Phase 3 DFS solver landed (CPS, trail-based backtracking; delimited conts deferred). `pl-solve!` + `pl-solve-eq!` + `pl-solve-user!` + `pl-try-clauses!` + `pl-solve-once!` + `pl-solve-count!` in runtime.sx. Built-ins: `true/0`, `fail/0`, `=/2`, `,/2`. New `tests/solve.sx` 18/18 green covers atomic goals, =, conjunction, fact lookup, multi-solution count, recursive ancestor rule, trail-undo verification. Bug fix: `pl-instantiate` had no `("clause" h b)` case → vars in rule head/body were never instantiated, so rule resolution silently failed against runtime-var goals. Added clause case to recurse with shared var-env. Total 104 (+18).
+- 2026-04-24 — Phase 3 clause DB landed: `pl-mk-db` + `pl-head-key` / `pl-clause-key` / `pl-goal-key` + `pl-db-add!` / `pl-db-load!` / `pl-db-lookup` / `pl-db-lookup-goal` in runtime.sx. New `tests/clausedb.sx` 14/14 green. Total 86 (+14). Loader preserves declaration order (append!).
+- 2026-04-24 — Verified phase 1+2 already implemented on loops/prolog: `pl-parse-tests-run!` 25/25, `pl-unify-tests-run!` 47/47 (72 total). Ticked phase 1+2 boxes.
 - _(awaiting phase 1)_
 
 ## Blockers