prolog: cut !/0 with two-cut-box barrier scheme, 6 tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled

This commit is contained in:
2026-04-25 01:14:12 +00:00
parent 738f44e47d
commit f019d42727
3 changed files with 110 additions and 11 deletions

View File

@@ -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))))

View File

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

View File

@@ -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.