⏺ Clean build with no warnings. Here's a summary of what was completed: #2
No reviewers
Labels
No labels
bug
documentation
duplicate
enhancement
good first issue
help wanted
invalid
question
wontfix
No milestone
No project
No assignees
1 participant
No due date set.
Dependencies
No dependencies set.
Reference
navicore/patch-prolog-v1!2
Loading…
Add table
Add a link
Reference in a new issue
No description provided.
Delete branch "phase-5"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Phase 5 — Complete
All 203 tests pass (132 unit + 71 integration), zero warnings.
Implementation (from previous session)
All Phase 5 builtins were implemented across builtins.rs, solver.rs, tokenizer.rs, and parser.rs:
Bugs found and fixed this session
Tests added (38 new integration tests)
Covering: compare, term ordering operators, functor (decompose/construct/number), arg, =.. (decompose/construct/in-rule), between
(basic/single/empty/in-rule/with-findall), copy_term, succ, plus, msort, sort, number_chars, number_codes, and combined scenarios like sort-in-rule and
functor-in-rule.
patch-prolog Completeness & Usability Plan
Context
patch-prolog is a Rust-based Prolog engine for linting generative AI output. It compiles
.plrules at build time into a binary, then runs queries at runtime. The core engine works — unification, backtracking, cut, negation-as-failure, arithmetic — and Phase 1+2 improvements are complete.Phase 1: Critical Built-ins — COMPLETE
1a. Type-checking predicates in
builtins.rsvar/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/11b. List predicates as Prolog rules in
knowledge/stdlib.plmember/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/31c. Solution collection:
findall/31d. If-then-else and disjunction
->(Arrow) and;(Semicolon) tokensparse_paren_body()handles(Cond -> Then ; Else)and(A ; B)BuiltinResultvariants — Disjunction, IfThenElse, IfThen, ConjunctionPhase 2: Robustness & Safety — COMPLETE
2a. Recursion depth limit
max_depthfield on Solver (default 10,000)with_max_depth()builder methodSolveResult::Errorinstead of stack overflow2b. Integer overflow protection
checked_add,checked_sub,checked_mul,checked_div,checked_neg2c. Float NaN/Infinity detection
check_float()validates every float operation resultPhase 3: Usability — COMPLETE
3a.
once/1andcall/1once/1— solve goal, take first solution, cut (usestry_solve_once+ choice stack truncation)call/1— execute a term as a goal (basic meta-call)builtins.rs,solver.rs3b. Atom/string predicates
atom_length/2atom_concat/3atom_chars/2builtins.rs(BuiltinResult variants),solver.rs(execution with mutable interner)3c. Additional arithmetic functions
Added to
is/2evaluation:abs/1max/2min/2sign/1builtins.rsPhase 4: Testing — COMPLETE
4a. Integration tests (
tests/integration.rs)4b. Edge case tests
4c. Stdlib tests
Test counts
Phase 5: Nice-to-have — COMPLETE
write/1,writeln/1,nl/0— I/O for debugging rulescompare/3,@</2,@>/2,@=</2,@>=/2— term ordering (ISO standard order)functor/3,arg/3,=../2— term introspection/decompositionbetween/3— integer enumeration (with backtracking, works inside findall)copy_term/2— term copying with fresh variablessucc/2,plus/3— Peano arithmetic (bidirectional)msort/2,sort/2— list sorting (sort removes duplicates)number_chars/2,number_codes/2— number/string conversion (bidirectional)assert/1,retract/1— dynamic predicates (future)Architecture Notes
patch-prologbinary +crates/prolog-corelibrarybuild.rscompilesknowledge/*.plinto binary via bincode[]and!always interned:CompiledDatabase::new()ensures this (required for findall, list ops, once/1)disjunction: boolflag on ChoicePoint to distinguish from clause alternativesparse_paren_body()handles;,->, and,as control flow operatorsCurrent Built-in Predicates (~55 total)
true,fail,false,!,=,\=,is,<,>,=<,>=,=:=,=\=,\+var/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/1;/2(disjunction),->/2(if-then),,/2(conjunction)once/1,call/1findall/3atom_length/2,atom_concat/3,atom_chars/2+,-,*,/,mod, unary-,abs/1,max/2,min/2,sign/1write/1,writeln/1,nl/0compare/3,@</2,@>/2,@=</2,@>=/2functor/3,arg/3,=../2between/3copy_term/2succ/2,plus/3msort/2,sort/2number_chars/2,number_codes/2Stdlib (knowledge/stdlib.pl)
member/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/3patch-prolog Completeness & Usability Plan
Context
patch-prolog is a Rust-based Prolog engine for linting generative AI output. It compiles
.plrules at build time into a binary, then runs queries at runtime. The core engine works — unification, backtracking, cut, negation-as-failure, arithmetic — and Phase 1+2 improvements are complete.Phase 1: Critical Built-ins — COMPLETE
1a. Type-checking predicates in
builtins.rsvar/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/11b. List predicates as Prolog rules in
knowledge/stdlib.plmember/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/31c. Solution collection:
findall/31d. If-then-else and disjunction
->(Arrow) and;(Semicolon) tokensparse_paren_body()handles(Cond -> Then ; Else)and(A ; B)BuiltinResultvariants — Disjunction, IfThenElse, IfThen, ConjunctionPhase 2: Robustness & Safety — COMPLETE
2a. Recursion depth limit
max_depthfield on Solver (default 10,000)with_max_depth()builder methodSolveResult::Errorinstead of stack overflow2b. Integer overflow protection
checked_add,checked_sub,checked_mul,checked_div,checked_neg2c. Float NaN/Infinity detection
check_float()validates every float operation resultPhase 3: Usability — COMPLETE
3a.
once/1andcall/1once/1— solve goal, take first solution, cut (usestry_solve_once+ choice stack truncation)call/1— execute a term as a goal (basic meta-call)builtins.rs,solver.rs3b. Atom/string predicates
atom_length/2atom_concat/3atom_chars/2builtins.rs(BuiltinResult variants),solver.rs(execution with mutable interner)3c. Additional arithmetic functions
Added to
is/2evaluation:abs/1max/2min/2sign/1builtins.rsPhase 4: Testing — COMPLETE
4a. Integration tests (
tests/integration.rs)4b. Edge case tests
4c. Stdlib tests
Test counts
Phase 5: Nice-to-have — COMPLETE
write/1,writeln/1,nl/0— I/O for debugging rulescompare/3,@</2,@>/2,@=</2,@>=/2— term ordering (ISO standard order)functor/3,arg/3,=../2— term introspection/decompositionbetween/3— integer enumeration (with backtracking, works inside findall)copy_term/2— term copying with fresh variablessucc/2,plus/3— Peano arithmetic (bidirectional)msort/2,sort/2— list sorting (sort removes duplicates)number_chars/2,number_codes/2— number/string conversion (bidirectional)assert/1,retract/1— dynamic predicates (future)Architecture Notes
patch-prologbinary +crates/prolog-corelibrarybuild.rscompilesknowledge/*.plinto binary via bincode[]and!always interned:CompiledDatabase::new()ensures this (required for findall, list ops, once/1)disjunction: boolflag on ChoicePoint to distinguish from clause alternativesparse_paren_body()handles;,->, and,as control flow operatorsCurrent Built-in Predicates (~55 total)
true,fail,false,!,=,\=,is,<,>,=<,>=,=:=,=\=,\+var/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/1;/2(disjunction),->/2(if-then),,/2(conjunction)once/1,call/1findall/3atom_length/2,atom_concat/3,atom_chars/2+,-,*,/,mod, unary-,abs/1,max/2,min/2,sign/1write/1,writeln/1,nl/0compare/3,@</2,@>/2,@=</2,@>=/2functor/3,arg/3,=../2between/3copy_term/2succ/2,plus/3msort/2,sort/2number_chars/2,number_codes/2Stdlib (knowledge/stdlib.pl)
member/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/3patch-prolog Completeness & Usability Plan
Context
patch-prolog is a Rust-based Prolog engine for linting generative AI output. It compiles
.plrules at build time into a binary, then runs queries at runtime. The core engine works — unification, backtracking, cut, negation-as-failure, arithmetic — and Phase 1+2 improvements are complete.Phase 1: Critical Built-ins — COMPLETE
1a. Type-checking predicates in
builtins.rsvar/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/11b. List predicates as Prolog rules in
knowledge/stdlib.plmember/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/31c. Solution collection:
findall/31d. If-then-else and disjunction
->(Arrow) and;(Semicolon) tokensparse_paren_body()handles(Cond -> Then ; Else)and(A ; B)BuiltinResultvariants — Disjunction, IfThenElse, IfThen, ConjunctionPhase 2: Robustness & Safety — COMPLETE
2a. Recursion depth limit
max_depthfield on Solver (default 10,000)with_max_depth()builder methodSolveResult::Errorinstead of stack overflow2b. Integer overflow protection
checked_add,checked_sub,checked_mul,checked_div,checked_neg2c. Float NaN/Infinity detection
check_float()validates every float operation resultPhase 3: Usability — COMPLETE
3a.
once/1andcall/1once/1— solve goal, take first solution, cut (usestry_solve_once+ choice stack truncation)call/1— execute a term as a goal (basic meta-call)builtins.rs,solver.rs3b. Atom/string predicates
atom_length/2atom_concat/3atom_chars/2builtins.rs(BuiltinResult variants),solver.rs(execution with mutable interner)3c. Additional arithmetic functions
Added to
is/2evaluation:abs/1max/2min/2sign/1builtins.rsPhase 4: Testing — COMPLETE
4a. Integration tests (
tests/integration.rs)4b. Edge case tests
4c. Stdlib tests
Test counts
Phase 5: Nice-to-have — COMPLETE
write/1,writeln/1,nl/0— I/O for debugging rulescompare/3,@</2,@>/2,@=</2,@>=/2— term ordering (ISO standard order)functor/3,arg/3,=../2— term introspection/decompositionbetween/3— integer enumeration (with backtracking, works inside findall)copy_term/2— term copying with fresh variablessucc/2,plus/3— Peano arithmetic (bidirectional)msort/2,sort/2— list sorting (sort removes duplicates)number_chars/2,number_codes/2— number/string conversion (bidirectional)assert/1,retract/1— dynamic predicates (future)Architecture Notes
patch-prologbinary +crates/prolog-corelibrarybuild.rscompilesknowledge/*.plinto binary via bincode[]and!always interned:CompiledDatabase::new()ensures this (required for findall, list ops, once/1)disjunction: boolflag on ChoicePoint to distinguish from clause alternativesparse_paren_body()handles;,->, and,as control flow operatorsCurrent Built-in Predicates (~55 total)
true,fail,false,!,=,\=,is,<,>,=<,>=,=:=,=\=,\+var/1,nonvar/1,atom/1,number/1,integer/1,float/1,compound/1,is_list/1;/2(disjunction),->/2(if-then),,/2(conjunction)once/1,call/1findall/3atom_length/2,atom_concat/3,atom_chars/2+,-,*,/,mod, unary-,abs/1,max/2,min/2,sign/1write/1,writeln/1,nl/0compare/3,@</2,@>/2,@=</2,@>=/2functor/3,arg/3,=../2between/3copy_term/2succ/2,plus/3msort/2,sort/2number_chars/2,number_codes/2Stdlib (knowledge/stdlib.pl)
member/2,append/3,length/2,last/2,reverse/2,nth0/3,nth1/3PR Review: Phase 5 Builtins
Overall the implementation is solid. Several correctness issues and one performance issue need attention.
Bug: negation-as-failure with between/3 gives wrong result when X is bound
File: crates/prolog-core/src/solver.rs, lines 1586-1595 (try_exec_misc)
try_exec_misc for Between only tries low and ignores the rest of the range. try_solve_once (used by + and once/1) dispatches here and never iterates further values.
Concrete failure: + between(1, 5, 3) incorrectly succeeds:
Similarly once(between(2, 5, X)), X = 3 fails when it should succeed.
Fix: try_exec_misc for Between must iterate the full range the same way try_solve_collecting does (lines 1389-1400).
Bug: compare/3, @</2, @>/2 etc. -- shallow walk misses bound variables inside compound args
Files:
Both call subst.walk() (shallow) before passing to term_compare. For a compound like f(X) where X=1, walk(f(X)) returns f(X) unchanged; term_compare then compares raw VarIds instead of bound values.
Concrete failure: X = 1, Y = 2, compare(Order, f(X), f(Y)) -- Expected Order = <; actual result depends on which VarId is numerically larger.
Fix: Use subst.apply() instead of subst.walk() at these call sites.
Bug: succ/2 -- unchecked integer overflow at i64::MAX
File: crates/prolog-core/src/solver.rs, lines 678-679 and 1607
Release mode wraps silently; debug mode panics. Every other arithmetic op in this codebase uses checked_add. Same issue in try_exec_misc at line 1607.
Fix: Use x.checked_add(1).ok_or_else(...) consistent with arithmetic evaluator.
Bug: plus/3 -- unchecked integer arithmetic
File: crates/prolog-core/src/solver.rs, lines 712-729 and 1619-1629
All three modes use raw + / - without overflow checks, unlike is/2 which uses checked_add/checked_sub throughout: Term::Integer(x + y) at line 713, Term::Integer(z - x) at line 719, Term::Integer(z - y) at line 725.
Fix: Apply checked_add/checked_sub and return an error on overflow.
Correctness: if-then-else evaluates condition twice
File: crates/prolog-core/src/solver.rs, lines 231-282
The IfThenElse and IfThen handlers run cond via try_solve_once, discard its bindings with undo_to(mark), then re-insert cond into the goal list to run again in the main loop. Consequences:
Since try_solve_once leaves bindings on success, the fix is to skip undo_to(mark) when the condition succeeds, truncate only the choice stack, and continue with just then (not cond, then).
Correctness: term_compare List vs arity-2 Compound hardcodes Less
File: crates/prolog-core/src/builtins.rs, lines 686-691
When comparing Term::List against a Term::Compound with arity 2, the tiebreak after the arity comparison is hardcoded Ordering::Less. A Term::Compound { functor: ".", args: [H,T] } (structurally identical to Term::List) compares as Less instead of Equal, breaking sort/2 and compare/3. This can arise from =.. reconstruction of list terms.
Performance: goals.remove(0) is O(n) -- quadratic goal processing
File: crates/prolog-core/src/solver.rs, lines 163, 1032, 1245
All three solve loops call .remove(0) on a Vec, shifting every remaining element on each step. For deeply nested conjunctions this is O(n^2) in goal-list length.
Fix: Replace Vec with VecDeque; .remove(0) becomes .pop_front() and .insert(0, x) becomes .push_front(x).
Missing: atom_chars/2 reverse direction (char list to atom)
File: crates/prolog-core/src/solver.rs, lines 359-382
When the first argument is unbound and the second is a ground char list, the implementation errors instead of building the atom. ISO 8.16.4 requires both directions. number_chars/2 already handles the reverse case (lines 805-843).
Summary
PR Review — Phase 5 Builtins
Reviewed:
builtins.rs,solver.rs,tokenizer.rs,parser.rs, integration tests.Bug 1 —
write/1andwriteln/1use shallowwalkinstead of deepapplysolver.rsmain loop (~line 374) andtry_exec_misc(~lines 1570–1578)walkonly follows a top-level variable chain. Iftermresolves to a compound, it is returned unchanged with its argument variables unresolved.term_to_stringthen formats those as_N.Concrete failure:
Fix: replace
self.subst.walk(&term)withself.subst.apply(&term)in both the main-loopWrite/Writelnhandlers and intry_exec_misc. (compare/3and@<already correctly useapply.)Bug 2 —
number_chars/2andnumber_codes/2reverse mode absent fromtry_exec_miscsolver.rstry_exec_misc(~lines 1750–1808)The main solve loop handles reverse mode (unbound number, bound char/code list) correctly. But
try_exec_misc— which handles these predicates when they appear insideonce/1,\+, if-then conditions, orfindallgoals — hits the catch-all_ => Some(false)whennum_argis an unbound variable.Concrete failures:
The reverse-mode parse logic from the main loop needs to also appear (or be extracted and shared) in
try_exec_miscfor bothNumberCharsandNumberCodes.Bug 3 —
term_compareNaN makes sort/msort non-totalbuiltins.rslines 656–660f64::NAN.partial_cmp(x)always returnsNone, sounwrap_or(Ordering::Equal)makes NaN compare equal to every value.sort_byrequires a strict total order; violating this gives undefined sort output in release mode. The same pattern appears in the mixedFloat/Integerarms.Recommend: detect NaN at comparison time and return an evaluation error (ISO:
undefined), or use a deterministic canonical fallback (e.g. NaN sorts last, bit-pattern tiebreak).Non-compliance — ISO standard order for equal-valued float/integer
builtins.rslines 657–660ISO 8.4.2.1 specifies that when a float and an integer have the same arithmetic value, the float is less in standard order. SWI-Prolog:
compare(Order, 1.0, 1)→Order = <.The current value-based
partial_cmpreturnsEqualfor1.0vs1. This affectscompare/3,@</@>,sort/2, andmsort/2.Fix: in the mixed-type arms, after value comparison yields
Equal, tiebreak: returnLesswhen left isFloatand right isInteger,Greaterfor the converse.Minor —
try_exec_miscBetweencannot backtrack inside conjunctionssolver.rs~lines 1677–1688When
x_argis unbound,try_exec_miscbinds it tolowon the first successful unify and returns immediately. This is intentional foronceand NAF callers that hold their own trail mark. However,betweeninside atry_solve_onceconjunction cannot backtrack to try higher values:Inside NAF,
try_solve_oncebinds X=1, then1 > 3fails, so the conjunction fails and NAF succeeds — incorrectly (X=4 and X=5 would satisfy the constraint). The main-loop implementation is correct here via choice points. No test currently covers this case.Positive observations
VecDequemigration eliminates O(n) front-removes on goal lists — correct throughout.succ/2andplus/3usechecked_add/checked_subconsistently — good.arg/3correctly backtracks (not errors) for out-of-range N.copy_term_freshcorrectly walks at each recursion level, handling full variable chains.IfThenElseand NAF across all three solver paths.unify.rs.between/3is correct: creates one choice point atlow+1rather than O(n) choice points.@=<tokenization (peek_at(1)guard after consuming@) is correct.Code Review — PR #2 (Phase 5 builtins)
The VecDeque migration is clean and the if-then/if-then-else fix (dropping the double-evaluation of the condition) is correct. Arithmetic uses checked_add/checked_sub throughout. Several real bugs below.
Bug 1 — functor/3 in try_exec_misc drops Term::List and Term::Var cases
File:
crates/prolog-core/src/solver.rs:1618-1636The main
solve()loop handles bothTerm::List(~line 437) andTerm::Var(construction, ~line 475) correctly.try_exec_miscis called whenfunctor/3appears insideonce/1,\+, orfindall/3. The_ => Some(false)catch-all silently returns failure for both cases:once(functor([a,b], F, A))fails — should bindF = '.', A = 2once(functor(T, foo, 2))fails — should constructfoo(_,_)findall(A, functor([_|_], _, A), As)gives[]instead of[2]Bug 2 — =../2 in try_exec_misc drops Term::List case
File:
crates/prolog-core/src/solver.rs:1657-1697Same asymmetry. The main
solve()loop handles the list case at ~line 593 (decomposing[H|T]to['.', H, T]). The_ => Some(false)catch-all intry_exec_miscsilently fails forTerm::List:once([a,b] =.. L)silently fails — should bindL = ['.', a, [b]]findall(L, ([a] =.. L), Ls)gives[]Both bugs 1 and 2 stem from the same root:
try_exec_miscwas designed as a shared helper but theFunctorandUnivmatch arms were not kept in sync with the mainsolve()match.Bug 3 — atom_chars/2 reverse mode uses byte-length for single-character test
File:
crates/prolog-core/src/solver.rs:376, 1218, ~1462ch.len() == 1tests byte length, not character count. A single-character atom consisting of a multi-byte UTF-8 codepoint (e.g., a 2-byte accented letter) hasch.len() == 2and is silently dropped from the assembled string.atom_chars(X, [AccentedChar])bindsXto the empty atom instead of the correct atom. The same pattern appears in thetry_solve_onceandtry_solve_collectingcopies of this arm.Fix:
ch.chars().count() == 1Bug 4 — functor/3 construction: *arity as u32 silently truncates large arities
File:
crates/prolog-core/src/solver.rs:501The guard
*arity > 0passes for any positivei64. Theas u32cast wraps silently:functor(T, f, 4294967296)— arity wraps to 0, constructsf()with wrong arityfunctor(T, f, 1000000000)— tries to allocate ~1BTerm::Varentries, causing OOMA bounds check before the cast (e.g.,
if *arity < 0 || *arity > MAX_ARITY) would prevent both.Bug 5 — number_codes/2 reverse mode: negative code values wrap via as u32
File:
crates/prolog-core/src/solver.rs:1866(and matching arm intry_exec_misc~line 1862)*code as u32for a negativei64wraps to a large value (e.g.,-1i64 as u32 = 4294967295).char::from_u32(4294967295)returnsNone, so the element is silently dropped rather than producing an error. ISO requirestype_error(character_code, Code)for invalid codes.Minor — BuiltinResult::Between arm in try_exec_misc is dead code
File:
crates/prolog-core/src/solver.rs:1699-1711Both
try_solve_once(line 1236) andtry_solve_collecting(~line 1527) have explicitBuiltinResult::Betweenarms that match before theOk(other)fallthrough. TheBetweenarm insidetry_exec_miscis therefore unreachable. No correctness impact, but the stale code is misleading.Positive observations
pop_front()replacesremove(0)with O(1) semantics.term_comparehandles Float vs Integer cross-comparison (ISO 8.4.2.1: float < integer for same value), NaN ordering, and compound arity-first ordering correctly.succ/2andplus/3usechecked_add/checked_suband raise proper overflow errors in the mainsolve()path.copy_term/2correctly walks through the substitution before copying.PR Review - Phase 5 Builtins
All 203 tests pass, and the VecDeque conversion for goal lists is a clean O(1) win. A few correctness bugs I am confident about:
Bug 1 - between/3: unchecked integer overflow in solve() [solver.rs:665]
The choice-point path does:
low + 1 is an unchecked i64 addition. When low == i64::MAX this panics in debug mode or silently wraps in release. The other two between paths (try_solve_once and try_solve_collecting) use a range loop which avoids that specific panic, but see Bug 4.
Fix: low.checked_add(1) and propagate as a runtime error.
Bug 2 - once/1 inside findall collects all solutions instead of one [solver.rs:1422-1426]
try_solve_collecting enumerates ALL solutions. Pushing inner_goal directly onto the goal list means once(member(X,[a,b,c])) behaves identically to member(X,[a,b,c]) inside a findall, collecting [a,b,c] instead of the correct [a].
The fix is to call try_solve_once(vec![walked]), keep its bindings on success, and then continue collecting:
There is no test for findall(X, once(member(X,[a,b,c])), L).
Bug 3 - var_counter not restored after NAF inner-goal in try_solve_once and try_solve_collecting [solver.rs:1098-1106, 1360-1368]
In solve() the NAF branch saves and restores var_counter (lines 190, 198):
In try_solve_once (line 1098) and try_solve_collecting (line 1360) the restore is missing:
try_solve_once calls rename_clause which increments var_counter. Each + call permanently inflates the counter. While exhausting the VarId space in practice is unlikely, the missing restore is inconsistent with the save/restore invariant used everywhere else in the solver.
Bug 4 - between/3 in try_solve_once / try_solve_collecting: no iteration bound [solver.rs:1251, 1507]
+ between(0, 1_000_000_000, _) or findall(X, between(0, 1_000_000_000, X), _) iterates a billion times with no guard. The main solve() path avoids this because it creates recursive choice points bounded by max_depth, but these helper paths bypass that guard entirely.
A simple mitigation is to check high - low against a reasonable cap before entering the loop.
Minor - sort/2 dedup closure semantics [solver.rs:808-810]
dedup_by(|a, b|) removes a (the later element) and retains b (the earlier one). The comparison is symmetric so this is correct today, but the argument naming convention is easy to confuse with dedup_by_key. Worth a clarifying comment.
No issues found in
PR #2 Review — Phase 5 Built-ins
Reviewed
builtins.rs,solver.rs, andtests/integration.rs. The implementation is well-structured overall. Issues below are ordered by severity. Only confirmed bugs/semantic gaps are listed.Bugs
1. Float formatting in
number_chars/2andnumber_codes/2drops.0solver.rslines 849 and 931:Rust's default float display prints
1.0_f64as"1", not"1.0". ISOnumber_chars(1.0, X)must produce['1','.','0']. As-is,number_chars(1.0, X), number_chars(Y, X)givesY = 1(integer), notY = 1.0. Fix: useformat!("{:e}", f)or checkf.fract() == 0.0and append".0"explicitly. Same bug atsolver.rs:1846and1904in thetry_exec_miscmirror.2.
moduses truncated remainder instead of ISO floored modulobuiltins.rsline 580:ISO defines
modas floored division remainder. Rust%is truncated. For(-7) mod 2, ISO requires1; this returns-1. Fix:((a % b) + b) % b(usingcheckedvariants), or usei64::rem_euclidand adjust sign to match the dividend's sign convention for ISO floor-mod.3.
self.depthis a step counter, not a call-stack depth countersolver.rslines 156–160:depthis incremented every goal-resolution step and never decremented (confirmed: it is only written at line 156). A query likefindall(X, between(1, 10001, X), L)will hit the 10,000-step error without being infinitely recursive. The namedepthand the error message"Maximum recursion depth exceeded"are both misleading — this is really a fuel/step limit. Either rename itstepsand document it as such, or implement a proper call-stack depth counter that decrements on return.Safety
4.
try_solve_once/try_solve_collectinghave no recursion depth limitsolver.rslines 1090 and 1345: neither function reads or updatesself.depth. Both are mutually recursive with themselves and with user-defined clause matching. A left-recursive rule called inside\+orfindallwill recurse into native Rust stack frames without any limit, eventually causing a stack overflow panic. The existingtest_depth_limitunit test only exercises the mainsolveloop.5.
write/1does not flush stdoutsolver.rslines 403–407:print!is line-buffered; output is not flushed until a newline or explicit flush. A sequence likewrite(hello), nlmay appear fine in a terminal but will silently drop output in piped or redirected contexts. Adduse std::io::Write; let _ = std::io::stdout().flush();after theprint!.Prolog Semantics
6.
succ/2raises an error insolvebut silently fails intry_exec_miscsolver.rsline 729 (main path, negative first arg):SolveResult::Error("succ/2: argument must be non-negative").solver.rsline 1785 (try_exec_misc, same case):Some(false)(silent failure).So
succ(-1, X)errors, butonce(succ(-1, X))silently fails. ISO should raisetype_erroruniformly. At minimum the two paths should agree.7.
number_chars/2reverse mode accepts bareTerm::Integer(0..=9)— non-ISOsolver.rslines 882–884:ISO
number_chars/2requires all list elements to be single-character atoms. Accepting bare integer terms0–9is a non-standard extension that silently widens the contract. The testtest_number_chars_reverseat integration.rs line 717 exercises this non-standard path with[4, 5, 6](integers), not['4','5','6'](atoms). This extension also creates a round-trip inconsistency: the forward direction produces atoms, sonumber_chars(456, X), number_chars(Y, X)goes through the atom path, but a hand-constructed list[4,5,6]takes the integer path.8.
=../2silently backtracks instead of raisingtype_errorwhen functor is a non-atom with argssolver.rsaround line 610: when the list inT =.. [42, a, b]has length > 1 and the head is not an atom, the code falls through toreturn self.backtrack(). ISO 8.5.3 requirestype_error(atom, F)in this case.9.
functor/3with negative arity gives wrong error messagesolver.rsline 523: A call likefunctor(T, f, -1)reaches the fall-through atreturn SolveResult::Error("functor/3: insufficient arguments")rather than ISO'stype_error(integer, Arity)(or at least a message that says "arity must be non-negative").Test Coverage Gaps
number_charsornumber_codeswith a float argument (the float formatting bug in issue #1 above would be caught here).test_number_chars_reverse(integration.rs:717) uses[4, 5, 6](integers) — should use['4', '5', '6']to test the ISO-standard path.functor(T, f, -1)(negative arity error).compare(Order, X, Y)whereXandYare distinct unbound variables (unbound variables have a defined ISO standard order based on internal identity).test comment
test
line1
test with solve_fn reference
Bug 1: succ/2 succ_X_0 errors instead of failing. solver.rs lines 745-766. When succ_X_0 is called with X unbound, match arm 4 of shape '(, Term::Integer())' matches and returns SolveResult::Error. ISO semantics say this should FAIL rather than error.
test: try_solve_once returns false on step limit
test: map().collect approach fix
test: checked_add(1) approach
test: solve() and collect_list() and is_proper_list()
test newline
second line
third line
PR Review - Phase 5 Builtins
Reviewed builtins.rs, solver.rs, unify.rs, parser.rs, and tests/integration.rs.
The overall structure is sound: trail-based backtracking is correct, the occurs check is present, cut semantics look right, and arithmetic uses checked ops throughout. Issues below.
Bug 1: succ/2 - succ(X, 0) errors instead of failing
solver.rs lines 745-766
When succ(X, 0) is called with X unbound, the match arms evaluate as follows:
ISO/Edinburgh semantics: succ(X, 0) should FAIL (there is no non-negative predecessor of 0), not produce a runtime error. The equivalent case in try_exec_misc at line 1810 correctly returns Some(false) (failure), so the two handlers are inconsistent.
Bug 2: number_chars/2 and number_codes/2 silently drop non-conforming list elements
solver.rs lines 891-913 (main solve), 966-990 (codes), 1887-1913 (try_exec_misc)
In the reverse direction (list to number), filter_map silently drops any element that is not a single-character atom for number_chars, or not a valid Unicode codepoint integer for number_codes.
Concrete consequence: number_chars(X, ['1', bad_atom, '2']) succeeds with X = 12 instead of failing. Similarly number_codes(X, [49, foo, 50]) gives X = 12 instead of failing because foo is not an integer and gets silently skipped.
Fix: replace filter_map with map().collect() returning Option so that any non-conforming element causes the predicate to fail. This bug affects all three execution paths: the main solve loop, try_solve_once (used for negation-as-failure and if-then conditions), and try_exec_misc (used inside findall).
Bug 3: negation-as-failure silently succeeds when inner goal hits step limit
solver.rs lines 1114-1117
The main solve loop correctly returns SolveResult::Error on step-limit at lines 168-173. However try_solve_once returns false, making an aborted goal (step limit exceeded) indistinguishable from a genuinely failing goal. Since try_solve_once evaluates the inner goal of negation-as-failure, this means negation of an expensive true goal can produce a wrong answer when the proof tree is cut short by the step counter.
Safety: is_proper_list and term_compare use recursive list traversal
builtins.rs lines 808-813
is_proper_list recurses once per list element. A list of roughly 8000 elements can stack-overflow on typical systems. Unlike collect_list which is already iterative, is_proper_list needs to be rewritten as an iterative loop.
builtins.rs lines 724-726 show the same pattern inside term_compare for list-vs-list comparison. sort/2 and msort/2 call term_compare, so sorting a list whose elements are themselves long lists triggers recursion proportional to inner list lengths.
Missing test coverage
Minor notes (not blocking)
Generated with Claude Code
Phase 5 Code Review
Reviewed the Phase 5 built-in predicate additions. Four issues found, ranging from a crash-level bug to semantic correctness issues.
1. PANIC:
arith_modcrashes oni64::MINdivisorFile:
crates/prolog-core/src/builtins.rslines 585–587i64::MIN.abs()overflowsi64and panics in debug builds (wraps toi64::MINin release, corrupting the result). Any query likeX is 5 mod -9223372036854775808will crash the process in debug mode.The zero-divisor guard on line 581 only catches
b = 0, notb = i64::MIN. Fix: add a case(ArithVal::Int(_), ArithVal::Int(i64::MIN)) => Err(...)before the general integer arm, or replace both.abs()calls with.checked_abs().unwrap_or(...).2.
atom_chars/2reverse mode silently corrupts outputFile:
crates/prolog-core/src/solver.rslines 383–396 (also duplicated intry_solve_once~line 1263 andtry_solve_collecting~line 1397)Non-single-character atoms and non-atoms in the list are silently discarded rather than causing failure.
atom_chars(X, [a, bc, d])(wherebcis a two-character atom) succeeds withX = adinstead of failing or throwing a type error. ISO 8.16.7 requirestype_error(character, bc). Thefilter_mapshould be replaced with a plainmapthat short-circuits on any invalid element.This bug is present in all three copies of the reverse-direction code: the main
solvehandler (~line 380),try_solve_once(~line 1260), andtry_solve_collecting.3.
succ/2overflow error silently becomes failure insidefindall/\+File:
crates/prolog-core/src/solver.rs—solveloop lines 739–743 vstry_exec_misclines 1816–1819In the main
solveloop,succ(9223372036854775807, X)returnsSolveResult::Error("succ/2: integer overflow"). Intry_exec_misc(used byfindalland negation-as-failure contexts), the same case returnsSome(false):So
findall(X, succ(9223372036854775807, X), Xs)silently givesXs = []instead of propagating an error. The same asymmetry applies toplus/3overflow intry_exec_misc(~lines 1831–1843).4.
format_floatproduces non-round-trippable strings for NaN and InfinityFile:
crates/prolog-core/src/solver.rslines 13–20format!("{}", f64::NAN)produces"NaN"andformat!("{}", f64::INFINITY)produces"inf". Neither contains'.'or'e', so the function appends.0, yielding"NaN.0"and"inf.0". Rust'sf64parser does not accept"NaN.0"or"inf.0", sonumber_chars(X, Chars)followed bynumber_chars(N, Chars)will silently fail to round-trip for these special values. Add explicit guards before the suffix logic.Positive observations
VecDequemigration correctly eliminates the O(n)remove(0)/insert(0)costs from the oldVec-based approach.IfThenElse/IfThenfix (keeping cond's bindings instead of undoing and re-running) is semantically correct and avoids double-execution of cond side-effects.arith_modISO-sign semantics (result sign matches divisor) are correctly implemented for all non-i64::MINinputs.copy_term_freshcorrectly deep-walks the substitution at each level via the per-nodeself.subst.walk()insidecopy_term_impl.between/3choice-point chaining (bumping low+1 in the alternative goal) is the right approach for backtracking across solutions in the main solve loop.term_comparecorrectly handles the list-as-./2representation for cross-type comparisons.Phase 5 Code Review
Reviewed:
builtins.rs,solver.rs,tokenizer.rs,parser.rs,tests/integration.rs.Overall the phase is solid — the
arith_modfloored-division fix,VecDequegoal list, and the if-then-else bindings rewrite are all correct. Several real bugs follow.Bug 1 —
between/3silently fails for ranges larger thanmax_depthin negation and findall contextsFiles:
crates/prolog-core/src/solver.rs:1299-1301(try_solve_once) andsolver.rs:1569-1571(try_solve_collecting)When
range_size > max_depththe code returnsfalseas ifbetweenhas no solutions. This is wrong in two ways:Negation-as-failure:
\+ between(1, 20001, 1)callstry_solve_oncefor the inner goal. The range check fires (20001 > 10000), returnsfalse, so\+succeeds — butbetween(1, 20001, 1)is provable, so the negation should fail.findall:
findall(X, between(1, 20001, X), L)callstry_solve_collecting. Same early return givesL = []instead of[1, 2, ..., 20001].The existing test suite only exercises
betweenwith ranges of 5-10 elements (test_between_with_findall,test_between_conjunction_in_negation), so the defaultmax_depth = 10_000hides this. The fix is to drop the range guard and rely on the step counter, or special-case the already-boundXscenario (low <= X <= highis O(1) and needs no iteration).Bug 2 —
copy_term_implis unbounded recursion; will stack-overflow on deep termsFile:
crates/prolog-core/src/solver.rs:2004-2028A list with N elements is represented as N nested
List { head, tail }nodes.copy_term_implrecurses once per node via theTerm::Listarm (tail is a recursive call). A 5000-element list uses ~5000 stack frames. On the default 8 MB Rust thread stack this overflows around 50 000-100 000 elements, but even a few thousand can be reached in normal Prolog programs (msortorsortresults fed intocopy_term). There is no depth limit. The list-tail traversal should use an iterative loop, consistent with the iterative approach already used inis_proper_listandterm_compare's list path.Bug 3 —
term_comparerecurses into compound arguments without depth protectionFile:
crates/prolog-core/src/builtins.rs:719-726The list-vs-list path is correctly made iterative (lines 728-754), but in the
(Compound, Compound)arm the per-argument comparison at line 720 (term_compare(x, y, interner)) is still recursive. Forf(f(f(...)))nested N levels deep this is O(N) Rust stack frames.sort/2,msort/2, andcompare/3all callterm_compare, so a user can trigger this withsort([f(f(f(...))), ...], X). Consider an explicit stack or depth counter, consistent with the iterative approach already used for the list case.Bug 4 —
arg/3type check is inconsistent betweensolveandtry_exec_miscFiles:
solver.rs:561-566(main loop) vs.solver.rs:~1790-1810(try_exec_misc)In the main
solveloop,arg(1, atom, X)when the second argument is neither Compound nor List falls through toreturn SolveResult::Error("arg/3: second argument must be compound"). Intry_exec_misc(reached fromtry_solve_onceandtry_solve_collecting, i.e. inside\+andfindall), there is no explicit error arm so it falls through toSome(false)— a silent failure.ISO 8.5.2 requires
type_error(compound, atom)in all contexts. As-is,\+ arg(1, atom, X)succeeds (failure inverts to success) but directarg(1, atom, X)errors. Thetry_exec_miscArgbranch should propagate an error for the non-compound, non-list case.Verified correct (no action needed)
arith_modISO floored semantics: all four sign combinations produce correct results. Thei64::MINdivisor guard is correct.term_compareFloat/Integer mixed ordering matches ISO 8.4.2.1 (float < integer at equal arithmetic value).@=</@>=tokenizer:peek_at(1)correctly addresses one position past the current cursor; all four@operators tokenize correctly.collect_listalways called aftersubst.apply(); no unresolved-variable escape.try_solve_oncemodifiesself.substin place; bindings from the condition are correctly retained on success withoutundo_to. The previous double-execution ofcondis correctly eliminated.between/3overflow guard in the mainsolveloop:checked_add(1)on line 692 is used; the choice-point-based implementation is correct.sort/2dedup:sort_by+dedup_bywithterm_compare == Equalcorrectly removes duplicates by ISO standard order.copy_termvariable aliasing (f(X,X)-> freshf(A,A)): thevar_mapcorrectly shares one fresh id per original variable id, confirmed bytest_copy_term_aliasing.Code Review Phase 5 Builtins
Issue 1 Occurs check enabled by default in =/2 ISO deviation [Medium]
crates/prolog-core/src/unify.rs lines 97-103
The standard unify method runs a full occurs check on every variable binding. ISO and Edinburgh Prolog both specify that plain =/2 does NOT perform an occurs check - that is reserved for unify_with_occurs_check/2. Enabling it by default means X = f(X) fails where standard Prolog succeeds, breaking difference-list idioms and any program that intentionally unifies a variable with a term containing it. The occurs check also adds O(n) overhead to every variable binding.
Issue 2 succ/2 and plus/3 behave differently inside negation/once/findall [Medium]
crates/prolog-core/src/solver.rs lines 771-775 vs 1843-1844
crates/prolog-core/src/solver.rs lines 822-825 vs 1864
In the main solve loop, calling succ(X, Y) or plus(X, Y, Z) with all arguments unbound hits the wildcard arm and returns SolveResult::Error. But in try_exec_misc (used by +, once, findall, and ->) the equivalent arm is Some(false) - a silent failure. The error is swallowed.
Consequence: + succ(X, Y) incorrectly succeeds because the inner instantiation error is treated as inner-goal failure, so negation-as-failure flips it. The same query at top level produces an error. This violates transparent + semantics.
Issue 3 try_exec_misc catch-all silently suppresses unhandled builtins [Medium]
crates/prolog-core/src/solver.rs line 2006, lines 1325-1334, lines 1601-1609
try_exec_misc ends with _ => None, and every call site treats None as failure. Any BuiltinResult variant that exists in exec_builtin but is not handled in try_exec_misc will silently fail (rather than execute) inside +, once, findall, and ->. Adding a new builtin to exec_builtin and forgetting try_exec_misc produces silent wrong answers with no compile-time warning.
Issue 4 copy_term_fresh variable counter not guaranteed disjoint from query variables [Low]
crates/prolog-core/src/solver.rs lines 87, 101
The solver var_counter is initialised to 1000. The query parser assigns variable IDs starting from 0. The separation relies entirely on the assumption that no single query has >= 1000 distinct variables. This is not enforced: there is no assertion or mechanism to initialise var_counter to max(query_max_var_id) + 1. A pathological query or a large generated term could cause a fresh copy-term variable to alias a live query variable.
Issue 5 copy_term_impl iterative list traversal falls back to recursion for variable-threaded lists [Low]
crates/prolog-core/src/solver.rs lines 2040-2063
The iterative traversal for Term::List only advances the loop cursor to the un-walked tail (current = tail at line 2063). On the next iteration, if tail is Term::Var(id) bound to another Term::List, the match at line 2040 sees Term::Var(id) not Term::List, and falls into the wildcard arm, calling copy_term_impl recursively. The iterative path is only taken for immediately-concrete list cells; any variable-indirected spine reverts to deep recursion. A list of 10000 elements threaded through variables could stack-overflow.
Issue 6 number_chars/2 silently fails on non-character list elements instead of type_error [Low]
crates/prolog-core/src/solver.rs lines 900-926
When the char list contains non-atom elements (e.g. number_chars(X, [1, 2, 3]) with unquoted integers), the wildcard None arm at line 912 causes the string accumulation to return None, and execution falls through to self.backtrack() - a silent failure. ISO requires type_error(character, 1). The existing test at integration.rs lines 1098-1103 covers bad_atom but not integer elements.
Issue 7 number_chars(123, X) test uses ambiguous expected value [Low]
tests/integration.rs lines 711-712
term_to_string renders Term::Atom without quotes, so the char-atom '1' and the integer Term::Integer(1) produce the same display string. The test passes even if the implementation returns integers instead of character atoms. A quoting-aware renderer or direct Term inspection would make the test meaningful.
Summary
Issue 1: unify.rs:97-103 - Occurs check on every unification, ISO =/2 must not occurs-check - Severity: Medium
Issue 2: solver.rs:771-775 vs 1843-1844 and 822-825 vs 1864 - succ/2 and plus/3 errors swallowed as failure inside +/once/findall - Severity: Medium
Issue 3: solver.rs:2006, 1325-1334, 1601-1609 - try_exec_misc catch-all silently fails any builtin not present in that function - Severity: Medium
Issue 4: solver.rs:87,101 - copy_term_fresh counter relies on magic constant 1000 being greater than max query vars - Severity: Low
Issue 5: solver.rs:2040-2063 - copy_term_impl iterative list traversal degrades to recursion on var-threaded spines - Severity: Low
Issue 6: solver.rs:900-926 - number_chars/2 silently fails on integer-typed list elements instead of type_error - Severity: Low
Issue 7: integration.rs:711-712 - number_chars test expected value is ambiguous (atom vs integer look identical) - Severity: Low
Arithmetic overflow guards (checked_*) and float NaN/Infinity detection (check_float) are correct. between/3 backtracking, arg/3 1-based indexing, =../2 on atomic terms, and compare/3 substitution application are all implemented correctly.
PR #2 Code Review — Prolog Engine Phase 5
Reviewed: correctness, Prolog semantics, arithmetic safety, backtracking, term handling, performance, and test coverage. All findings cite specific file paths and line numbers.
🔴 High Severity
1. Cut (
!) is silently ignored intry_solve_once— wrong results for\+,once, findall conditionscrates/prolog-core/src/solver.rs:1172When
!fires insidetry_solve_once(used for\+,once/1, findall's goal, if-then conditions), it is treated as a no-op — execution just falls through to the next goal. Cut should succeed as a goal AND prevent any alternative clauses from being tried for earlier goals in the conjunction. Withcontinue, code like\+((member(X,[a,b,c]), !, fail))iterates all three members instead of cutting after the first, producing wrong true/false for\+. Same issue attry_solve_collectingline ~1446.Fix: treat
Cutas an immediate success and break the goal loop (returntrueintry_solve_once).2. Disjunction left branch is not walked before being stored —
(X ; b)fails whenXis boundcrates/prolog-core/src/builtins.rs:285,300leftis the walked version ofargs[0], but when the if-then check fails, the code returns the original un-walkedargs[0]. Ifargs[0]is a variable bound to a goal term, the disjunction branch receives the raw variable, which the solver cannot resolve as a goal, causing it to fail instead of calling the bound goal.Fix:
Ok(BuiltinResult::Disjunction(left, subst.walk(&args[1])))3.
between/3with unboundXintry_solve_oncehas no step-limit protectioncrates/prolog-core/src/solver.rs:1340–1351The step counter (line 1160) is incremented once before entering
between, but the inner loop iterates up tohigh - low + 1times with no guard.\+ between(1, 1_000_000_000, X)hangs indefinitely, bypassing themax_depthprotection entirely.Fix: add an iteration counter inside the loop and check against
self.max_depth, or propagate the range as a resumable state (WAM-style).4.
parse_list_tailandparse_paren_comma_listare unboundedly recursive — stack overflow on large inputscrates/prolog-core/src/parser.rs:406–436and368–383parse_list_tailcalls itself recursively for each list element (line 411).parse_paren_comma_listcalls itself for each conjunction element (line 374). A list or conjunction with ~10,000 elements will overflow the Rust call stack and panic rather than returning a parse error.Fix: convert both to iterative loops (collect elements into a
Vec, then build theTerm::List/Compoundspine in reverse).5.
term_comparerecurses into compound arguments — stack overflow on deeply nested termscrates/prolog-core/src/builtins.rs:718–726The list comparison is iterative (line 729), but compound term argument comparison calls
term_comparerecursively (line 720) with no depth limit. A term likef(f(f(...)))with sufficient nesting will overflow the stack when used withsort/2,msort/2,compare/3, or any@</@>comparison.🟡 Medium Severity
6. Errors from
succ/2,plus/3, andfunctor/3intry_exec_miscare silently converted to failurecrates/prolog-core/src/solver.rs:1870, 1885, 1889, 1893In the main
solveloop,succ/2overflow returnsSolveResult::Error(...). Intry_exec_misc(used by\+,once,findall):once(succ(9223372036854775807, X))silently fails instead of throwing an arithmetic error. Same pattern forplus/3(lines 1885, 1889, 1893) andfunctor/3with negative arity (line ~1788). Programs relying on error signals from these predicates get wrong behavior insideonce/1or\+.7. Float NaN unification uses IEEE
==— two NaN floats cannot unify with themselvescrates/prolog-core/src/unify.rs:127In Rust (IEEE 754),
f64::NAN == f64::NANisfalse. If NaN ever appears as aTerm::Floatvalue (e.g. loaded from a database, or ifcheck_floatguard is relaxed),X = Xwould fail forX = nan. ISO Prolog requires structural/syntactic equality for unification, not arithmetic equality.Fix:
a.to_bits() == b.to_bits()8.
Float / Int(0)reports "Infinity result" instead of "Division by zero"crates/prolog-core/src/builtins.rs:575When
b == 0, this arm falls through without the zero-divisor guard at line 572 (which only coversFloat / Float(0.0)).check_floatthen returnsErr("Arithmetic error: Infinity result")— a misleading message for what is clearly a division-by-zero.Fix: add
(ArithVal::Float(_), ArithVal::Int(0)) => Err("Division by zero".to_string()),before the general float/int arm.9. Error state not preserved across
next()callscrates/prolog-core/src/solver.rs:148–156After
solve()returnsSolveResult::Error,solutions_foundis still0and the initial choice point has been consumed. The next call tonext()falls intoself.backtrack(). If the error occurred after partial substitution bindings were applied,backtrack()may find surviving choice points and continue producing solutions from an inconsistent solver state — silently swallowing the error. At minimum, the first error should be latched so subsequentnext()calls always returnFailureor re-surface the error.10.
atom_chars/2rejects integer and float arguments (ISO violation)crates/prolog-core/src/solver.rs:381–398ISO Prolog 8.16.2 specifies that
atom_chars/2must accept numbers:atom_chars(42, X)→X = ['4','2']. The current implementation throws an error for any non-atom/non-var first argument. The same gap applies toatom_length/2andatom_concat/3.11. Quadratic cost from cloning the remaining goal list in
try_solve_oncecrates/prolog-core/src/solver.rs:1344This is inside the
between/3enumeration loop and also at line 1381 intry_clauses(new_goals.extend(rest_goals.iter().cloned())). Each resolution step clones the entire remaining goal list (O(n)), making deeply nested goals O(n²) overall. For programs with large conjunctions or heavybetweenusage this is a significant performance problem.🟠 Missing ISO Predicate
12.
unify_with_occurs_check/2is never exposed as a builtincrates/prolog-core/src/unify.rs:162–179occurs_inis implemented and tagged#[allow(dead_code)], butunify_with_occurs_check/2is not registered inis_builtinorexec_builtin. Any Prolog program calling it gets an unexpected failure (undefined predicate). ISO 8.2.2 requires this predicate.13.
call/Nfor N > 1 is not supportedcrates/prolog-core/src/builtins.rs:310Only
call/1is dispatched.call/2..N(appending extra arguments to a closure) is the foundation ofmaplist/2,maplist/3,foldl/4, and all higher-order Prolog idioms. Without it, any library predicate using these patterns will fail with an existence error or incorrect silent failure.🔵 Test Coverage Gaps
\+with a cut inside: no test for\+((member(X,[a,b,c]), !, fail))— directly exercises bug #1.X = foo, (X ; bar)— exercises bug #2.sort/2/msort/2with compound terms: all existing tests use atoms/integers; no test exercises the compound branch ofterm_compare(which has the unbounded-recursion risk, bug #5).succ/2overflow insideonce/1:once(succ(9223372036854775807, X))— exercises bug #6, should produce an error not silent failure.number_chars/2andnumber_codes/2insidefindall: exercises thetry_exec_misccode path, which has the error-suppression pattern from bug #6.atom_chars(42, X): exercises the ISO numeric-atom_chars path missing in bug #10.arg(1, [a,b], X)andarg(2, [a,b], X): theTerm::Listbranch ofarg/3in the solver has no integration test.Review posted - see below
PR Review: Phase 5 Builtins
All 203 tests pass. The new builtins are well-structured. The arith_mod ISO semantics fix and the Float/Int(0) division-by-zero guard are correct. Pre-interning [] and ! in CompiledDatabase::new safely guards the lookup calls. Trail-based backtracking is correctly wired for all new builtins. No panics on malformed input found.
Three issues worth fixing before merge.
Issue 1: between/3 iteration bypasses max_depth step limit
solver.rs:1344-1356 (try_solve_once) and solver.rs:1633-1644 (try_solve_collecting)
The range iteration loop increments self.steps exactly once before entering (at the outer try_solve_once / try_solve_collecting entry), not once per iteration. The step-limit guard has no effect on range width.
Example: between(1, 1000000000, X) inside negation-as-failure or findall iterates 10^9 times unimpeded:
The solve() loop is safe -- each alternative is a new choice point that re-enters solve() and counts one step. The looping versions in try_solve_once and try_solve_collecting need per-iteration protection.
Minimal fix: add self.steps += 1; if self.steps > self.max_depth { return false; } at the top of each for-loop body at solver.rs:1345 and solver.rs:1633.
Issue 2: =../2 construct mode with unbound 1-element list silently unifies instead of erroring
solver.rs:647-651 (solve()) and solver.rs:1865-1868 (try_exec_misc)
T =.. [F] where F is an unbound variable: collect_list yields [Term::Var(f_id)]. The Term::Atom arm does not match, but elems.len() == 1 is true so the code calls self.subst.unify on T and the unbound variable -- T stays uninstantiated. ISO 8.5.3.3 requires instantiation_error here. The silent success can cause confusing downstream backtracking.
Fix: before the elems.len() == 1 arm, check for an unbound functor and return SolveResult::Error instead.
Issue 3: number_chars/number_codes reverse mode silently backtracks on non-numeric strings
solver.rs:944-945, solver.rs:1029-1031, and their try_exec_misc mirrors
number_chars(X, [a,b,c]) collects chars into a String, tries parse as i64 then f64. When both fail it falls through to return self.backtrack() -- silent failure. ISO 8.16.7 requires syntax_error(not_a_number). As a consequence, negation-as-failure over these predicates gives a misleadingly clean success.
Fix: replace the silent return self.backtrack() after the second failed parse with return SolveResult::Error(...). Same in try_exec_misc.
Minor (not blocking):
Phase 5 Code Review - see inline comments below. Issues found: (1) cut in findall has no effect on clause iteration solver.rs:1479-1481+1683-1701, (2) exec_findall shares self.steps causing silent partial results solver.rs:1427-1451, (3) is_list fails for bound variable tails builtins.rs:274-281+828-836, (4) cut_in_try_solve not reset after try_solve_once calls from solve solver.rs:220-241+272-303+323-336, (5) number_chars/number_codes can bind NaN/Inf solver.rs:941-950+1031-1040, (6) between clones goal list O(RK) solver.rs:1352-1366+1643-1658, (7) try_solve_collecting unbounded recursion on goal depth solver.rs:1453-1703. Verified correct: =/2 no occurs check (ISO), all checked_ arithmetic, arith_mod sign semantics, check_float on results, arith_div zero guards, trail backtracking, rename_clause freshness, copy_term iterative list spine, functor arity bounds.
Phase 5 Detailed Review (6 bugs + 2 perf/safety): BUG 1 HIGH cut in findall has no effect on clause iteration solver.rs:1479-1481 and 1683-1701. try_solve_collecting handles BuiltinResult::Cut by continuing goals but the user-predicate loop iterates ALL candidates. findall(X, (p(X), !), Xs) with p(1) p(2) p(3) returns [1,2,3] instead of [1]. try_solve_once correctly stops at cut_in_try_solve line 1410 but try_solve_collecting has no equivalent guard. BUG 2 HIGH exec_findall shares self.steps causing silent truncation solver.rs:1427-1451. exec_findall never saves or restores self.steps. When try_solve_collecting hits the step limit it returns false with partial results and exec_findall returns that partial list as Ok() with no error. findall(X, between(1, 20000, X), Xs) silently returns a short list violating ISO 8.10.1. Fix: save self.steps before and restore after, propagate as SolveResult::Error on truncation. BUG 3 HIGH is_list/1 fails for lists with bound variable tails builtins.rs:274-281 and 828-836. is_list/1 uses subst.walk (shallow) then calls is_proper_list with no substitution access. A list [1,2|T] where T is unified to [] returns false because is_proper_list sees Var(id) not []. msort and sort correctly use self.subst.apply before collect_list. Fix is_list/1 to use apply instead of walk. BUG 4 HIGH cut_in_try_solve not reset after try_solve_once called from solve, lines 220-241, 272-303, 323-336. All four call sites in solve (NAF, IfThenElse, IfThen, Once) do not reset self.cut_in_try_solve. BuiltinResult::Cut arm at line 1187 sets it without save/restore. A subsequent try_solve_once call sees saved_cut=true (dirty); if new inner goal does not fire cut, cut_in_try_solve is restored to true, causing next predicate to stop clause iteration prematurely. Fix: self.cut_in_try_solve = false before each call in solve. BUG 5 MEDIUM number_chars/2 and number_codes/2 reverse path binds NaN/Inf solver.rs:941-950 and 1031-1040. Rust str::parse succeeds for NaN inf -inf so number_chars(N, ['N','a','N']) succeeds binding N to NaN float. check_float only guards arithmetic results not inputs. NaN in comparisons silently returns false instead of evaluation_error(undefined). Fix: after parse succeeds reject if f.is_nan() or f.is_infinite(). PERF 6 MEDIUM between/3 in try_solve_once and try_solve_collecting clones goal list each iteration solver.rs:1352 1366 1643 1658. goal_list.iter().cloned().collect() is O(K) per iteration giving O(RK) total. solve avoids this with a lazy between(low+1, high, X) choice point. SAFETY 7 MEDIUM try_solve_collecting unbounded recursion on goal depth solver.rs:1453-1703. Each findall goal adds one Rust stack frame. 10000-step guard counts steps not frames so deep conjunctions inside findall can overflow the stack. Conjunction and Success arms are tail calls that could be flattened. VERIFIED CORRECT: =/2 no occurs check (ISO 8.3.2), all checked_ integer arithmetic, arith_mod sign semantics, check_float on every float result, arith_div zero guards, trail backtracking, rename_clause freshness, copy_term iterative list spine, functor/3 arity bounds.
Phase 5 Built-ins: Review
The overall implementation is solid — backtracking semantics for
between/3, checked arithmetic, and theapplyfix foris_listare all correct. Found several issues worth addressing:1.
functor/3negative arity: inconsistent error vs. silent failuresolver.rs:543-546(mainsolveloop) vs.solver.rs:1867(try_exec_misc)In the main
solveloop,functor(X, foo, -1)returnsSolveResult::Error("functor/3: arity must be non-negative"). Intry_exec_misc(used bytry_solve_onceandtry_solve_collecting), the negative-arity case falls through to_ => Some(false)— silent failure.The guard at
solver.rs:1851only handlesarity > 0 && arity <= 1024; anything outside that range falls to the final_ => Some(false)arm.Effect:
\+ functor(X, foo, -1)incorrectly succeeds (failure inside\+= success) instead of propagating an error.findall(X, functor(X, foo, -1), Xs)givesXs = []instead of an error.2.
between/3intry_solve_onceclones goal continuation on every iterationsolver.rs:1385(and matching pattern intry_solve_collecting~line 1690)Inside the iteration loop,
goal_list.iter().cloned().collect()allocates and clones the entire remaining goal list on every iteration, giving O(range_size x |remaining goals|) allocations. Forbetween(1, 10000, X)with a non-trivial continuation this is measurably expensive. Building the clone once before the loop would fix it.3.
apply_implcycle detection usesVec::contains— O(n^2)unify.rs:78seenis aVec<VarId>using linear search. For a variable chain of depth n (possible afterX = f(X)without occurs check),applybecomes O(n^2). AFnvHashSet<VarId>reduces this to O(n). In practice this only matters for cyclic terms, butapplyruns on every solution extraction and everycopy_terminvocation.4.
term_comparefinal match arm should beunreachable!(), notOrdering::Equalbuiltins.rs, last arm of theterm_comparematchThis arm is dead code today — the preceding arms are exhaustive for all current
Termvariants. If a newTermvariant is added without updatingterm_compare, this silently returnsEqualfor any comparison involving the new variant, corrupting sort order andcompare/3results with no diagnostic. Should beunreachable!("term_compare: unhandled Term variant").5. Missing test:
arith_mod(i64::MIN, -1)builtins.rstest moduleThe new
test_mod_i64_min_divisorcovers divisor =i64::MIN. There is no test for dividend =i64::MINwith an odd negative divisor, which exercisesrem_euclidoni64::MINand ther == 0branch. The implementation returns0(correct), but a regression test would lock this in:Summary
functor/3negative arity: error insolve, silent failure intry_exec_misc(solver.rs:1867)between/3clones goal continuation O(range x goals) per iteration (solver.rs:1385, ~1690)apply_implO(n^2) cycle detection viaVec::contains(unify.rs:78)term_comparewildcard arm should beunreachable!()(builtins.rs)arith_mod(i64::MIN, -1)not coveredCode Review - Phase 5 (PR #2)
Reviewed: solver.rs, builtins.rs, unify.rs, parser.rs, tokenizer.rs, integration.rs.
Bug 1 - Step-limit inside try_solve_once silently converts timeout to failure
File: crates/prolog-core/src/solver.rs, lines 1194-1197
try_solve_oncereturnsbool. When the step counter is exceeded it returnsfalse. The dangerous case is negation-as-failure: both the negation handler insolve(line 220) and intry_solve_collecting(line 1519) calltry_solve_onceand interpretfalseas "inner goal failed", so\+(expensive_goal)will incorrectly succeed when the goal hits the step limit instead of returning an error.A minimal fix is a shared
steps_exceeded: boolflag onSolverthattry_solve_oncesets, with all callers checking it immediately after to bubble the error up.Bug 2 - succ/2 raises an error in the main loop but silently fails inside once/findall
File: crates/prolog-core/src/solver.rs, lines 791-800 vs. lines 1950-1958
In the main
solveloop,succ(-1, S)returnsSolveResult::Error("succ/2: argument must be non-negative"). But whensucc/2runs insideonce/1orfindall/3, the dispatch goes throughtry_exec_misc, which returnsSome(false)for all unrecognized cases. Soonce(succ(-1, _))silently fails; the identical goal at the top level produces a runtime error.The same inconsistency exists for
plus/3overflow and error arms (main loop lines 821-825 vs.try_exec_misclines 1969-1973).Bug 3 - between/3 in the main solve loop builds O(N) choice points when X is pre-bound
File: crates/prolog-core/src/solver.rs, lines 712-750
When X is already bound to an integer inside the range, the code still pushes one choice point per value from
lowup to X before the unification succeeds. Forbetween(1, 1_000_000, 3)it pushes choice points for low=1 (fails), low=2 (fails), low=3 (succeeds), and then on backtrack pushes many more until the step limit fires.try_solve_oncealready has an O(1) fast path for this case (lines 1368-1374): it walksx_argfirst, checks if it is a bound integer, and either returns immediately or falls through to the enumeration loop. The main solve loop should mirror this before pushing any choice point.Bug 4 - try_solve_collecting is directly recursive; Rust stack can overflow before the step counter fires
File: crates/prolog-core/src/solver.rs, lines 1715-1743
For user-defined predicates inside
findall,try_solve_collectingcalls itself recursively on each clause body. The step counter increments once per goal but each Rust stack frame is far larger than one tick. A deeply recursive program insidefindallcan exhaust the native stack beforemax_depthis reached, causing an uncontrolled process abort instead of a cleanSolveResult::Error.try_solve_oncehas the same structural issue (lines 1420-1428).Options: add a separate Rust-frame depth counter checked at every recursive entry, or convert the recursion to an explicit Vec-based worklist.
Missing test coverage
between/3with pre-bound X in a top-level query (covers Bug 3):solve_all("", "between(1,10,5)")should give one solution;between(1,10,11)should fail. Currently only the unbound-X case is tested.succ/2with a negative argument insideonce/1(covers Bug 2):solve_expect_error("", "once(succ(-1, _))")should raise an error, not fail silently.\+(infinite_recursion_predicate)returns an error rather than succeeding.=../2decomposition of a list with a non-nil tail:T = [a|b], T =.. Lshould giveL = ['.', a, b].number_chars/2round-trip for floats:number_chars(3.14, Cs), number_chars(X, Cs)should reconstruct3.14.Phase 5 PR Review
All 203 tests pass and the new predicates work correctly for the common cases. The issues below are the ones I'm confident about.
1. Overflow errors silently become failures inside
findall/\+/once— semantic bugsolver.rs:2009–2035(try_exec_misc)In the main
solveloop,succ/2andplus/3overflow correctly propagate asSolveResult::Error. Insidetry_exec_misc(the shared handler fortry_solve_onceandtry_solve_collecting), the same overflow cases returnSome(false)— a failure — instead of surfacing the error.Consequence:
findall(X, succ(9223372036854775806, X), Xs)givesXs = []instead of an error. Same for\+ succ(MaxInt, _)— it succeeds when it should error. This breaks the ISO requirement that arithmetic exceptions propagate regardless of context.The same inconsistency applies to
plus/3overflow (lines 2024–2035). Consider adding a helper that returnsResult<Option<bool>, String>so errors can be propagated, or surfacing them viaself.steps_exceeded-style flag.2.
findallresets the step counter, creating an effective bypass ofmax_depthsolver.rs:1502–1514After
exec_findallreturns,self.stepsis restored to its pre-findall value. A program can usefindallto run an extramax_depthsteps per call, effectively multiplying the real work by however many nested findalls exist. Two nested findalls of depth 10,000 each give 30,000 total steps against amax_depthof 10,000. This lets adversarial or buggy programs run much longer than intended.Consider accumulating (not resetting) the step count, or subtracting the used steps from the outer budget.
3.
try_solve_collectingis fully stack-recursive — stack-overflow risk near step limitsolver.rs:1537–1803try_solve_collectingcalls itself recursively for every goal step (e.g. line 1561:return self.try_solve_collecting(goal_list, template, results)). Withmax_depth = 10_000, a deeply chained set of goals can push ~10,000 Rust call frames before the step limit fires. For a program like:each clause resolution adds frames. The default Rust stack is 8 MB; 10,000 frames with non-trivial locals can overflow. Either convert to an iterative approach (loop + explicit stack) or lower the default
max_depthused insidetry_solve_collecting.4.
between/3in the main solver clones the full remaining goal list per backtrack — quadratic memorysolver.rs:782–784For
between(1, N, X)with M remaining goals, each of the N backtracks clones the entire M-element goal list, giving O(N × M) allocations. Forbetween(1, 1000, X)with a moderate goal tail, this is noticeable. The disjunction choice point has the same pattern (line 261–262), butbetweenis the only builtin that generates O(range-size) choice points at runtime.One option: store the high-bound and current value directly in the
ChoicePointstruct (aBetweenStatevariant) instead of re-encoding as a newbetween(Low+1, High, X)goal.5. Error vs. failure inconsistency for
=../2with empty list intry_exec_miscsolver.rs:672–674(main loop) vs.solver.rs:1974–1996(try_exec_misc)In the main solve loop:
In
try_exec_misc(used inside findall/+):X =.. []should be an instantiation/type error in all contexts. Same concern applies tofunctor/3with a negative arity (errors in main loop, returnsSome(false)in try_exec_misc lines 1925–1926).6.
arith_modcomputesb.abs()but thei64::MINguard only matches the divisorbuiltins.rs:583–585The guard correctly catches
divisor = i64::MIN. ✓ However, the same protection is missing forrem_euclidwhen the dividenda = i64::MIN—i64::MIN.rem_euclid(b.abs())is well-defined (it callswrapping_remandwrapping_addinternally for negative dividends), so no panic. The implementation is actually correct; just worth verifying the ISO mod semantics hold for all four sign combinations, which they do per the code logic.Minor / FYI
copy_term_implfor compounds is still recursive (solver.rs:2204–2209). The list spine was made iterative (good), but deeply nested compound terms can still overflow the stack. This is pre-existing but worth noting sincecopy_term/2is new.atom_concat/3is not reversible — requires both first arguments to be bound. Pre-existing, not introduced here.\+(negation-as-failure) insidetry_solve_oncedoesn't save/restore the choice stack (solver.rs:1257–1270). If the innertry_solve_oncecall somehow pushes choice points (it currently can't sincetry_solve_oncedoesn't push them), they'd be left orphaned. This is safe today but fragile if the implementation changes.Overall the new predicates are implemented carefully — arithmetic overflow is guarded with
checked_*, float NaN/Infinity is caught bycheck_float, and thebetween/3iterative approach with step counting is solid. The main concerns are the error-vs-failure inconsistency intry_exec_misc(issue 1) and the step-counter reset inexec_findall(issue 2), which can cause incorrect program behavior rather than just performance degradation.Code Review: PR 2 (Phase 5 builtins)
Overall the implementation is solid: checked arithmetic throughout, NaN/Infinity detection, proper trail-based undo, and
try_solve_collectingcorrectly enumeratingbetween/3insidefindall. Issues below are real bugs I am confident about.1. Integer precision loss in
term_comparefor large integers vs floatscrates/prolog-core/src/builtins.rs:685(and symmetric arm ~697)(*a as f64)is a lossy cast for|a| > 2^53. For example,9007199254740993_i64 as f64 == 9007199254740992.0, soterm_compare(Integer(9007199254740993), Float(9007199254740992.0))reports Equal (then Greater) when the values are numerically different. ISO 8.4.2.1 requires the numeric comparison to be exact before applying the float-before-integer tiebreak. A correct fix checks whether the i64 is exactly representable as f64 (i.e.*a == (*a as f64) as i64) and falls back to sign/magnitude ordering when it is not.2.
succ/2overflow is a hard error insolve()but silent failure intry_exec_misc()crates/prolog-core/src/solver.rs:822-825(main loop returnsSolveResult::Error)crates/prolog-core/src/solver.rs:2008-2010(try_exec_miscreturnsSome(false))The overflow arm in
try_exec_misc:succ(9223372036854775807, S)errors when called directly, but silently fails when called inside\+,once/1, orfindall/3(all dispatched throughtry_exec_misc). A guard like\+ succ(max_int, _)would incorrectly succeed rather than raise an error.The same error-vs-failure inconsistency exists in two other builtins:
functor/3arity > 1024:solver.rs:~1924returnsSome(false)vsSolveResult::Errorin the main loop at lines ~586-590arg/3non-compound second argument:solver.rs:~1946returnsSome(false)vsSolveResult::Errorat line ~626All three should return
Nonefromtry_exec_misc(causing callers to treat the result as an error) rather than silently failing.3.
between/3overflow protection is implicit intry_solve_collectingcrates/prolog-core/src/solver.rs:1739The main
solve()loop guards withlow.checked_add(1)(lines 769-776). Intry_solve_collecting, the range*low..=*highis formed directly and the only protection is the per-iteration step counter. Iflow = i64::MINandhigh = i64::MAX, the range spans 2^64 values; correct termination depends entirely onmax_depth. The same explicit overflow check used in the main loop should be applied here.4. Missing test: cut inside
findallgoalThe new integration tests cover
betweeninsidefindall,sort/msort,copy_term,succ, andplus, but no test exercises!inside afindallgoal body. For example:should give
L = [2]. Thecut_in_try_solveflag intry_solve_collectingis intended to handle this, but the path is unexercised by the test suite.Summary
int as f64precision loss interm_comparefor large integers vs floatssucc/2overflow silently fails intry_exec_miscinstead of erroringfunctor/3arity > 1024 silently fails intry_exec_miscarg/3non-compound silently fails intry_exec_miscbetween/3intry_solve_collectingrelies on step limit for overflow semanticsfindallgoal is untestedPhase 5 review posted below as separate comment due to formatting constraints.
Code Review: Phase 5 Built-ins
Reviewed the diff. Issues in order of severity.
Bug 1 (Critical): copy_term/2 infinite recursion on circular terms
File: crates/prolog-core/src/solver.rs, line 2207
This PR removes the occurs check from =/2, which is correct per ISO — X = f(X) now succeeds, creating a circular binding Var(0) -> Compound(f, [Var(0)]). But copy_term_impl has no cycle guard. Walking Var(0) yields Compound(f, [Var(0)]), the Compound arm at line 2207 recurses on arg Var(0), which walks back to Compound again — unbounded stack recursion.
apply_impl in unify.rs handles this correctly via a seen: Vec stack (push before following a binding, pop after). copy_term_impl needs the same treatment: if a VarId is already in seen, emit a fresh unbound variable to break the cycle instead of recursing.
Reproducer: X = f(X), copy_term(X, Y). — stack-overflows today with no test catching it.
Bug 2 (Medium): term_compare gives wrong ordering for large integers vs. floats
File: crates/prolog-core/src/builtins.rs, line 685
For integers with |n| > 2^53, the i64->f64 cast loses precision. The equal-value tie-break then fires on values that appear equal but differ. Concrete failing case:
-9007199254740993 cast to f64 rounds to -9007199254740992.0. partial_cmp returns Equal; the tie-break claims integer greater-than float — but the integer is actually less.
Affects compare/3, the @-ordering predicates, sort/2, and msort/2 when mixing large-magnitude integers with nearby floats. Fix: detect |a| >= 2^53 and resolve ordering from the rounding direction rather than the lossy cast.
Bug 3 (Low / architectural): Cut removes innermost barrier CP only, not the enclosing predicate's
File: crates/prolog-core/src/solver.rs, lines 215-219
The new code is better than the old (which left the first barrier CP on the stack). For a simple one-level predicate with ! it is now correct. For nested predicates it still fails:
When ! fires, stack = [foo_CP(barrier, untried=[qux]), bar_CP(barrier, untried=[b])]. The loop pops bar_CP and stops. foo_CP survives, so backtracking from baz can retry qux. ISO requires ! to cut all choice points created since foo was called, including foo_CP.
The correct fix is to track cut-depth as an integer rather than a boolean flag (architectural change). A regression test for this nested pattern would at least document the limitation.
Safety: var_counter not checked for overflow in functor/3 construction mode
File: crates/prolog-core/src/solver.rs, around line 1030 and in try_exec_misc
functor/3 in construction mode increments var_counter (a u32) by up to 1024 per call using plain addition. Wrapping silently aliases freshly-generated variables with existing ones, causing incorrect unification with no diagnostic. Using checked_add and returning a SolveResult::Error on overflow would prevent silent corruption.
Coverage gaps (the copy_term circular case is a confirmed crash today):
Minor: In try_solve_collecting, Ok(BuiltinResult::Failure) appears after the atom-chars block rather than grouped with Success and Cut at the top of the match. No correctness impact.