Files
rose-ash/plans/prolog-on-sx.md
giles bf250a24bf
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
Progress log: sub_atom+aggregate_all, 496/496
2026-04-25 13:50:54 +00:00

127 lines
24 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# Prolog-on-SX: mini-Prolog interpreter on delimited continuations
Horn clauses + unification + cut + arithmetic, implemented as an **interpreter** (clauses live as SX data, a SX-implemented solver walks them). Backtracking is powered by the delimited-continuations machinery in `lib/callcc.sx` + `spec/evaluator.sx` Step 5 — this is the reason Prolog fits SX well.
End-state goal: **200+ tests passing** (classic programs + Hirst's ISO conformance subset + Hyperscript integration suite). Long-lived background agent driving the scoreboard up.
## Ground rules
- **Scope:** only touch `lib/prolog/**` and `plans/prolog-on-sx.md`. Do **not** edit `spec/`, `hosts/`, `shared/`, `lib/js/**`, `lib/hyperscript/**`, `lib/lua/**`, `lib/stdlib.sx`, or anything in `lib/` root. Prolog primitives go in `lib/prolog/runtime.sx`.
- **Shared-file issues** go under "Blockers" below with a minimal repro; do not fix from this loop.
- **SX files:** use `sx-tree` MCP tools only.
- **Architecture:** Prolog source → term AST → clause DB. Solver is SX code walking the DB; backtracking via delimited continuations, not a separate trail machine.
- **Commits:** one feature per commit. Keep `## Progress log` updated and tick boxes.
## Architecture sketch
```
Prolog source text
lib/prolog/tokenizer.sx — atoms, vars, numbers, punct, comments
lib/prolog/parser.sx — term AST; phase 1: f(a,b) syntax only, no operator table
lib/prolog/runtime.sx — clause DB, unify!, trail, solver (DFS + delimited-cont backtracking)
│ built-ins: =/2, \=/2, !/0, is/2, call/1, findall/3, …
solutions / side-effects
```
Representation choices (finalise in phase 1, document here):
- **Term:** nested SX list. Compound `(functor arg1 arg2)`. Atom = symbol. Number = number. Variable = `{:var "X" :binding <ref>}` with mutable binding slot.
- **List:** cons-cell compound `(. H T)` or similar. `[1,2,3]` sugar desugared at parse.
- **Clause:** `{:head <term> :body <term>}` where body is the conjunction goal.
- **Clause DB:** dict `"functor/arity" → list of clauses`.
## Roadmap
### Phase 1 — tokenizer + term parser (no operator table)
- [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
- [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
- [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.
- [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.
- [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.
- [x] Classic programs in `lib/prolog/tests/programs/`:
- [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]).
- [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.
- [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.
- [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.).
- [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 + `\=`.
- [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.
- [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)
- [x] Operator table parsing (prefix/infix/postfix, precedence, assoc) — `pl-op-table` (15 entries: `, ; -> = \= is < > =< >= + - * / mod`); precedence-climbing parser via `pp-parse-primary` + `pp-parse-term-prec` + `pp-parse-op-rhs`. Parens override precedence. Args inside compounds parsed at 999 so `,` stays as separator. xfx/xfy/yfx supported; prefix/postfix deferred (so `-5` still tokenises as bare atom + num as before). Comparison built-ins `</2 >/2 =</2 >=/2` added. New `tests/operators.sx` 19 tests cover assoc/precedence/parens + solver via infix.
- [x] `assert/1`, `asserta/1`, `assertz/1`, `retract/1``assert` aliases `assertz`. Helpers `pl-rt-to-ast` (deep-walk + replace runtime vars with `_G<id>` parse markers) + `pl-build-clause` (detect `:-` head). `assertz` uses `pl-db-add!`; `asserta` uses new `pl-db-prepend!`. `retract` walks goal, looks up by functor/arity, tries each clause via unification, removes first match by index (`pl-list-without`). 11 tests in `tests/dynamic.sx`. Rule-asserts now work — `:-` added to op table (prec 1200 xfx) with fix to `pl-token-op` accepting `"op"` token type. 15 tests in `tests/assert_rules.sx`.
- [x] `findall/3`, `bagof/3`, `setof/3` — shared `pl-collect-solutions` runs the goal in a fresh cut-box, deep-copies the template (via `pl-deep-copy` with var-map for shared-var preservation) on each success, returns false to backtrack, then restores trail. `findall` always succeeds with a (possibly empty) list. `bagof` fails on empty. `setof` builds a string-keyed dict via `pl-format-term` for sort+dedupe (via `keys` + `sort`), fails on empty. Existential `^` deferred (operator). 11 tests in `tests/findall.sx`.
- [x] `copy_term/2`, `functor/3`, `arg/3`, `=../2``copy_term/2` reuses `pl-deep-copy` with a fresh var-map (preserves source aliasing). `functor/3` handles 4 modes: compound→{name, arity}, atom→{atom, 0}, num→{num, 0}, var with ground name+arity→constructed term (`pl-make-fresh-args` for compound case). `arg/3` extracts 1-indexed arg from compound. **`=../2` deferred** — the tokenizer treats `.` as the clause terminator unconditionally, so `=..` lexes as `=` + `.` + `.`; needs special-case lex (or surface syntax via a different name). 14 tests in `tests/term_inspect.sx`.
- [x] String/atom predicates
### Phase 5 — Hyperscript integration
- [x] `prolog-query` primitive callable from SX/Hyperscript
- [ ] Hyperscript DSL: `when allowed(user, :edit) then …`**blocked** (needs `lib/hyperscript/**`, out of scope)
- [ ] Integration suite
### Phase 6 — ISO conformance
- [x] Vendor Hirst's conformance tests
- [x] Drive scoreboard to 200+
### Phase 7 — compiler (later, optional)
- [ ] Compile clauses to SX continuations for speed
- [ ] Keep interpreter as the reference
## Progress log
_Newest first. Agent appends on every commit._
- 2026-04-25 — `sub_atom/5` (non-deterministic substring enumeration; CPS loop over all (start,sublen) pairs; trail-undo only on backtrack) + `aggregate_all/3` (6 templates: count/bag/sum/max/min/set; uses `pl-collect-solutions`). 25 tests in `tests/string_agg.sx`. Total **496** (+25).
- 2026-04-25 — `:-` operator + assert with rules: added `(list ":-" 1200 "xfx")` to `pl-op-table`; fixed `pl-token-op` to accept `"op"` token type (tokenizer emits `:-` as `"op"`, not `"atom"`). `pl-build-clause` already handled `("compound" ":-" ...)`. `assert((head :- body))` now works for facts+rules. 15 tests in `tests/assert_rules.sx`. Total **471** (+15).
- 2026-04-25 — IO/term predicates: `term_to_atom/2` (bidirectional: format term or parse atom), `term_string/2` (alias), `with_output_to/2` (atom/string sinks — saves/restores `pl-output-buffer`), `writeln/1`, `format/1` (~n/~t/~~), `format/2` (~w/~a/~d pull from arg list). 24 tests in `tests/io_predicates.sx`. Total **456** (+24).
- 2026-04-25 — Char predicates: `char_type/2` (9 modes: alpha/alnum/digit/digit(N)/space/white/upper(L)/lower(U)/ascii(C)/punct), `upcase_atom/2`, `downcase_atom/2`, `string_upper/2`, `string_lower/2`. 10 helpers using `char-code`/`char-from-code` SX primitives. 27 tests in `tests/char_predicates.sx`. Total **432** (+27).
- 2026-04-25 — Set/fold predicates: `foldl/4` (CPS fold-left, threads accumulator via `pl-apply-goal`), `list_to_set/2` (dedup preserving first-occurrence), `intersection/3`, `subtract/3`, `union/3` (all via `pl-struct-eq?`). 3 new helpers, 15 tests in `tests/set_predicates.sx`. Total **405** (+15).
- 2026-04-25 — Meta-call predicates: `forall/2` (negation-of-counterexample), `maplist/2` (goal over list), `maplist/3` (map goal building output list), `include/3` (filter by goal success), `exclude/3` (filter by goal failure). New `pl-apply-goal` helper extends a goal with extra args. 15 tests in `tests/meta_call.sx`. Total **390** (+15).
- 2026-04-25 — List/utility predicates: `==/2`, `\==/2` (structural equality/inequality via `pl-struct-eq?`), `flatten/2` (deep Prolog-list flatten), `numlist/3` (integer range list), `atomic_list_concat/2` (join with no sep), `atomic_list_concat/3` (join with separator), `sum_list/2`, `max_list/2`, `min_list/2` (arithmetic folds), `delete/3` (remove all struct-equal elements). 7 new helpers, 33 tests in `tests/list_predicates.sx`. Total **375** (+33).
- 2026-04-25 — Meta/logic predicates: `\+/1` (negation-as-failure, trail-undo on success), `not/1` (alias), `once/1` (commit to first solution via if-then-else), `ignore/1` (always succeed), `ground/1` (all vars bound), `sort/2` (sort + dedup by formatted key), `msort/2` (sort, keep dups), `atom_number/2` (bidirectional), `number_string/2` (bidirectional). 2 helpers (`pl-ground?`, `pl-sort-pairs-dedup`). 25 tests in `tests/meta_predicates.sx`. Total **342** (+25).
- 2026-04-25 — ISO utility predicates batch: `succ/2` (bidirectional), `plus/3` (3-mode bidirectional), `between/3` (backtracking range generator), `length/2` (bidirectional list length + var-list constructor), `last/2`, `nth0/3`, `nth1/3`, `max/2` + `min/2` in arithmetic eval. 6 new helper functions (`pl-list-length`, `pl-make-list-of-vars`, `pl-between-loop!`, `pl-solve-between!`, `pl-solve-last!`, `pl-solve-nth0!`). 29 tests in `tests/iso_predicates.sx`. Phase 6 complete: scoreboard already at 317, far above 200+ target. Hyperscript DSL blocked (needs `lib/hyperscript/**`). Total **317** (+29).
- 2026-04-25 — `prolog-query` SX API (`lib/prolog/query.sx`). New public API layer: `pl-load source-str → db`, `pl-query-all db query-str → list of solution dicts`, `pl-query-one db query-str → dict or nil`, `pl-query src query → list` (convenience). Each solution dict maps variable name strings to their formatted term strings. Var names extracted from pre-instantiation parse AST. Trail is marked before solve and reset after to ensure clean state. 16 tests in `tests/query_api.sx` cover fact lookup, no-solution, boolean queries, multi-var, recursive rules, is/2 built-in, query-one, convenience form. Total **288** (+16).
- 2026-04-25 — String/atom predicates. Type-test predicates: `var/1`, `nonvar/1`, `atom/1`, `number/1`, `integer/1`, `float/1` (always-fail), `compound/1`, `callable/1`, `atomic/1`, `is_list/1`. String/atom operations: `atom_length/2`, `atom_concat/3` (3 modes: both-ground, result+first, result+second), `atom_chars/2` (bidirectional), `atom_codes/2` (bidirectional), `char_code/2` (bidirectional), `number_codes/2`, `number_chars/2`. 7 helper functions in runtime.sx (`pl-list-to-prolog`, `pl-proper-list?`, `pl-prolog-list-to-sx`, `pl-solve-atom-concat!`, `pl-solve-atom-chars!`, `pl-solve-atom-codes!`, `pl-solve-char-code!`). 34 tests in `tests/atoms.sx`. Total **272** (+34).
- 2026-04-25 — `copy_term/2` + `functor/3` + `arg/3` (term inspection). `copy_term` is a one-line dispatch to existing `pl-deep-copy`. `functor/3` is bidirectional — decomposes a bound compound/atom/num into name+arity OR constructs from ground name+arity (atom+positive-arity → compound with N anonymous fresh args via `pl-make-fresh-args`; arity 0 → atom/num). `arg/3` extracts 1-indexed arg with bounds-fail. New helper `pl-solve-eq2!` for paired-unification with shared trail-undo. 14 tests in `tests/term_inspect.sx`. Total **238** (+14). `=..` deferred — `.` always tokenizes as clause terminator; needs special lexer case.
- 2026-04-25 — `findall/3` + `bagof/3` + `setof/3`. Shared collector `pl-collect-solutions` runs the goal in a fresh cut-box, deep-copies the template per success (`pl-deep-copy` walks term, allocates fresh runtime vars via shared var-map so co-occurrences keep aliasing), returns false to keep backtracking, then `pl-trail-undo-to!` to clean up. `findall` always builds a list. `bagof` fails on empty. `setof` uses a `pl-format-term`-keyed dict + SX `sort` for dedupe + ordering. New `tests/findall.sx` 11 tests. Total **224** (+11). Existential `^` deferred — needs operator.
- 2026-04-25 — Dynamic clauses: `assert/1`, `assertz/1`, `asserta/1`, `retract/1`. New helpers `pl-rt-to-ast` (deep-walk runtime term → parse-AST, mapping unbound runtime vars to `_G<id>` markers so `pl-instantiate-fresh` produces fresh vars per call) + `pl-build-clause` + `pl-db-prepend!` + `pl-list-without`. `retract` keeps runtime vars (so the caller's vars get bound), walks head for the functor/arity key, tries each stored clause via `pl-unify!`, removes the first match by index. 11 tests in `tests/dynamic.sx`; conformance script gained dynamic row. Total **213** (+11). Rule-form asserts (`(H :- B)`) deferred until `:-` is in the op table.
- 2026-04-25 — Phase 4 starts: operator-table parsing. Parser rewrite uses precedence climbing (xfx/xfy/yfx); 15-op table covers control (`, ; ->`), comparison (`= \\= is < > =< >=`), arithmetic (`+ - * / mod`). Parens override. Backwards-compatible: prefix-syntax compounds (`=(X, Y)`, `+(2, 3)`) still parse as before; existing 183 tests untouched. Added comparison built-ins `</2 >/2 =</2 >=/2` to runtime (eval both sides, compare). New `tests/operators.sx` 19 tests; conformance script gained an operators row. Total **202** (+19). Prefix/postfix deferred — `-5` keeps old bare-atom semantics.
- 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
_Shared-file issues that need someone else to fix. Minimal repro only._
- **Phase 5 Hyperscript DSL** — `lib/hyperscript/**` is out of scope for this loop. Needs `lib/hyperscript/parser.sx` + evaluator to add `when allowed(user, :edit) then …` syntax. Skipping; Phase 5 item 1 (`prolog-query` SX API) is done.