From 738f44e47d2f7896330b35c364988fa49132eb22 Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 25 Apr 2026 00:38:50 +0000 Subject: [PATCH] prolog: DFS solver (CPS, trail-based) + true/fail/=/conj built-ins, 18 tests --- lib/prolog/runtime.sx | 91 +++++++++++++++++++ lib/prolog/tests/solve.sx | 184 ++++++++++++++++++++++++++++++++++++++ plans/prolog-on-sx.md | 3 +- 3 files changed, 277 insertions(+), 1 deletion(-) create mode 100644 lib/prolog/tests/solve.sx diff --git a/lib/prolog/runtime.sx b/lib/prolog/runtime.sx index 60d4f0ca..ee62c626 100644 --- a/lib/prolog/runtime.sx +++ b/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 {}))) @@ -278,3 +283,89 @@ (define pl-db-lookup-goal (fn (db goal) (pl-db-lookup db (pl-goal-key goal)))) + +(define + pl-solve! + (fn + (db goal trail k) + (let + ((g (pl-walk goal))) + (cond + ((pl-var? g) false) + ((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! + db + (first (pl-args g)) + trail + (fn () (pl-solve! db (nth (pl-args g) 1) trail k)))) + (true (pl-solve-user! db g trail 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 k) + (pl-try-clauses! db goal trail (pl-db-lookup-goal db goal) k))) + +(define + pl-try-clauses! + (fn + (db goal trail clauses 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 k))) + (cond + (r true) + (true + (begin + (pl-trail-undo-to! trail mark) + (pl-try-clauses! db goal trail (rest clauses) k)))))) + (true + (begin + (pl-trail-undo-to! trail mark) + (pl-try-clauses! db goal trail (rest clauses) k))))))))))) + +(define + pl-solve-once! + (fn (db goal trail) (pl-solve! db goal trail (fn () true)))) + +(define + pl-solve-count! + (fn + (db goal trail) + (let + ((box {:n 0})) + (pl-solve! + db + goal + trail + (fn () (begin (dict-set! box :n (+ (dict-get box :n) 1)) false))) + (dict-get box :n)))) diff --git a/lib/prolog/tests/solve.sx b/lib/prolog/tests/solve.sx new file mode 100644 index 00000000..f2e286c2 --- /dev/null +++ b/lib/prolog/tests/solve.sx @@ -0,0 +1,184 @@ +;; 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-solve-tests-run! (fn () {:failed pl-s-test-fail :passed pl-s-test-pass :total pl-s-test-count :failures pl-s-test-failures})) diff --git a/plans/prolog-on-sx.md b/plans/prolog-on-sx.md index 47f7b28a..6a53d61f 100644 --- a/plans/prolog-on-sx.md +++ b/plans/prolog-on-sx.md @@ -51,7 +51,7 @@ Representation choices (finalise in phase 1, document here): ### Phase 3 — clause DB + DFS solver + cut + first classic programs - [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 - [ ] Built-ins: `=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2` inside `;`, `call/1`, `write/1`, `nl/0` - [ ] Arithmetic `is/2` with `+ - * / mod abs` @@ -88,6 +88,7 @@ Representation choices (finalise in phase 1, document here): _Newest first. Agent appends on every commit._ +- 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)_