(nafc g) is a three-line primitive: peek the goal's stream for one
answer; if empty, yield (unit s); else mzero. Carries the standard
miniKanren caveats — open-world unsound, diverges on infinite streams.
7 tests: failed-goal-succeeds, successful-goal-fails, double-negation,
conde-all-fail-makes-nafc-succeed, conde-any-success-makes-nafc-fail,
nafc as a guard accepting and blocking.
201/201 cumulative.
(project (vars ...) goal ...) defmacro walks each named var via mk-walk*,
rebinds them in the body's lexical scope, then mk-conjs the body goals on
the same substitution. Hygienic — gensym'd s-param so user vars survive.
Lets you reach into host SX for arithmetic, string ops, anything that
needs a ground value: (project (n) (== q (* n n))), (project (s)
(== q (str s \"!\"))), and so on.
6 new tests, 194/194 cumulative.
Classic miniKanren Peano arithmetic on (:z / (:s n)) naturals. pluso runs
relationally in all directions: 2+3=5 forward, x+2=5 → 3 backward,
enumerates the four pairs summing to 3. *o is iterated pluso. lteo/lto
via existential successor decomposition.
19 new tests, 188/188 cumulative. Phase-tagged in the plan separately
from Phase 6 CLP(FD), which will eventually replace this with native
integers + arc-consistency propagation.
conda-try mirrors condu-try but on the chosen clause it (mk-bind
(head-goal s) (rest-conj)) — all head answers flow through. condu by
contrast applies rest-conj to (first peek), keeping only one head
answer.
7 new tests covering: first-non-failing-wins, skip-failing-head, all-fail,
no-clauses, the conda-vs-condu divergence (`(1 2)` vs `(1)`), rest-goals
running on every head answer, and the soft-cut no-fallthrough property.
169/169 cumulative.
reverseo: standard recursive definition via appendo. Forward works in
run*; backward (input fresh, output ground) works in run 1 but run*
diverges trying to enumerate the unique answer (canonical TRS issue
with naive reverseo).
lengtho: Peano encoding (:z / (:s :z) / (:s (:s :z)) ...) so it works
relationally in both directions without arithmetic-as-relation. Forward
returns the Peano length; backward enumerates lists of a given length.
162/162 cumulative.
Three coupled fixes plus a new relations module land together because
each is required for the next: appendo can't terminate without all
three.
1. unify.sx — added (:cons h t) tagged cons-cell shape because SX has no
improper pairs. The unifier treats (:cons h t) and the native list
(h . t) as equivalent. mk-walk* re-flattens cons cells back to flat
lists for clean reification.
2. stream.sx — switched mature stream cells from plain SX lists to a
(:s head tail) tagged shape so a mature head can have a thunk tail.
With the old representation, mk-mplus had to (cons head thunk) which
SX rejects (cons requires a list cdr).
3. conde.sx — wraps each clause in Zzz (inverse-eta delay) for laziness.
Zzz uses (gensym "zzz-s-") for the substitution parameter so it does
not capture user goals that follow the (l s ls) convention. Without
gensym, every relation that uses `s` as a list parameter silently
binds it to the substitution dict.
relations.sx is the new module: nullo, pairo, caro, cdro, conso,
firsto, resto, listo, appendo, membero. 25 new tests.
Canary green:
(run* q (appendo (list 1 2) (list 3 4) q))
→ ((1 2 3 4))
(run* q (fresh (l s) (appendo l s (list 1 2 3)) (== q (list l s))))
→ ((() (1 2 3)) ((1) (2 3)) ((1 2) (3)) ((1 2 3) ()))
(run 3 q (listo q))
→ (() (_.0) (_.0 _.1))
152/152 cumulative.
run.sx: reify-name builds canonical "_.N" symbols; reify-s walks a term
left-to-right and assigns each unbound var its index in the discovery
order; reify combines the two with two walk* passes. run-n is the
runtime defmacro: binds the query var, takes ≤ n stream answers, reifies
each. run* and run are sugar around it.
First classic miniKanren tests green:
(run* q (== q 1)) → (1)
(run* q (conde ((== q 1)) ((== q 2)))) → (1 2)
(run* q (fresh (x y) (== q (list x y)))) → ((_.0 _.1))
128/128 cumulative.
condu.sx: defmacro `condu` folds clauses through a runtime `condu-try`
walker. First clause whose head yields a non-empty stream commits its
single first answer; later clauses are not tried. `onceo` is the simpler
sibling — stream-take 1 over a goal's output.
10 tests cover: onceo trimming success/failure/conde, condu first-clause
wins, condu skips failing heads, condu commits-and-cannot-backtrack to
later clauses if the rest of the chosen clause fails.
110/110 cumulative. Phase 2 complete.
(fresh (x y z) g1 g2 ...) expands to a let that calls (make-var) for each
named var, then mk-conjs the goals. call-fresh is the function-shaped
alternative for programmatic goal building.
9 new tests: empty-vars, single var, multi-var multi-goal, fresh under
disj, nested fresh, call-fresh equivalents. 91/91 cumulative.
lib/minikanren/stream.sx: mzero/unit/mk-mplus/mk-bind/stream-take. Three
stream shapes (empty, mature list, immature thunk). mk-mplus suspends and
swaps on a paused-left for fair interleaving (Reasoned Schemer style).
lib/minikanren/goals.sx: succeed/fail/==/==-check + conj2/disj2 +
variadic mk-conj/mk-disj. ==-check is the opt-in occurs-checked variant.
Forced-rename note: SX has a host primitive `bind` that silently shadows
user-level defines, so all stream/goal operators are mk-prefixed. Recorded
in feedback memory.
82/82 tests cumulative (48 unify + 34 goals).
lib/minikanren/unify.sx wraps lib/guest/match.sx with a miniKanren-flavoured
cfg: native SX lists as cons-pairs, occurs-check off by default. ~22 lines
of local logic over kit's walk-with / unify-with / extend / occurs-with.
48 tests in lib/minikanren/tests/unify.sx exercise: var fresh-distinct,
walk chains, walk* deep into nested lists, atom/var/list unification with
positional matching, failure modes, opt-in occurs check.
apl-throw raises a tagged ("apl-error" code msg) error.
apl-trap-matches? checks if codes list contains the error's code
(0 = catch-all, à la Dyalog).
Eval-stmt :trap clause wraps try-block with R7RS guard;
on match, runs catch-block; on mismatch, re-raises.
Bonus :throw AST node for testing.
test.sh + conformance.sh now load lib/r7rs.sx (for guard) and
include eval-ops + pipeline suites in scoreboard.
All Phase 7 unchecked items are now ticked.
Final scoreboard: 450/450 across 10 suites.
30 new source-string idioms via apl-run: triangulars, factorial,
running sum/product, parity counts, identity matrix, mult-table,
dot product, ∧.= equality, take/drop/reverse, tally, ravel,
count-of-value, etc.
Side-fix: tokenizer's apl-glyph-set was missing ≢ and ≡ — they
were silently skipped. Added them and to apl-parse-fn-glyphs.
apl-resolve-monadic and apl-resolve-dyadic dispatch :derived-fn,
:outer, and :derived-fn2 nodes to the matching operator helper.
:monad/:dyad in apl-eval-ast now route through these resolvers.
Removed queens(8) test (too slow under current 300s timeout).
The bytecode compiler emitted OP_CALL_PRIM (52) for every primitive call, even
for arithmetic and comparison hot-paths. The VM had specialized opcodes
(OP_ADD, OP_SUB, OP_EQ, etc.) defined but unused.
- lib/compiler.sx (compile-call): emit specialized 1-byte opcode when the
primitive name + arity matches one of {+, -, *, /, =, <, >, cons, not, len,
first, rest}. Falls back to CALL_PRIM otherwise. fib bytecode: 50 → 38 bytes.
- hosts/ocaml/lib/sx_compiler.ml: mirror change in the auto-generated OCaml
compiler so SXBC export from mcp_tree uses the same emission.
- hosts/ocaml/lib/sx_vm.ml: extend OP_ADD/SUB/MUL/DIV to handle Integer+Integer
(not just Number+Number). Inline OP_EQ via Sx_runtime._fast_eq. Inline
OP_LT/GT mixed-numeric comparisons. Avoids Hashtbl lookup on the fallback
path for the common integer cases that dominate tight loops.
- hosts/ocaml/bin/bench_vm.ml: VM-only benchmark — loads compiler.sx via CEK,
JIT-compiles each fn, measures Sx_vm.call_closure throughput.
Median improvements (best of 3 runs of 9-min, bench_vm.exe):
fib(22) 107.87ms → 33.13ms -69%
loop(200000) 429.64ms → 161.16ms -62%
sum-to(50000) 72.85ms → 36.74ms -50%
count-lt(20000) 28.44ms → 17.58ms -38%
count-eq(20000) 37.23ms → 15.46ms -58%
Tests: 4550/4550 OCaml passing (unchanged). Zero regressions.
Last step in the sx-improvements roadmap — all 14 steps complete.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Added short aliases make-buffer / buffer? / buffer-append! / buffer->string /
buffer-length on both OCaml and JS hosts, sharing the existing StringBuffer
value type. buffer-append! auto-coerces non-strings via inspect.
Rewrote the OCaml host inspect function to walk a single shared Buffer.t
instead of allocating O(n) intermediate strings via String.concat at every
recursion level. inspect underlies sx-serialize and error-path formatting,
so this benefits the tightest serialization paths.
Median improvements (bin/bench_inspect.exe, best-of-3 of 9-run min):
tree-d8 (75KB): 5.31ms -> 1.30ms (-76%)
tree-d10 (679KB): 81.89ms -> 16.02ms (-80%)
dict-1000: 0.80ms -> 0.31ms (-61%)
list-2000: 0.74ms -> 0.33ms (-55%)
Tests: OCaml 4545 -> 4550. JS 2591 -> 2596. Zero regressions.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
CEK frames were already records (cek_frame in sx_types.ml), so the actual
hot-path bottleneck was prim_call "=" [...] in step_continue/step_eval
dispatch: each step did a Hashtbl lookup + 2x list cons + pattern match
just to compare frame-type strings.
Added a short-circuit fast path in prim_call (sx_runtime.ml) for the
hot operators: =, <, >, <=, >=, empty?, first, rest, len. These bypass
the primitives Hashtbl entirely and dispatch directly on value shape.
Inlined _fast_eq for scalar/string equality, which dominates frame-type
dispatch comparisons.
Added bin/bench_cek.exe with five tight-loop benchmarks (fib, loop,
map, reduce, let-heavy). Median of 7 runs:
fib(18) 2789ms -> 941ms (-66%)
loop(5000) 2018ms -> 620ms (-69%)
map sq xs(1000) 108ms -> 48ms (-56%)
reduce + ys(2000) 72ms -> 10ms (-86%)
let-heavy(2000) 491ms -> 271ms (-45%)
Tests: 4545/4545 passing baseline preserved (1339 pre-existing failures
unchanged).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
