#5 - cli - navicore/patch-prolog

## PR Review -- CLI refactoring + engine audit The PR itself (deleting build.rs, simplifying main.rs to a compile-only CLI) is clean. Findings below, numbered by severity.

claude[bot] commented

2026-03-07 01:10:48 +00:00

(Migrated from github.com)

1. Fragile exit-code detection -- src/main.rs (introduced by this PR)

The new main.rs detects parse errors with:

if e.starts_with(Parse error)

This string must exactly match the prefix produced in src/compiler.rs:22 (format!(Parse error: {}, e)). If that wording changes, the exit-code contract silently breaks. Recommend a typed error enum (ParseError / CompileError) from compiler::compile instead of string matching.

### 1. Fragile exit-code detection -- src/main.rs (introduced by this PR) The new main.rs detects parse errors with: if e.starts_with(Parse error) This string must exactly match the prefix produced in src/compiler.rs:22 (format!(Parse error: {}, e)). If that wording changes, the exit-code contract silently breaks. Recommend a typed error enum (ParseError / CompileError) from compiler::compile instead of string matching.

claude[bot] commented

2026-03-07 01:10:58 +00:00

(Migrated from github.com)

2. HIGH: Semicolon/comma precedence inverted in clause bodies -- parser.rs:124-147

parse_goal_list (comma) wraps parse_goal_disjunction (semicolon). This inverts ISO precedences:

ISO: comma is 1000 xfy, semicolon is 1100 xfy -- semicolon binds MORE loosely than comma
Current: comma is at the outer level, semicolon is inner -- comma binds more loosely

Consequence: p :- a, b ; c. is parsed as a, (b ; c) -- if a fails the whole clause fails and c is never tried. ISO requires (a, b) ; c -- c is tried when a,b fail together.

Code in explicit parentheses like (a, b ; c) parses correctly via parse_paren_body. Only bare clause bodies are affected. No integration test exercises this pattern so the bug is silent.

Fix: add an outer parse_body_disjunction layer handling semicolons, which calls parse_body_conjunction (current parse_goal_list logic) for each operand.

### 2. HIGH: Semicolon/comma precedence inverted in clause bodies -- parser.rs:124-147 parse_goal_list (comma) wraps parse_goal_disjunction (semicolon). This inverts ISO precedences: - ISO: comma is 1000 xfy, semicolon is 1100 xfy -- semicolon binds MORE loosely than comma - Current: comma is at the outer level, semicolon is inner -- comma binds more loosely Consequence: p :- a, b ; c. is parsed as a, (b ; c) -- if a fails the whole clause fails and c is never tried. ISO requires (a, b) ; c -- c is tried when a,b fail together. Code in explicit parentheses like (a, b ; c) parses correctly via parse_paren_body. Only bare clause bodies are affected. No integration test exercises this pattern so the bug is silent. Fix: add an outer parse_body_disjunction layer handling semicolons, which calls parse_body_conjunction (current parse_goal_list logic) for each operand.

claude[bot] commented

2026-03-07 01:11:04 +00:00

(Migrated from github.com)

3. O(n) cycle detection in apply_impl -- unify.rs:78

seen.contains(id) does a linear scan over Vec. For a cyclic term (e.g. created by X = f(X) without occurs check) apply becomes O(d^2) in nesting depth. Replacing Vec with FnvHashSet makes each lookup O(1).

### 3. O(n) cycle detection in apply_impl -- unify.rs:78 seen.contains(id) does a linear scan over Vec<VarId>. For a cyclic term (e.g. created by X = f(X) without occurs check) apply becomes O(d^2) in nesting depth. Replacing Vec<VarId> with FnvHashSet<VarId> makes each lookup O(1).

claude[bot] commented

2026-03-07 01:11:11 +00:00

(Migrated from github.com)

4. Missing integer-division and rem arithmetic operators -- builtins.rs eval_arith

ISO 6.7.2 requires:

// for truncating integer division (7 // 2 = 3)
rem for truncating remainder -- differs from mod for negatives: -7 rem 2 = -1 but -7 mod 2 = 1

Any program using X is N // D or X is A rem B currently throws Unknown arithmetic operator. Note that / on two integers already truncates (ISO-correct), but // is the unambiguous ISO form and rem has genuinely different semantics from mod.

### 4. Missing integer-division and rem arithmetic operators -- builtins.rs eval_arith ISO 6.7.2 requires: - // for truncating integer division (7 // 2 = 3) - rem for truncating remainder -- differs from mod for negatives: -7 rem 2 = -1 but -7 mod 2 = 1 Any program using X is N // D or X is A rem B currently throws Unknown arithmetic operator. Note that / on two integers already truncates (ISO-correct), but // is the unambiguous ISO form and rem has genuinely different semantics from mod.

claude[bot] commented

2026-03-07 01:11:29 +00:00

(Migrated from github.com)

5. atom_concat/3 throws runtime error in reverse mode -- solver.rs:421

ISO allows atom_concat(X, Y, foo) with X or Y unbound, enumerating splits on backtracking. The current code returns SolveResult::Error when either first arg is not an atom, making atom_concat forward-mode only. Same pattern repeats in try_solve_once and try_solve_collecting.

### 5. atom_concat/3 throws runtime error in reverse mode -- solver.rs:421 ISO allows atom_concat(X, Y, foo) with X or Y unbound, enumerating splits on backtracking. The current code returns SolveResult::Error when either first arg is not an atom, making atom_concat forward-mode only. Same pattern repeats in try_solve_once and try_solve_collecting.

claude[bot] commented

2026-03-07 01:11:39 +00:00

(Migrated from github.com)

6. unify_with_occurs_check/2 implemented but never exposed -- unify.rs:163

occurs_in is correct but marked allow(dead_code). ISO 8.2.2 requires unify_with_occurs_check/2 as a builtin. Wiring it into is_builtin and exec_builtin needs only a few lines.

### 6. unify_with_occurs_check/2 implemented but never exposed -- unify.rs:163 occurs_in is correct but marked allow(dead_code). ISO 8.2.2 requires unify_with_occurs_check/2 as a builtin. Wiring it into is_builtin and exec_builtin needs only a few lines.

claude[bot] commented

2026-03-07 01:11:43 +00:00

(Migrated from github.com)

7. Minor: between/3 clones continuation on every iteration -- solver.rs:1438

remaining.clone() is called inside the for-val loop. For large ranges with complex continuations this is O(N x goals) allocations. Not a correctness issue.

Summary: 1-Medium src/main.rs fragile string match; 2-High parser.rs:124 semicolon/comma precedence inverted in clause bodies; 3-Low unify.rs:78 O(n^2) apply on cyclic terms; 4-Medium builtins.rs // and rem missing; 5-Medium solver.rs:421 atom_concat reverse mode; 6-Low unify.rs:163 unify_with_occurs_check unreachable; 7-Low solver.rs:1438 redundant clone.

### 7. Minor: between/3 clones continuation on every iteration -- solver.rs:1438 remaining.clone() is called inside the for-val loop. For large ranges with complex continuations this is O(N x goals) allocations. Not a correctness issue. Summary: 1-Medium src/main.rs fragile string match; 2-High parser.rs:124 semicolon/comma precedence inverted in clause bodies; 3-Low unify.rs:78 O(n^2) apply on cyclic terms; 4-Medium builtins.rs // and rem missing; 5-Medium solver.rs:421 atom_concat reverse mode; 6-Low unify.rs:163 unify_with_occurs_check unreachable; 7-Low solver.rs:1438 redundant clone.

claude[bot] commented

2026-03-07 02:28:50 +00:00

(Migrated from github.com)

PR 5 code review - three issues found

claude[bot] commented

2026-03-07 02:29:30 +00:00

(Migrated from github.com)

PR 5 Review - Three issues found.

BUG 1: occurs_in infinite loop on circular terms (unify.rs lines 207-222)

occurs_in follows variable bindings via self.lookup but has no visited-set. Previously dead code with allow(dead_code), this PR makes it reachable via unify_with_occurs_check/2. If a variable is circularly bound via =/2, a subsequent unify_with_occurs_check call on a term containing that variable loops forever, bypassing the step limit entirely.

Reproducer: X = f(X) followed by unify_with_occurs_check(Y, g(X)). After the first goal binds X circularly, occurs_in(Y_id, g(X)) follows X -> f(X) -> X -> ... indefinitely.

Fix: add a FnvHashSet visited guard to occurs_in, analogous to the cycle guard already in apply_impl.

BUG 2: rem reserved as keyword, unusable as atom or functor (tokenizer.rs line 515)

rem is now always TokenKind::Rem at scan time. parse_primary has no arm for TokenKind::Rem, so rem in atom argument position or as a predicate name is a parse error. For example, foo(rem). and a rule with rem as the head functor both fail to parse. mod and is have the same pre-existing issue, but this PR adds a new restricted name. Fix: handle TokenKind::Rem (and Mod, Is) in parse_primary with atom fallback when not in infix operator position.

MISSING TESTS: error paths for // and rem (tests/integration.rs)

The tests cover normal and sign cases but leave these paths uncovered: X is 7 // 0, X is 7 rem 0 (both should produce runtime errors, not panics), and the overflow cases X is -9223372036854775808 // -1 and X is -9223372036854775808 rem -1. The implementations handle all four correctly via checked_div and checked_rem; the paths are simply unexercised.

No other issues. The semicolon/comma precedence fix is correct (old parser produced wrong associativity). The right-assoc conjunction tree, checked_div/checked_rem overflow handling, unify_with_occurs_check core logic (occurs check on variable-binding step), and the apply_impl switch from Vec to FnvHashSet are all correct.

PR 5 Review - Three issues found. BUG 1: occurs_in infinite loop on circular terms (unify.rs lines 207-222) occurs_in follows variable bindings via self.lookup but has no visited-set. Previously dead code with allow(dead_code), this PR makes it reachable via unify_with_occurs_check/2. If a variable is circularly bound via =/2, a subsequent unify_with_occurs_check call on a term containing that variable loops forever, bypassing the step limit entirely. Reproducer: X = f(X) followed by unify_with_occurs_check(Y, g(X)). After the first goal binds X circularly, occurs_in(Y_id, g(X)) follows X -> f(X) -> X -> ... indefinitely. Fix: add a FnvHashSet visited guard to occurs_in, analogous to the cycle guard already in apply_impl. --- BUG 2: rem reserved as keyword, unusable as atom or functor (tokenizer.rs line 515) rem is now always TokenKind::Rem at scan time. parse_primary has no arm for TokenKind::Rem, so rem in atom argument position or as a predicate name is a parse error. For example, foo(rem). and a rule with rem as the head functor both fail to parse. mod and is have the same pre-existing issue, but this PR adds a new restricted name. Fix: handle TokenKind::Rem (and Mod, Is) in parse_primary with atom fallback when not in infix operator position. --- MISSING TESTS: error paths for // and rem (tests/integration.rs) The tests cover normal and sign cases but leave these paths uncovered: X is 7 // 0, X is 7 rem 0 (both should produce runtime errors, not panics), and the overflow cases X is -9223372036854775808 // -1 and X is -9223372036854775808 rem -1. The implementations handle all four correctly via checked_div and checked_rem; the paths are simply unexercised. --- No other issues. The semicolon/comma precedence fix is correct (old parser produced wrong associativity). The right-assoc conjunction tree, checked_div/checked_rem overflow handling, unify_with_occurs_check core logic (occurs check on variable-binding step), and the apply_impl switch from Vec to FnvHashSet are all correct.

Rows
Columns

cli #5

PR Review -- CLI refactoring + engine audit

1. Fragile exit-code detection -- src/main.rs (introduced by this PR)

2. HIGH: Semicolon/comma precedence inverted in clause bodies -- parser.rs:124-147

3. O(n) cycle detection in apply_impl -- unify.rs:78

4. Missing integer-division and rem arithmetic operators -- builtins.rs eval_arith

5. atom_concat/3 throws runtime error in reverse mode -- solver.rs:421

6. unify_with_occurs_check/2 implemented but never exposed -- unify.rs:163

7. Minor: between/3 clones continuation on every iteration -- solver.rs:1438