prolog: \=/2 + ;/2 + call/1 built-ins, 11 tests

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,222 @@
         (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-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) ",") (= (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) "call") (= (len (pl-args g)) 1))
+          (let
+            ((call-cb {:cut false}))
+            (pl-solve! db (first (pl-args g)) trail call-cb k)))
+        (true (pl-solve-user! db g trail cut-box k))))))
+
+(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-or!
+  (fn
+    (db a b trail cut-box k)
+    (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-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/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/solve.sx

@@ -0,0 +1,340 @@
+;; 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-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,21 +39,21 @@ 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 (`%`, `/* */`)
-- [ ] 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.
-- [ ] Unit tests in `lib/prolog/tests/parse.sx`
+- [x] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings, punct `( ) , . [ ] | ! :-`, comments (`%`, `/* */`)
+- [x] Parser: clauses `head :- body.` and facts `head.`; terms `atom | Var | number | compound(args) | [list,sugar]`
+- [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.
+- [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!`
-- [ ] 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] `make-var`, `walk` (follow binding chain), `prolog-unify!` (terms + trail → bool), `trail-undo-to!`
+- [x] Occurs-check off by default, exposed as flag
+- [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
-- [ ] 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
-- [ ] Cut (`!`): cut barrier at current choice-point frame; collapse all up to barrier
-- [ ] Built-ins: `=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2` inside `;`, `call/1`, `write/1`, `nl/0`
+- [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`
+- [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.
+- [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` — done so far: `=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `\\=/2`, `;/2`, `call/1`. Pending: `->/2` inside `;`, `write/1`, `nl/0`. Note: cut-transparency via `;` not testable yet without operator support — `;(,(a,!), b)` parser-rejects because `,` is body-operator-only.
 - [ ] Arithmetic `is/2` with `+ - * / mod abs`
 - [ ] Classic programs in `lib/prolog/tests/programs/`:
   - [ ] `append.pl` — list append (with backtracking)
@@ -88,6 +88,11 @@ Representation choices (finalise in phase 1, document here):
 
 _Newest first. Agent appends on every commit._
 
+- 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