56 Commits

Author SHA1 Message Date
08f4a7babd mk: enumerate-i / enumerate-from-i — 501/501 milestone
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
(enumerate-i l result): result is l with each element paired with its
0-based index. (enumerate-from-i n l result): same but starts at n.

  (enumerate-i (list :a :b :c) q) -> (((0 :a) (1 :b) (2 :c)))

5 new tests, 501/501 cumulative.
2026-05-08 12:20:03 +00:00
221c7fef35 mk: partitiono — split list by predicate
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 26s
(partitiono pred l yes no) — yes is the elements of l where pred
succeeds; no is the rest. Conde dispatches on each element via the
predicate goal vs nafc-of-the-predicate, threading the head through
the matching output list.

Composes with intarith / membero / etc. for any predicate-shaped goal:
  (partitiono (fn (x) (lto-i x 5)) (list 1 7 2 8 3) yes no)
    yes -> (1 2 3); no -> (7 8)

5 new tests, 496/496 cumulative.
2026-05-08 12:18:25 +00:00
363ebc8f04 mk: appendo3 — 3-list append
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Composes two appendos: (appendo a b mid) ∧ (appendo mid c r). Runs
forward (concatenate three known lists) and backward (recover any of
the three from the other two and the result).

5 new tests, 491/491 cumulative.
2026-05-08 12:16:40 +00:00
7ff72cefb2 mk: lengtho-i — integer-indexed length
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Drop-in fast replacement for Peano lengtho when the count fits in a
host integer. Two conde clauses: empty list -> 0; recurse, n = 1 +
length(tail). Uses pluso-i so the length walks to a native int.

5 new tests, 486/486 cumulative.
2026-05-08 12:15:53 +00:00
064ab2900b mk: sumo + producto — fold list to integer
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Sum and product over a list of ground integers via fold + intarith.
Empty list yields the identity (0 for sum, 1 for product). Recurse
combines the head with the recursively-computed tail value via
pluso-i / *o-i.

9 new tests, 481/481 cumulative.
2026-05-08 12:14:15 +00:00
4f5f8015fb mk: mino + maxo — find min/max of a list
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Two conde clauses each: singleton -> the element; multi -> compare head
against the recursive min/max of the tail and pick. Uses lteo-i / lto-i
for the comparisons, so the input must be ground integers.

mino + maxo can run together: (fresh (mn mx) (mino l mn) (maxo l mx)
(== q (list mn mx))) recovers both.

9 new tests, 472/472 cumulative.
2026-05-08 12:12:32 +00:00
c4b6f1fa0f mk: sortedo — list is non-decreasing (intarith)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Three conde clauses: empty list / singleton list / two-or-more (where
the first two satisfy lteo-i and the rest is recursively sorted). Uses
ground-only integer comparison (intarith), so the input list must
walk to ground integers.

7 new tests, 463/463 cumulative.
2026-05-08 12:10:52 +00:00
6454603568 mk: subseto — every element of l1 is in l2
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 26s
Recursive: empty l1 trivially holds; otherwise the head is in l2 (via
membero) and the tail is a subset. Duplicates in l1 are allowed since
each is independently checked.

7 new tests, 456/456 cumulative.
2026-05-08 12:09:06 +00:00
4df277803d mk: cycle-free path search test
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 44s
Mitigation for the cyclic-graph divergence (see tests/cyclic-graph.sx).
Threads a `visited` accumulator through the recursion; each candidate
next-step is gated by `nafc (membero z visited)`. Terminates on graphs
with cycles, no Phase-7 tabling required for the simple acyclic-path
query.

Demonstrates a viable alternative to tabling for the common case where
the user wants finite path enumeration over a graph with cycles.

3 new tests, 449/449 cumulative.
2026-05-08 12:07:00 +00:00
58d78de32a mk: removeo-allo — remove every occurrence
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 49s
Three conde clauses: empty list -> empty result; head matches x ->
skip and recurse; head differs (nafc-gated) -> keep and recurse.
Distinct from rembero, which removes only the first occurrence.

5 new tests, 446/446 cumulative.
2026-05-08 12:04:17 +00:00
6bc3c14dac mk: btree-walko — binary-tree walker via matche
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 44s
Demo of matche dispatch + conde + recursion for tree traversal:
  (matche tree
    ((:leaf x)   (== v x))
    ((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))

Test tree ((1 2) (3 (4 5))) yields all 5 leaves under run*. Also tests
membership (run 1) and absence.

4 new tests, 441/441 cumulative.
2026-05-08 12:02:13 +00:00
eb69039935 mk: swap-firsto — swap first two list elements
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 48s
Four conso calls express the (a b . rest) -> (b a . rest) rewrite as a
purely relational constraint. Self-inverse on length-2+ lists; runs
forward (swap given input) and backward (recover original from the
swapped form). Fails on lists shorter than 2.

6 new tests, 437/437 cumulative.
2026-05-08 11:59:41 +00:00
c04ddd105b mk: pairlisto — relational zip
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 39s
(pairlisto l1 l2 pairs): pairs is the zipped list of pairs (l1[i] l2[i]).
Recurses on both l1 and l2 in lockstep, building pairs in parallel.

Runs forward, can recover l1 given l2 and pairs, can recover l2 given
l1 and pairs. Different-length lists fail.

5 new tests, 431/431 cumulative.
2026-05-08 11:57:12 +00:00
136cacbd3f mk: iterate-no — apply a relation n times
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
(iterate-no rel n x result) holds when applying the 2-arg relation rel
n times (Peano n) starting from x produces result. Base case: zero
iterations means result equals x. Recursive case: rel x mid, then
iterate-no n-1 from mid.

Generalises common chains:
  succ iteration:  (iterate-no succ-rel n :z q) -> n in Peano
  list growth:     (iterate-no cons-rel n () q) -> n-element list

4 new tests, 426/426 cumulative.
2026-05-08 11:54:24 +00:00
6fc155ddd8 mk: rev-acco + rev-2o — accumulator-style reverse
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s
rev-acco is the standard tail-recursive reverse with an accumulator;
rev-2o starts the accumulator at the empty list. Faster than the
appendo-driven reverseo for forward queries because there is no nested
appendo per element.

Trade-off: rev-acco is asymmetric. The accumulator's initial-empty
cannot be enumerated backwards the way reverseo does, so reverseo is
still the right choice when both directions matter.

A test verifies rev-2o and reverseo agree on forward queries.

6 new tests, 422/422 cumulative.
2026-05-08 11:51:51 +00:00
d992788a03 mk: even-i / odd-i — host-arithmetic parity goals
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 27s
Two-line definitions over project + host even?/odd?. Ground-only — no
relational behaviour, but they pair cleanly with membero for filtered
enumeration:
  (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x))
    -> (2 4 6)

5 new tests, 416/416 cumulative.
2026-05-08 11:49:47 +00:00
4d861575df mk: selecto — choose element + rest of list
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 29s
Classic miniKanren relation. (selecto x rest l) holds when l contains
x at any position with `rest` being everything else. Direct base case
(l = (x . rest)) plus the skip-head recursion that threads the head
through to the result rest.

Run modes: enumerate every (x, rest) split; recover rest given an
element; recover an element given the rest; (and ground/all combinations).

6 new tests, 411/411 cumulative.
2026-05-08 11:47:27 +00:00
e202c81a0d mk: subo — contiguous sublist relation
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 32s
Composes two appendos: l = front ++ s ++ back, equivalently
  (appendo front-and-s back l) and (appendo front s front-and-s).

Goal order matters: doing the (appendo ground:l) split first makes the
search finitary; the second appendo is then deterministic given
front-and-s and ground s. Reversing the order causes divergence on
failing inputs (the front search becomes unbounded).

7 new tests, 405/405 cumulative.
2026-05-08 11:45:31 +00:00
fc14a8063b mk: prefixo + suffixo — appendo-derived sublist relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
Two-line definitions over appendo:
  (prefixo p l) ≡ ∃rest. (appendo p rest l)
  (suffixo s l) ≡ ∃front. (appendo front s l)

Both enumerate all prefixes/suffixes when called with a fresh first
arg, and serve as decision relations when called with both grounded.

9 new tests, 398/398 cumulative.
2026-05-08 11:40:28 +00:00
6ee02db2ab mk: palindromeo — list reads same forwards/backwards
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Two-line definition: a list is a palindrome iff it equals its reverse.
Direct composition of reverseo + ==.

7 new tests: empty / singleton / equal pair / unequal pair /
5-element-yes / 5-element-no / strings.

389/389 cumulative.
2026-05-08 11:38:29 +00:00
7b6cb64548 mk: not-membero — relational "x is not in l"
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Mirrors the structure all-distincto already uses internally: walk the
list, ensure each element is not equal to x via nafc, recurse on tail.
Useful as a constraint-style filter:

  (membero x (list 1 2 3 4 5))
  (not-membero x (list 2 4))
    -> x in {1, 3, 5}

4 new tests, 382/382 cumulative.
2026-05-08 11:36:14 +00:00
c2b238635f mk: repeato + concato
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
repeato: produces (or recognizes) a list of n copies of a value, with n
Peano-encoded. Runs forward, backward (recover the count from a uniform
list), and bidirectionally.

concato: fold-appendo over a list-of-lists. (concato (list (list 1 2)
(list) (list 3 4 5)) q) -> ((1 2 3 4 5)).

10 new tests, 378/378 cumulative.
2026-05-08 11:34:28 +00:00
8c48a0be63 mk: tako + dropo — Peano-indexed prefix and suffix
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
(tako n l prefix) — prefix is the first n elements of l.
(dropo n l suffix) — suffix is l after dropping the first n.

Both use a Peano natural for the count. Round-trip holds:
  (tako n l) ⊕ (dropo n l) = l   (verified by an end-to-end test)

9 new tests, 368/368 cumulative.
2026-05-08 11:32:33 +00:00
54a58c704e mk: eveno + oddo — Peano parity predicates
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
eveno: zero, or (s (s m)) when m is even.
oddo:  one, or (s (s m)) when m is odd.

Both run forward (predicate test on a Peano number) and backward
(enumerate even / odd numbers). The two are mutually exclusive — no
number satisfies both.

12 new tests, 359/359 cumulative.
2026-05-08 11:30:02 +00:00
ada405b37b mk: defrel — Prolog-style relation-definition macro
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...) expands to
(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...))).

Mirrors Prolog's `name(Args) :- goals.` shape. Inherits the Zzz-on-each-
clause laziness from conde, so user relations defined via defrel
terminate on partial answers without needing manual delay. Tests
redefine membero / listo / pluso through defrel and verify equivalence.

3 new tests, 347/347 cumulative.
2026-05-08 11:27:49 +00:00
99066430fd mk: lasto + init-o — last and not-last list relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
lasto: x is the final element of l. Direct base case (l = (x)) plus
recurse-on-cdr.

init-o: init is l without its last element. Base case for singleton:
(== init ()). Otherwise recurse, threading the head through to the
init result via conso.

Together with appendo, the round-trip init append (list last) = l
holds, which is exercised by an end-to-end test.

8 new tests, 344/344 cumulative.
2026-05-08 11:25:12 +00:00
48835f2d4f mk: relational database queries — Datalog-style demo
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
tests/rdb.sx shows the library as a small Datalog engine over fact
tables. Each table is an SX list of tuples, wrapped by a relation that
does (membero (list ...) table). Queries compose selection, projection,
and joins entirely in run* / fresh / conde / membero / intarith / nafc.

Five queries: dept filter, salary > threshold, employee-project join,
intersection (engineers on a specific project), anyone on multiple
distinct projects.

5 new tests, 336/336 cumulative.
2026-05-08 11:22:12 +00:00
16fe22669a mk: cyclic-graph behaviour test — motivates Phase 7 tabling
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 28s
Demonstrates the naive-patho behaviour on a 2-cycle (a <-> b, plus
b -> c). Without Phase-7 tabling, the search produces ever-longer
paths: (a b), (a b a b), (a b a b a b), ... `run 5` truncates to a
finite prefix; `run*` diverges. Documenting this as a regression-style
test gives Phase 7 a concrete starting point.

3 new tests, 331/331 cumulative.
2026-05-08 11:19:29 +00:00
2d51a8c4ea mk: numbero / stringo / symbolo type predicates
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Ground-only type tests via project. Each succeeds iff its argument
walks to the corresponding host value type. Composes with membero for
type-filtered enumeration:

  (fresh (x) (membero x (list 1 "a" 2 "b" 3)) (numbero x) (== q x))
    -> (1 2 3)

12 new tests, 328/328 cumulative. Caveat: SX keywords are strings, so
(stringo :k) succeeds.
2026-05-08 11:17:27 +00:00
b4c1253891 mk: graph reachability via patho — classic miniKanren
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Defines a small graph as a fact list, edgeo for fact lookup, and patho
that recursively constructs paths. Direct-edge clause yields (x y);
otherwise traverse one edge to z, recurse for z->y, prepend x.

Enumerates all paths between two nodes, including alternates through
shortcut edges:
  (run* q (patho :a :d q))
    -> ((:a :b :c :d) (:a :c :d))    ; both routes

6 new tests, 316/316 cumulative.
2026-05-08 11:15:24 +00:00
e7dca2675c mk: everyo / someo — predicate-style relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
(everyo rel l): every element of l satisfies the unary relation rel.
(someo rel l): some element does. Both compose with intarith and other
predicate-shaped goals:
  (everyo (fn (x) (lto-i x 10)) (list 1 5 9))    -> succeeds
  (someo  (fn (x) (lto-i 100 x)) (list 5 50 200)) -> succeeds

10 new tests, 310/310 cumulative.
2026-05-08 11:13:22 +00:00
f00054309d mk: mapo (relational map) — 300/300 milestone
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
(mapo rel l1 l2) takes a 2-argument relation rel and asserts l2 is l1
with each element rel-related to its counterpart. Recursive on both
lists in lockstep. Works forward (fixed l1, find l2), backward (fixed
l2, find l1), or constraining mid-pipeline.

Composes with intarith for arithmetic transforms:
  (mapo (fn (a b) (*o-i a a b)) (list 1 2 3 4) q) -> ((1 4 9 16))

7 new tests, 300/300 cumulative.
2026-05-08 11:11:26 +00:00
cfb43a3cdf mk: samelengtho — equal-length relation
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Recurses positionally, dropping a head from each list each step. Both
arguments can be unbound, giving the natural enumeration:

  (run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2))))
    -> (((), ())                         empty/empty
        ((_.0), (_.1))                   pair of 1-element lists
        ((_.0 _.1), (_.2 _.3)))          pair of 2-element lists

5 new tests, 293/293 cumulative.
2026-05-08 11:09:48 +00:00
186171fec3 mk: pythagorean triples search — intarith showcase
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 27s
Finds all (a, b, c) with a, b, c in [1..10], a <= b, a^2 + b^2 = c^2.
Result: ((3 4 5) (6 8 10)) — the two smallest Pythagorean triples
within the domain.

Demonstrates the enumerate-then-filter pattern:
  (ino a dom) (ino b dom) (ino c dom) — generate
  (lteo-i a b) — symmetry break
  (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) — squares
  (pluso-i a-sq b-sq sum) (== sum c-sq) — Pythagorean equation

288/288 cumulative.
2026-05-08 11:07:33 +00:00
9795532f7d mk: intarith.sx — ground-only integer arithmetic via project
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic
in project. They run at native speed but require their inputs to walk
to ground numbers — they are NOT relational the way Peano pluso is.
Use them when puzzle size makes Peano impractical (which is most cases
beyond toy examples).

Composes with relational goals — for instance,
  (fresh (x) (membero x (1 2 3 4 5)) (lto-i x 3) (== q x))
filters the domain by < 3 and returns (1 2).

18 new tests, 287/287 cumulative.
2026-05-08 11:02:09 +00:00
b89b0def93 mk: 2x2 Latin square — small classic FD constraint demo
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
Defines latin-2x2 over 4 cells and 4 all-distincto constraints. Enumerates
exactly 2 squares ((1 2)(2 1)) and ((2 1)(1 2)); a corner clue narrows to
one. 3 new tests, 269/269 cumulative.

3x3 (12 squares, the natural showcase) is too slow under naive enumerate-
then-filter — that is the motivating test for Phase 6 arc-consistency.
2026-05-08 11:00:12 +00:00
428ca79f61 mk: rembero / assoco / nth-o — more list relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
rembero (remove-first) uses nafc to gate the skip-element clause so
the result is well-defined on ground lists. assoco is alist lookup —
runs forward (key -> value) and backward (find keys with a given
value). nth-o uses Peano-encoded indices into a list, mirroring lengtho.

13 new tests, 266/266 cumulative.
2026-05-08 10:50:28 +00:00
bf9fe8b365 mk: flatteno — nested list flattener
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 49s
Three conde clauses: nullo tree -> nullo flat; pairo tree -> recurse on
car & cdr, appendo their flattenings; otherwise tree must be a ground
non-list atom (nafc nullo + nafc pairo) and flat = (list tree).

Works on ground inputs of arbitrary nesting:
  (run* q (flatteno (list 1 (list 2 3) (list (list 4) 5)) q))
    -> ((1 2 3 4 5))

7 tests, 253/253 cumulative. Phase 4 list relations now complete.
2026-05-08 10:46:13 +00:00
2ae848dfe7 mk: laziness tests — Zzz-conde + interleaving fairness
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 38s
Verifies that the Zzz-wraps-each-conde-clause + mk-mplus-suspend-on-
paused-left machinery produces fair interleaving and gives finite
prefixes from infinitely-recursive relations:

- listo-aux has no base case under run* but run 4 q ... produces
  exactly the four shortest list shapes, in order.
- mk-disj of two infinite generators (ones-gen, twos-gen) with
  run 4 q ... must include both 1-prefixed and 2-prefixed answers
  (no starvation).
- run* terminates on a goal that has a finite answer set.

3 tests, 246/246 cumulative.
2026-05-08 10:43:45 +00:00
33693fc957 mk: 4-queens classic benchmark green
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 46s
queens.sx encodes a queen in row i at column ci. ino-each constrains
each ci to {1..n}; all-distincto handles the row/column distinct
property; safe-diag uses project to escape into host arithmetic for the
|c_i - c_j| != |i - j| diagonal guard. all-cells-safe iterates pairs at
goal-construction time so the constraint set is materialised once,
then driven by the search.

  (run* q (fresh (a b c d) (== q (list a b c d))
                            (queens-cols (list a b c d) 4)))
    -> ((2 4 1 3) (3 1 4 2))

Both valid 4-queens placements found. 6 new tests including the
two-solution invariant; 243/243 cumulative.
2026-05-08 10:41:02 +00:00
3d2a5b1814 mk: phase 6A — minimal FD (ino + all-distincto)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 55s
ino is membero with the constraint-store-friendly argument order
(`(ino x dom)` reads as "x in dom"). all-distincto checks pairwise
distinctness via nafc + membero on the recursive tail. These two are
enough to express the enumerate-then-filter style of finite-domain
solving:

  (fresh (a b c)
    (ino a (list 1 2 3)) (ino b (list 1 2 3)) (ino c (list 1 2 3))
    (all-distincto (list a b c)))

enumerates all 6 distinct triples from {1, 2, 3}. Full CLP(FD) with
arc-consistency, fd-plus, etc. remains pending under Phase 6 proper.

9 new tests, 237/237 cumulative.
2026-05-08 07:56:58 +00:00
bc9261e90a mk: matche keyword pattern fix + classic puzzles
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
matche-pattern->expr now treats keyword patterns as literals that emit
themselves bare, rather than wrapping in (quote ...). SX keywords
self-evaluate to their string name; quoting them flips them to a
keyword type that does not unify with the bare-keyword usage at the
target site. This was visible only as a test failure on the diffo
clauses below — tightened the pattern rules.

tests/classics.sx exercises three end-to-end miniKanren programs:
  - 3-friend / 3-pet permutation puzzle
  - grandparent inference over a fact list (membero + fresh)
  - symbolic differentiation dispatched by matche on
    :x / (:+ a b) / (:* a b)

228/228 cumulative.
2026-05-08 07:50:03 +00:00
fd73f3c51b mk: phase 5D — matche pattern matching, phase 5 complete
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Pattern grammar: _, symbol, atom (number/string/keyword/bool), (), and
(p1 ... pn) list patterns (recursive). Symbols become fresh vars in a
fresh form, atoms become literals to unify against, lists recurse
position-wise. Repeated names produce the same fresh var (so they
unify by ==).

Macro is built with explicit cons/list rather than a quasiquote because
the quasiquote expander does not recurse into nested lambda bodies —
the natural `\`(matche-clause (quote ,target) cl)` spelling left
literal `(unquote target)` forms in the output.

14 tests, 222/222 cumulative. Phase 5 done (project, conda, condu,
onceo, nafc, matche all green).
2026-05-08 07:41:51 +00:00
b8a0c504bc mk: phase 4C — permuteo (with inserto helper)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 58s
inserto a l p: p is l with a inserted at some position. Recursive: head
of l first, then push past head and recurse.

permuteo l p: classical recursive permutation. Empty -> empty; otherwise
take a head off l, recursively permute the tail, insert head at any
position in the recursive result.

7 new tests including all-6-perms-of-3 as a set check (independent of
generation order). 208/208 cumulative.
2026-05-08 07:22:41 +00:00
a038d41815 mk: phase 5C — nafc, negation as finite failure
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
(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.
2026-05-07 23:29:08 +00:00
d61b355413 mk: phase 5B — project, escape into host SX
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 56s
(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.
2026-05-07 23:27:16 +00:00
43d58e6ca9 mk: peano arithmetic (zeroo, pluso, minuso, *o, lteo, lto)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
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.
2026-05-07 21:54:16 +00:00
240ed90b20 mk: phase 5A — conda, soft-cut without onceo
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
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.
2026-05-07 21:51:52 +00:00
f4ab7f2534 mk: phase 4B — reverseo + lengtho, 10 new tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
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.
2026-05-07 21:49:38 +00:00
cae87c1e2c mk: phase 4A — appendo canary green, both directions
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
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.
2026-05-07 20:24:42 +00:00
52070e07fc mk: phase 3 — run* / run / reify, 18 new tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
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.
2026-05-07 20:03:42 +00:00
2de6727e83 mk: phase 2D — condu + onceo, phase 2 complete
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
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.
2026-05-07 20:01:10 +00:00
c754a8ee05 mk: phase 2C — conde, the canonical and-or sugar
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 50s
conde.sx is a single defmacro: (conde (g1a g1b ...) (g2a g2b ...) ...) folds
to (mk-disj (mk-conj g1a g1b ...) (mk-conj g2a g2b ...) ...). 9 tests cover
single/multi-clause, mixed success/failure, conjunction inside clauses,
fresh+disj inside a clause, nesting, and all-fail / no-clauses.

100/100 cumulative.
2026-05-07 19:59:17 +00:00
f43ad04f91 mk: phase 2B — fresh, defmacro form + call-fresh
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
(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.
2026-05-07 19:56:40 +00:00
0ba60d6a25 mk: phase 2A — streams + ==/conj/disj, 34 new tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 57s
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).
2026-05-07 19:54:43 +00:00
f13e03e625 mk: phase 1 — unify.sx + 48 tests, kit-driven
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
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.
2026-05-07 19:45:47 +00:00
70 changed files with 5407 additions and 48 deletions

42
lib/minikanren/conda.sx Normal file
View File

@@ -0,0 +1,42 @@
;; lib/minikanren/conda.sx — Phase 5 piece A: `conda`, the soft-cut.
;;
;; (conda (g0 g ...) (h0 h ...) ...)
;; — first clause whose head g0 produces ANY answer wins; ALL of g0's
;; answers are then conj'd with the rest of that clause; later
;; clauses are NOT tried.
;; — differs from condu only in not wrapping g0 in onceo: condu
;; commits to the SINGLE first answer, conda lets the head's full
;; answer-set flow into the rest of the clause.
;; (Reasoned Schemer chapter 10; Byrd 5.3.)
(define
conda-try
(fn
(clauses s)
(cond
((empty? clauses) mzero)
(:else
(let
((cl (first clauses)))
(let
((head-goal (first cl)) (rest-goals (rest cl)))
(let
((peek (stream-take 1 (head-goal s))))
(if
(empty? peek)
(conda-try (rest clauses) s)
(mk-bind (head-goal s) (mk-conj-list rest-goals))))))))))
(defmacro
conda
(&rest clauses)
(quasiquote
(fn
(s)
(conda-try
(list
(splice-unquote
(map
(fn (cl) (quasiquote (list (splice-unquote cl))))
clauses)))
s))))

39
lib/minikanren/conde.sx Normal file
View File

@@ -0,0 +1,39 @@
;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
;; miniKanren and-or form, with implicit Zzz inverse-eta delay so recursive
;; relations like appendo terminate.
;;
;; (conde (g1a g1b ...) (g2a g2b ...) ...)
;; ≡ (mk-disj (Zzz (mk-conj g1a g1b ...))
;; (Zzz (mk-conj g2a g2b ...)) ...)
;;
;; `Zzz g` wraps a goal expression in (fn (S) (fn () (g S))) so that
;; `g`'s body isn't constructed until the surrounding fn is applied to a
;; substitution AND the returned thunk is forced. This is what gives
;; miniKanren its laziness — recursive goal definitions can be `(conde
;; ... (... (recur ...)))` without infinite descent at construction time.
;;
;; Hygiene: the substitution parameter is gensym'd so that user goal
;; expressions which themselves bind `s` (e.g. `(appendo l s ls)`) keep
;; their lexical `s` and don't accidentally reference the wrapper's
;; substitution. Without gensym, miniKanren relations that follow the
;; common (l s ls) parameter convention are silently miscompiled.
(defmacro
Zzz
(g)
(let
((s-sym (gensym "zzz-s-")))
(quasiquote
(fn ((unquote s-sym)) (fn () ((unquote g) (unquote s-sym)))))))
(defmacro
conde
(&rest clauses)
(quasiquote
(mk-disj
(splice-unquote
(map
(fn
(clause)
(quasiquote (Zzz (mk-conj (splice-unquote clause)))))
clauses)))))

58
lib/minikanren/condu.sx Normal file
View File

@@ -0,0 +1,58 @@
;; lib/minikanren/condu.sx — Phase 2 piece D: `condu` and `onceo`.
;;
;; Both are commitment forms (no backtracking into discarded options):
;;
;; (onceo g) — succeeds at most once: takes the first answer
;; stream-take produces from (g s).
;;
;; (condu (g0 g ...) (h0 h ...) ...)
;; — first clause whose head goal succeeds wins; only
;; the first answer of the head is propagated to the
;; rest of that clause; later clauses are not tried.
;; (Reasoned Schemer chapter 10; Byrd 5.4.)
(define
onceo
(fn
(g)
(fn
(s)
(let
((peek (stream-take 1 (g s))))
(if (empty? peek) mzero (unit (first peek)))))))
;; condu-try — runtime walker over a list of clauses (each clause a list of
;; goals). Forces the head with stream-take 1; if head fails, recurse to
;; the next clause; if head succeeds, commits its single answer through
;; the rest of the clause.
(define
condu-try
(fn
(clauses s)
(cond
((empty? clauses) mzero)
(:else
(let
((cl (first clauses)))
(let
((head-goal (first cl)) (rest-goals (rest cl)))
(let
((peek (stream-take 1 (head-goal s))))
(if
(empty? peek)
(condu-try (rest clauses) s)
((mk-conj-list rest-goals) (first peek))))))))))
(defmacro
condu
(&rest clauses)
(quasiquote
(fn
(s)
(condu-try
(list
(splice-unquote
(map
(fn (cl) (quasiquote (list (splice-unquote cl))))
clauses)))
s))))

25
lib/minikanren/defrel.sx Normal file
View File

@@ -0,0 +1,25 @@
;; lib/minikanren/defrel.sx — Prolog-style defrel macro.
;;
;; (defrel (NAME ARG1 ARG2 ...)
;; (CLAUSE1 ...)
;; (CLAUSE2 ...)
;; ...)
;;
;; expands to
;;
;; (define NAME (fn (ARG1 ARG2 ...) (conde (CLAUSE1 ...) (CLAUSE2 ...))))
;;
;; This puts each clause's goals immediately after the head, mirroring
;; Prolog's `name(Args) :- goals.` shape. Clauses are conde-conjoined
;; goals — `Zzz`-wrapping is automatic via `conde`, so recursive
;; relations terminate on partial answers.
(defmacro
defrel
(head &rest clauses)
(let
((name (first head)) (args (rest head)))
(list
(quote define)
name
(list (quote fn) args (cons (quote conde) clauses)))))

25
lib/minikanren/fd.sx Normal file
View File

@@ -0,0 +1,25 @@
;; lib/minikanren/fd.sx — Phase 6 piece A: minimal finite-domain helpers.
;;
;; A full CLP(FD) engine (arc consistency, native integer domains, fd-plus
;; etc.) is Phase 6 proper. For now we expose two small relations layered
;; on the existing list machinery — they're sufficient for permutation
;; puzzles, the N-queens-style core of constraint solving:
;;
;; (ino x dom) — x is a member of dom (alias for membero with the
;; constraint-store-friendly argument order).
;; (all-distincto l) — all elements of l are pairwise distinct.
;;
;; all-distincto uses nafc + membero on the tail — it requires the head
;; element of each recursive step to be ground enough for membero to be
;; finitary, so order matters: prefer (in x dom) goals BEFORE
;; (all-distincto (list x ...)) so values get committed first.
(define ino (fn (x dom) (membero x dom)))
(define
all-distincto
(fn
(l)
(conde
((nullo l))
((fresh (a d) (conso a d l) (nafc (membero a d)) (all-distincto d))))))

23
lib/minikanren/fresh.sx Normal file
View File

@@ -0,0 +1,23 @@
;; lib/minikanren/fresh.sx — Phase 2 piece B: `fresh` for introducing
;; logic variables inside a goal body.
;;
;; (fresh (x y z) goal1 goal2 ...)
;; ≡ (let ((x (make-var)) (y (make-var)) (z (make-var)))
;; (mk-conj goal1 goal2 ...))
;;
;; A macro rather than a function so user-named vars are real lexical
;; bindings — which is also what miniKanren convention expects.
;; The empty-vars form (fresh () goal ...) is just a goal grouping.
(defmacro
fresh
(vars &rest goals)
(quasiquote
(let
(unquote (map (fn (v) (list v (list (quote make-var)))) vars))
(mk-conj (splice-unquote goals)))))
;; call-fresh — functional alternative for code that builds goals
;; programmatically:
;; ((call-fresh (fn (x) (== x 7))) empty-s) → ({:_.N 7})
(define call-fresh (fn (f) (fn (s) ((f (make-var)) s))))

58
lib/minikanren/goals.sx Normal file
View File

@@ -0,0 +1,58 @@
;; lib/minikanren/goals.sx — Phase 2 piece B: core goals.
;;
;; A goal is a function (fn (s) → stream-of-substitutions).
;; Goals built here:
;; succeed — always returns (unit s)
;; fail — always returns mzero
;; == — unifies two terms; succeeds with a singleton, else fails
;; ==-check — opt-in occurs-checked equality
;; conj2 / mk-conj — sequential conjunction of goals
;; disj2 / mk-disj — interleaved disjunction of goals (raw — `conde` adds
;; the implicit-conj-per-clause sugar in a later commit)
(define succeed (fn (s) (unit s)))
(define fail (fn (s) mzero))
(define
==
(fn
(u v)
(fn
(s)
(let ((s2 (mk-unify u v s))) (if (= s2 nil) mzero (unit s2))))))
(define
==-check
(fn
(u v)
(fn
(s)
(let ((s2 (mk-unify-check u v s))) (if (= s2 nil) mzero (unit s2))))))
(define conj2 (fn (g1 g2) (fn (s) (mk-bind (g1 s) g2))))
(define disj2 (fn (g1 g2) (fn (s) (mk-mplus (g1 s) (g2 s)))))
;; Fold goals in a list. (mk-conj-list ()) ≡ succeed; (mk-disj-list ()) ≡ fail.
(define
mk-conj-list
(fn
(gs)
(cond
((empty? gs) succeed)
((empty? (rest gs)) (first gs))
(:else (conj2 (first gs) (mk-conj-list (rest gs)))))))
(define
mk-disj-list
(fn
(gs)
(cond
((empty? gs) fail)
((empty? (rest gs)) (first gs))
(:else (disj2 (first gs) (mk-disj-list (rest gs)))))))
(define mk-conj (fn (&rest gs) (mk-conj-list gs)))
(define mk-disj (fn (&rest gs) (mk-disj-list gs)))

129
lib/minikanren/intarith.sx Normal file
View File

@@ -0,0 +1,129 @@
;; lib/minikanren/intarith.sx — fast integer arithmetic via project.
;;
;; These are ground-only escapes into host arithmetic. They run at native
;; speed (host ints) but require their arguments to walk to actual numbers
;; — they are not relational the way `pluso` (Peano) is. Use them when
;; the puzzle size makes Peano impractical.
;;
;; Naming: `-i` suffix marks "integer-only" goals.
(define
pluso-i
(fn
(a b c)
(project
(a b)
(if (and (number? a) (number? b)) (== c (+ a b)) fail))))
(define
minuso-i
(fn
(a b c)
(project
(a b)
(if (and (number? a) (number? b)) (== c (- a b)) fail))))
(define
*o-i
(fn
(a b c)
(project
(a b)
(if (and (number? a) (number? b)) (== c (* a b)) fail))))
(define
lto-i
(fn
(a b)
(project
(a b)
(if (and (number? a) (and (number? b) (< a b))) succeed fail))))
(define
lteo-i
(fn
(a b)
(project
(a b)
(if (and (number? a) (and (number? b) (<= a b))) succeed fail))))
(define
neqo-i
(fn
(a b)
(project
(a b)
(if (and (number? a) (and (number? b) (not (= a b)))) succeed fail))))
(define numbero (fn (x) (project (x) (if (number? x) succeed fail))))
(define stringo (fn (x) (project (x) (if (string? x) succeed fail))))
(define symbolo (fn (x) (project (x) (if (symbol? x) succeed fail))))
(define
even-i
(fn (n) (project (n) (if (and (number? n) (even? n)) succeed fail))))
(define
odd-i
(fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))
(define
sortedo
(fn
(l)
(conde
((nullo l))
((fresh (a) (== l (list a))))
((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid))))))
(define
mino
(fn
(l m)
(conde
((fresh (a) (== l (list a)) (== m a)))
((fresh (a d rest-min) (conso a d l) (mino d rest-min) (conde ((lteo-i a rest-min) (== m a)) ((lto-i rest-min a) (== m rest-min))))))))
(define
maxo
(fn
(l m)
(conde
((fresh (a) (== l (list a)) (== m a)))
((fresh (a d rest-max) (conso a d l) (maxo d rest-max) (conde ((lteo-i rest-max a) (== m a)) ((lto-i a rest-max) (== m rest-max))))))))
(define
sumo
(fn
(l total)
(conde
((nullo l) (== total 0))
((fresh (a d rest-sum) (conso a d l) (sumo d rest-sum) (pluso-i a rest-sum total))))))
(define
producto
(fn
(l total)
(conde
((nullo l) (== total 1))
((fresh (a d rest-prod) (conso a d l) (producto d rest-prod) (*o-i a rest-prod total))))))
(define
lengtho-i
(fn
(l n)
(conde
((nullo l) (== n 0))
((fresh (a d n-1) (conso a d l) (lengtho-i d n-1) (pluso-i 1 n-1 n))))))
(define
enumerate-from-i
(fn
(start l result)
(conde
((nullo l) (nullo result))
((fresh (a d r-rest start-prime) (conso a d l) (conso (list start a) r-rest result) (pluso-i 1 start start-prime) (enumerate-from-i start-prime d r-rest))))))
(define enumerate-i (fn (l result) (enumerate-from-i 0 l result)))

76
lib/minikanren/matche.sx Normal file
View File

@@ -0,0 +1,76 @@
;; lib/minikanren/matche.sx — Phase 5 piece D: pattern matching over terms.
;;
;; (matche TARGET
;; (PATTERN1 g1 g2 ...)
;; (PATTERN2 g1 ...)
;; ...)
;;
;; Pattern grammar:
;; _ wildcard — fresh anonymous var
;; x plain symbol — fresh var, bind by name
;; ATOM literal (number, string, boolean) — must equal
;; :keyword keyword literal — emitted bare (keywords self-evaluate
;; to their string name in SX, so quoting them changes
;; their type from string to keyword)
;; () empty list — must equal
;; (p1 p2 ... pn) list pattern — recurse on each element
;;
;; The macro expands to a `conde` whose clauses are
;; `((fresh (vars-in-pat) (== target pat-expr) body...))`.
;;
;; Repeated symbol names within a pattern produce the same fresh var, so
;; they unify by `==`. Fixed-length list patterns only — head/tail
;; destructuring uses `(fresh (a d) (conso a d target) body)` directly.
;;
;; Note: the macro builds the expansion via `cons` / `list` rather than a
;; quasiquote — quasiquote does not recurse into nested lambda bodies in
;; SX, so `\`(matche-clause (quote ,target) cl)` left literal
;; `(unquote target)` in the output.
(define matche-symbol-var? (fn (s) (symbol? s)))
(define
matche-collect-vars-acc
(fn
(pat acc)
(cond
((matche-symbol-var? pat)
(if (some (fn (s) (= s pat)) acc) acc (append acc (list pat))))
((and (list? pat) (not (empty? pat)))
(reduce (fn (a p) (matche-collect-vars-acc p a)) acc pat))
(:else acc))))
(define
matche-collect-vars
(fn (pat) (matche-collect-vars-acc pat (list))))
(define
matche-pattern->expr
(fn
(pat)
(cond
((matche-symbol-var? pat) pat)
((and (list? pat) (empty? pat)) (list (quote list)))
((list? pat) (cons (quote list) (map matche-pattern->expr pat)))
((keyword? pat) pat)
(:else (list (quote quote) pat)))))
(define
matche-clause
(fn
(target cl)
(let
((pat (first cl)) (body (rest cl)))
(let
((vars (matche-collect-vars pat)))
(let
((pat-expr (matche-pattern->expr pat)))
(list
(cons
(quote fresh)
(cons vars (cons (list (quote ==) target pat-expr) body)))))))))
(defmacro
matche
(target &rest clauses)
(cons (quote conde) (map (fn (cl) (matche-clause target cl)) clauses)))

24
lib/minikanren/nafc.sx Normal file
View File

@@ -0,0 +1,24 @@
;; lib/minikanren/nafc.sx — Phase 5 piece C: negation as finite failure.
;;
;; (nafc g)
;; succeeds (yields the input substitution) if g has zero answers
;; against that substitution; fails (mzero) if g has at least one.
;;
;; Caveat: `nafc` is unsound under the open-world assumption. It only
;; makes sense for goals over fully-ground terms, or with the explicit
;; understanding that adding more facts could flip the answer. Use
;; `(project (...) ...)` to ensure the relevant vars are ground first.
;;
;; Caveat 2: stream-take forces g for at least one answer; if g is
;; infinitely-ground (say, a divergent search over an unbound list),
;; nafc itself will diverge. Standard miniKanren limitation.
(define
nafc
(fn
(g)
(fn
(s)
(let
((peek (stream-take 1 (g s))))
(if (empty? peek) (unit s) mzero)))))

51
lib/minikanren/peano.sx Normal file
View File

@@ -0,0 +1,51 @@
;; lib/minikanren/peano.sx — Peano-encoded natural-number relations.
;;
;; Same encoding as `lengtho`: zero is the keyword `:z`; successors are
;; `(:s n)`. So 3 = `(:s (:s (:s :z)))`. `(:z)` and `(:s ...)` are normal
;; SX values that unify positionally — no special primitives needed.
;;
;; Peano arithmetic is the canonical miniKanren way to test addition /
;; multiplication / less-than relationally without an FD constraint store.
;; (CLP(FD) integers come in Phase 6.)
(define zeroo (fn (n) (== n :z)))
(define succ-of (fn (n m) (== m (list :s n))))
(define
pluso
(fn
(a b c)
(conde
((== a :z) (== b c))
((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (pluso a-1 b c-1))))))
(define minuso (fn (a b c) (pluso b c a)))
(define lteo (fn (a b) (fresh (k) (pluso a k b))))
(define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b))))
(define
eveno
(fn
(n)
(conde
((== n :z))
((fresh (m) (== n (list :s (list :s m))) (eveno m))))))
(define
oddo
(fn
(n)
(conde
((== n (list :s :z)))
((fresh (m) (== n (list :s (list :s m))) (oddo m))))))
(define
*o
(fn
(a b c)
(conde
((== a :z) (== c :z))
((fresh (a-1 ab-1) (== a (list :s a-1)) (*o a-1 b ab-1) (pluso b ab-1 c))))))

25
lib/minikanren/project.sx Normal file
View File

@@ -0,0 +1,25 @@
;; lib/minikanren/project.sx — Phase 5 piece B: `project`.
;;
;; (project (x y) g1 g2 ...)
;; — rebinds each named var to (mk-walk* var s) within the body's
;; lexical scope, then runs the conjunction of the body goals on
;; the same substitution. Use to escape into regular SX (arithmetic,
;; string ops, host predicates) when you need a ground value.
;;
;; If any of the projected vars is still unbound at this point, the body
;; sees the raw `(:var NAME)` term — that is intentional and lets you
;; mix project with `(== ground? var)` patterns or with conda guards.
;;
;; Hygiene: substitution parameter is gensym'd so it doesn't capture user
;; vars (`s` is a popular relation parameter name).
(defmacro
project
(vars &rest goals)
(let
((s-sym (gensym "proj-s-")))
(quasiquote
(fn
((unquote s-sym))
((let (unquote (map (fn (v) (list v (list (quote mk-walk*) v s-sym))) vars)) (mk-conj (splice-unquote goals)))
(unquote s-sym))))))

67
lib/minikanren/queens.sx Normal file
View File

@@ -0,0 +1,67 @@
;; lib/minikanren/queens.sx — N-queens via ino + all-distincto + project.
;;
;; Encoding: q = (c1 c2 ... cn) where ci is the column of the queen in
;; row i. Each ci ∈ {1..n}; all distinct (no two queens share a column);
;; no two queens on the same diagonal (|ci - cj| ≠ |i - j| for i ≠ j).
;;
;; The diagonal check uses `project` to escape into host arithmetic
;; once both column values are ground.
(define
safe-diag
(fn
(a b dist)
(project (a b) (if (= (abs (- a b)) dist) fail succeed))))
(define
safe-cell-vs-rest
(fn
(c c-row others next-row)
(cond
((empty? others) succeed)
(:else
(mk-conj
(safe-diag c (first others) (- next-row c-row))
(safe-cell-vs-rest c c-row (rest others) (+ next-row 1)))))))
(define
all-cells-safe
(fn
(cols start-row)
(cond
((empty? cols) succeed)
(:else
(mk-conj
(safe-cell-vs-rest
(first cols)
start-row
(rest cols)
(+ start-row 1))
(all-cells-safe (rest cols) (+ start-row 1)))))))
(define
range-1-to-n
(fn
(n)
(cond
((= n 0) (list))
(:else (append (range-1-to-n (- n 1)) (list n))))))
(define
ino-each
(fn
(cols dom)
(cond
((empty? cols) succeed)
(:else (mk-conj (ino (first cols) dom) (ino-each (rest cols) dom))))))
(define
queens-cols
(fn
(cols n)
(let
((dom (range-1-to-n n)))
(mk-conj
(ino-each cols dom)
(all-distincto cols)
(all-cells-safe cols 1)))))

305
lib/minikanren/relations.sx Normal file
View File

@@ -0,0 +1,305 @@
;; lib/minikanren/relations.sx — Phase 4 standard relations.
;;
;; Programs use native SX lists as data. Relations decompose lists via the
;; tagged cons-cell shape `(:cons h t)` because SX has no improper pairs;
;; the unifier treats `(:cons h t)` and the native list `(h . t)` as
;; equivalent, and `mk-walk*` flattens cons cells back to flat lists for
;; reification.
;; --- pair / list shape relations ---
(define nullo (fn (l) (== l (list))))
(define pairo (fn (p) (fresh (a d) (== p (mk-cons a d)))))
(define caro (fn (p a) (fresh (d) (== p (mk-cons a d)))))
(define cdro (fn (p d) (fresh (a) (== p (mk-cons a d)))))
(define conso (fn (a d p) (== p (mk-cons a d))))
(define firsto caro)
(define resto cdro)
(define
listo
(fn (l) (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo d))))))
;; --- appendo: the canary ---
;;
;; (appendo l s ls) — `ls` is the concatenation of `l` and `s`.
;; Runs forwards (l, s known → ls), backwards (ls known → all (l, s) pairs),
;; and bidirectionally (mix of bound + unbound).
(define
appendo
(fn
(l s ls)
(conde
((nullo l) (== s ls))
((fresh (a d res) (conso a d l) (conso a res ls) (appendo d s res))))))
;; --- membero ---
;; (membero x l) — x appears (at least once) in l.
(define
appendo3
(fn
(l1 l2 l3 result)
(fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result))))
(define
partitiono
(fn
(pred l yes no)
(conde
((nullo l) (nullo yes) (nullo no))
((fresh (a d y-rest n-rest) (conso a d l) (conde ((pred a) (conso a y-rest yes) (== no n-rest) (partitiono pred d y-rest n-rest)) ((nafc (pred a)) (== yes y-rest) (conso a n-rest no) (partitiono pred d y-rest n-rest))))))))
(define
membero
(fn
(x l)
(conde
((fresh (d) (conso x d l)))
((fresh (a d) (conso a d l) (membero x d))))))
(define
not-membero
(fn
(x l)
(conde
((nullo l))
((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d))))))
(define
subseto
(fn
(l1 l2)
(conde
((nullo l1))
((fresh (a d) (conso a d l1) (membero a l2) (subseto d l2))))))
(define
reverseo
(fn
(l r)
(conde
((nullo l) (nullo r))
((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
(define
rev-acco
(fn
(l acc result)
(conde
((nullo l) (== result acc))
((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result))))))
(define rev-2o (fn (l result) (rev-acco l (list) result)))
(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
(define prefixo (fn (p l) (fresh (rest) (appendo p rest l))))
(define suffixo (fn (s l) (fresh (front) (appendo front s l))))
(define
subo
(fn
(s l)
(fresh
(front-and-s back front)
(appendo front-and-s back l)
(appendo front s front-and-s))))
(define
selecto
(fn
(x rest l)
(conde
((conso x rest l))
((fresh (a d r) (conso a d l) (conso a r rest) (selecto x r d))))))
(define
lengtho
(fn
(l n)
(conde
((nullo l) (== n :z))
((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))
(define
inserto
(fn
(a l p)
(conde
((conso a l p))
((fresh (h t pt) (conso h t l) (conso h pt p) (inserto a t pt))))))
(define
permuteo
(fn
(l p)
(conde
((nullo l) (nullo p))
((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))
(define
flatteno
(fn
(tree flat)
(conde
((nullo tree) (nullo flat))
((pairo tree)
(fresh
(h t hf tf)
(conso h t tree)
(flatteno h hf)
(flatteno t tf)
(appendo hf tf flat)))
((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
(define
rembero
(fn
(x l out)
(conde
((nullo l) (nullo out))
((fresh (a d) (conso a d l) (== a x) (== out d)))
((fresh (a d res) (conso a d l) (nafc (== a x)) (conso a res out) (rembero x d res))))))
(define
removeo-allo
(fn
(x l result)
(conde
((nullo l) (nullo result))
((fresh (a d) (conso a d l) (== a x) (removeo-allo x d result)))
((fresh (a d r-rest) (conso a d l) (nafc (== a x)) (conso a r-rest result) (removeo-allo x d r-rest))))))
(define
assoco
(fn
(key pairs val)
(fresh
(rest)
(conde
((conso (list key val) rest pairs))
((fresh (other) (conso other rest pairs) (assoco key rest val)))))))
(define
nth-o
(fn
(n l elem)
(conde
((== n :z) (fresh (d) (conso elem d l)))
((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (nth-o n-1 d elem))))))
(define
samelengtho
(fn
(l1 l2)
(conde
((nullo l1) (nullo l2))
((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (samelengtho d d-prime))))))
(define
mapo
(fn
(rel l1 l2)
(conde
((nullo l1) (nullo l2))
((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (rel a a-prime) (mapo rel d d-prime))))))
(define
iterate-no
(fn
(rel n x result)
(conde
((== n :z) (== result x))
((fresh (n-1 mid) (== n (list :s n-1)) (rel x mid) (iterate-no rel n-1 mid result))))))
(define
pairlisto
(fn
(l1 l2 pairs)
(conde
((nullo l1) (nullo l2) (nullo pairs))
((fresh (a1 d1 a2 d2 d-pairs) (conso a1 d1 l1) (conso a2 d2 l2) (conso (list a1 a2) d-pairs pairs) (pairlisto d1 d2 d-pairs))))))
(define
swap-firsto
(fn
(l result)
(fresh
(a b rest mid-l mid-r)
(conso a mid-l l)
(conso b rest mid-l)
(conso b mid-r result)
(conso a rest mid-r))))
(define
everyo
(fn
(rel l)
(conde
((nullo l))
((fresh (a d) (conso a d l) (rel a) (everyo rel d))))))
(define
someo
(fn
(rel l)
(conde
((fresh (a d) (conso a d l) (rel a)))
((fresh (a d) (conso a d l) (someo rel d))))))
(define
lasto
(fn
(l x)
(conde
((conso x (list) l))
((fresh (a d) (conso a d l) (lasto d x))))))
(define
init-o
(fn
(l init)
(conde
((fresh (x) (conso x (list) l) (== init (list))))
((fresh (a d d-init) (conso a d l) (conso a d-init init) (init-o d d-init))))))
(define
tako
(fn
(n l prefix)
(conde
((== n :z) (== prefix (list)))
((fresh (n-1 a d p-rest) (== n (list :s n-1)) (conso a d l) (conso a p-rest prefix) (tako n-1 d p-rest))))))
(define
dropo
(fn
(n l suffix)
(conde
((== n :z) (== suffix l))
((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (dropo n-1 d suffix))))))
(define
repeato
(fn
(x n result)
(conde
((== n :z) (== result (list)))
((fresh (n-1 r-rest) (== n (list :s n-1)) (conso x r-rest result) (repeato x n-1 r-rest))))))
(define
concato
(fn
(lists result)
(conde
((nullo lists) (nullo result))
((fresh (h t r-rest) (conso h t lists) (appendo h r-rest result) (concato t r-rest))))))

56
lib/minikanren/run.sx Normal file
View File

@@ -0,0 +1,56 @@
;; lib/minikanren/run.sx — Phase 3: drive a goal + reify the query var.
;;
;; reify-name N — make the canonical "_.N" reified symbol.
;; reify-s term rs — walk term in rs, add a mapping from each fresh
;; unbound var to its _.N name (left-to-right order).
;; reify q s — walk* q in s, build reify-s, walk* again to
;; substitute reified names in.
;; run-n n q-name g... — defmacro: bind q-name to a fresh var, conj goals,
;; take ≤ n answers from the stream, reify each
;; through q-name. n = -1 takes all (used by run*).
;; run* — defmacro: (run* q g...) ≡ (run-n -1 q g...)
;; run — defmacro: (run n q g...) ≡ (run-n n q g...)
;; The two-segment form is the standard TRS API.
(define reify-name (fn (n) (make-symbol (str "_." n))))
(define
reify-s
(fn
(term rs)
(let
((w (mk-walk term rs)))
(cond
((is-var? w) (extend (var-name w) (reify-name (len rs)) rs))
((mk-list-pair? w) (reduce (fn (acc a) (reify-s a acc)) rs w))
(:else rs)))))
(define
reify
(fn
(term s)
(let
((w (mk-walk* term s)))
(let ((rs (reify-s w (empty-subst)))) (mk-walk* w rs)))))
(defmacro
run-n
(n q-name &rest goals)
(quasiquote
(let
(((unquote q-name) (make-var)))
(map
(fn (s) (reify (unquote q-name) s))
(stream-take
(unquote n)
((mk-conj (splice-unquote goals)) empty-s))))))
(defmacro
run*
(q-name &rest goals)
(quasiquote (run-n -1 (unquote q-name) (splice-unquote goals))))
(defmacro
run
(n q-name &rest goals)
(quasiquote (run-n (unquote n) (unquote q-name) (splice-unquote goals))))

66
lib/minikanren/stream.sx Normal file
View File

@@ -0,0 +1,66 @@
;; lib/minikanren/stream.sx — Phase 2 piece A: lazy streams of substitutions.
;;
;; SX has no improper pairs (cons requires a list cdr), so we use a
;; tagged stream-cell shape for mature stream elements:
;;
;; stream ::= mzero empty (the SX empty list)
;; | (:s HEAD TAIL) mature cell, TAIL is a stream
;; | thunk (fn () ...) → stream when forced
;;
;; HEAD is a substitution dict. TAIL is again a stream (possibly a thunk),
;; which is what gives us laziness — mk-mplus can return a mature head with
;; a thunk in the tail, deferring the rest of the search.
(define mzero (list))
(define s-cons (fn (h t) (list :s h t)))
(define
s-cons?
(fn (s) (and (list? s) (not (empty? s)) (= (first s) :s))))
(define s-car (fn (s) (nth s 1)))
(define s-cdr (fn (s) (nth s 2)))
(define unit (fn (s) (s-cons s mzero)))
(define stream-pause? (fn (s) (and (not (list? s)) (callable? s))))
;; mk-mplus — interleave two streams. If s1 is paused we suspend and
;; swap (Reasoned Schemer "interleave"); otherwise mature-cons head with
;; mk-mplus of the rest.
(define
mk-mplus
(fn
(s1 s2)
(cond
((empty? s1) s2)
((stream-pause? s1) (fn () (mk-mplus s2 (s1))))
(:else (s-cons (s-car s1) (mk-mplus (s-cdr s1) s2))))))
;; mk-bind — apply goal g to every substitution in stream s, mk-mplus-ing.
(define
mk-bind
(fn
(s g)
(cond
((empty? s) mzero)
((stream-pause? s) (fn () (mk-bind (s) g)))
(:else (mk-mplus (g (s-car s)) (mk-bind (s-cdr s) g))))))
;; stream-take — force up to n results out of a (possibly lazy) stream
;; into a flat SX list of substitutions. n = -1 means take all.
(define
stream-take
(fn
(n s)
(cond
((= n 0) (list))
((empty? s) (list))
((stream-pause? s) (stream-take n (s)))
(:else
(cons
(s-car s)
(stream-take
(if (= n -1) -1 (- n 1))
(s-cdr s)))))))

View File

@@ -0,0 +1,49 @@
;; lib/minikanren/tests/appendo3.sx — 3-list append.
(mk-test
"appendo3-forward"
(run*
q
(appendo3
(list 1 2)
(list 3 4)
(list 5 6)
q))
(list
(list 1 2 3 4 5 6)))
(mk-test
"appendo3-empty-everything"
(run* q (appendo3 (list) (list) (list) q))
(list (list)))
(mk-test
"appendo3-recover-middle"
(run*
q
(appendo3
(list 1 2)
q
(list 5 6)
(list 1 2 3 4 5 6)))
(list (list 3 4)))
(mk-test
"appendo3-empty-middle"
(run*
q
(appendo3
(list 1 2)
(list)
(list 3 4)
q))
(list (list 1 2 3 4)))
(mk-test
"appendo3-empty-first-and-last"
(run*
q
(appendo3 (list) (list 1 2 3) (list) q))
(list (list 1 2 3)))
(mk-tests-run!)

View File

@@ -0,0 +1,54 @@
;; lib/minikanren/tests/btree-walko.sx — walk a leaves-of-binary-tree relation
;; using matche dispatch on (:leaf v) and (:node left right) patterns.
(define
btree-walko
(fn
(tree v)
(matche
tree
((:leaf x) (== v x))
((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))))
;; A small test tree: ((1 2) (3 (4 5))).
(define
test-btree
(list
:node (list :node (list :leaf 1) (list :leaf 2))
(list
:node (list :leaf 3)
(list :node (list :leaf 4) (list :leaf 5)))))
(mk-test
"btree-walko-enumerates-all-leaves"
(let
((leaves (run* q (btree-walko test-btree q))))
(and
(= (len leaves) 5)
(and
(some (fn (l) (= l 1)) leaves)
(and
(some (fn (l) (= l 2)) leaves)
(and
(some (fn (l) (= l 3)) leaves)
(and
(some (fn (l) (= l 4)) leaves)
(some (fn (l) (= l 5)) leaves)))))))
true)
(mk-test
"btree-walko-find-3-membership"
(run 1 q (btree-walko test-btree 3))
(list (make-symbol "_.0")))
(mk-test
"btree-walko-find-99-not-present"
(run* q (btree-walko test-btree 99))
(list))
(mk-test
"btree-walko-leaf-only"
(run* q (btree-walko (list :leaf 42) q))
(list 42))
(mk-tests-run!)

View File

@@ -0,0 +1,87 @@
;; lib/minikanren/tests/classics.sx — small classic-style puzzles that
;; exercise the full system end to end (relations + conde + matche +
;; fresh + run*). Each test is a self-contained miniKanren program.
;; -----------------------------------------------------------------------
;; Pet puzzle (3 friends, 3 pets, 1-each).
;; -----------------------------------------------------------------------
(mk-test
"classics-pet-puzzle"
(run*
q
(fresh
(a b c)
(== q (list a b c))
(permuteo (list :dog :cat :fish) (list a b c))
(== b :fish)
(conde ((== a :cat)) ((== a :fish)))))
(list (list :cat :fish :dog)))
;; -----------------------------------------------------------------------
;; Family-relations puzzle (uses membero on a fact list).
;; -----------------------------------------------------------------------
(define
parent-facts
(list
(list "alice" "bob")
(list "alice" "carol")
(list "bob" "dave")
(list "carol" "eve")
(list "dave" "frank")))
(define parento (fn (x y) (membero (list x y) parent-facts)))
(define grandparento (fn (x z) (fresh (y) (parento x y) (parento y z))))
(mk-test
"classics-grandparents-of-frank"
(run* q (grandparento q "frank"))
(list "bob"))
(mk-test
"classics-grandchildren-of-alice"
(run* q (grandparento "alice" q))
(list "dave" "eve"))
;; -----------------------------------------------------------------------
;; Symbolic differentiation, matche-driven.
;; Variable :x: d/dx x = 1
;; Sum (:+ a b): d/dx (a+b) = (da + db)
;; Product (:* a b): d/dx (a*b) = (da*b + a*db)
;; -----------------------------------------------------------------------
(define
diffo
(fn
(expr var d)
(matche
expr
(:x (== d 1))
((:+ a b)
(fresh
(da db)
(== d (list :+ da db))
(diffo a var da)
(diffo b var db)))
((:* a b)
(fresh
(da db)
(== d (list :+ (list :* da b) (list :* a db)))
(diffo a var da)
(diffo b var db))))))
(mk-test "classics-diff-of-x" (run* q (diffo :x :x q)) (list 1))
(mk-test
"classics-diff-of-x-plus-x"
(run* q (diffo (list :+ :x :x) :x q))
(list (list :+ 1 1)))
(mk-test
"classics-diff-of-x-times-x"
(run* q (diffo (list :* :x :x) :x q))
(list (list :+ (list :* 1 :x) (list :* :x 1))))
(mk-tests-run!)

View File

@@ -0,0 +1,75 @@
;; lib/minikanren/tests/conda.sx — Phase 5 piece A tests for `conda`.
;; --- conda commits to first non-failing head, keeps ALL its answers ---
(mk-test
"conda-first-clause-keeps-all"
(run*
q
(conda
((mk-disj (== q 1) (== q 2)))
((== q 100))))
(list 1 2))
(mk-test
"conda-skips-failing-head"
(run*
q
(conda
((== 1 2))
((mk-disj (== q 10) (== q 20)))))
(list 10 20))
(mk-test
"conda-all-fail"
(run*
q
(conda ((== 1 2)) ((== 3 4))))
(list))
(mk-test "conda-no-clauses" (run* q (conda)) (list))
;; --- conda DIFFERS from condu: conda keeps all head answers ---
(mk-test
"conda-vs-condu-divergence"
(list
(run*
q
(conda
((mk-disj (== q 1) (== q 2)))
((== q 100))))
(run*
q
(condu
((mk-disj (== q 1) (== q 2)))
((== q 100)))))
(list (list 1 2) (list 1)))
;; --- conda head's rest-goals run on every head answer ---
(mk-test
"conda-rest-goals-run-on-all-answers"
(run*
q
(fresh
(x r)
(conda
((mk-disj (== x 1) (== x 2))
(== r (list :tag x))))
(== q r)))
(list (list :tag 1) (list :tag 2)))
;; --- if rest-goals fail on a head answer, that head answer is filtered;
;; the clause does not fall through to next clauses (per soft-cut). ---
(mk-test
"conda-rest-fails-no-fallthrough"
(run*
q
(conda
((mk-disj (== q 1) (== q 2)) (== q 99))
((== q 200))))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,89 @@
;; lib/minikanren/tests/conde.sx — Phase 2 piece C tests for `conde`.
;;
;; Note on ordering: conde clauses are wrapped in Zzz (inverse-eta delay),
;; so applying the conde goal to a substitution returns thunks. mk-mplus
;; suspends-and-swaps when its left operand is paused, giving fair
;; interleaving — this is exactly what makes recursive relations work,
;; but it does mean conde answers can interleave rather than appear in
;; strict left-to-right clause order.
;; --- single-clause conde ≡ conj of clause body ---
(mk-test
"conde-one-clause"
(let ((q (mk-var "q"))) (run* q (conde ((== q 7)))))
(list 7))
(mk-test
"conde-one-clause-multi-goals"
(let
((q (mk-var "q")))
(run* q (conde ((fresh (x) (== x 5) (== q (list x x)))))))
(list (list 5 5)))
;; --- multi-clause: produces one row per clause (interleaved) ---
(mk-test
"conde-three-clauses-as-set"
(let
((qs (run* q (conde ((== q 1)) ((== q 2)) ((== q 3))))))
(and
(= (len qs) 3)
(and
(some (fn (x) (= x 1)) qs)
(and
(some (fn (x) (= x 2)) qs)
(some (fn (x) (= x 3)) qs)))))
true)
(mk-test
"conde-mixed-success-failure-as-set"
(let
((qs (run* q (conde ((== q "a")) ((== 1 2)) ((== q "b"))))))
(and
(= (len qs) 2)
(and (some (fn (x) (= x "a")) qs) (some (fn (x) (= x "b")) qs))))
true)
;; --- conde with conjuncts inside clauses ---
(mk-test
"conde-clause-conj-as-set"
(let
((rows (run* q (fresh (x y) (conde ((== x 1) (== y 10)) ((== x 2) (== y 20))) (== q (list x y))))))
(and
(= (len rows) 2)
(and
(some (fn (r) (= r (list 1 10))) rows)
(some (fn (r) (= r (list 2 20))) rows))))
true)
;; --- nested conde ---
(mk-test
"conde-nested-yields-three"
(let
((qs (run* q (conde ((conde ((== q 1)) ((== q 2)))) ((== q 3))))))
(and
(= (len qs) 3)
(and
(some (fn (x) (= x 1)) qs)
(and
(some (fn (x) (= x 2)) qs)
(some (fn (x) (= x 3)) qs)))))
true)
;; --- conde all clauses fail → empty stream ---
(mk-test
"conde-all-fail"
(run*
q
(conde ((== 1 2)) ((== 3 4))))
(list))
;; --- empty conde: no clauses ⇒ fail ---
(mk-test "conde-no-clauses" (run* q (conde)) (list))
(mk-tests-run!)

View File

@@ -0,0 +1,86 @@
;; lib/minikanren/tests/condu.sx — Phase 2 piece D tests for `onceo` and `condu`.
;; --- onceo: at most one answer ---
(mk-test
"onceo-single-success-passes-through"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((onceo (== q 7)) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 7))
(mk-test
"onceo-multi-success-trimmed-to-one"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((onceo (mk-disj (== q 1) (== q 2) (== q 3))) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 1))
(mk-test
"onceo-failure-stays-failure"
((onceo (== 1 2)) empty-s)
(list))
(mk-test
"onceo-conde-trimmed"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((onceo (conde ((== q "a")) ((== q "b")))) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list "a"))
;; --- condu: first clause with successful head wins ---
(mk-test
"condu-first-clause-wins"
(let
((q (mk-var "q")))
(let
((res (stream-take 10 ((condu ((== q 1)) ((== q 2))) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 1))
(mk-test
"condu-skips-failing-head"
(let
((q (mk-var "q")))
(let
((res (stream-take 10 ((condu ((== 1 2)) ((== q 100)) ((== q 200))) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 100))
(mk-test
"condu-all-fail-empty"
((condu ((== 1 2)) ((== 3 4)))
empty-s)
(list))
(mk-test "condu-empty-clauses-fail" ((condu) empty-s) (list))
;; --- condu commits head's first answer; rest-goals can still backtrack
;; within that committed substitution but cannot revisit other heads. ---
(mk-test
"condu-head-onceo-rest-runs"
(let
((q (mk-var "q")) (r (mk-var "r")))
(let
((res (stream-take 10 ((condu ((mk-disj (== q 1) (== q 2)) (== r 99))) empty-s))))
(map (fn (s) (list (mk-walk q s) (mk-walk r s))) res)))
(list (list 1 99)))
(mk-test
"condu-rest-goals-can-fail-the-clause"
(let
((q (mk-var "q")))
(let
((res (stream-take 10 ((condu ((== q 1) (== 2 3)) ((== q 99))) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,48 @@
;; lib/minikanren/tests/cyclic-graph.sx — demonstrates the naive-patho
;; behaviour on a cyclic graph. Without Phase-7 tabling/SLG, the search
;; produces ever-longer paths revisiting the cycle. `run n` truncates;
;; `run*` would diverge.
(define cyclic-edges (list (list :a :b) (list :b :a) (list :b :c)))
(define cyclic-edgeo (fn (x y) (membero (list x y) cyclic-edges)))
(define
cyclic-patho
(fn
(x y path)
(conde
((cyclic-edgeo x y) (== path (list x y)))
((fresh (z mid) (cyclic-edgeo x z) (cyclic-patho z y mid) (conso x mid path))))))
;; --- direct edge ---
(mk-test
"cyclic-direct"
(run 1 q (cyclic-patho :a :b q))
(list (list :a :b)))
;; --- runs first 5 paths from a to b: bare edge, then increasing
;; numbers of cycle traversals (a->b->a->b, etc.) ---
(mk-test
"cyclic-enumerates-prefix-via-run-n"
(let
((paths (run 5 q (cyclic-patho :a :b q))))
(and
(= (len paths) 5)
(and
(every? (fn (p) (= (first p) :a)) paths)
(every? (fn (p) (= (last p) :b)) paths))))
true)
(mk-test
"cyclic-finds-c-via-cycle-or-direct"
(let
((paths (run 3 q (cyclic-patho :a :c q))))
(and
(>= (len paths) 1)
(some (fn (p) (= p (list :a :b :c))) paths)))
true)
(mk-tests-run!)

View File

@@ -0,0 +1,40 @@
;; lib/minikanren/tests/defrel.sx — Prolog-style relation definition macro.
(defrel
(my-membero x l)
((fresh (d) (conso x d l)))
((fresh (a d) (conso a d l) (my-membero x d))))
(mk-test
"defrel-defines-membero"
(run* q (my-membero q (list 1 2 3)))
(list 1 2 3))
(defrel
(my-listo l)
((nullo l))
((fresh (a d) (conso a d l) (my-listo d))))
(mk-test
"defrel-listo-bounded"
(run 3 q (my-listo q))
(list
(list)
(list (make-symbol "_.0"))
(list (make-symbol "_.0") (make-symbol "_.1"))))
;; Multi-arg relation with arithmetic.
(defrel
(my-pluso a b c)
((== a :z) (== b c))
((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (my-pluso a-1 b c-1))))
(mk-test
"defrel-pluso-2-3"
(run*
q
(my-pluso (list :s (list :s :z)) (list :s (list :s (list :s :z))) q))
(list (list :s (list :s (list :s (list :s (list :s :z)))))))
(mk-tests-run!)

View File

@@ -0,0 +1,31 @@
;; lib/minikanren/tests/enumerate.sx — index-each-element relation.
(mk-test
"enumerate-i-empty"
(run* q (enumerate-i (list) q))
(list (list)))
(mk-test
"enumerate-i-three"
(run* q (enumerate-i (list :a :b :c) q))
(list
(list (list 0 :a) (list 1 :b) (list 2 :c))))
(mk-test
"enumerate-i-strings"
(run* q (enumerate-i (list "x" "y" "z") q))
(list
(list (list 0 "x") (list 1 "y") (list 2 "z"))))
(mk-test
"enumerate-from-i-100"
(run* q (enumerate-from-i 100 (list :x :y :z) q))
(list
(list (list 100 :x) (list 101 :y) (list 102 :z))))
(mk-test
"enumerate-from-i-singleton"
(run* q (enumerate-from-i 0 (list :only) q))
(list (list (list 0 :only))))
(mk-tests-run!)

View File

@@ -0,0 +1,75 @@
;; lib/minikanren/tests/fd.sx — Phase 6 piece A: ino + all-distincto.
;; --- ino ---
(mk-test
"ino-element-in-domain"
(run* q (ino q (list 1 2 3)))
(list 1 2 3))
(mk-test "ino-empty-domain" (run* q (ino q (list))) (list))
(mk-test
"ino-singleton-domain"
(run* q (ino q (list 42)))
(list 42))
;; --- all-distincto ---
(mk-test
"all-distincto-empty"
(run* q (all-distincto (list)))
(list (make-symbol "_.0")))
(mk-test
"all-distincto-singleton"
(run* q (all-distincto (list 1)))
(list (make-symbol "_.0")))
(mk-test
"all-distincto-distinct-three"
(run* q (all-distincto (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"all-distincto-duplicate-fails"
(run* q (all-distincto (list 1 2 1)))
(list))
(mk-test
"all-distincto-adjacent-duplicate-fails"
(run* q (all-distincto (list 1 1 2)))
(list))
;; --- ino + all-distincto: classic enumerate-all-permutations ---
(mk-test
"fd-puzzle-three-distinct-from-domain"
(let
((perms (run* q (fresh (a b c) (== q (list a b c)) (ino a (list 1 2 3)) (ino b (list 1 2 3)) (ino c (list 1 2 3)) (all-distincto (list a b c))))))
(and
(= (len perms) 6)
(and
(some (fn (p) (= p (list 1 2 3))) perms)
(and
(some
(fn (p) (= p (list 1 3 2)))
perms)
(and
(some
(fn (p) (= p (list 2 1 3)))
perms)
(and
(some
(fn (p) (= p (list 2 3 1)))
perms)
(and
(some
(fn (p) (= p (list 3 1 2)))
perms)
(some
(fn (p) (= p (list 3 2 1)))
perms))))))))
true)
(mk-tests-run!)

View File

@@ -0,0 +1,42 @@
(mk-test "flatteno-empty" (run* q (flatteno (list) q)) (list (list)))
(mk-test
"flatteno-atom"
(run* q (flatteno 5 q))
(list (list 5)))
(mk-test
"flatteno-flat-list"
(run* q (flatteno (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"flatteno-singleton"
(run* q (flatteno (list 1) q))
(list (list 1)))
(mk-test
"flatteno-nested-once"
(run*
q
(flatteno (list 1 (list 2 3) 4) q))
(list (list 1 2 3 4)))
(mk-test
"flatteno-nested-twice"
(run*
q
(flatteno
(list
1
(list 2 (list 3 4))
5)
q))
(list (list 1 2 3 4 5)))
(mk-test
"flatteno-keywords"
(run* q (flatteno (list :a (list :b :c) :d) q))
(list (list :a :b :c :d)))
(mk-tests-run!)

View File

@@ -0,0 +1,101 @@
;; lib/minikanren/tests/fresh.sx — Phase 2 piece B tests for `fresh`.
;; --- empty fresh: pure goal grouping ---
(mk-test
"fresh-empty-vars-equiv-conj"
(stream-take 5 ((fresh () (== 1 1)) empty-s))
(list empty-s))
(mk-test
"fresh-empty-vars-no-goals-is-succeed"
(stream-take 5 ((fresh ()) empty-s))
(list empty-s))
;; --- single var ---
(mk-test
"fresh-one-var-bound"
(let
((s (first (stream-take 5 ((fresh (x) (== x 7)) empty-s)))))
(first (vals s)))
7)
;; --- multiple vars + multiple goals ---
(mk-test
"fresh-two-vars-three-goals"
(let
((q (mk-var "q"))
(g
(fresh
(x y)
(== x 10)
(== y 20)
(== q (list x y)))))
(mk-walk* q (first (stream-take 5 (g empty-s)))))
(list 10 20))
(mk-test
"fresh-three-vars"
(let
((q (mk-var "q"))
(g
(fresh
(a b c)
(== a 1)
(== b 2)
(== c 3)
(== q (list a b c)))))
(mk-walk* q (first (stream-take 5 (g empty-s)))))
(list 1 2 3))
;; --- fresh interacts with disj ---
(mk-test
"fresh-with-disj"
(let
((q (mk-var "q")))
(let
((g (fresh (x) (mk-disj (== x 1) (== x 2)) (== q x))))
(let
((res (stream-take 5 (g empty-s))))
(map (fn (s) (mk-walk q s)) res))))
(list 1 2))
;; --- nested fresh ---
(mk-test
"fresh-nested"
(let
((q (mk-var "q"))
(g
(fresh
(x)
(fresh
(y)
(== x 1)
(== y 2)
(== q (list x y))))))
(mk-walk* q (first (stream-take 5 (g empty-s)))))
(list 1 2))
;; --- call-fresh (functional alternative) ---
(mk-test
"call-fresh-binds-and-walks"
(let
((s (first (stream-take 5 ((call-fresh (fn (x) (== x 99))) empty-s)))))
(first (vals s)))
99)
(mk-test
"call-fresh-distinct-from-outer-vars"
(let
((q (mk-var "q")))
(let
((g (call-fresh (fn (x) (mk-conj (== x 5) (== q (list x x)))))))
(mk-walk* q (first (stream-take 5 (g empty-s))))))
(list 5 5))
(mk-tests-run!)

View File

@@ -0,0 +1,260 @@
;; lib/minikanren/tests/goals.sx — Phase 2 tests for stream.sx + goals.sx.
;;
;; Streams use a tagged shape internally (`(:s head tail)`) so that mature
;; cells can have thunk tails — SX has no improper pairs. Test assertions
;; therefore stream-take into a plain SX list, or check goal effects via
;; mk-walk on the resulting subst, instead of inspecting raw streams.
;; --- stream-take base cases (input streams use s-cons / mzero) ---
(mk-test
"stream-take-zero-from-mature"
(stream-take 0 (s-cons (empty-subst) mzero))
(list))
(mk-test "stream-take-from-mzero" (stream-take 5 mzero) (list))
(mk-test
"stream-take-mature-pair"
(stream-take 5 (s-cons :a (s-cons :b mzero)))
(list :a :b))
(mk-test
"stream-take-fewer-than-available"
(stream-take 1 (s-cons :a (s-cons :b mzero)))
(list :a))
(mk-test
"stream-take-all-with-neg-1"
(stream-take -1 (s-cons :a (s-cons :b (s-cons :c mzero))))
(list :a :b :c))
;; --- stream-take forces immature thunks ---
(mk-test
"stream-take-forces-thunk"
(stream-take 5 (fn () (s-cons :x mzero)))
(list :x))
(mk-test
"stream-take-forces-nested-thunks"
(stream-take 5 (fn () (fn () (s-cons :y mzero))))
(list :y))
;; --- mk-mplus interleaves ---
(mk-test
"mplus-empty-left"
(stream-take 5 (mk-mplus mzero (s-cons :r mzero)))
(list :r))
(mk-test
"mplus-empty-right"
(stream-take 5 (mk-mplus (s-cons :l mzero) mzero))
(list :l))
(mk-test
"mplus-mature-mature"
(stream-take
5
(mk-mplus (s-cons :a (s-cons :b mzero)) (s-cons :c (s-cons :d mzero))))
(list :a :b :c :d))
(mk-test
"mplus-with-paused-left-swaps"
(stream-take
5
(mk-mplus
(fn () (s-cons :a (s-cons :b mzero)))
(s-cons :c (s-cons :d mzero))))
(list :c :d :a :b))
;; --- mk-bind ---
(mk-test
"bind-empty-stream"
(stream-take 5 (mk-bind mzero (fn (s) (unit s))))
(list))
(mk-test
"bind-singleton-identity"
(stream-take
5
(mk-bind (s-cons 5 mzero) (fn (x) (unit x))))
(list 5))
(mk-test
"bind-flat-multi"
(stream-take
10
(mk-bind
(s-cons 1 (s-cons 2 mzero))
(fn (x) (s-cons x (s-cons (* x 10) mzero)))))
(list 1 10 2 20))
(mk-test
"bind-fail-prunes-some"
(stream-take
10
(mk-bind
(s-cons 1 (s-cons 2 (s-cons 3 mzero)))
(fn (x) (if (= x 2) mzero (unit x)))))
(list 1 3))
;; --- core goals: succeed / fail ---
(mk-test
"succeed-yields-singleton"
(stream-take 5 (succeed empty-s))
(list empty-s))
(mk-test "fail-yields-mzero" (stream-take 5 (fail empty-s)) (list))
;; --- == ---
(mk-test
"eq-ground-success"
(stream-take 5 ((== 1 1) empty-s))
(list empty-s))
(mk-test
"eq-ground-failure"
(stream-take 5 ((== 1 2) empty-s))
(list))
(mk-test
"eq-binds-var"
(let
((x (mk-var "x")))
(mk-walk
x
(first (stream-take 5 ((== x 7) empty-s)))))
7)
(mk-test
"eq-list-success"
(let
((x (mk-var "x")))
(mk-walk
x
(first
(stream-take
5
((== x (list 1 2)) empty-s)))))
(list 1 2))
(mk-test
"eq-list-mismatch-fails"
(stream-take
5
((== (list 1 2) (list 1 3)) empty-s))
(list))
;; --- conj2 / mk-conj ---
(mk-test
"conj2-both-bind"
(let
((x (mk-var "x")) (y (mk-var "y")))
(let
((s (first (stream-take 5 ((conj2 (== x 1) (== y 2)) empty-s)))))
(list (mk-walk x s) (mk-walk y s))))
(list 1 2))
(mk-test
"conj2-conflict-empty"
(let
((x (mk-var "x")))
(stream-take
5
((conj2 (== x 1) (== x 2)) empty-s)))
(list))
(mk-test
"conj-empty-is-succeed"
(stream-take 5 ((mk-conj) empty-s))
(list empty-s))
(mk-test
"conj-single-is-goal"
(let
((x (mk-var "x")))
(mk-walk
x
(first
(stream-take 5 ((mk-conj (== x 99)) empty-s)))))
99)
(mk-test
"conj-three-bindings"
(let
((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
(let
((s (first (stream-take 5 ((mk-conj (== x 1) (== y 2) (== z 3)) empty-s)))))
(list (mk-walk x s) (mk-walk y s) (mk-walk z s))))
(list 1 2 3))
;; --- disj2 / mk-disj ---
(mk-test
"disj2-both-succeed"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((disj2 (== q 1) (== q 2)) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 1 2))
(mk-test
"disj2-fail-or-succeed"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((disj2 fail (== q 5)) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list 5))
(mk-test
"disj-empty-is-fail"
(stream-take 5 ((mk-disj) empty-s))
(list))
(mk-test
"disj-three-clauses"
(let
((q (mk-var "q")))
(let
((res (stream-take 5 ((mk-disj (== q "a") (== q "b") (== q "c")) empty-s))))
(map (fn (s) (mk-walk q s)) res)))
(list "a" "b" "c"))
;; --- conj/disj nesting ---
(mk-test
"disj-of-conj"
(let
((x (mk-var "x")) (y (mk-var "y")))
(let
((res (stream-take 5 ((mk-disj (mk-conj (== x 1) (== y 2)) (mk-conj (== x 3) (== y 4))) empty-s))))
(map (fn (s) (list (mk-walk x s) (mk-walk y s))) res)))
(list (list 1 2) (list 3 4)))
;; --- ==-check ---
(mk-test
"eq-check-no-occurs-fails"
(let
((x (mk-var "x")))
(stream-take 5 ((==-check x (list 1 x)) empty-s)))
(list))
(mk-test
"eq-check-no-occurs-non-occurring-succeeds"
(let
((x (mk-var "x")))
(mk-walk
x
(first (stream-take 5 ((==-check x 5) empty-s)))))
5)
(mk-tests-run!)

View File

@@ -0,0 +1,70 @@
;; lib/minikanren/tests/graph.sx — directed-graph reachability via patho.
(define
test-edges
(list (list :a :b) (list :b :c) (list :c :d) (list :a :c) (list :d :e)))
(define edgeo (fn (from to) (membero (list from to) test-edges)))
(define
patho
(fn
(x y path)
(conde
((edgeo x y) (== path (list x y)))
((fresh (z mid-path) (edgeo x z) (patho z y mid-path) (conso x mid-path path))))))
;; --- direct edges ---
(mk-test "patho-direct" (run* q (patho :a :b q)) (list (list :a :b)))
(mk-test "patho-no-direct-edge" (run* q (patho :e :a q)) (list))
;; --- indirect ---
(mk-test
"patho-multi-hop"
(let
((paths (run* q (patho :a :d q))))
(and
(= (len paths) 2)
(and
(some (fn (p) (= p (list :a :b :c :d))) paths)
(some (fn (p) (= p (list :a :c :d))) paths))))
true)
(mk-test
"patho-to-leaf"
(let
((paths (run* q (patho :a :e q))))
(and
(= (len paths) 2)
(and
(some (fn (p) (= p (list :a :b :c :d :e))) paths)
(some (fn (p) (= p (list :a :c :d :e))) paths))))
true)
;; --- enumeration with multiplicity ---
;; Each path contributes one tuple, so reachable nodes can repeat. Here
;; targets are: b (1 path), c (2 paths), d (2 paths), e (2 paths) = 7.
(mk-test
"patho-enumerate-from-a-with-multiplicity"
(let
((targets (run* q (fresh (path) (patho :a q path)))))
(and
(= (len targets) 7)
(and
(some (fn (t) (= t :b)) targets)
(and
(some (fn (t) (= t :c)) targets)
(and
(some (fn (t) (= t :d)) targets)
(some (fn (t) (= t :e)) targets))))))
true)
;; --- unreachable target ---
(mk-test "patho-unreachable" (run* q (patho :a :z q)) (list))
(mk-tests-run!)

View File

@@ -0,0 +1,103 @@
;; lib/minikanren/tests/intarith.sx — ground-only integer arithmetic
;; goals that escape into host operations via project.
;; --- pluso-i ---
(mk-test
"pluso-i-forward"
(run* q (pluso-i 7 8 q))
(list 15))
(mk-test
"pluso-i-zero"
(run* q (pluso-i 0 0 q))
(list 0))
(mk-test
"pluso-i-negatives"
(run* q (pluso-i -5 3 q))
(list -2))
(mk-test
"pluso-i-non-ground-fails"
(run* q (fresh (a) (pluso-i a 3 5)))
(list))
;; --- minuso-i ---
(mk-test
"minuso-i-forward"
(run* q (minuso-i 10 4 q))
(list 6))
(mk-test
"minuso-i-zero"
(run* q (minuso-i 5 5 q))
(list 0))
;; --- *o-i ---
(mk-test
"times-i-forward"
(run* q (*o-i 6 7 q))
(list 42))
(mk-test
"times-i-by-zero"
(run* q (*o-i 0 99 q))
(list 0))
(mk-test
"times-i-by-one"
(run* q (*o-i 1 17 q))
(list 17))
;; --- comparisons ---
(mk-test
"lto-i-true"
(run 1 q (lto-i 2 5))
(list (make-symbol "_.0")))
(mk-test "lto-i-false" (run* q (lto-i 5 2)) (list))
(mk-test "lto-i-equal-false" (run* q (lto-i 3 3)) (list))
(mk-test
"lteo-i-equal"
(run 1 q (lteo-i 4 4))
(list (make-symbol "_.0")))
(mk-test
"lteo-i-less"
(run 1 q (lteo-i 1 4))
(list (make-symbol "_.0")))
(mk-test "lteo-i-more" (run* q (lteo-i 9 4)) (list))
(mk-test
"neqo-i-different"
(run 1 q (neqo-i 3 5))
(list (make-symbol "_.0")))
(mk-test "neqo-i-same" (run* q (neqo-i 3 3)) (list))
;; --- composition with relational vars ---
(mk-test
"intarith-with-membero"
(run*
q
(fresh
(x)
(membero
x
(list 1 2 3 4 5))
(lto-i x 3)
(== q x)))
(list 1 2))
(mk-test "even-i-pos" (run* q (even-i 4)) (list (make-symbol "_.0")))
(mk-test "even-i-neg" (run* q (even-i 5)) (list))
(mk-test "odd-i-pos" (run* q (odd-i 7)) (list (make-symbol "_.0")))
(mk-test "odd-i-neg" (run* q (odd-i 4)) (list))
(mk-test
"even-i-filter"
(run* q (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x)))
(list 2 4 6))
(mk-tests-run!)

View File

@@ -0,0 +1,38 @@
;; lib/minikanren/tests/iterate-no.sx — iterated relation application.
(define
mk-nat
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
(mk-test
"iterate-no-zero"
(run*
q
(iterate-no
(fn (a b) (== b (list :wrap a)))
(mk-nat 0)
:seed q))
(list :seed))
(mk-test
"iterate-no-three-wraps"
(run*
q
(iterate-no (fn (a b) (== b (list :wrap a))) (mk-nat 3) :x q))
(list (list :wrap (list :wrap (list :wrap :x)))))
(mk-test
"iterate-no-succ-three-times"
(run*
q
(iterate-no (fn (a b) (== b (list :s a))) (mk-nat 3) :z q))
(list (mk-nat 3)))
(mk-test
"iterate-no-with-list-cons"
(run*
q
(iterate-no (fn (a b) (conso :a a b)) (mk-nat 4) (list) q))
(list (list :a :a :a :a)))
(mk-tests-run!)

View File

@@ -0,0 +1,38 @@
;; lib/minikanren/tests/lasto.sx — last-element + init-without-last.
(mk-test
"lasto-singleton"
(run* q (lasto (list 5) q))
(list 5))
(mk-test
"lasto-multi"
(run* q (lasto (list 1 2 3 4) q))
(list 4))
(mk-test "lasto-empty" (run* q (lasto (list) q)) (list))
(mk-test "lasto-strings" (run* q (lasto (list "a" "b" "c") q)) (list "c"))
(mk-test
"init-o-multi"
(run* q (init-o (list 1 2 3 4) q))
(list (list 1 2 3)))
(mk-test
"init-o-singleton"
(run* q (init-o (list 7) q))
(list (list)))
(mk-test "init-o-empty" (run* q (init-o (list) q)) (list))
(mk-test
"lasto-init-o-roundtrip"
(run*
q
(fresh
(init last)
(lasto (list 1 2 3 4) last)
(init-o (list 1 2 3 4) init)
(appendo init (list last) q)))
(list (list 1 2 3 4)))
(mk-tests-run!)

View File

@@ -0,0 +1,61 @@
;; lib/minikanren/tests/latin.sx — 2x2 Latin square via ino + all-distincto.
;;
;; A 2x2 Latin square has 2 distinct fillings:
;; ((1 2) (2 1)) and ((2 1) (1 2)).
;; The 3x3 version has 12 fillings but takes minutes under naive search;
;; full CLP(FD) (Phase 6 proper) would handle it in milliseconds.
(define
latin-2x2
(fn
(cells)
(let
((c11 (nth cells 0))
(c12 (nth cells 1))
(c21 (nth cells 2))
(c22 (nth cells 3))
(dom (list 1 2)))
(mk-conj
(ino c11 dom)
(ino c12 dom)
(ino c21 dom)
(ino c22 dom)
(all-distincto (list c11 c12))
(all-distincto (list c21 c22))
(all-distincto (list c11 c21))
(all-distincto (list c12 c22)))))) ;; col 2
(mk-test
"latin-2x2-count"
(let
((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
(len squares))
2)
(mk-test
"latin-2x2-as-set"
(let
((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
(and
(= (len squares) 2)
(and
(some
(fn (s) (= s (list 1 2 2 1)))
squares)
(some
(fn (s) (= s (list 2 1 1 2)))
squares))))
true)
(mk-test
"latin-2x2-with-clue"
(run*
q
(fresh
(a b c d)
(== a 1)
(== q (list a b c d))
(latin-2x2 (list a b c d))))
(list (list 1 2 2 1)))
(mk-tests-run!)

View File

@@ -0,0 +1,77 @@
;; lib/minikanren/tests/laziness.sx — verify Zzz wrapping (in conde)
;; lets infinitely-recursive relations produce finite prefixes via run-n.
;; --- a relation that has no base case but conde-protects via Zzz ---
(define
listo-aux
(fn
(l)
(conde ((nullo l)) ((fresh (a d) (conso a d l) (listo-aux d))))))
(mk-test
"infinite-relation-truncates-via-run-n"
(run 4 q (listo-aux q))
(list
(list)
(list (make-symbol "_.0"))
(list (make-symbol "_.0") (make-symbol "_.1"))
(list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
;; --- two infinite generators interleaved via mk-disj must both produce
;; answers (no starvation) — the fairness test ---
(define
ones-gen
(fn
(l)
(conde
((== l (list)))
((fresh (d) (conso 1 d l) (ones-gen d))))))
(define
twos-gen
(fn
(l)
(conde
((== l (list)))
((fresh (d) (conso 2 d l) (twos-gen d))))))
(mk-test
"interleaving-keeps-both-streams-alive"
(let
((res (run 4 q (mk-disj (ones-gen q) (twos-gen q)))))
(and
(= (len res) 4)
(and
(some
(fn
(x)
(and
(list? x)
(and (not (empty? x)) (= (first x) 1))))
res)
(some
(fn
(x)
(and
(list? x)
(and (not (empty? x)) (= (first x) 2))))
res))))
true)
;; --- run* terminates on a relation whose conde has finite base case
;; reached from any starting point ---
(mk-test
"run-star-terminates-on-bounded-relation"
(run*
q
(fresh
(l)
(== l (list 1 2 3))
(listo l)
(== q :ok)))
(list :ok))
(mk-tests-run!)

View File

@@ -0,0 +1,28 @@
;; lib/minikanren/tests/lengtho-i.sx — integer-indexed length (fast).
(mk-test "lengtho-i-empty" (run* q (lengtho-i (list) q)) (list 0))
(mk-test
"lengtho-i-singleton"
(run* q (lengtho-i (list :a) q))
(list 1))
(mk-test
"lengtho-i-three"
(run* q (lengtho-i (list 1 2 3) q))
(list 3))
(mk-test
"lengtho-i-five"
(run*
q
(lengtho-i
(list 1 2 3 4 5)
q))
(list 5))
(mk-test
"lengtho-i-mixed-types"
(run*
q
(lengtho-i (list 1 "two" :three (list 4 5)) q))
(list 4))
(mk-tests-run!)

View File

@@ -0,0 +1,126 @@
;; lib/minikanren/tests/list-relations.sx — rembero, assoco, nth-o, samelengtho.
;; --- rembero (remove first occurrence) ---
(mk-test
"rembero-element-present"
(run*
q
(rembero 2 (list 1 2 3 2) q))
(list (list 1 3 2)))
(mk-test
"rembero-element-not-present"
(run* q (rembero 99 (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"rembero-empty"
(run* q (rembero 1 (list) q))
(list (list)))
(mk-test
"rembero-only-element"
(run* q (rembero 5 (list 5) q))
(list (list)))
(mk-test
"rembero-first-of-many"
(run*
q
(rembero 1 (list 1 2 3 4) q))
(list (list 2 3 4)))
;; --- assoco (alist lookup) ---
(define
test-pairs
(list
(list "alice" 30)
(list "bob" 25)
(list "carol" 35)))
(mk-test
"assoco-found"
(run* q (assoco "bob" test-pairs q))
(list 25))
(mk-test
"assoco-first"
(run* q (assoco "alice" test-pairs q))
(list 30))
(mk-test "assoco-missing" (run* q (assoco "dave" test-pairs q)) (list))
(mk-test
"assoco-find-keys-with-value"
(run* q (assoco q test-pairs 25))
(list "bob"))
;; --- nth-o (Peano-indexed access) ---
(mk-test
"nth-o-zero"
(run* q (nth-o :z (list 10 20 30) q))
(list 10))
(mk-test
"nth-o-one"
(run* q (nth-o (list :s :z) (list 10 20 30) q))
(list 20))
(mk-test
"nth-o-two"
(run*
q
(nth-o (list :s (list :s :z)) (list 10 20 30) q))
(list 30))
(mk-test
"nth-o-out-of-range"
(run*
q
(nth-o
(list :s (list :s (list :s :z)))
(list 10 20 30)
q))
(list))
;; --- samelengtho ---
(mk-test
"samelengtho-equal"
(run*
q
(samelengtho (list 1 2 3) (list :a :b :c)))
(list (make-symbol "_.0")))
(mk-test
"samelengtho-different-fails"
(run* q (samelengtho (list 1 2) (list :a :b :c)))
(list))
(mk-test
"samelengtho-empty-equal"
(run* q (samelengtho (list) (list)))
(list (make-symbol "_.0")))
(mk-test
"samelengtho-builds-vars"
(run 1 q (samelengtho (list 1 2 3) q))
(list (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
(mk-test
"samelengtho-enumerates-pairs"
(run
3
q
(fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2))))
(list
(list (list) (list))
(list (list (make-symbol "_.0")) (list (make-symbol "_.1")))
(list
(list (make-symbol "_.0") (make-symbol "_.1"))
(list (make-symbol "_.2") (make-symbol "_.3")))))
(mk-tests-run!)

View File

@@ -0,0 +1,62 @@
;; lib/minikanren/tests/mapo.sx — relational map.
(mk-test
"mapo-identity"
(run*
q
(mapo (fn (a b) (== a b)) (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"mapo-tag-each"
(run*
q
(mapo
(fn (a b) (== b (list :tag a)))
(list 1 2 3)
q))
(list
(list
(list :tag 1)
(list :tag 2)
(list :tag 3))))
(mk-test
"mapo-backward"
(run*
q
(mapo (fn (a b) (== a b)) q (list 1 2 3)))
(list (list 1 2 3)))
(mk-test
"mapo-empty"
(run* q (mapo (fn (a b) (== a b)) (list) q))
(list (list)))
(mk-test
"mapo-duplicate"
(run* q (mapo (fn (a b) (== b (list a a))) (list :x :y) q))
(list (list (list :x :x) (list :y :y))))
(mk-test
"mapo-different-length-fails"
(run*
q
(mapo
(fn (a b) (== a b))
(list 1 2)
(list 1 2 3)))
(list))
;; mapo + arithmetic via intarith
(mk-test
"mapo-square-each"
(run*
q
(mapo
(fn (a b) (*o-i a a b))
(list 1 2 3 4)
q))
(list (list 1 4 9 16)))
(mk-tests-run!)

View File

@@ -0,0 +1,138 @@
;; lib/minikanren/tests/matche.sx — Phase 5 piece D tests for `matche`.
;; --- literal patterns ---
(mk-test
"matche-literal-number"
(run* q (matche q (1 (== q 1))))
(list 1))
(mk-test
"matche-literal-string"
(run* q (matche q ("hello" (== q "hello"))))
(list "hello"))
(mk-test
"matche-literal-no-clause-matches"
(run*
q
(matche 7 (1 (== q :a)) (2 (== q :b))))
(list))
;; --- variable patterns ---
(mk-test
"matche-symbol-pattern"
(run* q (fresh (x) (== x 99) (matche x (a (== q a)))))
(list 99))
(mk-test
"matche-wildcard"
(run* q (fresh (x) (== x 7) (matche x (_ (== q :any)))))
(list :any))
;; --- list patterns ---
(mk-test
"matche-empty-list"
(run* q (matche (list) (() (== q :ok))))
(list :ok))
(mk-test
"matche-pair-binds"
(run*
q
(fresh
(x)
(== x (list 1 2))
(matche x ((a b) (== q (list b a))))))
(list (list 2 1)))
(mk-test
"matche-triple-binds"
(run*
q
(fresh
(x)
(== x (list 1 2 3))
(matche x ((a b c) (== q (list :sum a b c))))))
(list (list :sum 1 2 3)))
(mk-test
"matche-mixed-literal-and-var"
(run*
q
(fresh
(x)
(== x (list 1 99 3))
(matche x ((1 m 3) (== q m)))))
(list 99))
;; --- multi-clause dispatch ---
(mk-test
"matche-multi-clause-shape"
(run*
q
(fresh
(x)
(== x (list 5 6))
(matche
x
(() (== q :empty))
((a) (== q (list :one a)))
((a b) (== q (list :two a b))))))
(list (list :two 5 6)))
(mk-test
"matche-three-shapes-via-fresh"
(run*
q
(fresh
(x)
(matche
x
(() (== q :empty))
((a) (== q (list :one a)))
((a b) (== q (list :two a b))))))
(list
:empty (list :one (make-symbol "_.0"))
(list :two (make-symbol "_.0") (make-symbol "_.1"))))
;; --- nested patterns ---
(mk-test
"matche-nested"
(run*
q
(fresh
(x)
(==
x
(list (list 1 2) (list 3 4)))
(matche x (((a b) (c d)) (== q (list a b c d))))))
(list (list 1 2 3 4)))
;; --- repeated var names create the same fresh var → must unify ---
(mk-test
"matche-repeated-var-implies-equality"
(run*
q
(fresh
(x)
(== x (list 7 7))
(matche x ((a a) (== q a)))))
(list 7))
(mk-test
"matche-repeated-var-mismatch-fails"
(run*
q
(fresh
(x)
(== x (list 7 8))
(matche x ((a a) (== q a)))))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,49 @@
;; lib/minikanren/tests/minmax.sx — mino + maxo via intarith.
(mk-test
"mino-singleton"
(run* q (mino (list 7) q))
(list 7))
(mk-test
"mino-of-3"
(run* q (mino (list 5 1 3) q))
(list 1))
(mk-test
"mino-of-5"
(run*
q
(mino (list 5 1 3 2 4) q))
(list 1))
(mk-test
"mino-with-dups"
(run* q (mino (list 3 3 3) q))
(list 3))
(mk-test "mino-empty-fails" (run* q (mino (list) q)) (list))
(mk-test
"maxo-singleton"
(run* q (maxo (list 7) q))
(list 7))
(mk-test
"maxo-of-5"
(run*
q
(maxo (list 5 1 3 2 4) q))
(list 5))
(mk-test
"maxo-of-negs"
(run* q (maxo (list -5 -1 -3) q))
(list -1))
(mk-test
"min-and-max-of-list"
(run*
q
(fresh
(mn mx)
(mino (list 5 1 3 2 4) mn)
(maxo (list 5 1 3 2 4) mx)
(== q (list mn mx))))
(list (list 1 5)))
(mk-tests-run!)

View File

@@ -0,0 +1,50 @@
;; lib/minikanren/tests/nafc.sx — Phase 5 piece C tests for `nafc`.
(mk-test
"nafc-failed-goal-succeeds"
(run* q (nafc (== 1 2)))
(list (make-symbol "_.0")))
(mk-test
"nafc-successful-goal-fails"
(run* q (nafc (== 1 1)))
(list))
(mk-test
"nafc-double-negation"
(run* q (nafc (nafc (== 1 1))))
(list (make-symbol "_.0")))
(mk-test
"nafc-with-conde-no-clauses-succeed"
(run*
q
(nafc
(conde ((== 1 2)) ((== 3 4)))))
(list (make-symbol "_.0")))
(mk-test
"nafc-with-conde-some-clause-succeeds-fails"
(run*
q
(nafc
(conde ((== 1 1)) ((== 3 4)))))
(list))
;; --- composing nafc with == as a guard ---
(mk-test
"nafc-as-guard"
(run*
q
(fresh (x) (== x 5) (nafc (== x 99)) (== q x)))
(list 5))
(mk-test
"nafc-guard-blocking"
(run*
q
(fresh (x) (== x 5) (nafc (== x 5)) (== q x)))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,29 @@
;; lib/minikanren/tests/not-membero.sx — relational "not in list".
(mk-test
"not-membero-absent"
(run* q (not-membero 99 (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"not-membero-present"
(run* q (not-membero 2 (list 1 2 3)))
(list))
(mk-test
"not-membero-empty"
(run* q (not-membero 1 (list)))
(list (make-symbol "_.0")))
(mk-test
"not-membero-as-filter"
(run*
q
(fresh
(x)
(membero
x
(list 1 2 3 4 5))
(not-membero x (list 2 4))
(== q x)))
(list 1 3 5))
(mk-tests-run!)

View File

@@ -0,0 +1,41 @@
;; lib/minikanren/tests/pairlisto.sx — zip two lists into pair list.
(mk-test
"pairlisto-empty"
(run* q (pairlisto (list) (list) q))
(list (list)))
(mk-test
"pairlisto-equal-lengths"
(run*
q
(pairlisto (list 1 2 3) (list :a :b :c) q))
(list
(list (list 1 :a) (list 2 :b) (list 3 :c))))
(mk-test
"pairlisto-recover-l1"
(run*
q
(pairlisto
q
(list :a :b :c)
(list (list 10 :a) (list 20 :b) (list 30 :c))))
(list (list 10 20 30)))
(mk-test
"pairlisto-recover-l2"
(run*
q
(pairlisto
(list 1 2 3)
q
(list (list 1 :x) (list 2 :y) (list 3 :z))))
(list (list :x :y :z)))
(mk-test
"pairlisto-different-lengths-fails"
(run* q (pairlisto (list 1 2) (list :a :b :c) q))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,44 @@
;; lib/minikanren/tests/palindromeo.sx — palindromic list relation.
(mk-test
"palindromeo-empty"
(run* q (palindromeo (list)))
(list (make-symbol "_.0")))
(mk-test
"palindromeo-singleton"
(run* q (palindromeo (list :a)))
(list (make-symbol "_.0")))
(mk-test
"palindromeo-pair-equal"
(run* q (palindromeo (list 1 1)))
(list (make-symbol "_.0")))
(mk-test
"palindromeo-pair-unequal-fails"
(run* q (palindromeo (list 1 2)))
(list))
(mk-test
"palindromeo-five-yes"
(run*
q
(palindromeo
(list 1 2 3 2 1)))
(list (make-symbol "_.0")))
(mk-test
"palindromeo-five-no"
(run*
q
(palindromeo
(list 1 2 3 4 5)))
(list))
(mk-test
"palindromeo-strings"
(run* q (palindromeo (list "a" "b" "a")))
(list (make-symbol "_.0")))
(mk-tests-run!)

View File

@@ -0,0 +1,58 @@
;; lib/minikanren/tests/parity.sx — eveno + oddo Peano predicates.
(define
mk-nat
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
(mk-test "eveno-zero" (run* q (eveno :z)) (list (make-symbol "_.0")))
(mk-test
"eveno-2"
(run* q (eveno (mk-nat 2)))
(list (make-symbol "_.0")))
(mk-test
"eveno-4"
(run* q (eveno (mk-nat 4)))
(list (make-symbol "_.0")))
(mk-test "eveno-1-fails" (run* q (eveno (mk-nat 1))) (list))
(mk-test "eveno-3-fails" (run* q (eveno (mk-nat 3))) (list))
(mk-test
"oddo-1"
(run* q (oddo (mk-nat 1)))
(list (make-symbol "_.0")))
(mk-test
"oddo-3"
(run* q (oddo (mk-nat 3)))
(list (make-symbol "_.0")))
(mk-test "oddo-zero-fails" (run* q (oddo :z)) (list))
(mk-test "oddo-2-fails" (run* q (oddo (mk-nat 2))) (list))
;; Enumerate small evens.
(mk-test
"eveno-enumerates"
(run 4 q (eveno q))
(list
(mk-nat 0)
(mk-nat 2)
(mk-nat 4)
(mk-nat 6)))
;; Enumerate small odds.
(mk-test
"oddo-enumerates"
(run 4 q (oddo q))
(list
(mk-nat 1)
(mk-nat 3)
(mk-nat 5)
(mk-nat 7)))
;; A number is even XOR odd (no overlap).
(mk-test
"even-odd-no-overlap"
(run*
q
(mk-conj (eveno (mk-nat 4)) (oddo (mk-nat 4))))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,75 @@
;; lib/minikanren/tests/partitiono.sx — partition list by predicate.
(mk-test
"partitiono-empty"
(run*
q
(fresh
(yes no)
(partitiono (fn (x) (== x 1)) (list) yes no)
(== q (list yes no))))
(list (list (list) (list))))
(mk-test
"partitiono-by-equality"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (== x 2))
(list 1 2 3 2 4)
yes
no)
(== q (list yes no))))
(list
(list
(list 2 2)
(list 1 3 4))))
(mk-test
"partitiono-by-numeric-pred"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i x 5))
(list 1 7 2 8 3)
yes
no)
(== q (list yes no))))
(list
(list
(list 1 2 3)
(list 7 8))))
(mk-test
"partitiono-all-yes"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i x 100))
(list 1 2 3)
yes
no)
(== q (list yes no))))
(list (list (list 1 2 3) (list))))
(mk-test
"partitiono-all-no"
(run*
q
(fresh
(yes no)
(partitiono
(fn (x) (lto-i 100 x))
(list 1 2 3)
yes
no)
(== q (list yes no))))
(list (list (list) (list 1 2 3))))
(mk-tests-run!)

View File

@@ -0,0 +1,40 @@
;; lib/minikanren/tests/path-cycle-free.sx — cycle-free reachability search.
;;
;; Threads a "visited" accumulator through the recursion, using nafc +
;; membero to prevent revisiting nodes. Demonstrates how to make the
;; cyclic-graph divergence problem (see tests/cyclic-graph.sx) tractable
;; for graphs with cycles, without invoking Phase-7 tabling.
(define
cf-edges
(list (list :a :b) (list :b :a) (list :b :c) (list :c :d) (list :d :a))) ; another cycle
(define cf-edgeo (fn (from to) (membero (list from to) cf-edges)))
(define
patho-no-cycles
(fn
(x y visited path)
(conde
((cf-edgeo x y) (nafc (membero y visited)) (== path (list x y)))
((fresh (z mid v-prime) (cf-edgeo x z) (nafc (membero z visited)) (conso z visited v-prime) (patho-no-cycles z y v-prime mid) (conso x mid path))))))
(define cf-patho (fn (x y path) (patho-no-cycles x y (list x) path)))
(mk-test
"cycle-free-finds-finitely"
(let
((paths (run* q (cf-patho :a :d q))))
(and
(>= (len paths) 1)
(every? (fn (p) (and (= (first p) :a) (= (last p) :d))) paths)))
true)
(mk-test
"cycle-free-direct-edge"
(run* q (cf-patho :a :b q))
(list (list :a :b)))
(mk-test "cycle-free-no-self-loop" (run* q (cf-patho :a :a q)) (list))
(mk-tests-run!)

View File

@@ -0,0 +1,119 @@
;; lib/minikanren/tests/peano.sx — Peano arithmetic.
;;
;; Builds Peano numbers via a host-side helper so tests stay readable.
;; (mk-nat 3) → (:s (:s (:s :z))).
(define
mk-nat
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
;; --- zeroo ---
(mk-test
"zeroo-zero-succeeds"
(run* q (zeroo :z))
(list (make-symbol "_.0")))
(mk-test
"zeroo-non-zero-fails"
(run* q (zeroo (mk-nat 1)))
(list))
;; --- pluso forward ---
(mk-test
"pluso-forward-2-3"
(run* q (pluso (mk-nat 2) (mk-nat 3) q))
(list (mk-nat 5)))
(mk-test "pluso-forward-zero-zero" (run* q (pluso :z :z q)) (list :z))
(mk-test
"pluso-forward-zero-n"
(run* q (pluso :z (mk-nat 4) q))
(list (mk-nat 4)))
(mk-test
"pluso-forward-n-zero"
(run* q (pluso (mk-nat 4) :z q))
(list (mk-nat 4)))
;; --- pluso backward ---
(mk-test
"pluso-recover-augend"
(run* q (pluso q (mk-nat 2) (mk-nat 5)))
(list (mk-nat 3)))
(mk-test
"pluso-recover-addend"
(run* q (pluso (mk-nat 2) q (mk-nat 5)))
(list (mk-nat 3)))
(mk-test
"pluso-enumerate-pairs-summing-to-3"
(run*
q
(fresh (a b) (pluso a b (mk-nat 3)) (== q (list a b))))
(list
(list :z (mk-nat 3))
(list (mk-nat 1) (mk-nat 2))
(list (mk-nat 2) (mk-nat 1))
(list (mk-nat 3) :z)))
;; --- minuso ---
(mk-test
"minuso-5-2-3"
(run* q (minuso (mk-nat 5) (mk-nat 2) q))
(list (mk-nat 3)))
(mk-test
"minuso-n-n-zero"
(run* q (minuso (mk-nat 7) (mk-nat 7) q))
(list :z))
;; --- *o ---
(mk-test
"times-2-3"
(run* q (*o (mk-nat 2) (mk-nat 3) q))
(list (mk-nat 6)))
(mk-test
"times-zero-anything-zero"
(run* q (*o :z (mk-nat 99) q))
(list :z))
(mk-test
"times-3-4"
(run* q (*o (mk-nat 3) (mk-nat 4) q))
(list (mk-nat 12)))
;; --- lteo / lto ---
(mk-test
"lteo-success"
(run 1 q (lteo (mk-nat 2) (mk-nat 5)))
(list (make-symbol "_.0")))
(mk-test
"lteo-equal-success"
(run 1 q (lteo (mk-nat 3) (mk-nat 3)))
(list (make-symbol "_.0")))
(mk-test
"lteo-greater-fails"
(run* q (lteo (mk-nat 5) (mk-nat 2)))
(list))
(mk-test
"lto-strict-success"
(run 1 q (lto (mk-nat 2) (mk-nat 5)))
(list (make-symbol "_.0")))
(mk-test
"lto-equal-fails"
(run* q (lto (mk-nat 3) (mk-nat 3)))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,87 @@
;; lib/minikanren/tests/predicates.sx — everyo, someo.
;; --- everyo ---
(mk-test
"everyo-empty-trivially-true"
(run* q (everyo (fn (x) (== x 1)) (list)))
(list (make-symbol "_.0")))
(mk-test
"everyo-all-match"
(run*
q
(everyo
(fn (x) (== x 1))
(list 1 1 1)))
(list (make-symbol "_.0")))
(mk-test
"everyo-some-mismatch"
(run*
q
(everyo
(fn (x) (== x 1))
(list 1 2 1)))
(list))
(mk-test
"everyo-with-intarith"
(run*
q
(everyo
(fn (x) (lto-i x 10))
(list 1 5 9)))
(list (make-symbol "_.0")))
(mk-test
"everyo-with-intarith-fail"
(run*
q
(everyo
(fn (x) (lto-i x 5))
(list 1 5 9)))
(list))
;; --- someo ---
(mk-test
"someo-finds-element"
(run*
q
(someo
(fn (x) (== x 2))
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"someo-not-found"
(run*
q
(someo
(fn (x) (== x 99))
(list 1 2 3)))
(list))
(mk-test
"someo-empty-fails"
(run* q (someo (fn (x) (== x 1)) (list)))
(list))
(mk-test
"someo-multiple-matches-yields-multiple"
(let
((res (run* q (fresh (x) (someo (fn (y) (== y x)) (list 1 2 1)) (== q x)))))
(len res))
3)
(mk-test
"someo-with-intarith"
(run*
q
(someo
(fn (x) (lto-i 100 x))
(list 5 50 200)))
(list (make-symbol "_.0")))
(mk-tests-run!)

View File

@@ -0,0 +1,76 @@
;; lib/minikanren/tests/prefix-suffix.sx — appendo-derived sublist relations.
(mk-test
"prefixo-empty"
(run* q (prefixo (list) (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"prefixo-full"
(run*
q
(prefixo
(list 1 2 3)
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"prefixo-partial"
(run*
q
(prefixo
(list 1 2)
(list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"prefixo-mismatch-fails"
(run*
q
(prefixo
(list 1 3)
(list 1 2 3)))
(list))
(mk-test
"prefixo-enumerates-all"
(run* q (prefixo q (list 1 2 3)))
(list
(list)
(list 1)
(list 1 2)
(list 1 2 3)))
(mk-test
"suffixo-empty"
(run* q (suffixo (list) (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"suffixo-full"
(run*
q
(suffixo
(list 1 2 3)
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"suffixo-partial"
(run*
q
(suffixo
(list 2 3)
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"suffixo-enumerates-all"
(run* q (suffixo q (list 1 2 3)))
(list
(list 1 2 3)
(list 2 3)
(list 3)
(list)))
(mk-tests-run!)

View File

@@ -0,0 +1,60 @@
;; lib/minikanren/tests/project.sx — Phase 5 piece B tests for `project`.
;; --- project rebinds vars to ground values for SX use ---
(mk-test
"project-square-via-host"
(run* q (fresh (n) (== n 5) (project (n) (== q (* n n)))))
(list 25))
(mk-test
"project-multi-vars"
(run*
q
(fresh
(a b)
(== a 3)
(== b 4)
(project (a b) (== q (+ a b)))))
(list 7))
(mk-test
"project-with-string-host-op"
(run* q (fresh (s) (== s "hello") (project (s) (== q (str s "!")))))
(list "hello!"))
;; --- project nested inside conde ---
(mk-test
"project-inside-conde"
(run*
q
(fresh
(n)
(conde ((== n 3)) ((== n 4)))
(project (n) (== q (* n 10)))))
(list 30 40))
;; --- project body can be multiple goals (mk-conj'd) ---
(mk-test
"project-multi-goal-body"
(run*
q
(fresh
(n)
(== n 7)
(project (n) (== q (+ n 1)) (== q (+ n 1)))))
(list 8))
(mk-test
"project-multi-goal-body-conflict"
(run*
q
(fresh
(n)
(== n 7)
(project (n) (== q (+ n 1)) (== q (+ n 2)))))
(list))
(mk-tests-run!)

View File

@@ -0,0 +1,36 @@
;; lib/minikanren/tests/pythag.sx — Pythagorean triple search.
;;
;; Uses ino + intarith goals to find triples (a, b, c) with
;; a, b, c ∈ [1..N], a ≤ b, a² + b² = c². With intarith escapes
;; the search runs at host-arithmetic speed.
(define
digits-1-10
(list
1
2
3
4
5
6
7
8
9
10))
(mk-test
"pythag-triples-1-to-10"
(let
((triples (run* q (fresh (a b c a-sq b-sq sum c-sq) (ino a digits-1-10) (ino b digits-1-10) (ino c digits-1-10) (lteo-i a b) (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) (pluso-i a-sq b-sq sum) (== sum c-sq) (== q (list a b c))))))
(and
(= (len triples) 2)
(and
(some
(fn (t) (= t (list 3 4 5)))
triples)
(some
(fn (t) (= t (list 6 8 10)))
triples))))
true)
(mk-tests-run!)

View File

@@ -0,0 +1,45 @@
;; lib/minikanren/tests/queens.sx — N-queens, the classic miniKanren benchmark.
;; --- safe-diag (helper) ---
(mk-test
"safe-diag-different-cols-different-distance"
(run* q (safe-diag 1 4 2))
(list (make-symbol "_.0")))
(mk-test
"safe-diag-same-distance-fails"
(run* q (safe-diag 1 4 3))
(list))
(mk-test
"safe-diag-same-distance-other-direction-fails"
(run* q (safe-diag 4 1 3))
(list))
;; --- ino-each / range ---
(mk-test
"range-1-to-4"
(range-1-to-n 4)
(list 1 2 3 4))
(mk-test "range-empty" (range-1-to-n 0) (list))
;; --- 4-queens: two solutions ---
(mk-test
"queens-4"
(let
((sols (run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols (list a b c d) 4)))))
(and
(= (len sols) 2)
(and
(some
(fn (s) (= s (list 2 4 1 3)))
sols)
(some
(fn (s) (= s (list 3 1 4 2)))
sols))))
true)
(mk-tests-run!)

View File

@@ -0,0 +1,90 @@
;; lib/minikanren/tests/rdb.sx — relational database queries.
;;
;; Demonstrates how miniKanren can serve as a Datalog-style query engine
;; over fact tables. Tables are SX lists of tuples; the relation just
;; wraps `membero` over the table.
(define
rdb-employees
(list
(list "alice" "engineering" 100000)
(list "bob" "marketing" 80000)
(list "carol" "engineering" 90000)
(list "dave" "engineering" 85000)
(list "eve" "sales" 75000)))
(define
rdb-projects
(list
(list "alice" "compiler")
(list "carol" "compiler")
(list "dave" "runtime")
(list "alice" "runtime")
(list "eve" "outreach")))
;; Relation views over the tables.
(define
employees
(fn (name dept salary) (membero (list name dept salary) rdb-employees)))
(define
on-project
(fn (name project) (membero (list name project) rdb-projects)))
;; --- queries ---
(mk-test
"rdb-engineering-staff"
(let
((res (run* q (fresh (n s) (employees n "engineering" s) (== q n)))))
(and
(= (len res) 3)
(and
(some (fn (n) (= n "alice")) res)
(and
(some (fn (n) (= n "carol")) res)
(some (fn (n) (= n "dave")) res)))))
true)
(mk-test
"rdb-high-salary"
(let
((res (run* q (fresh (n d s) (employees n d s) (lto-i 85000 s) (== q (list n s))))))
(and
(= (len res) 2)
(and
(some (fn (r) (= r (list "alice" 100000))) res)
(some (fn (r) (= r (list "carol" 90000))) res))))
true)
(mk-test
"rdb-join-employee-project"
(let
((res (run* q (fresh (n d s) (employees n d s) (on-project n "compiler") (== q n)))))
(and
(= (len res) 2)
(and
(some (fn (n) (= n "alice")) res)
(some (fn (n) (= n "carol")) res))))
true)
(mk-test
"rdb-engineers-on-runtime"
(let
((res (run* q (fresh (n s) (employees n "engineering" s) (on-project n "runtime") (== q n)))))
(and
(= (len res) 2)
(and
(some (fn (n) (= n "alice")) res)
(some (fn (n) (= n "dave")) res))))
true)
(mk-test
"rdb-people-on-multiple-projects"
(let
((res (run* q (fresh (n p1 p2) (on-project n p1) (on-project n p2) (nafc (== p1 p2)) (== q n)))))
(some (fn (n) (= n "alice")) res))
true)
(mk-tests-run!)

View File

@@ -0,0 +1,291 @@
;; lib/minikanren/tests/relations.sx — Phase 4 standard relations.
;;
;; Includes the classic miniKanren canaries: appendo forwards / backwards /
;; bidirectionally, membero, listo enumeration.
;; --- nullo / pairo ---
(mk-test
"nullo-empty-succeeds"
(run* q (nullo (list)))
(list (make-symbol "_.0")))
(mk-test "nullo-non-empty-fails" (run* q (nullo (list 1))) (list))
(mk-test
"pairo-non-empty-succeeds"
(run* q (pairo (list 1 2)))
(list (make-symbol "_.0")))
(mk-test "pairo-empty-fails" (run* q (pairo (list))) (list))
;; --- caro / cdro / firsto / resto ---
(mk-test
"caro-extracts-head"
(run* q (caro (list 1 2 3) q))
(list 1))
(mk-test
"cdro-extracts-tail"
(run* q (cdro (list 1 2 3) q))
(list (list 2 3)))
(mk-test
"firsto-alias-of-caro"
(run* q (firsto (list 10 20) q))
(list 10))
(mk-test
"resto-alias-of-cdro"
(run* q (resto (list 10 20) q))
(list (list 20)))
(mk-test
"caro-cdro-build"
(run*
q
(fresh
(h t)
(caro (list 1 2 3) h)
(cdro (list 1 2 3) t)
(== q (list h t))))
(list (list 1 (list 2 3))))
;; --- conso ---
(mk-test
"conso-forward"
(run* q (conso 0 (list 1 2 3) q))
(list (list 0 1 2 3)))
(mk-test
"conso-extract-head"
(run*
q
(conso
q
(list 2 3)
(list 1 2 3)))
(list 1))
(mk-test
"conso-extract-tail"
(run* q (conso 1 q (list 1 2 3)))
(list (list 2 3)))
;; --- listo ---
(mk-test
"listo-empty-succeeds"
(run* q (listo (list)))
(list (make-symbol "_.0")))
(mk-test
"listo-finite-list-succeeds"
(run* q (listo (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"listo-enumerates-shapes"
(run 3 q (listo q))
(list
(list)
(list (make-symbol "_.0"))
(list (make-symbol "_.0") (make-symbol "_.1"))))
;; --- appendo: the canary ---
(mk-test
"appendo-forward-simple"
(run*
q
(appendo (list 1 2) (list 3 4) q))
(list (list 1 2 3 4)))
(mk-test
"appendo-forward-empty-l"
(run* q (appendo (list) (list 3 4) q))
(list (list 3 4)))
(mk-test
"appendo-forward-empty-s"
(run* q (appendo (list 1 2) (list) q))
(list (list 1 2)))
(mk-test
"appendo-recovers-tail"
(run*
q
(appendo
(list 1 2)
q
(list 1 2 3 4)))
(list (list 3 4)))
(mk-test
"appendo-recovers-prefix"
(run*
q
(appendo
q
(list 3 4)
(list 1 2 3 4)))
(list (list 1 2)))
(mk-test
"appendo-backward-all-splits"
(run*
q
(fresh
(l s)
(appendo l s (list 1 2 3))
(== q (list l s))))
(list
(list (list) (list 1 2 3))
(list (list 1) (list 2 3))
(list (list 1 2) (list 3))
(list (list 1 2 3) (list))))
(mk-test
"appendo-empty-empty-empty"
(run* q (appendo (list) (list) q))
(list (list)))
;; --- membero ---
(mk-test
"membero-element-present"
(run
1
q
(membero 2 (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"membero-element-absent-empty"
(run* q (membero 99 (list 1 2 3)))
(list))
(mk-test
"membero-enumerates"
(run* q (membero q (list "a" "b" "c")))
(list "a" "b" "c"))
;; --- reverseo ---
(mk-test
"reverseo-forward"
(run* q (reverseo (list 1 2 3) q))
(list (list 3 2 1)))
(mk-test "reverseo-empty" (run* q (reverseo (list) q)) (list (list)))
(mk-test
"reverseo-singleton"
(run* q (reverseo (list 42) q))
(list (list 42)))
(mk-test
"reverseo-five"
(run*
q
(reverseo (list 1 2 3 4 5) q))
(list (list 5 4 3 2 1)))
(mk-test
"reverseo-backward-one"
(run 1 q (reverseo q (list 1 2 3)))
(list (list 3 2 1)))
(mk-test
"reverseo-round-trip"
(run*
q
(fresh (mid) (reverseo (list "a" "b" "c") mid) (reverseo mid q)))
(list (list "a" "b" "c")))
;; --- lengtho (Peano-style) ---
(mk-test "lengtho-empty-is-z" (run* q (lengtho (list) q)) (list :z))
(mk-test
"lengtho-of-3"
(run* q (lengtho (list "a" "b" "c") q))
(list (list :s (list :s (list :s :z)))))
(mk-test
"lengtho-empty-from-zero"
(run 1 q (lengtho q :z))
(list (list)))
(mk-test
"lengtho-enumerates-of-length-2"
(run 1 q (lengtho q (list :s (list :s :z))))
(list (list (make-symbol "_.0") (make-symbol "_.1"))))
;; --- inserto ---
(mk-test
"inserto-front"
(run* q (inserto 0 (list 1 2 3) q))
(list
(list 0 1 2 3)
(list 1 0 2 3)
(list 1 2 0 3)
(list 1 2 3 0)))
(mk-test
"inserto-empty"
(run* q (inserto 0 (list) q))
(list (list 0)))
;; --- permuteo ---
(mk-test "permuteo-empty" (run* q (permuteo (list) q)) (list (list)))
(mk-test
"permuteo-singleton"
(run* q (permuteo (list 42) q))
(list (list 42)))
(mk-test
"permuteo-two"
(run* q (permuteo (list 1 2) q))
(list (list 1 2) (list 2 1)))
(mk-test
"permuteo-three-as-set"
(let
((perms (run* q (permuteo (list 1 2 3) q))))
(and
(= (len perms) 6)
(and
(some (fn (p) (= p (list 1 2 3))) perms)
(and
(some
(fn (p) (= p (list 2 1 3)))
perms)
(and
(some
(fn (p) (= p (list 1 3 2)))
perms)
(and
(some
(fn (p) (= p (list 2 3 1)))
perms)
(and
(some
(fn (p) (= p (list 3 1 2)))
perms)
(some
(fn (p) (= p (list 3 2 1)))
perms))))))))
true)
(mk-test
"permuteo-backward-finds-input"
(run 1 q (permuteo q (list "a" "b" "c")))
(list (list "a" "b" "c")))
(mk-tests-run!)

View File

@@ -0,0 +1,39 @@
;; lib/minikanren/tests/removeo-allo.sx — remove every occurrence of x.
(mk-test
"removeo-allo-multi"
(run*
q
(removeo-allo
2
(list 1 2 3 2 4 2)
q))
(list (list 1 3 4)))
(mk-test
"removeo-allo-single"
(run*
q
(removeo-allo 2 (list 1 2 3) q))
(list (list 1 3)))
(mk-test
"removeo-allo-no-match"
(run*
q
(removeo-allo 99 (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"removeo-allo-everything"
(run*
q
(removeo-allo 1 (list 1 1 1) q))
(list (list)))
(mk-test
"removeo-allo-empty"
(run* q (removeo-allo 1 (list) q))
(list (list)))
(mk-tests-run!)

View File

@@ -0,0 +1,69 @@
;; lib/minikanren/tests/repeato-concato.sx — repeat element n times +
;; concatenate a list of lists.
(define
mk-nat
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
;; --- repeato ---
(mk-test
"repeato-zero"
(run* q (repeato :a (mk-nat 0) q))
(list (list)))
(mk-test
"repeato-one"
(run* q (repeato :a (mk-nat 1) q))
(list (list :a)))
(mk-test
"repeato-three"
(run* q (repeato :a (mk-nat 3) q))
(list (list :a :a :a)))
(mk-test
"repeato-numeric"
(run* q (repeato 7 (mk-nat 4) q))
(list (list 7 7 7 7)))
(mk-test
"repeato-recover-count"
(run* q (repeato :x q (list :x :x :x :x)))
(list (mk-nat 4)))
;; --- concato ---
(mk-test "concato-empty" (run* q (concato (list) q)) (list (list)))
(mk-test
"concato-single"
(run* q (concato (list (list 1 2 3)) q))
(list (list 1 2 3)))
(mk-test
"concato-multi"
(run*
q
(concato
(list
(list 1 2)
(list 3)
(list 4 5 6))
q))
(list
(list 1 2 3 4 5 6)))
(mk-test
"concato-all-empty"
(run* q (concato (list (list) (list) (list)) q))
(list (list)))
(mk-test
"concato-mixed-empty"
(run*
q
(concato
(list (list 1) (list) (list 2 3))
q))
(list (list 1 2 3)))
(mk-tests-run!)

View File

@@ -0,0 +1,46 @@
;; lib/minikanren/tests/rev-acco.sx — accumulator-style reverse.
;;
;; Faster than reverseo for forward queries (no quadratic appendos).
;; Trade-off: rev-acco is asymmetric (acc=initial-empty for the public
;; interface), so it does not cleanly run backwards in run* the way
;; reverseo does.
(mk-test "rev-2o-empty" (run* q (rev-2o (list) q)) (list (list)))
(mk-test
"rev-2o-singleton"
(run* q (rev-2o (list 7) q))
(list (list 7)))
(mk-test
"rev-2o-three"
(run* q (rev-2o (list 1 2 3) q))
(list (list 3 2 1)))
(mk-test
"rev-2o-five"
(run*
q
(rev-2o (list 1 2 3 4 5) q))
(list (list 5 4 3 2 1)))
(mk-test
"rev-2o-strings"
(run* q (rev-2o (list "a" "b" "c") q))
(list (list "c" "b" "a")))
(mk-test
"rev-2o-reverseo-agree"
(let
((via-reverseo (first (run* q (reverseo (list 1 2 3 4 5) q))))
(via-rev-2o
(first
(run*
q
(rev-2o
(list 1 2 3 4 5)
q)))))
(= via-reverseo via-rev-2o))
true)
(mk-tests-run!)

114
lib/minikanren/tests/run.sx Normal file
View File

@@ -0,0 +1,114 @@
;; lib/minikanren/tests/run.sx — Phase 3 tests for run* / run / reify.
;; --- canonical TRS one-liners ---
(mk-test "run*-eq-one" (run* q (== q 1)) (list 1))
(mk-test "run*-eq-string" (run* q (== q "hello")) (list "hello"))
(mk-test "run*-eq-symbol" (run* q (== q (quote sym))) (list (quote sym)))
(mk-test "run*-fail-empty" (run* q (== 1 2)) (list))
;; --- run with a count ---
(mk-test
"run-3-of-many"
(run
3
q
(conde
((== q 1))
((== q 2))
((== q 3))
((== q 4))
((== q 5))))
(list 1 2 3))
(mk-test "run-zero-empty" (run 0 q (== q 1)) (list))
(mk-test
"run-1-takes-one"
(run 1 q (conde ((== q "a")) ((== q "b"))))
(list "a"))
;; --- reification: unbound vars get _.N left-to-right ---
(mk-test
"reify-single-unbound"
(run* q (fresh (x) (== q x)))
(list (make-symbol "_.0")))
(mk-test
"reify-pair-unbound"
(run* q (fresh (x y) (== q (list x y))))
(list (list (make-symbol "_.0") (make-symbol "_.1"))))
(mk-test
"reify-mixed-bound-unbound"
(run* q (fresh (x y) (== q (list 1 x 2 y))))
(list
(list 1 (make-symbol "_.0") 2 (make-symbol "_.1"))))
(mk-test
"reify-shared-unbound-same-name"
(run* q (fresh (x) (== q (list x x))))
(list (list (make-symbol "_.0") (make-symbol "_.0"))))
(mk-test
"reify-distinct-unbound-distinct-names"
(run* q (fresh (x y) (== q (list x y x y))))
(list
(list
(make-symbol "_.0")
(make-symbol "_.1")
(make-symbol "_.0")
(make-symbol "_.1"))))
;; --- conde + run* ---
(mk-test
"run*-conde-three"
(run*
q
(conde ((== q 1)) ((== q 2)) ((== q 3))))
(list 1 2 3))
(mk-test
"run*-conde-fresh-mix"
(run*
q
(conde ((fresh (x) (== q (list 1 x)))) ((== q "ground"))))
(list (list 1 (make-symbol "_.0")) "ground"))
;; --- run* + conjunction ---
(mk-test
"run*-conj-binds-q"
(run* q (fresh (x) (== x 5) (== q (list x x))))
(list (list 5 5)))
;; --- run* + condu ---
(mk-test
"run*-condu-first-wins"
(run* q (condu ((== q 1)) ((== q 2))))
(list 1))
(mk-test
"run*-onceo-trim"
(run* q (onceo (conde ((== q "a")) ((== q "b")))))
(list "a"))
;; --- multi-goal run ---
(mk-test
"run*-three-goals"
(run*
q
(fresh
(x y z)
(== x 1)
(== y 2)
(== z 3)
(== q (list x y z))))
(list (list 1 2 3)))
(mk-tests-run!)

View File

@@ -0,0 +1,46 @@
;; lib/minikanren/tests/selecto.sx — choose an element + rest of list.
(mk-test
"selecto-enumerate"
(run*
q
(fresh
(x r)
(selecto x r (list 1 2 3))
(== q (list x r))))
(list
(list 1 (list 2 3))
(list 2 (list 1 3))
(list 3 (list 1 2))))
(mk-test
"selecto-find-rest"
(run* q (selecto 2 q (list 1 2 3)))
(list (list 1 3)))
(mk-test
"selecto-find-element"
(run*
q
(selecto
q
(list 1 3)
(list 1 2 3)))
(list 2))
(mk-test
"selecto-element-not-present-fails"
(run* q (selecto 99 q (list 1 2 3)))
(list))
(mk-test
"selecto-empty-list-fails"
(run* q (selecto q (list) (list)))
(list))
(mk-test
"selecto-singleton"
(run* q (fresh (x r) (selecto x r (list :only)) (== q (list x r))))
(list (list :only (list))))
(mk-tests-run!)

View File

@@ -0,0 +1,40 @@
;; lib/minikanren/tests/sortedo.sx — checks list is non-decreasing.
(mk-test
"sortedo-empty"
(run* q (sortedo (list)))
(list (make-symbol "_.0")))
(mk-test
"sortedo-singleton"
(run* q (sortedo (list 42)))
(list (make-symbol "_.0")))
(mk-test
"sortedo-ascending"
(run* q (sortedo (list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"sortedo-with-equal-adjacent"
(run*
q
(sortedo (list 1 1 2 2 3)))
(list (make-symbol "_.0")))
(mk-test
"sortedo-out-of-order-fails"
(run* q (sortedo (list 1 3 2)))
(list))
(mk-test
"sortedo-descending-fails"
(run* q (sortedo (list 3 2 1)))
(list))
(mk-test
"sortedo-pair-equal"
(run* q (sortedo (list 5 5)))
(list (make-symbol "_.0")))
(mk-tests-run!)

View File

@@ -0,0 +1,60 @@
;; lib/minikanren/tests/subo.sx — contiguous-sublist relation.
(mk-test
"subo-simple-found"
(run*
q
(subo
(list 2 3)
(list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"subo-not-contiguous-fails"
(run*
q
(subo
(list 2 4)
(list 1 2 3 4)))
(list))
(mk-test
"subo-full-list-found"
(run*
q
(subo
(list 1 2 3)
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"subo-empty-list-found"
(let
((res (run* q (subo (list) (list 1 2 3)))))
(= (len res) 4))
true)
(mk-test
"subo-prefix"
(run*
q
(subo
(list 1 2)
(list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"subo-suffix"
(run*
q
(subo
(list 3 4)
(list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"subo-strings"
(run* q (subo (list "b" "c") (list "a" "b" "c" "d")))
(list (make-symbol "_.0")))
(mk-tests-run!)

View File

@@ -0,0 +1,62 @@
;; lib/minikanren/tests/subseto.sx — every element of l1 is in l2.
(mk-test
"subseto-empty"
(run* q (subseto (list) (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"subseto-singleton-yes"
(run*
q
(subseto (list 2) (list 1 2 3)))
(list (make-symbol "_.0")))
(mk-test
"subseto-singleton-no"
(run*
q
(subseto (list 99) (list 1 2 3)))
(list))
(mk-test
"subseto-multi-yes"
(run
1
q
(subseto
(list 1 3)
(list 1 2 3 4)))
(list (make-symbol "_.0")))
(mk-test
"subseto-multi-no"
(run*
q
(subseto
(list 1 99)
(list 1 2 3)))
(list))
(mk-test
"subseto-equal-sets"
(run
1
q
(subseto
(list 1 2 3)
(list 1 2 3)))
(list (make-symbol "_.0")))
;; allow duplicates in l1 — each just needs membership in l2.
(mk-test
"subseto-duplicates-allowed"
(run
1
q
(subseto
(list 1 1 2)
(list 1 2 3)))
(list (make-symbol "_.0")))
(mk-tests-run!)

View File

@@ -0,0 +1,44 @@
;; lib/minikanren/tests/sum-product.sx — fold list to integer.
(mk-test "sumo-empty" (run* q (sumo (list) q)) (list 0))
(mk-test
"sumo-1-to-5"
(run*
q
(sumo (list 1 2 3 4 5) q))
(list 15))
(mk-test
"sumo-zeros"
(run* q (sumo (list 0 0 0) q))
(list 0))
(mk-test
"sumo-negs"
(run* q (sumo (list 5 -3 8) q))
(list 10))
(mk-test "producto-empty" (run* q (producto (list) q)) (list 1))
(mk-test
"producto-1-to-4"
(run* q (producto (list 1 2 3 4) q))
(list 24))
(mk-test
"producto-with-0"
(run* q (producto (list 5 0 7) q))
(list 0))
(mk-test
"producto-of-1s"
(run* q (producto (list 1 1 1) q))
(list 1))
(mk-test
"sum-product-pythagorean-square"
(run*
q
(fresh
(s sq2)
(sumo (list 3 4 5) s)
(producto (list 3 3) sq2)
(== q (list s sq2))))
(list (list 12 9)))
(mk-tests-run!)

View File

@@ -0,0 +1,32 @@
;; lib/minikanren/tests/swap-firsto.sx — swap first two elements.
(mk-test
"swap-firsto-pair"
(run* q (swap-firsto (list 1 2) q))
(list (list 2 1)))
(mk-test
"swap-firsto-with-tail"
(run* q (swap-firsto (list 1 2 3 4) q))
(list (list 2 1 3 4)))
(mk-test
"swap-firsto-singleton-fails"
(run* q (swap-firsto (list 1) q))
(list))
(mk-test "swap-firsto-empty-fails" (run* q (swap-firsto (list) q)) (list))
(mk-test
"swap-firsto-self-inverse"
(run*
q
(fresh (mid) (swap-firsto (list :a :b :c :d) mid) (swap-firsto mid q)))
(list (list :a :b :c :d)))
(mk-test
"swap-firsto-backward"
(run* q (swap-firsto q (list :y :x :z)))
(list (list :x :y :z)))
(mk-tests-run!)

View File

@@ -0,0 +1,92 @@
;; lib/minikanren/tests/take-drop.sx — Peano-indexed prefix/suffix.
(define
mk-nat
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
;; --- tako ---
(mk-test
"tako-zero"
(run*
q
(tako (mk-nat 0) (list 1 2 3) q))
(list (list)))
(mk-test
"tako-two"
(run*
q
(tako
(mk-nat 2)
(list 1 2 3 4 5)
q))
(list (list 1 2)))
(mk-test
"tako-all"
(run*
q
(tako (mk-nat 3) (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"tako-too-many"
(run*
q
(tako (mk-nat 5) (list 1 2 3) q))
(list))
;; --- dropo ---
(mk-test
"dropo-zero"
(run*
q
(dropo (mk-nat 0) (list 1 2 3) q))
(list (list 1 2 3)))
(mk-test
"dropo-two"
(run*
q
(dropo
(mk-nat 2)
(list 1 2 3 4 5)
q))
(list (list 3 4 5)))
(mk-test
"dropo-all"
(run*
q
(dropo (mk-nat 3) (list 1 2 3) q))
(list (list)))
(mk-test
"dropo-too-many"
(run*
q
(dropo (mk-nat 5) (list 1 2 3) q))
(list))
;; --- take + drop round-trip ---
(mk-test
"tako-dropo-roundtrip"
(run*
q
(fresh
(p s)
(tako
(mk-nat 2)
(list 1 2 3 4 5)
p)
(dropo
(mk-nat 2)
(list 1 2 3 4 5)
s)
(appendo p s q)))
(list (list 1 2 3 4 5)))
(mk-tests-run!)

View File

@@ -0,0 +1,52 @@
;; lib/minikanren/tests/types.sx — type-predicate goals.
(mk-test
"numbero-on-int"
(run* q (numbero 5))
(list (make-symbol "_.0")))
(mk-test "numbero-on-string" (run* q (numbero "5")) (list))
(mk-test "numbero-on-symbol" (run* q (numbero (quote x))) (list))
(mk-test "numbero-on-list" (run* q (numbero (list 1))) (list))
(mk-test
"stringo-on-string"
(run* q (stringo "hi"))
(list (make-symbol "_.0")))
(mk-test "stringo-on-int" (run* q (stringo 5)) (list))
(mk-test
"stringo-on-keyword"
(run* q (stringo :k))
(list (make-symbol "_.0"))) ;; SX keywords ARE strings
(mk-test
"symbolo-on-symbol"
(run* q (symbolo (quote x)))
(list (make-symbol "_.0")))
(mk-test "symbolo-on-string" (run* q (symbolo "x")) (list))
(mk-test "symbolo-on-int" (run* q (symbolo 5)) (list))
;; --- combine with membero for type-filtered enumeration ---
(mk-test
"membero-numbero-filter"
(run*
q
(fresh
(x)
(membero x (list 1 "a" 2 "b" 3))
(numbero x)
(== q x)))
(list 1 2 3))
(mk-test
"membero-stringo-filter"
(run*
q
(fresh
(x)
(membero x (list 1 "a" 2 "b" 3))
(stringo x)
(== q x)))
(list "a" "b"))
(mk-tests-run!)

View File

@@ -0,0 +1,293 @@
;; lib/minikanren/tests/unify.sx — Phase 1 tests for unify.sx.
;;
;; Loads into a session that already has lib/guest/match.sx and
;; lib/minikanren/unify.sx defined. Tests are top-level forms.
;; Call (mk-tests-run!) afterwards to get the totals.
;;
;; Note: SX dict equality is reference-based, so tests check the *effect*
;; of a unification (success/failure flag, or walked bindings) rather than
;; the raw substitution dict.
(define mk-test-pass 0)
(define mk-test-fail 0)
(define mk-test-fails (list))
(define
mk-test
(fn
(name actual expected)
(if
(= actual expected)
(set! mk-test-pass (+ mk-test-pass 1))
(begin
(set! mk-test-fail (+ mk-test-fail 1))
(append! mk-test-fails {:name name :expected expected :actual actual})))))
(define mk-tests-run! (fn () {:total (+ mk-test-pass mk-test-fail) :passed mk-test-pass :failed mk-test-fail :fails mk-test-fails}))
(define mk-unified? (fn (s) (if (= s nil) false true)))
;; --- fresh variable construction ---
(mk-test
"make-var-distinct"
(let ((a (make-var)) (b (make-var))) (= (var-name a) (var-name b)))
false)
(mk-test "make-var-is-var" (mk-var? (make-var)) true)
(mk-test "var?-num" (mk-var? 5) false)
(mk-test "var?-list" (mk-var? (list 1 2)) false)
(mk-test "var?-string" (mk-var? "hi") false)
(mk-test "var?-empty" (mk-var? (list)) false)
(mk-test "var?-bool" (mk-var? true) false)
;; --- empty substitution ---
(mk-test "empty-s-walk-num" (mk-walk 5 empty-s) 5)
(mk-test "empty-s-walk-str" (mk-walk "x" empty-s) "x")
(mk-test
"empty-s-walk-list"
(mk-walk (list 1 2) empty-s)
(list 1 2))
(mk-test
"empty-s-walk-unbound-var"
(let ((x (make-var))) (= (mk-walk x empty-s) x))
true)
;; --- walk: top-level chain resolution ---
(mk-test
"walk-direct-binding"
(mk-walk (mk-var "x") (extend "x" 7 empty-s))
7)
(mk-test
"walk-two-step-chain"
(mk-walk
(mk-var "x")
(extend "x" (mk-var "y") (extend "y" 9 empty-s)))
9)
(mk-test
"walk-three-step-chain"
(mk-walk
(mk-var "a")
(extend
"a"
(mk-var "b")
(extend "b" (mk-var "c") (extend "c" 42 empty-s))))
42)
(mk-test
"walk-stops-at-list"
(mk-walk (list 1 (mk-var "x")) (extend "x" 5 empty-s))
(list 1 (mk-var "x")))
;; --- walk*: deep walk into lists ---
(mk-test
"walk*-flat-list-with-vars"
(mk-walk*
(list (mk-var "x") 2 (mk-var "y"))
(extend "x" 1 (extend "y" 3 empty-s)))
(list 1 2 3))
(mk-test
"walk*-nested-list"
(mk-walk*
(list 1 (mk-var "x") (list 2 (mk-var "y")))
(extend "x" 5 (extend "y" 6 empty-s)))
(list 1 5 (list 2 6)))
(mk-test
"walk*-unbound-stays-var"
(let
((x (mk-var "x")))
(= (mk-walk* (list 1 x) empty-s) (list 1 x)))
true)
(mk-test "walk*-atom" (mk-walk* 5 empty-s) 5)
;; --- unify atoms (success / failure semantics, not dict shape) ---
(mk-test
"unify-num-eq-succeeds"
(mk-unified? (mk-unify 5 5 empty-s))
true)
(mk-test "unify-num-neq-fails" (mk-unify 5 6 empty-s) nil)
(mk-test
"unify-str-eq-succeeds"
(mk-unified? (mk-unify "a" "a" empty-s))
true)
(mk-test "unify-str-neq-fails" (mk-unify "a" "b" empty-s) nil)
(mk-test
"unify-bool-eq-succeeds"
(mk-unified? (mk-unify true true empty-s))
true)
(mk-test "unify-bool-neq-fails" (mk-unify true false empty-s) nil)
(mk-test
"unify-nil-eq-succeeds"
(mk-unified? (mk-unify nil nil empty-s))
true)
(mk-test
"unify-empty-list-succeeds"
(mk-unified? (mk-unify (list) (list) empty-s))
true)
;; --- unify var with anything (walk to verify binding) ---
(mk-test
"unify-var-num-binds"
(mk-walk (mk-var "x") (mk-unify (mk-var "x") 5 empty-s))
5)
(mk-test
"unify-num-var-binds"
(mk-walk (mk-var "x") (mk-unify 5 (mk-var "x") empty-s))
5)
(mk-test
"unify-var-list-binds"
(mk-walk
(mk-var "x")
(mk-unify (mk-var "x") (list 1 2) empty-s))
(list 1 2))
(mk-test
"unify-var-var-same-no-extend"
(mk-unified? (mk-unify (mk-var "x") (mk-var "x") empty-s))
true)
(mk-test
"unify-var-var-different-walks-equal"
(let
((s (mk-unify (mk-var "x") (mk-var "y") empty-s)))
(= (mk-walk (mk-var "x") s) (mk-walk (mk-var "y") s)))
true)
;; --- unify lists positionally ---
(mk-test
"unify-list-equal-succeeds"
(mk-unified?
(mk-unify
(list 1 2 3)
(list 1 2 3)
empty-s))
true)
(mk-test
"unify-list-different-length-fails-1"
(mk-unify
(list 1 2)
(list 1 2 3)
empty-s)
nil)
(mk-test
"unify-list-different-length-fails-2"
(mk-unify
(list 1 2 3)
(list 1 2)
empty-s)
nil)
(mk-test
"unify-list-mismatch-fails"
(mk-unify
(list 1 2)
(list 1 3)
empty-s)
nil)
(mk-test
"unify-list-vs-atom-fails"
(mk-unify (list 1 2) 5 empty-s)
nil)
(mk-test
"unify-empty-vs-non-empty-fails"
(mk-unify (list) (list 1) empty-s)
nil)
(mk-test
"unify-list-with-vars-walks"
(mk-walk*
(list (mk-var "x") (mk-var "y"))
(mk-unify
(list (mk-var "x") (mk-var "y"))
(list 1 2)
empty-s))
(list 1 2))
(mk-test
"unify-nested-lists-with-vars-walks"
(mk-walk*
(list (mk-var "x") (list (mk-var "y") 3))
(mk-unify
(list (mk-var "x") (list (mk-var "y") 3))
(list 1 (list 2 3))
empty-s))
(list 1 (list 2 3)))
;; --- unify chained substitutions ---
(mk-test
"unify-chain-var-var-then-atom"
(let
((x (mk-var "x")) (y (mk-var "y")))
(let
((s1 (mk-unify x y empty-s)))
(mk-walk x (mk-unify y 7 s1))))
7)
(mk-test
"unify-already-bound-consistent"
(let
((s (extend "x" 5 empty-s)))
(mk-unified? (mk-unify (mk-var "x") 5 s)))
true)
(mk-test
"unify-already-bound-conflict-fails"
(let
((s (extend "x" 5 empty-s)))
(mk-unify (mk-var "x") 6 s))
nil)
;; --- occurs check (opt-in) ---
(mk-test
"unify-no-occurs-default-succeeds"
(let
((x (mk-var "x")))
(mk-unified? (mk-unify x (list 1 x) empty-s)))
true)
(mk-test
"unify-occurs-direct-fails"
(let ((x (mk-var "x"))) (mk-unify-check x (list 1 x) empty-s))
nil)
(mk-test
"unify-occurs-nested-fails"
(let
((x (mk-var "x")))
(mk-unify-check x (list 1 (list 2 x)) empty-s))
nil)
(mk-test
"unify-occurs-non-occurring-succeeds"
(let
((x (mk-var "x")))
(mk-unified? (mk-unify-check x 5 empty-s)))
true)
(mk-test
"unify-occurs-via-chain-fails"
(let
((x (mk-var "x")) (y (mk-var "y")))
(let ((s (extend "y" (list x) empty-s))) (mk-unify-check x y s)))
nil)
(mk-tests-run!)

82
lib/minikanren/unify.sx Normal file
View File

@@ -0,0 +1,82 @@
;; lib/minikanren/unify.sx — Phase 1 + cons-cell extension.
;;
;; miniKanren-on-SX, built on lib/guest/match.sx. The kit ships the heavy
;; lifting (walk-with, unify-with, occurs-with, extend, empty-subst,
;; mk-var/is-var?/var-name); this file supplies a miniKanren-shaped cfg
;; and a thin public API.
;;
;; Term shapes:
;; logic var : (:var NAME) — kit's mk-var
;; cons cell : (:cons HEAD TAIL) — for relational programming
;; (built by mk-cons; lets relations decompose lists by
;; head/tail without proper improper pairs in the host)
;; native list : SX list (a b c) — also unifies pair-style:
;; args = (head, tail) so (1 2 3) ≡ (:cons 1 (:cons 2 (:cons 3 ())))
;; atom : number / string / symbol / boolean / nil / ()
;;
;; Substitution: SX dict mapping VAR-NAME → term. Empty = (empty-subst).
(define mk-cons (fn (h t) (list :cons h t)))
(define
mk-cons-cell?
(fn (t) (and (list? t) (not (empty? t)) (= (first t) :cons))))
(define mk-cons-head (fn (t) (nth t 1)))
(define mk-cons-tail (fn (t) (nth t 2)))
(define
mk-list-pair?
(fn (t) (and (list? t) (not (empty? t)) (not (is-var? t)))))
(define mk-list-pair-head (fn (t) :pair))
(define
mk-list-pair-args
(fn
(t)
(cond
((mk-cons-cell? t) (list (mk-cons-head t) (mk-cons-tail t)))
(:else (list (first t) (rest t))))))
(define mk-cfg {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? false :var-name var-name :ctor-args mk-list-pair-args})
(define mk-cfg-occurs {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? true :var-name var-name :ctor-args mk-list-pair-args})
(define empty-s (empty-subst))
(define mk-fresh-counter 0)
(define
make-var
(fn
()
(begin
(set! mk-fresh-counter (+ mk-fresh-counter 1))
(mk-var (str "_." mk-fresh-counter)))))
(define mk-var? is-var?)
(define mk-walk (fn (t s) (walk-with mk-cfg t s)))
(define
mk-walk*
(fn
(t s)
(let
((w (mk-walk t s)))
(cond
((mk-cons-cell? w)
(let
((h (mk-walk* (mk-cons-head w) s))
(tl (mk-walk* (mk-cons-tail w) s)))
(cond
((empty? tl) (list h))
((mk-cons-cell? tl) tl)
((list? tl) (cons h tl))
(:else (mk-cons h tl)))))
((mk-list-pair? w) (map (fn (a) (mk-walk* a s)) w))
(:else w)))))
(define mk-unify (fn (u v s) (unify-with mk-cfg u v s)))
(define mk-unify-check (fn (u v s) (unify-with mk-cfg-occurs u v s)))

View File

@@ -50,68 +50,106 @@ Key semantic mappings:
## Roadmap ## Roadmap
### Phase 1 — variables + unification ### Phase 1 — variables + unification
- [ ] `make-var` → fresh logic variable (unique mutable box) - [x] `make-var` → fresh logic variable (unique mutable box)
- [ ] `var?` `v` → bool — is this a logic variable? - [x] `var?` `v` → bool — is this a logic variable?
- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var - [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts) - [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure) - [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
Handles: var/var, var/term, term/var, list unification, number/string/symbol equality. Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
No occurs check by default; `unify-check` with occurs check as opt-in. No occurs check by default; `unify-check` with occurs check as opt-in.
- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list) - [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs - [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
### Phase 2 — streams + goals ### Phase 2 — streams + goals
- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`), - [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave),
`mplus` (interleave two streams), `bind` (apply goal to stream) `mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host
- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy `bind` primitive that silently shadows user defines.
- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))` - [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends
- [ ] `succeed` / `fail` — trivial goals and swaps when its left operand is paused, giving fair interleaving.
- [ ] `fresh` `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many - [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))`
- [ ] `conde` — interleaving disjunction of goal lists - [x] `==-check` — opt-in occurs-checked equality goal
- [ ] `condu` — committed choice (soft-cut): only explores first successful clause - [x] `succeed` / `fail` — trivial goals
- [ ] `onceo` — succeeds at most once - [x] `conj2` / `mk-conj` (variadic) — sequential conjunction
- [ ] Tests: basic goal composition, backtracking, interleaving - [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde`
adds the implicit-conj-per-clause sugar later)
- [x] `fresh` — introduces logic variables inside a goal body. Implemented as a
defmacro: `(fresh (x y) g1 g2 ...)``(let ((x (make-var)) (y (make-var)))
(mk-conj g1 g2 ...))`. Also `call-fresh` for programmatic goal building.
- [x] `conde` — sugar over disj+conj, one row per clause; defmacro that
wraps each clause body in `mk-conj` and folds via `mk-disj`. Notes:
with eager streams ordering is left-clause-first DFS; true interleaving
requires paused thunks (Phase 4 recursive relations).
- [x] `condu` — committed choice. defmacro folding clauses into a runtime
`condu-try` walker; first clause whose head goal yields a non-empty
stream commits its first answer, rest-goals run on that single subst.
- [x] `onceo``(stream-take 1 (g s))`; trims a goal's stream to ≤1 answer.
- [x] Tests: basic goal composition, backtracking, interleaving (110 cumulative)
### Phase 3 — run + reification ### Phase 3 — run + reification
- [ ] `run*` `goal` → list of all answers (reified) - [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as
- [ ] `run n` `goal` → list of first n answers fresh var, conj goals, take all from stream, reify each.
- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names - [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all)
- [ ] `reify-s` builds reification substitution for naming unbound vars consistently - [x] `reify` `term` `subst` → walk* + build reification subst + walk* again
- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar - [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a
- [ ] Query variable conventions: `q` as canonical query variable `_.N` symbol via `(make-symbol (str "_." n))`
- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))``(1)`, - [x] `fresh` with multiple variables — already shipped Phase 2B.
- [x] Query variable conventions: `q` as canonical query variable (matches TRS)
- [x] Tests: classic miniKanren programs — `(run* q (== q 1))``(1)`,
`(run* q (conde ((== q 1)) ((== q 2))))``(1 2)`, `(run* q (conde ((== q 1)) ((== q 2))))``(1 2)`,
Peano arithmetic, `appendo` preview `(run* q (fresh (x y) (== q (list x y))))``((_.0 _.1))`. Peano +
`appendo` deferred to Phase 4.
### Phase 4 — standard relations ### Phase 4 — standard relations
- [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards - [x] `appendo` `l` `s` `ls` — list append, runs forwards AND backwards.
- [ ] `membero` `x` `l` — x is a member of l Canary green: `(run* q (appendo (1 2) (3 4) q))``((1 2 3 4))`;
- [ ] `listo` `l` — l is a proper list `(run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s))))`
- [ ] `nullo` `l` — l is empty all four splits.
- [ ] `pairo` `p` — p is a pair (cons cell) - [x] `membero` `x` `l` — enumerates: `(run* q (membero q (a b c)))``(a b c)`
- [ ] `caro` `p` `a` — car of pair - [x] `listo` `l` — l is a proper list; enumerates list shapes with laziness
- [ ] `cdro` `p` `d` — cdr of pair - [x] `nullo` `l` — l is empty
- [ ] `conso` `a` `d` `p` — cons - [x] `pairo` `p` — p is a (non-empty) cons-cell / list
- [ ] `firsto` / `resto` — aliases for caro/cdro - [x] `caro` / `cdro` / `conso` / `firsto` / `resto`
- [ ] `reverseo` `l` `r` — reverse of list - [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean,
- [ ] `flatteno` `l` `f` — flatten nested lists `run*` diverges due to interleaved unbounded list search (canonical TRS issue).
- [ ] `permuteo` `l` `p`permutation of list - [x] `flatteno` `l` `f`flatten nested lists. Three conde clauses:
- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer) empty → empty; pair → recurse on car & cdr + appendo; otherwise atom →
- [ ] Tests: run each relation forwards and backwards; generate from partial inputs `(== flat (list tree))`. Atom-ness is asserted via `nafc (nullo tree)
+ nafc (pairo tree)` — both succeed only when tree is a ground non-list.
Works on ground inputs.
- [x] `permuteo` `l` `p` — permutation of list. Built on `inserto` (insert at any
position) and recursive permutation of tail. All 6 perms of (1 2 3) generated
forward; backward `run 1 q (permuteo q (a b c))` finds the input.
- [x] `lengtho` `l` `n` — length as a relation, Peano-encoded:
`:z` / `(:s :z)` / `(:s (:s :z))` ... matches TRS. Forward is direct;
backward enumerates lists of a given length.
- [x] Tests: run each relation forwards and backwards (so far 25 in
`tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
### Phase 5 — `project` + `matche` + negation ### Phase 5 — `project` + `matche` + negation
- [ ] `project` `(x ...) body`access reified values of logic vars inside a goal; - [x] `project` `(x ...) body`defmacro: rebinds named vars to `(mk-walk* var s)`
escapes to ground values for arithmetic or string ops in the body's lexical scope, then runs `(mk-conj body...)` on the same
- [ ] `matche` — pattern matching over logic terms (extension from core.logic) substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
`(matche l ((head . tail) goal) (() goal))` - [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` /
- [ ] `conda` — soft-cut disjunction (like Prolog `->`) symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes
- [ ] `condu` — committed choice (already in phase 2; refine semantics here) `(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol
- [ ] `nafc` — negation as finite failure with constraint names in a pattern produce the same fresh var, so they unify (== check).
Built without quasiquote (the expander does not recurse into lambda
bodies). Fixed-length list patterns only — head/tail destructuring uses
`(fresh (a d) (conso a d target) body)` directly.
- [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
- [x] `condu` — committed choice (Phase 2)
- [x] `nafc` — negation as finite failure: `(nafc g)` yields the input subst
iff g has zero answers. Standard caveats apply (open-world unsoundness;
diverges if g is infinite). `Phase 5 piece C`.
- [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche` - [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche`
### Phase 6 — arithmetic constraints CLP(FD) ### Phase 6 — arithmetic constraints CLP(FD)
- [ ] Finite domain variables: `fd-var` with domain `[lo..hi]` - [ ] Finite domain variables: `fd-var` with domain `[lo..hi]`
- [ ] `in` `x` `domain`constrain x to domain - [x] `ino` `x` `domain`alias for `(membero x domain)` with the
constraint-store-friendly argument order. Sufficient for the
enumerate-then-filter style of finite-domain solving.
- [x] `all-distincto` `l` — pairwise-distinct elements via `nafc + membero`.
- [ ] `fd-eq` `x` `y` — x = y (constraint propagation) - [ ] `fd-eq` `x` `y` — x = y (constraint propagation)
- [ ] `fd-neq` `x` `y` — x ≠ y - [ ] `fd-neq` `x` `y` — x ≠ y
- [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints - [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints
@@ -135,4 +173,217 @@ _(none yet)_
_Newest first._ _Newest first._
_(awaiting phase 1)_ - **2026-05-08** — **enumerate-i / enumerate-from-i — 500-test milestone**: index-each-element relations. (enumerate-i l result) -> result is l with each element paired with its 0-based index. (enumerate-from-i n l result) starts at n. 5 new tests, **501/501** cumulative.
- **2026-05-08** — **partitiono**: relational partition. (partitiono pred l yes no) splits l so yes contains elements where pred succeeds and no contains the rest. Composes with intarith for numeric predicates. 5 new tests, 496/496 cumulative.
- **2026-05-08** — **appendo3**: 3-list append via two appendos. (appendo3 a b c r) is (appendo a b mid) ∧ (appendo mid c r). Recovers any of the three lists given the other two and the result. 5 new tests, 491/491 cumulative.
- **2026-05-08** — **lengtho-i**: integer-indexed length (intarith). Empty list -> 0; recurse with pluso-i. Drop-in fast replacement for Peano lengtho when the count fits in a host integer. 5 new tests, 486/486 cumulative.
- **2026-05-08** — **sumo + producto (intarith)**: fold a list of ground integers to its sum or product. Empty list -> identity (0 / 1). Recurse via pluso-i / *o-i. 9 new tests, 481/481 cumulative.
- **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative.
- **2026-05-08** — **sortedo (intarith)**: list is non-decreasing under integer ordering. Three conde clauses: empty / singleton / pair-and-recurse. Uses lteo-i for the adjacent-pair check (ground integers). 7 new tests, 463/463 cumulative.
- **2026-05-08** — **subseto**: every element of l1 is a member of l2. Recurses on l1, checking each element via membero. Allows duplicates in l1 (each independently in l2). 7 new tests, 456/456 cumulative.
- **2026-05-08** — **cycle-free path search**: mitigation for the cyclic-graph divergence — thread a accumulator through the recursion, gate each step with nafc + membero on visited. Terminates on graphs with cycles; no Phase-7 tabling required for the simple case. 3 new tests, 449/449 cumulative.
- **2026-05-08** — **removeo-allo**: removes every occurrence of x (vs rembero, which removes only the first). Three conde clauses: empty -> empty; head matches -> skip and recurse; head differs (nafc) -> keep and recurse. 5 new tests, 446/446 cumulative.
- **2026-05-08** — **btree-walko (matche showcase)**: walks a binary tree (:leaf v) | (:node l r) and emits each leaf value via conde. Demonstrates matche dispatch on tagged-list patterns, recursion through both branches via conde, and run* enumerating all 5 leaves of a small tree. 4 new tests, 441/441 cumulative.
- **2026-05-08** — **swap-firsto**: swap the first two elements of a list. Built via four conso constraints. Self-inverse on length-2+ lists; runs forward and backward. 6 new tests, 437/437 cumulative.
- **2026-05-08** — **pairlisto**: relational zip — pairs is the zipped list of (l1[i] l2[i]). Runs forward, recovers l1 given l2 and pairs, recovers l2 given l1 and pairs. 5 new tests, 431/431 cumulative.
- **2026-05-08** — **iterate-no**: relational iterated application. Applies a 2-arg relation n times (Peano n) starting from x to produce result. Generalises succ-iteration / list-cons-iteration / etc. 4 new tests, 426/426 cumulative.
- **2026-05-08** — **rev-acco / rev-2o**: accumulator-style reversal — faster than appendo-driven reverseo for forward queries because no quadratic appendos. Trade-off: rev-acco is asymmetric (cannot run cleanly backward in run*). 6 new tests, 422/422 cumulative.
- **2026-05-08** — **even-i / odd-i (intarith)**: ground-only parity goals via project. Composes with membero for filtered enumeration: -> . 5 new tests, 416/416 cumulative.
- **2026-05-08** — **selecto**: classic miniKanren "choose an element + rest". Direct base (l = (x . rest)) plus skip-head recurse. Enumerates all (element, rest) splits in run*; runs forward, backward, mid-pipeline. 6 new tests, 411/411 cumulative.
- **2026-05-08** — **subo (contiguous sublist)**: Two appendos chained — l = front ++ s ++ back. Goal order matters: appendo on the ground l first, so the search is finitary; then constrain front. 7 new tests, 405/405 cumulative.
- **2026-05-08** — **prefixo + suffixo**: classic appendo-derived sublist relations. (prefixo p l) ≡ p ⊕ ? = l; (suffixo s l) ≡ ? ⊕ s = l. Both enumerate all prefixes/suffixes when given a fresh first arg. 9 new tests, 398/398 cumulative.
- **2026-05-08** — **palindromeo**: 2-line definition (reverseo + ==). Succeeds when a list reads the same forwards and backwards. 7 new tests, 389/389 cumulative.
- **2026-05-08** — **not-membero**: relational "x is not a member of l".
Uses `nafc + ==` per element (the same skeleton all-distincto uses).
Useful as a constraint-style filter: `(membero x dom) (not-membero x
excluded)`. 4 new tests, 382/382 cumulative.
- **2026-05-08** — **repeato + concato**: repeato builds a list of n copies
(Peano n); concato is fold-appendo over a list of lists. Both run forward
and backward — repeato can recover the count from a uniform list. 10 new
tests, 378/378 cumulative.
- **2026-05-08** — **tako + dropo (Peano-indexed prefix/suffix)**: takes / drops
the first n elements via a Peano-encoded count. Round-trip
`(tako n l) ⊕ (dropo n l) = l` holds. 9 new tests, 368/368 cumulative.
- **2026-05-08** — **eveno / oddo Peano predicates**: classic miniKanren parity
relations. eveno: 0 or successor-of-successor of even; oddo: 1 or
successor-of-successor of odd. Both run forward (test) and backward
(enumerate). 12 new tests, 359/359 cumulative.
- **2026-05-08** — **defrel — Prolog-style relation definition macro**:
`(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...)` expands to
`(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...)))`.
Mirrors Prolog's clause syntax and inherits Zzz-via-conde so recursive
relations terminate. 3 new tests, 347/347 cumulative.
- **2026-05-08** — **lasto / init-o**: classic head/tail-style list relations.
lasto extracts the final element; init-o extracts everything-but-the-last.
Together with appendo, the round-trip `init ⊕ (last) = l` holds. 8 new
tests, 344/344 cumulative.
- **2026-05-08** — **Datalog-style relational database queries**: tests/rdb.sx
shows miniKanren as a query engine over fact tables. Defines two tables
(employees + project assignments), wraps each with a relation that does
membero over the table, then expresses queries: dept filter, salary >
threshold (intarith), join engineers ↔ runtime project, find anyone on
multiple distinct projects (nafc + ==). 5 new tests, 336/336 cumulative.
- **2026-05-08** — **Cyclic graph behaviour test (motivates Phase 7 tabling)**:
Demonstrates that naive patho on a 2-cycle generates ever-longer paths.
`run 5` truncates to a finite prefix; `run*` would diverge. This is
exactly the test case Phase 7 (tabled / SLG resolution) is designed
to fix. 3 new tests, 331/331 cumulative.
- **2026-05-08** — **numbero / stringo / symbolo (type predicates)**: ground-only
type tests via project. Compose with `membero` for type-filtered enumeration:
`(fresh (x) (membero x (1 "a" 2 "b" 3)) (numbero x) (== q x))``(1 2 3)`.
Note: SX keywords are strings, so `(stringo :k)` succeeds. 12 new tests,
328/328 cumulative.
- **2026-05-08** — **Graph reachability via patho**: classic miniKanren
graph search. `edgeo` looks up edges in a fact list via `membero`; `patho`
recursively builds paths via direct-edge OR (one edge + recurse + cons).
Enumerates all paths between two nodes, including alternates through
shortcuts. 6 new tests, 316/316 cumulative.
- **2026-05-08** — **everyo / someo (predicate-style relations)**:
`(everyo rel l)` — every element of l satisfies rel; `(someo rel l)`
some element does. Both compose with intarith for numeric tests:
`(everyo (fn (x) (lto-i x 10)) (list 1 5 9))` succeeds. 10 new tests,
310/310 cumulative.
- **2026-05-08** — **mapo (relational map) — 300 test milestone**: `(mapo
rel l1 l2)` succeeds when l2 is l1 with each element rel-related. Works
forward and backward; composes with intarith — `(mapo (fn (a b) (*o-i
a a b)) (1 2 3 4) q)` → `((1 4 9 16))`. 7 new tests, **300/300** cumulative.
- **2026-05-08** — **samelengtho**: classic miniKanren relation that
succeeds when two lists have equal length. Symmetric — works to enumerate
both lists fresh: `(run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q
(list l1 l2))))` produces empty/empty, then 1-elem pairs, then 2-elem.
5 new tests, 293/293 cumulative.
- **2026-05-08** — **Pythagorean triples (intarith showcase)**: search for
(a, b, c) ∈ [1..10]³, a ≤ b, a² + b² = c² via `ino + lteo-i + *o-i +
pluso-i + ==`. Finds exactly `(3 4 5)` and `(6 8 10)`. Demonstrates the
enumerate-then-filter pattern with intarith escape into host arithmetic.
1 new test, 288/288 cumulative.
- **2026-05-08** — **intarith.sx — fast ground-only integer arithmetic**:
pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic
via `project`. They are not relational like Peano `pluso` (require args
to walk to numbers), but run at native host speed — a viable escape
hatch when puzzle size makes Peano impractical. Composes with relational
goals: `(membero x dom) (lto-i x 3)` filters dom by `< 3`. 18 new tests,
287/287 cumulative.
- **2026-05-08** — **2x2 Latin square**: small classic constraint demo using
`ino` + 4 `all-distincto` constraints. Enumerates exactly 2 squares
(`((1 2)(2 1))` and `((2 1)(1 2))`); a clue (top-left = 1) narrows to one.
3 new tests, 269/269 cumulative. Note: 3x3 (12 squares) is the natural
showcase but too slow under naive enumerate-then-filter — needs Phase 6
arc-consistency.
- **2026-05-08** — **rembero / assoco / nth-o**: more standard list relations.
rembero removes the first occurrence (uses `nafc (== a x)` to gate the
skip clause, so it's well-defined on ground lists). assoco is alist
lookup — works forward (key → value) and backward (value → key). nth-o
uses Peano indices into a list. 13 new tests, 266/266 cumulative.
- **2026-05-08** — **flatteno**: nested-list flattener via conde + appendo.
Atom-ness is detected via `nafc (nullo ...) + nafc (pairo ...)` so the
third clause only fires when the input is a ground non-list. Works for
`()` / atoms / flat lists / arbitrarily-nested lists. 7 new tests,
253/253 cumulative. Phase 4 list relations all complete.
- **2026-05-08** — **Laziness tests**: explicitly verifies the
Zzz-on-conde-clauses + mk-mplus-swap-on-paused machinery: an
infinitely-recursive relation truncated via `run 4 q (listo-aux q)`
produces exactly `(() (_.0) (_.0 _.1) (_.0 _.1 _.2))`; mixing two
infinite generators via `mk-disj` keeps both alive (no starvation);
`run*` terminates on a bounded query. 3 new tests, 246/246 cumulative.
- **2026-05-08** — **N-queens (classic miniKanren benchmark green)**:
`lib/minikanren/queens.sx`. Encoding cols(i) = column of queen in row i;
`ino-each` + `all-distincto` cover row/column constraints; `safe-diag`
uses `project` to escape into host arithmetic for the `|c_i - c_j| ≠
|i - j|` diagonal check; `all-cells-safe` walks pairs at construction
time. `(run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols
(list a b c d) 4)))` returns the two valid 4-queens placements
`(2 4 1 3)` and `(3 1 4 2)`. 6 new tests, 243/243 cumulative.
- **2026-05-08** — **Phase 6 piece A — minimal FD (ino + all-distincto)**:
`lib/minikanren/fd.sx`. `ino` is `membero` with the FD-style argument
order; `all-distincto` is `nafc + membero` walking the list. Together
they cover the enumerate-then-filter style of finite-domain solving —
`(fresh (a b c) (ino a D) (ino b D) (ino c D) (all-distincto (list a b c)))`
enumerates all distinct triples from D. Full FD with arc-consistency,
fd-plus etc. is still pending. 9 new tests, 237/237 cumulative.
- **2026-05-08** — **Classic puzzles + matche keyword fix**: matche now emits
keywords bare in the pattern->expr conversion so they self-evaluate to their
string name and unify with the same-keyword target value (instead of becoming
a quoted-keyword type). New `tests/classics.sx`: pet permutation puzzle,
parent/grandparent inference over a fact list, symbolic differentiation
driven by matche dispatch on `:x` / `(:+ a b)` / `(:* a b)` patterns.
6 new tests, 228/228 cumulative.
- **2026-05-08** — **Phase 5 piece D — matche, Phase 5 done**: pattern matching
macro (`lib/minikanren/matche.sx`) — symbols become fresh vars, atoms become
literals, lists recurse positionally, repeated names unify. 14 new tests
(literals, vars, wildcards, list patterns, multi-clause dispatch, nested
patterns, repeated-var-implies-eq). Built via `cons`/`list` rather than
quasiquote because SX's quasiquote does not recurse into lambda bodies — a
worth-knowing gotcha. 222/222 cumulative.
- **2026-05-08** — **Phase 4 piece C — permuteo + inserto**: standard recursive
insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3
as a set check. 208/208 cumulative.
- **2026-05-07** — **Phase 5 piece C — nafc**: `lib/minikanren/nafc.sx`. Three-line
primitive: stream-take 1; if empty, `(unit s)`, else `mzero`. 7 tests including
double-negation and use as a guard. 201/201 cumulative.
- **2026-05-07** — **Phase 5 piece B — project**: `lib/minikanren/project.sx` —
defmacro that walks each named var, rebinds them, and runs the body's mk-conj.
Demonstrated escape into host arithmetic / string ops (`(* n n)`, `(str s "!")`).
Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
- **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)
(== q (list a b))))` → all 4 pairs summing to 3. *o uses repeated pluso —
works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
- **2026-05-07** — **Phase 5 piece A — conda**: soft-cut. Mirrors `condu` minus
the `onceo` on the head: all head answers are conjuncted through the rest of
the chosen clause. 7 new tests including the conda-vs-condu divergence test.
169/169 cumulative.
- **2026-05-07** — **Phase 4 piece B — reverseo + lengtho**: reverseo runs forward
cleanly and `run 1`-cleanly backward; lengtho uses Peano-encoded lengths so it
works as a true relation in both directions (tests use the encoding directly).
10 new tests, 162/162 cumulative.
- **2026-05-07** — **Phase 4 piece A — appendo canary green**: cons-cell support
in `unify.sx` + `(:s head tail)` lazy stream refactor in `stream.sx` + hygienic
`Zzz` (gensym'd subst-name) wrapping each `conde` clause + `lib/minikanren/
relations.sx` with `nullo` / `pairo` / `caro` / `cdro` / `conso` / `firsto` /
`resto` / `listo` / `appendo` / `membero`. 25 new tests in `tests/relations.sx`,
152/152 cumulative.
- **Three deep fixes shipped together**, all required to make `appendo`
terminate in both directions:
1. SX has no improper pairs, so a stream cell of mature subst + thunk
tail can't use `cons` — moved to a `(:s head tail)` tagged shape.
2. `(Zzz g)` wrapped its inner fn in a parameter named `s`, capturing
the user goal's own `s` binding (the `(appendo l s ls)` convention).
Replaced with `(gensym "zzz-s-")` for hygiene.
3. SX cons cells `(:cons h t)` for relational decomposition (so
`(conso a d l)` can split a list by head/tail without proper
improper pairs); `mk-walk*` re-flattens cons cells back to native
lists for clean reification output.
- **2026-05-07** — **Phase 3 done** (run + reification): `lib/minikanren/run.sx` (~28 lines).
`reify`/`reify-s`/`reify-name` for canonical `_.N` rendering of unbound vars in
left-to-right occurrence order; `run*` / `run` / `run-n` defmacros. 18 new tests
in `tests/run.sx`, including the **first classic miniKanren tests green**:
`(run* q (== q 1))` → `(1)`; `(run* q (fresh (x y) (== q (list x y))))` →
`((_.0 _.1))`. 128/128 cumulative.
- **2026-05-07** — **Phase 2 piece D + done** (`condu` / `onceo`): `lib/minikanren/condu.sx`.
Both are commitment forms: `onceo` is `(stream-take 1 ...)`; `condu` walks clauses
and commits the first one whose head produces an answer. 10 tests in `tests/condu.sx`,
110/110 cumulative. Phase 2 complete — ready for Phase 3 (run + reification).
- **2026-05-07** — **Phase 2 piece C** (`conde`): `lib/minikanren/conde.sx` — single
defmacro folding clauses through `mk-disj` with internal `mk-conj`. 9 tests in
`tests/conde.sx`, 100/100 cumulative. Confirmed eager DFS ordering for ==-only
streams; true interleaving is a Phase 4 concern (paused thunks under recursion).
- **2026-05-07** — **Phase 2 piece B** (`fresh`): `lib/minikanren/fresh.sx` (~10 lines).
defmacro form for nice user-facing syntax + `call-fresh` for programmatic use.
9 new tests in `tests/fresh.sx`, 91/91 cumulative.
- **2026-05-07** — **Phase 2 piece A** (streams + ==/conj/disj): `lib/minikanren/stream.sx`
(mzero/unit/mk-mplus/mk-bind/stream-take, ~25 lines of code) + `lib/minikanren/goals.sx`
(succeed/fail/==/==-check/conj2/disj2/mk-conj/mk-disj, ~30 lines). Found and noted
a host-primitive name clash: `bind` is built in and silently shadows user defines —
must use `mk-bind`/`mk-mplus` etc. throughout. 34 tests in `tests/goals.sx`,
82/82 cumulative all green. fresh/conde/condu/onceo still pending.
- **2026-05-07** — **Phase 1 done**: `lib/minikanren/unify.sx` (53 lines, ~22 lines of actual code) +
`lib/minikanren/tests/unify.sx` (48 tests, all green). Kit consumption: `walk-with`,
`unify-with`, `occurs-with`, `extend`, `empty-subst`, `mk-var`, `is-var?`, `var-name`
all supplied by `lib/guest/match.sx`. Local additions: a miniKanren-flavoured cfg
(treats native SX lists as cons-pairs via `:ctor-head = :pair`, occurs-check off),
`make-var` fresh-counter, deep `mk-walk*` (kit's `walk*` only recurses into `:ctor`
form, not native lists), and `mk-unify` / `mk-unify-check` thin wrappers. The kit
earns its keep ~3× over by line count — confirms lib-guest match kit is reusable
for logic-language hosts as designed.