From f019d4272725f74226f721fbf51e8fe5b825bee5 Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 25 Apr 2026 01:14:12 +0000 Subject: [PATCH] prolog: cut !/0 with two-cut-box barrier scheme, 6 tests --- lib/prolog/runtime.sx | 59 ++++++++++++++++++++++++++++++++------- lib/prolog/tests/solve.sx | 59 +++++++++++++++++++++++++++++++++++++++ plans/prolog-on-sx.md | 3 +- 3 files changed, 110 insertions(+), 11 deletions(-) diff --git a/lib/prolog/runtime.sx b/lib/prolog/runtime.sx index ee62c626..b30044e1 100644 --- a/lib/prolog/runtime.sx +++ b/lib/prolog/runtime.sx @@ -284,14 +284,19 @@ 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 k) + (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)) @@ -301,8 +306,9 @@ 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)))))) + cut-box + (fn () (pl-solve! db (nth (pl-args g) 1) trail cut-box k)))) + (true (pl-solve-user! db g trail cut-box k)))))) (define pl-solve-eq! @@ -322,13 +328,25 @@ (define pl-solve-user! (fn - (db goal trail k) - (pl-try-clauses! db goal trail (pl-db-lookup-goal db goal) k))) + (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 k) + (db goal trail clauses outer-cut-box outer-was-cut inner-cut-box k) (cond ((empty? clauses) false) (true @@ -341,21 +359,41 @@ (cond ((pl-unify! goal head trail) (let - ((r (pl-solve! db body trail k))) + ((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) k)))))) + (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) k))))))))))) + (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 (fn () true)))) + (fn (db goal trail) (pl-solve! db goal trail {:cut false} (fn () true)))) (define pl-solve-count! @@ -367,5 +405,6 @@ db goal trail + {:cut false} (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 index f2e286c2..965a05ca 100644 --- a/lib/prolog/tests/solve.sx +++ b/lib/prolog/tests/solve.sx @@ -181,4 +181,63 @@ (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) + (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 6a53d61f..435b9bce 100644 --- a/plans/prolog-on-sx.md +++ b/plans/prolog-on-sx.md @@ -52,7 +52,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` - [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` - [ ] Arithmetic `is/2` with `+ - * / mod abs` - [ ] Classic programs in `lib/prolog/tests/programs/`: @@ -88,6 +88,7 @@ Representation choices (finalise in phase 1, document here): _Newest first. Agent appends on every commit._ +- 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.