From 57a84b372d2dca46402048fb8613379abf87d2ec Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 23:01:54 +0000 Subject: [PATCH] Merge loops/minikanren into architecture: full miniKanren-on-SX library MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Squash merge of 76 commits from loops/minikanren. Adds lib/minikanren/ — a complete miniKanren-on-SX implementation built on top of lib/guest/match.sx, validating the lib-guest unify-and-match kit as intended. Modules (20 .sx files, ~1700 LOC): unify, stream, goals, fresh, conde, condu, conda, run, relations, peano, intarith, project, nafc, matche, fd, queens, defrel, clpfd, tabling Phases 1–5 fully done (core miniKanren API, all classic relations, matche, conda, project, nafc). Phase 6 — native CLP(FD): domain primitives, fd-in / fd-eq / fd-neq / fd-lt / fd-lte / fd-plus / fd-times / fd-distinct / fd-label, with constraint reactivation iterating to fixed point. N-queens via FD: 4-queens 2 solutions, 5-queens 10 solutions (vs naive timeout past N=4). Phase 7 — naive ground-arg tabling: table-1 / table-2 / table-3. Fibonacci canary: tab-fib(25) = 75025 in seconds, naive fib(25) times out at 60s. Ackermann via table-3: A(3,3) = 61. 71 test files, 644+ tests passing across the suite. Producer/consumer SLG (cyclic patho, mutual recursion) deferred — research-grade work. The lib-guest validation experiment is conclusive: lib/minikanren/ unify.sx adds ~50 lines of local logic (custom cfg, deep walk*, fresh counter) over lib/guest/match.sx's ~100-line kit. The kit earns its keep ~3× by line count. --- lib/minikanren/clpfd.sx | 590 ++++++++++++++++++ lib/minikanren/conda.sx | 42 ++ lib/minikanren/conde.sx | 39 ++ lib/minikanren/condu.sx | 58 ++ lib/minikanren/defrel.sx | 25 + lib/minikanren/fd.sx | 25 + lib/minikanren/fresh.sx | 23 + lib/minikanren/goals.sx | 58 ++ lib/minikanren/intarith.sx | 151 +++++ lib/minikanren/matche.sx | 76 +++ lib/minikanren/nafc.sx | 24 + lib/minikanren/peano.sx | 51 ++ lib/minikanren/project.sx | 25 + lib/minikanren/queens.sx | 67 ++ lib/minikanren/relations.sx | 361 +++++++++++ lib/minikanren/run.sx | 56 ++ lib/minikanren/stream.sx | 66 ++ lib/minikanren/tabling.sx | 157 +++++ lib/minikanren/tests/appendo3.sx | 49 ++ lib/minikanren/tests/arith-prog.sx | 33 + lib/minikanren/tests/btree-walko.sx | 54 ++ lib/minikanren/tests/classics.sx | 87 +++ lib/minikanren/tests/clpfd-distinct.sx | 52 ++ lib/minikanren/tests/clpfd-domains.sx | 133 ++++ lib/minikanren/tests/clpfd-in-label.sx | 120 ++++ lib/minikanren/tests/clpfd-neq.sx | 82 +++ lib/minikanren/tests/clpfd-ord.sx | 128 ++++ lib/minikanren/tests/clpfd-plus.sx | 62 ++ lib/minikanren/tests/clpfd-times.sx | 85 +++ lib/minikanren/tests/conda.sx | 75 +++ lib/minikanren/tests/conde.sx | 89 +++ lib/minikanren/tests/condu.sx | 86 +++ lib/minikanren/tests/counto.sx | 35 ++ lib/minikanren/tests/cyclic-graph.sx | 48 ++ lib/minikanren/tests/defrel.sx | 40 ++ lib/minikanren/tests/enumerate.sx | 31 + lib/minikanren/tests/fd.sx | 75 +++ lib/minikanren/tests/flat-mapo.sx | 39 ++ lib/minikanren/tests/flatteno.sx | 42 ++ lib/minikanren/tests/foldl-o.sx | 48 ++ lib/minikanren/tests/foldr-o.sx | 38 ++ lib/minikanren/tests/fresh.sx | 101 +++ lib/minikanren/tests/goals.sx | 260 ++++++++ lib/minikanren/tests/graph.sx | 70 +++ lib/minikanren/tests/intarith.sx | 103 +++ lib/minikanren/tests/iterate-no.sx | 38 ++ lib/minikanren/tests/lasto.sx | 38 ++ lib/minikanren/tests/latin.sx | 61 ++ lib/minikanren/tests/laziness.sx | 77 +++ lib/minikanren/tests/lengtho-i.sx | 28 + lib/minikanren/tests/list-relations.sx | 126 ++++ lib/minikanren/tests/mapo.sx | 62 ++ lib/minikanren/tests/matche.sx | 138 ++++ lib/minikanren/tests/minmax.sx | 49 ++ lib/minikanren/tests/nafc.sx | 50 ++ lib/minikanren/tests/not-membero.sx | 29 + lib/minikanren/tests/nub-o.sx | 31 + lib/minikanren/tests/pairlisto.sx | 41 ++ lib/minikanren/tests/palindromeo.sx | 44 ++ lib/minikanren/tests/parity.sx | 58 ++ lib/minikanren/tests/partitiono.sx | 75 +++ lib/minikanren/tests/path-cycle-free.sx | 40 ++ lib/minikanren/tests/peano.sx | 119 ++++ lib/minikanren/tests/predicates.sx | 87 +++ lib/minikanren/tests/prefix-suffix.sx | 76 +++ lib/minikanren/tests/project.sx | 60 ++ lib/minikanren/tests/pythag.sx | 36 ++ lib/minikanren/tests/queens-fd.sx | 97 +++ lib/minikanren/tests/queens.sx | 45 ++ lib/minikanren/tests/rdb.sx | 90 +++ lib/minikanren/tests/relations.sx | 291 +++++++++ lib/minikanren/tests/removeo-allo.sx | 39 ++ lib/minikanren/tests/repeato-concato.sx | 69 ++ lib/minikanren/tests/rev-acco.sx | 46 ++ lib/minikanren/tests/run.sx | 114 ++++ lib/minikanren/tests/selecto.sx | 46 ++ lib/minikanren/tests/simplifyo.sx | 47 ++ lib/minikanren/tests/sortedo.sx | 40 ++ lib/minikanren/tests/subo.sx | 60 ++ lib/minikanren/tests/subseto.sx | 62 ++ lib/minikanren/tests/sum-product.sx | 44 ++ lib/minikanren/tests/swap-firsto.sx | 32 + lib/minikanren/tests/tabling-more.sx | 55 ++ lib/minikanren/tests/tabling.sx | 60 ++ lib/minikanren/tests/take-drop.sx | 92 +++ lib/minikanren/tests/take-while-drop-while.sx | 80 +++ lib/minikanren/tests/types.sx | 52 ++ lib/minikanren/tests/unify.sx | 293 +++++++++ lib/minikanren/tests/zip-with-o.sx | 52 ++ lib/minikanren/unify.sx | 82 +++ plans/minikanren-on-sx.md | 414 ++++++++++-- 91 files changed, 7571 insertions(+), 53 deletions(-) create mode 100644 lib/minikanren/clpfd.sx create mode 100644 lib/minikanren/conda.sx create mode 100644 lib/minikanren/conde.sx create mode 100644 lib/minikanren/condu.sx create mode 100644 lib/minikanren/defrel.sx create mode 100644 lib/minikanren/fd.sx create mode 100644 lib/minikanren/fresh.sx create mode 100644 lib/minikanren/goals.sx create mode 100644 lib/minikanren/intarith.sx create mode 100644 lib/minikanren/matche.sx create mode 100644 lib/minikanren/nafc.sx create mode 100644 lib/minikanren/peano.sx create mode 100644 lib/minikanren/project.sx create mode 100644 lib/minikanren/queens.sx create mode 100644 lib/minikanren/relations.sx create mode 100644 lib/minikanren/run.sx create mode 100644 lib/minikanren/stream.sx create mode 100644 lib/minikanren/tabling.sx create mode 100644 lib/minikanren/tests/appendo3.sx create mode 100644 lib/minikanren/tests/arith-prog.sx create mode 100644 lib/minikanren/tests/btree-walko.sx create mode 100644 lib/minikanren/tests/classics.sx create mode 100644 lib/minikanren/tests/clpfd-distinct.sx create mode 100644 lib/minikanren/tests/clpfd-domains.sx create mode 100644 lib/minikanren/tests/clpfd-in-label.sx create mode 100644 lib/minikanren/tests/clpfd-neq.sx create mode 100644 lib/minikanren/tests/clpfd-ord.sx create mode 100644 lib/minikanren/tests/clpfd-plus.sx create mode 100644 lib/minikanren/tests/clpfd-times.sx create mode 100644 lib/minikanren/tests/conda.sx create mode 100644 lib/minikanren/tests/conde.sx create mode 100644 lib/minikanren/tests/condu.sx create mode 100644 lib/minikanren/tests/counto.sx create mode 100644 lib/minikanren/tests/cyclic-graph.sx create mode 100644 lib/minikanren/tests/defrel.sx create mode 100644 lib/minikanren/tests/enumerate.sx create mode 100644 lib/minikanren/tests/fd.sx create mode 100644 lib/minikanren/tests/flat-mapo.sx create mode 100644 lib/minikanren/tests/flatteno.sx create mode 100644 lib/minikanren/tests/foldl-o.sx create mode 100644 lib/minikanren/tests/foldr-o.sx create mode 100644 lib/minikanren/tests/fresh.sx create mode 100644 lib/minikanren/tests/goals.sx create mode 100644 lib/minikanren/tests/graph.sx create mode 100644 lib/minikanren/tests/intarith.sx create mode 100644 lib/minikanren/tests/iterate-no.sx create mode 100644 lib/minikanren/tests/lasto.sx create mode 100644 lib/minikanren/tests/latin.sx create mode 100644 lib/minikanren/tests/laziness.sx create mode 100644 lib/minikanren/tests/lengtho-i.sx create mode 100644 lib/minikanren/tests/list-relations.sx create mode 100644 lib/minikanren/tests/mapo.sx create mode 100644 lib/minikanren/tests/matche.sx create mode 100644 lib/minikanren/tests/minmax.sx create mode 100644 lib/minikanren/tests/nafc.sx create mode 100644 lib/minikanren/tests/not-membero.sx create mode 100644 lib/minikanren/tests/nub-o.sx create mode 100644 lib/minikanren/tests/pairlisto.sx create mode 100644 lib/minikanren/tests/palindromeo.sx create mode 100644 lib/minikanren/tests/parity.sx create mode 100644 lib/minikanren/tests/partitiono.sx create mode 100644 lib/minikanren/tests/path-cycle-free.sx create mode 100644 lib/minikanren/tests/peano.sx create mode 100644 lib/minikanren/tests/predicates.sx create mode 100644 lib/minikanren/tests/prefix-suffix.sx create mode 100644 lib/minikanren/tests/project.sx create mode 100644 lib/minikanren/tests/pythag.sx create mode 100644 lib/minikanren/tests/queens-fd.sx create mode 100644 lib/minikanren/tests/queens.sx create mode 100644 lib/minikanren/tests/rdb.sx create mode 100644 lib/minikanren/tests/relations.sx create mode 100644 lib/minikanren/tests/removeo-allo.sx create mode 100644 lib/minikanren/tests/repeato-concato.sx create mode 100644 lib/minikanren/tests/rev-acco.sx create mode 100644 lib/minikanren/tests/run.sx create mode 100644 lib/minikanren/tests/selecto.sx create mode 100644 lib/minikanren/tests/simplifyo.sx create mode 100644 lib/minikanren/tests/sortedo.sx create mode 100644 lib/minikanren/tests/subo.sx create mode 100644 lib/minikanren/tests/subseto.sx create mode 100644 lib/minikanren/tests/sum-product.sx create mode 100644 lib/minikanren/tests/swap-firsto.sx create mode 100644 lib/minikanren/tests/tabling-more.sx create mode 100644 lib/minikanren/tests/tabling.sx create mode 100644 lib/minikanren/tests/take-drop.sx create mode 100644 lib/minikanren/tests/take-while-drop-while.sx create mode 100644 lib/minikanren/tests/types.sx create mode 100644 lib/minikanren/tests/unify.sx create mode 100644 lib/minikanren/tests/zip-with-o.sx create mode 100644 lib/minikanren/unify.sx diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx new file mode 100644 index 00000000..ab2fb10b --- /dev/null +++ b/lib/minikanren/clpfd.sx @@ -0,0 +1,590 @@ +;; lib/minikanren/clpfd.sx — Phase 6: native CLP(FD) on miniKanren. +;; +;; The substitution dict carries an extra reserved key "_fd" that holds a +;; constraint-store record: +;; +;; {:domains {var-name -> sorted-int-list} +;; :constraints (... pending constraint closures ...)} +;; +;; Domains are sorted SX lists of ints (no duplicates). +;; Constraints are functions s -> s-or-nil that propagate / re-check. +;; They are re-fired after every label binding via fd-fire-store. + +(define fd-key "_fd") + +;; --- domain primitives --- + +(define + fd-dom-rev + (fn + (xs acc) + (cond + ((empty? xs) acc) + (:else (fd-dom-rev (rest xs) (cons (first xs) acc)))))) + +(define + fd-dom-insert + (fn + (x desc) + (cond + ((empty? desc) (list x)) + ((= x (first desc)) desc) + ((> x (first desc)) (cons x desc)) + (:else (cons (first desc) (fd-dom-insert x (rest desc))))))) + +(define + fd-dom-sort-dedupe + (fn + (xs acc) + (cond + ((empty? xs) (fd-dom-rev acc (list))) + (:else (fd-dom-sort-dedupe (rest xs) (fd-dom-insert (first xs) acc)))))) + +(define fd-dom-from-list (fn (xs) (fd-dom-sort-dedupe xs (list)))) + +(define fd-dom-empty? (fn (d) (empty? d))) +(define + fd-dom-singleton? + (fn (d) (and (not (empty? d)) (empty? (rest d))))) +(define fd-dom-min (fn (d) (first d))) + +(define + fd-dom-last + (fn + (d) + (cond ((empty? (rest d)) (first d)) (:else (fd-dom-last (rest d)))))) + +(define fd-dom-max (fn (d) (fd-dom-last d))) +(define fd-dom-member? (fn (x d) (some (fn (y) (= x y)) d))) + +(define + fd-dom-intersect + (fn + (a b) + (cond + ((empty? a) (list)) + ((empty? b) (list)) + ((= (first a) (first b)) + (cons (first a) (fd-dom-intersect (rest a) (rest b)))) + ((< (first a) (first b)) (fd-dom-intersect (rest a) b)) + (:else (fd-dom-intersect a (rest b)))))) + +(define + fd-dom-without + (fn + (x d) + (cond + ((empty? d) (list)) + ((= (first d) x) (rest d)) + ((> (first d) x) d) + (:else (cons (first d) (fd-dom-without x (rest d))))))) + +(define + fd-dom-range + (fn + (lo hi) + (cond + ((> lo hi) (list)) + (:else (cons lo (fd-dom-range (+ lo 1) hi)))))) + +;; --- constraint store accessors --- + +(define fd-store-empty (fn () {:domains {} :constraints (list)})) + +(define + fd-store-of + (fn + (s) + (cond ((has-key? s fd-key) (get s fd-key)) (:else (fd-store-empty))))) + +(define fd-domains-of (fn (s) (get (fd-store-of s) :domains))) +(define fd-with-store (fn (s store) (assoc s fd-key store))) + +(define + fd-domain-of + (fn + (s var-name) + (let + ((doms (fd-domains-of s))) + (cond ((has-key? doms var-name) (get doms var-name)) (:else nil))))) + +(define + fd-set-domain + (fn + (s var-name d) + (cond + ((fd-dom-empty? d) nil) + (:else + (let + ((store (fd-store-of s))) + (let + ((doms-prime (assoc (get store :domains) var-name d))) + (let + ((store-prime (assoc store :domains doms-prime))) + (fd-with-store s store-prime)))))))) + +(define + fd-add-constraint + (fn + (s c) + (let + ((store (fd-store-of s))) + (let + ((cs-prime (cons c (get store :constraints)))) + (let + ((store-prime (assoc store :constraints cs-prime))) + (fd-with-store s store-prime)))))) + +(define + fd-fire-list + (fn + (cs s) + (cond + ((empty? cs) s) + (:else + (let + ((s2 ((first cs) s))) + (cond ((= s2 nil) nil) (:else (fd-fire-list (rest cs) s2)))))))) + +(define + fd-store-signature + (fn + (s) + (let + ((doms (fd-domains-of s))) + (let + ((dom-sizes (reduce (fn (acc k) (+ acc (len (get doms k)))) 0 (keys doms)))) + (+ dom-sizes (len (keys s))))))) + +(define + fd-fire-store + (fn + (s) + (let + ((s2 (fd-fire-list (get (fd-store-of s) :constraints) s))) + (cond + ((= s2 nil) nil) + ((= (fd-store-signature s) (fd-store-signature s2)) s2) + (:else (fd-fire-store s2)))))) + +;; --- user-facing goals --- + +(define + fd-in + (fn + (x dom-list) + (fn + (s) + (let + ((new-dom (fd-dom-from-list dom-list))) + (let + ((wx (mk-walk x s))) + (cond + ((number? wx) + (cond ((fd-dom-member? wx new-dom) (unit s)) (:else mzero))) + ((is-var? wx) + (let + ((existing (fd-domain-of s (var-name wx)))) + (let + ((narrowed (cond ((= existing nil) new-dom) (:else (fd-dom-intersect existing new-dom))))) + (let + ((s2 (fd-set-domain s (var-name wx) narrowed))) + (cond ((= s2 nil) mzero) (:else (unit s2))))))) + (:else mzero))))))) + +;; --- fd-neq --- + +(define + fd-neq-prop + (fn + (x y s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s))) + (cond + ((and (number? wx) (number? wy)) + (cond ((= wx wy) nil) (:else s))) + ((and (number? wx) (is-var? wy)) + (let + ((y-dom (fd-domain-of s (var-name wy)))) + (cond + ((= y-dom nil) s) + (:else + (fd-set-domain s (var-name wy) (fd-dom-without wx y-dom)))))) + ((and (number? wy) (is-var? wx)) + (let + ((x-dom (fd-domain-of s (var-name wx)))) + (cond + ((= x-dom nil) s) + (:else + (fd-set-domain s (var-name wx) (fd-dom-without wy x-dom)))))) + (:else s))))) + +(define + fd-neq + (fn + (x y) + (fn + (s) + (let + ((c (fn (s-prime) (fd-neq-prop x y s-prime)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-lt --- + +(define + fd-lt-prop + (fn + (x y s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s))) + (cond + ((and (number? wx) (number? wy)) + (cond ((< wx wy) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((= yd nil) s) + (:else + (fd-set-domain + s + (var-name wy) + (filter (fn (v) (> v wx)) yd)))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((= xd nil) s) + (:else + (fd-set-domain + s + (var-name wx) + (filter (fn (v) (< v wy)) xd)))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((or (= xd nil) (= yd nil)) s) + (:else + (let + ((xd-prime (filter (fn (v) (< v (fd-dom-max yd))) xd))) + (let + ((s2 (fd-set-domain s (var-name wx) xd-prime))) + (cond + ((= s2 nil) nil) + (:else + (let + ((yd-prime (filter (fn (v) (> v (fd-dom-min xd-prime))) yd))) + (fd-set-domain s2 (var-name wy) yd-prime)))))))))) + (:else s))))) + +(define + fd-lt + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-lt-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-lte --- + +(define + fd-lte-prop + (fn + (x y s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s))) + (cond + ((and (number? wx) (number? wy)) + (cond ((<= wx wy) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((= yd nil) s) + (:else + (fd-set-domain + s + (var-name wy) + (filter (fn (v) (>= v wx)) yd)))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((= xd nil) s) + (:else + (fd-set-domain + s + (var-name wx) + (filter (fn (v) (<= v wy)) xd)))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((or (= xd nil) (= yd nil)) s) + (:else + (let + ((xd-prime (filter (fn (v) (<= v (fd-dom-max yd))) xd))) + (let + ((s2 (fd-set-domain s (var-name wx) xd-prime))) + (cond + ((= s2 nil) nil) + (:else + (let + ((yd-prime (filter (fn (v) (>= v (fd-dom-min xd-prime))) yd))) + (fd-set-domain s2 (var-name wy) yd-prime)))))))))) + (:else s))))) + +(define + fd-lte + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-lte-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-eq --- + +(define + fd-eq-prop + (fn + (x y s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s))) + (cond + ((and (number? wx) (number? wy)) + (cond ((= wx wy) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((and (not (= yd nil)) (not (fd-dom-member? wx yd))) nil) + (:else + (let + ((s2 (mk-unify wy wx s))) + (cond ((= s2 nil) nil) (:else s2))))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((and (not (= xd nil)) (not (fd-dom-member? wy xd))) nil) + (:else + (let + ((s2 (mk-unify wx wy s))) + (cond ((= s2 nil) nil) (:else s2))))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((and (= xd nil) (= yd nil)) + (let + ((s2 (mk-unify wx wy s))) + (cond ((= s2 nil) nil) (:else s2)))) + (:else + (let + ((shared (cond ((= xd nil) yd) ((= yd nil) xd) (:else (fd-dom-intersect xd yd))))) + (cond + ((fd-dom-empty? shared) nil) + (:else + (let + ((s2 (fd-set-domain s (var-name wx) shared))) + (cond + ((= s2 nil) nil) + (:else + (let + ((s3 (fd-set-domain s2 (var-name wy) shared))) + (cond + ((= s3 nil) nil) + (:else (mk-unify wx wy s3)))))))))))))) + (:else s))))) + +(define + fd-eq + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-eq-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- labelling --- + +(define + fd-try-each-value + (fn + (x dom s) + (cond + ((empty? dom) mzero) + (:else + (let + ((s2 (mk-unify x (first dom) s))) + (let + ((s3 (cond ((= s2 nil) nil) (:else (fd-fire-store s2))))) + (let + ((this-stream (cond ((= s3 nil) mzero) (:else (unit s3)))) + (rest-stream (fd-try-each-value x (rest dom) s))) + (mk-mplus this-stream rest-stream)))))))) + +(define + fd-label-one + (fn + (x) + (fn + (s) + (let + ((wx (mk-walk x s))) + (cond + ((number? wx) (unit s)) + ((is-var? wx) + (let + ((dom (fd-domain-of s (var-name wx)))) + (cond + ((= dom nil) mzero) + (:else (fd-try-each-value wx dom s))))) + (:else mzero)))))) + +(define + fd-label + (fn + (vars) + (cond + ((empty? vars) succeed) + (:else (mk-conj (fd-label-one (first vars)) (fd-label (rest vars))))))) + +;; --- fd-distinct (pairwise distinct via fd-neq) --- + +(define + fd-distinct-from-head + (fn + (x others) + (cond + ((empty? others) succeed) + (:else + (mk-conj + (fd-neq x (first others)) + (fd-distinct-from-head x (rest others))))))) + +(define + fd-distinct + (fn + (vars) + (cond + ((empty? vars) succeed) + ((empty? (rest vars)) succeed) + (:else + (mk-conj + (fd-distinct-from-head (first vars) (rest vars)) + (fd-distinct (rest vars))))))) + +;; --- fd-plus (x + y = z, ground-cases propagator) --- + +(define + fd-bind-or-narrow + (fn + (w target s) + (cond + ((number? w) (cond ((= w target) s) (:else nil))) + ((is-var? w) + (let + ((wd (fd-domain-of s (var-name w)))) + (cond + ((and (not (= wd nil)) (not (fd-dom-member? target wd))) nil) + (:else + (let + ((s2 (mk-unify w target s))) + (cond ((= s2 nil) nil) (:else s2))))))) + (:else nil)))) + +(define + fd-plus-prop + (fn + (x y z s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s)) (wz (mk-walk z s))) + (cond + ((and (number? wx) (number? wy) (number? wz)) + (cond ((= (+ wx wy) wz) s) (:else nil))) + ((and (number? wx) (number? wy)) + (fd-bind-or-narrow wz (+ wx wy) s)) + ((and (number? wx) (number? wz)) + (fd-bind-or-narrow wy (- wz wx) s)) + ((and (number? wy) (number? wz)) + (fd-bind-or-narrow wx (- wz wy) s)) + (:else s))))) + +(define + fd-plus + (fn + (x y z) + (fn + (s) + (let + ((c (fn (sp) (fd-plus-prop x y z sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-times (x * y = z, ground-cases propagator) --- + +(define + fd-times-prop + (fn + (x y z s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s)) (wz (mk-walk z s))) + (cond + ((and (number? wx) (number? wy) (number? wz)) + (cond ((= (* wx wy) wz) s) (:else nil))) + ((and (number? wx) (number? wy)) + (fd-bind-or-narrow wz (* wx wy) s)) + ((and (number? wx) (number? wz)) + (cond + ((= wx 0) (cond ((= wz 0) s) (:else nil))) + ((not (= (mod wz wx) 0)) nil) + (:else (fd-bind-or-narrow wy (/ wz wx) s)))) + ((and (number? wy) (number? wz)) + (cond + ((= wy 0) (cond ((= wz 0) s) (:else nil))) + ((not (= (mod wz wy) 0)) nil) + (:else (fd-bind-or-narrow wx (/ wz wy) s)))) + (:else s))))) + +(define + fd-times + (fn + (x y z) + (fn + (s) + (let + ((c (fn (sp) (fd-times-prop x y z sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) diff --git a/lib/minikanren/conda.sx b/lib/minikanren/conda.sx new file mode 100644 index 00000000..6806c10a --- /dev/null +++ b/lib/minikanren/conda.sx @@ -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)))) diff --git a/lib/minikanren/conde.sx b/lib/minikanren/conde.sx new file mode 100644 index 00000000..b09eb0b4 --- /dev/null +++ b/lib/minikanren/conde.sx @@ -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))))) diff --git a/lib/minikanren/condu.sx b/lib/minikanren/condu.sx new file mode 100644 index 00000000..3c24b1d9 --- /dev/null +++ b/lib/minikanren/condu.sx @@ -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)))) diff --git a/lib/minikanren/defrel.sx b/lib/minikanren/defrel.sx new file mode 100644 index 00000000..03604542 --- /dev/null +++ b/lib/minikanren/defrel.sx @@ -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))))) diff --git a/lib/minikanren/fd.sx b/lib/minikanren/fd.sx new file mode 100644 index 00000000..fb0c06ab --- /dev/null +++ b/lib/minikanren/fd.sx @@ -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)))))) diff --git a/lib/minikanren/fresh.sx b/lib/minikanren/fresh.sx new file mode 100644 index 00000000..e10abb5c --- /dev/null +++ b/lib/minikanren/fresh.sx @@ -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)))) diff --git a/lib/minikanren/goals.sx b/lib/minikanren/goals.sx new file mode 100644 index 00000000..6f6cc227 --- /dev/null +++ b/lib/minikanren/goals.sx @@ -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))) diff --git a/lib/minikanren/intarith.sx b/lib/minikanren/intarith.sx new file mode 100644 index 00000000..6aaf57bb --- /dev/null +++ b/lib/minikanren/intarith.sx @@ -0,0 +1,151 @@ +;; 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))) + +(define + counto + (fn + (x l n) + (conde + ((nullo l) (== n 0)) + ((fresh (a d n-rest) (conso a d l) (conde ((== a x) (counto x d n-rest) (pluso-i 1 n-rest n)) ((nafc (== a x)) (counto x d n)))))))) + +(define + mk-arith-prog + (fn + (start step len) + (cond + ((= len 0) (list)) + (:else (cons start (mk-arith-prog (+ start step) step (- len 1))))))) + +(define + arith-progo + (fn + (start step len result) + (project (start step len) (== result (mk-arith-prog start step len))))) diff --git a/lib/minikanren/matche.sx b/lib/minikanren/matche.sx new file mode 100644 index 00000000..5b9ecab6 --- /dev/null +++ b/lib/minikanren/matche.sx @@ -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))) diff --git a/lib/minikanren/nafc.sx b/lib/minikanren/nafc.sx new file mode 100644 index 00000000..181c84ac --- /dev/null +++ b/lib/minikanren/nafc.sx @@ -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))))) diff --git a/lib/minikanren/peano.sx b/lib/minikanren/peano.sx new file mode 100644 index 00000000..cdbec76e --- /dev/null +++ b/lib/minikanren/peano.sx @@ -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)))))) diff --git a/lib/minikanren/project.sx b/lib/minikanren/project.sx new file mode 100644 index 00000000..476b18f7 --- /dev/null +++ b/lib/minikanren/project.sx @@ -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)))))) diff --git a/lib/minikanren/queens.sx b/lib/minikanren/queens.sx new file mode 100644 index 00000000..27daa3fc --- /dev/null +++ b/lib/minikanren/queens.sx @@ -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))))) diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx new file mode 100644 index 00000000..35d87cb5 --- /dev/null +++ b/lib/minikanren/relations.sx @@ -0,0 +1,361 @@ +;; 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 + foldr-o + (fn + (rel l acc result) + (conde + ((nullo l) (== result acc)) + ((fresh (a d r-rest) (conso a d l) (foldr-o rel d acc r-rest) (rel a r-rest result)))))) + +(define + foldl-o + (fn + (rel l acc result) + (conde + ((nullo l) (== result acc)) + ((fresh (a d new-acc) (conso a d l) (rel acc a new-acc) (foldl-o rel d new-acc result)))))) + +(define + flat-mapo + (fn + (rel l result) + (conde + ((nullo l) (nullo result)) + ((fresh (a d a-result rest-result) (conso a d l) (rel a a-result) (flat-mapo rel d rest-result) (appendo a-result rest-result result)))))) + +(define + nub-o + (fn + (l result) + (conde + ((nullo l) (nullo result)) + ((fresh (a d r-rest) (conso a d l) (conde ((membero a d) (nub-o d result)) ((nafc (membero a d)) (conso a r-rest result) (nub-o d r-rest)))))))) + + +(define + take-while-o + (fn + (pred l result) + (conde + ((nullo l) (nullo result)) + ((fresh (a d r-rest) (conso a d l) (conde ((pred a) (conso a r-rest result) (take-while-o pred d r-rest)) ((nafc (pred a)) (== result (list))))))))) + +(define + drop-while-o + (fn + (pred l result) + (conde + ((nullo l) (nullo result)) + ((fresh (a d) (conso a d l) (conde ((pred a) (drop-while-o pred d result)) ((nafc (pred a)) (== result l)))))))) + +(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 + zip-with-o + (fn + (rel l1 l2 result) + (conde + ((nullo l1) (nullo l2) (nullo result)) + ((fresh (a1 d1 a2 d2 a-result d-result) (conso a1 d1 l1) (conso a2 d2 l2) (rel a1 a2 a-result) (conso a-result d-result result) (zip-with-o rel d1 d2 d-result)))))) + +(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)))))) diff --git a/lib/minikanren/run.sx b/lib/minikanren/run.sx new file mode 100644 index 00000000..811eebc5 --- /dev/null +++ b/lib/minikanren/run.sx @@ -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)))) diff --git a/lib/minikanren/stream.sx b/lib/minikanren/stream.sx new file mode 100644 index 00000000..04173707 --- /dev/null +++ b/lib/minikanren/stream.sx @@ -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))))))) diff --git a/lib/minikanren/tabling.sx b/lib/minikanren/tabling.sx new file mode 100644 index 00000000..8dad2174 --- /dev/null +++ b/lib/minikanren/tabling.sx @@ -0,0 +1,157 @@ +;; lib/minikanren/tabling.sx — Phase 7 piece A: naive memoization. +;; +;; A `table-2` wrapper for 2-arg relations (input, output). Caches by +;; ground input (walked at call time). On hit, replays the cached output +;; values; on miss, runs the relation, collects all output values from +;; the answer stream, stores, then replays. +;; +;; Limitations of naive memoization (vs proper SLG / producer-consumer +;; tabling): +;; - Each call must terminate before its result enters the cache — +;; so cyclic recursive calls with the SAME ground input would still +;; diverge (not addressed here). +;; - Caching by full ground walk only; partially-ground args fall +;; through to the underlying relation. +;; +;; Despite the limitations, naive memoization is enough for the +;; canonical demo: Fibonacci goes from exponential to linear because +;; each fib(k) result is computed at most once. +;; +;; Cache lifetime: a single global mk-tab-cache. Use `(mk-tab-clear!)` +;; between independent queries. + +(define mk-tab-cache {}) + +(define mk-tab-clear! (fn () (set! mk-tab-cache {}))) + +(define + mk-tab-lookup + (fn + (key) + (cond + ((has-key? mk-tab-cache key) (get mk-tab-cache key)) + (:else :miss)))) + +(define + mk-tab-store! + (fn (key vals) (set! mk-tab-cache (assoc mk-tab-cache key vals)))) + +(define + mk-tab-ground-term? + (fn + (t) + (cond + ((is-var? t) false) + ((mk-cons-cell? t) + (and + (mk-tab-ground-term? (mk-cons-head t)) + (mk-tab-ground-term? (mk-cons-tail t)))) + ((mk-list-pair? t) (every? mk-tab-ground-term? t)) + (:else true)))) + +(define + mk-tab-replay-vals + (fn + (vals output s) + (cond + ((empty? vals) mzero) + (:else + (let + ((sp (mk-unify output (first vals) s))) + (let + ((this-stream (cond ((= sp nil) mzero) (:else (unit sp))))) + (mk-mplus this-stream (mk-tab-replay-vals (rest vals) output s)))))))) + +(define + table-2 + (fn + (name rel-fn) + (fn + (input output) + (fn + (s) + (let + ((winput (mk-walk* input s))) + (cond + ((mk-tab-ground-term? winput) + (let + ((key (str name "@" winput))) + (let + ((cached (mk-tab-lookup key))) + (cond + ((= cached :miss) + (let + ((all-substs (stream-take -1 ((rel-fn input output) s)))) + (let + ((vals (map (fn (s2) (mk-walk* output s2)) all-substs))) + (begin + (mk-tab-store! key vals) + (mk-tab-replay-vals vals output s))))) + (:else (mk-tab-replay-vals cached output s)))))) + (:else ((rel-fn input output) s)))))))) + +;; --- table-1: 1-arg relation (one input, no output to cache) --- +;; The relation is a predicate `(p input)` that succeeds or fails. +;; Cache stores either :ok or :no. + +(define + table-1 + (fn + (name rel-fn) + (fn + (input) + (fn + (s) + (let + ((winput (mk-walk* input s))) + (cond + ((mk-tab-ground-term? winput) + (let + ((key (str name "@1@" winput))) + (let + ((cached (mk-tab-lookup key))) + (cond + ((= cached :miss) + (let + ((stream ((rel-fn input) s))) + (let + ((peek (stream-take 1 stream))) + (cond + ((empty? peek) + (begin (mk-tab-store! key :no) mzero)) + (:else (begin (mk-tab-store! key :ok) stream)))))) + ((= cached :ok) (unit s)) + ((= cached :no) mzero) + (:else mzero))))) + (:else ((rel-fn input) s)))))))) + +;; --- table-3: 3-arg relation (input1 input2 output) --- +;; Cache keyed by (input1, input2). Output values cached as a list. + +(define + table-3 + (fn + (name rel-fn) + (fn + (i1 i2 output) + (fn + (s) + (let + ((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s))) + (cond + ((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2)) + (let + ((key (str name "@3@" wi1 "/" wi2))) + (let + ((cached (mk-tab-lookup key))) + (cond + ((= cached :miss) + (let + ((all-substs (stream-take -1 ((rel-fn i1 i2 output) s)))) + (let + ((vals (map (fn (s2) (mk-walk* output s2)) all-substs))) + (begin + (mk-tab-store! key vals) + (mk-tab-replay-vals vals output s))))) + (:else (mk-tab-replay-vals cached output s)))))) + (:else ((rel-fn i1 i2 output) s)))))))) diff --git a/lib/minikanren/tests/appendo3.sx b/lib/minikanren/tests/appendo3.sx new file mode 100644 index 00000000..36f58269 --- /dev/null +++ b/lib/minikanren/tests/appendo3.sx @@ -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!) diff --git a/lib/minikanren/tests/arith-prog.sx b/lib/minikanren/tests/arith-prog.sx new file mode 100644 index 00000000..2b1b7843 --- /dev/null +++ b/lib/minikanren/tests/arith-prog.sx @@ -0,0 +1,33 @@ +;; lib/minikanren/tests/arith-prog.sx — arithmetic progression generation. + +(mk-test + "arith-progo-zero-len" + (run* q (arith-progo 5 1 0 q)) + (list (list))) + +(mk-test + "arith-progo-1-to-5" + (run* q (arith-progo 1 1 5 q)) + (list (list 1 2 3 4 5))) + +(mk-test + "arith-progo-evens-from-0" + (run* q (arith-progo 0 2 5 q)) + (list (list 0 2 4 6 8))) + +(mk-test + "arith-progo-descending" + (run* q (arith-progo 10 -1 4 q)) + (list (list 10 9 8 7))) + +(mk-test + "arith-progo-zero-step" + (run* q (arith-progo 7 0 3 q)) + (list (list 7 7 7))) + +(mk-test + "arith-progo-negative-start" + (run* q (arith-progo -3 2 4 q)) + (list (list -3 -1 1 3))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/btree-walko.sx b/lib/minikanren/tests/btree-walko.sx new file mode 100644 index 00000000..0dc617b1 --- /dev/null +++ b/lib/minikanren/tests/btree-walko.sx @@ -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!) diff --git a/lib/minikanren/tests/classics.sx b/lib/minikanren/tests/classics.sx new file mode 100644 index 00000000..0a0b5435 --- /dev/null +++ b/lib/minikanren/tests/classics.sx @@ -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!) diff --git a/lib/minikanren/tests/clpfd-distinct.sx b/lib/minikanren/tests/clpfd-distinct.sx new file mode 100644 index 00000000..1c2d7d11 --- /dev/null +++ b/lib/minikanren/tests/clpfd-distinct.sx @@ -0,0 +1,52 @@ +;; lib/minikanren/tests/clpfd-distinct.sx — fd-distinct (alldifferent). + +(mk-test + "fd-distinct-empty" + (run* q (fd-distinct (list))) + (list (make-symbol "_.0"))) + +(mk-test + "fd-distinct-singleton" + (run* q (fd-distinct (list 5))) + (list (make-symbol "_.0"))) + +(mk-test + "fd-distinct-pair-distinct" + (run* q (fd-distinct (list 1 2))) + (list (make-symbol "_.0"))) + +(mk-test + "fd-distinct-pair-equal-fails" + (run* q (fd-distinct (list 5 5))) + (list)) + +(mk-test + "fd-distinct-3-perms-of-3" + (let + ((res (run* q (fresh (a b c) (fd-in a (list 1 2 3)) (fd-in b (list 1 2 3)) (fd-in c (list 1 2 3)) (fd-distinct (list a b c)) (fd-label (list a b c)) (== q (list a b c)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-distinct-4-perms-of-4-count" + (let + ((res (run* q (fresh (a b c d) (fd-in a (list 1 2 3 4)) (fd-in b (list 1 2 3 4)) (fd-in c (list 1 2 3 4)) (fd-in d (list 1 2 3 4)) (fd-distinct (list a b c d)) (fd-label (list a b c d)) (== q (list a b c d)))))) + (= (len res) 24)) + true) + +(mk-test + "fd-distinct-pigeonhole-fails" + (run* + q + (fresh + (a b c d) + (fd-in a (list 1 2 3)) + (fd-in b (list 1 2 3)) + (fd-in c (list 1 2 3)) + (fd-in d (list 1 2 3)) + (fd-distinct (list a b c d)) + (fd-label (list a b c d)) + (== q (list a b c d)))) + (list)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-domains.sx b/lib/minikanren/tests/clpfd-domains.sx new file mode 100644 index 00000000..a43a7270 --- /dev/null +++ b/lib/minikanren/tests/clpfd-domains.sx @@ -0,0 +1,133 @@ +;; lib/minikanren/tests/clpfd-domains.sx — Phase 6 piece B: domain primitives. + +;; --- domain construction --- + +(mk-test + "fd-dom-from-list-sorts" + (fd-dom-from-list + (list 3 1 2 1 5)) + (list 1 2 3 5)) + +(mk-test "fd-dom-from-list-empty" (fd-dom-from-list (list)) (list)) + +(mk-test + "fd-dom-from-list-single" + (fd-dom-from-list (list 7)) + (list 7)) + +(mk-test + "fd-dom-range-1-5" + (fd-dom-range 1 5) + (list 1 2 3 4 5)) + +(mk-test "fd-dom-range-empty" (fd-dom-range 5 1) (list)) + +;; --- predicates --- + +(mk-test "fd-dom-empty-yes" (fd-dom-empty? (list)) true) +(mk-test "fd-dom-empty-no" (fd-dom-empty? (list 1)) false) +(mk-test "fd-dom-singleton-yes" (fd-dom-singleton? (list 5)) true) +(mk-test + "fd-dom-singleton-multi" + (fd-dom-singleton? (list 1 2)) + false) +(mk-test "fd-dom-singleton-empty" (fd-dom-singleton? (list)) false) + +(mk-test + "fd-dom-min" + (fd-dom-min (list 3 7 9)) + 3) +(mk-test + "fd-dom-max" + (fd-dom-max (list 3 7 9)) + 9) + +(mk-test + "fd-dom-member-yes" + (fd-dom-member? + 3 + (list 1 2 3 4)) + true) +(mk-test + "fd-dom-member-no" + (fd-dom-member? + 9 + (list 1 2 3 4)) + false) + +;; --- intersect / without --- + +(mk-test + "fd-dom-intersect" + (fd-dom-intersect + (list 1 2 3 4 5) + (list 2 4 6)) + (list 2 4)) + +(mk-test + "fd-dom-intersect-disjoint" + (fd-dom-intersect + (list 1 2 3) + (list 4 5 6)) + (list)) + +(mk-test + "fd-dom-intersect-empty" + (fd-dom-intersect (list) (list 1 2 3)) + (list)) + +(mk-test + "fd-dom-intersect-equal" + (fd-dom-intersect + (list 1 2 3) + (list 1 2 3)) + (list 1 2 3)) + +(mk-test + "fd-dom-without-mid" + (fd-dom-without + 3 + (list 1 2 3 4 5)) + (list 1 2 4 5)) + +(mk-test + "fd-dom-without-missing" + (fd-dom-without 9 (list 1 2 3)) + (list 1 2 3)) + +(mk-test + "fd-dom-without-min" + (fd-dom-without 1 (list 1 2 3)) + (list 2 3)) + +;; --- store accessors --- + +(mk-test "fd-domain-of-unset" (fd-domain-of {} "x") nil) + +(mk-test + "fd-domain-of-set" + (let + ((s (fd-set-domain {} "x" (list 1 2 3)))) + (fd-domain-of s "x")) + (list 1 2 3)) + +(mk-test + "fd-set-domain-empty-fails" + (fd-set-domain {} "x" (list)) + nil) + +(mk-test + "fd-set-domain-overrides" + (let + ((s (fd-set-domain {} "x" (list 1 2 3)))) + (fd-domain-of (fd-set-domain s "x" (list 5)) "x")) + (list 5)) + +(mk-test + "fd-set-domain-multiple-vars" + (let + ((s (fd-set-domain (fd-set-domain {} "x" (list 1)) "y" (list 2 3)))) + (list (fd-domain-of s "x") (fd-domain-of s "y"))) + (list (list 1) (list 2 3))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-in-label.sx b/lib/minikanren/tests/clpfd-in-label.sx new file mode 100644 index 00000000..7393fdf6 --- /dev/null +++ b/lib/minikanren/tests/clpfd-in-label.sx @@ -0,0 +1,120 @@ +;; lib/minikanren/tests/clpfd-in-label.sx — fd-in (domain narrowing) + fd-label. + +;; --- fd-in: domain narrowing --- + +(mk-test + "fd-in-bare-label" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-label (list x)) + (== q x))) + (list 1 2 3 4 5)) + +(mk-test + "fd-in-intersection" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-in x (list 3 4 5 6 7)) + (fd-label (list x)) + (== q x))) + (list 3 4 5)) + +(mk-test + "fd-in-disjoint-empty" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-in x (list 7 8 9)) + (fd-label (list x)) + (== q x))) + (list)) + +(mk-test + "fd-in-singleton-domain" + (run* + q + (fresh (x) (fd-in x (list 5)) (fd-label (list x)) (== q x))) + (list 5)) + +;; --- ground value checks the domain --- + +(mk-test + "fd-in-ground-in-domain" + (run* + q + (fresh + (x) + (== x 3) + (fd-in x (list 1 2 3 4 5)) + (== q x))) + (list 3)) + +(mk-test + "fd-in-ground-not-in-domain" + (run* + q + (fresh + (x) + (== x 9) + (fd-in x (list 1 2 3 4 5)) + (== q x))) + (list)) + +;; --- fd-label across multiple vars --- + +(mk-test + "fd-label-multiple-vars" + (let + ((res (run* q (fresh (a b) (fd-in a (list 1 2 3)) (fd-in b (list 10 20)) (fd-label (list a b)) (== q (list a b)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-label-empty-vars" + (run* q (fd-label (list))) + (list (make-symbol "_.0"))) + +;; --- composition with regular goals --- + +(mk-test + "fd-in-with-membero-style-filtering" + (run* + q + (fresh + (x) + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-label (list x)) + (== q x))) + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-neq.sx b/lib/minikanren/tests/clpfd-neq.sx new file mode 100644 index 00000000..2a533e3c --- /dev/null +++ b/lib/minikanren/tests/clpfd-neq.sx @@ -0,0 +1,82 @@ +;; lib/minikanren/tests/clpfd-neq.sx — fd-neq with constraint propagation. + +;; --- ground / domain interaction --- + +(mk-test + "fd-neq-ground-distinct" + (run* + q + (fresh + (x) + (fd-neq x 5) + (fd-in x (list 4 5 6)) + (fd-label (list x)) + (== q x))) + (list 4 6)) + +(mk-test + "fd-neq-ground-equal-fails" + (run* q (fresh (x) (== x 5) (fd-neq x 5) (== q x))) + (list)) + +(mk-test + "fd-neq-symmetric" + (run* + q + (fresh + (x) + (fd-neq 7 x) + (fd-in x (list 5 6 7 8 9)) + (fd-label (list x)) + (== q x))) + (list 5 6 8 9)) + +;; --- two vars with overlapping domains --- + +(mk-test + "fd-neq-pair-from-3" + (let + ((res (run* q (fresh (x y) (fd-in x (list 1 2 3)) (fd-in y (list 1 2 3)) (fd-neq x y) (fd-label (list x y)) (== q (list x y)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-all-distinct-3-of-3" + (let + ((res (run* q (fresh (a b c) (fd-in a (list 1 2 3)) (fd-in b (list 1 2 3)) (fd-in c (list 1 2 3)) (fd-neq a b) (fd-neq a c) (fd-neq b c) (fd-label (list a b c)) (== q (list a b c)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-pigeonhole-fails" + (run* + q + (fresh + (a b c) + (fd-in a (list 1 2)) + (fd-in b (list 1 2)) + (fd-in c (list 1 2)) + (fd-neq a b) + (fd-neq a c) + (fd-neq b c) + (fd-label (list a b c)) + (== q (list a b c)))) + (list)) + +;; --- propagation when one side becomes ground --- + +(mk-test + "fd-neq-propagates-after-ground" + (run* + q + (fresh + (x y) + (fd-in x (list 1 2 3)) + (fd-in y (list 1 2 3)) + (fd-neq x y) + (== x 2) + (fd-label (list y)) + (== q y))) + (list 1 3)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-ord.sx b/lib/minikanren/tests/clpfd-ord.sx new file mode 100644 index 00000000..535f127d --- /dev/null +++ b/lib/minikanren/tests/clpfd-ord.sx @@ -0,0 +1,128 @@ +;; lib/minikanren/tests/clpfd-ord.sx — fd-lt / fd-lte / fd-eq. + +;; --- fd-lt --- + +(mk-test + "fd-lt-narrows-x-against-num" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lt x 3) + (fd-label (list x)) + (== q x))) + (list 1 2)) + +(mk-test + "fd-lt-narrows-x-against-num-symmetric" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lt 3 x) + (fd-label (list x)) + (== q x))) + (list 4 5)) + +(mk-test + "fd-lt-pair-ordered" + (let + ((res (run* q (fresh (x y) (fd-in x (list 1 2 3 4)) (fd-in y (list 1 2 3 4)) (fd-lt x y) (fd-label (list x y)) (== q (list x y)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-lt-impossible-fails" + (run* + q + (fresh + (x) + (fd-in x (list 5 6 7)) + (fd-lt x 3) + (fd-label (list x)) + (== q x))) + (list)) + +;; --- fd-lte --- + +(mk-test + "fd-lte-includes-equal" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lte x 3) + (fd-label (list x)) + (== q x))) + (list 1 2 3)) + +(mk-test + "fd-lte-equal-bound" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lte 3 x) + (fd-label (list x)) + (== q x))) + (list 3 4 5)) + +;; --- fd-eq --- + +(mk-test + "fd-eq-bind" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-eq x 3) + (== q x))) + (list 3)) + +(mk-test + "fd-eq-out-of-domain-fails" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-eq x 5) + (== q x))) + (list)) + +(mk-test + "fd-eq-two-vars-share-domain" + (run* + q + (fresh + (x y) + (fd-in x (list 1 2 3)) + (fd-in y (list 2 3 4)) + (fd-eq x y) + (fd-label (list x y)) + (== q (list x y)))) + (list (list 2 2) (list 3 3))) + +;; --- combine fd-lt + fd-neq for "between" puzzle --- + +(mk-test + "fd-lt-neq-combined" + (run* + q + (fresh + (x y z) + (fd-in x (list 1 2 3)) + (fd-in y (list 1 2 3)) + (fd-in z (list 1 2 3)) + (fd-lt x y) + (fd-lt y z) + (fd-label (list x y z)) + (== q (list x y z)))) + (list (list 1 2 3))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-plus.sx b/lib/minikanren/tests/clpfd-plus.sx new file mode 100644 index 00000000..81b01d18 --- /dev/null +++ b/lib/minikanren/tests/clpfd-plus.sx @@ -0,0 +1,62 @@ +;; lib/minikanren/tests/clpfd-plus.sx — fd-plus (x + y = z). + +(mk-test + "fd-plus-all-ground" + (run* q (fresh (z) (fd-plus 2 3 z) (== q z))) + (list 5)) + +(mk-test + "fd-plus-recover-x" + (run* q (fresh (x) (fd-plus x 3 5) (== q x))) + (list 2)) + +(mk-test + "fd-plus-recover-y" + (run* q (fresh (y) (fd-plus 2 y 5) (== q y))) + (list 3)) + +(mk-test + "fd-plus-impossible-fails" + (run* + q + (fresh + (z) + (fd-plus 2 3 z) + (== z 99) + (== q z))) + (list)) + +(mk-test + "fd-plus-domain-check" + (run* + q + (fresh + (x) + (fd-in x (list 3 4 5)) + (fd-plus x 3 5) + (== q x))) + (list)) + +(mk-test + "fd-plus-pairs-summing-to-5" + (run* + q + (fresh + (x y) + (fd-in x (list 1 2 3 4)) + (fd-in y (list 1 2 3 4)) + (fd-plus x y 5) + (fd-label (list x y)) + (== q (list x y)))) + (list + (list 1 4) + (list 2 3) + (list 3 2) + (list 4 1))) + +(mk-test + "fd-plus-z-derived" + (run* q (fresh (z) (fd-plus 7 8 z) (== q z))) + (list 15)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/clpfd-times.sx b/lib/minikanren/tests/clpfd-times.sx new file mode 100644 index 00000000..c858a537 --- /dev/null +++ b/lib/minikanren/tests/clpfd-times.sx @@ -0,0 +1,85 @@ +;; lib/minikanren/tests/clpfd-times.sx — fd-times (x * y = z). + +(mk-test + "fd-times-3-4" + (run* q (fresh (z) (fd-times 3 4 z) (== q z))) + (list 12)) + +(mk-test + "fd-times-recover-divisor" + (run* q (fresh (x) (fd-times x 5 30) (== q x))) + (list 6)) + +(mk-test + "fd-times-non-divisible-fails" + (run* q (fresh (x) (fd-times x 5 31) (== q x))) + (list)) + +(mk-test + "fd-times-by-zero" + (run* q (fresh (z) (fd-times 0 99 z) (== q z))) + (list 0)) + +(mk-test + "fd-times-zero-by-anything-zero" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-times x 0 0) + (fd-label (list x)) + (== q x))) + (list 1 2 3)) + +(mk-test + "fd-times-12-divisor-pairs" + (run* + q + (fresh + (x y) + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6)) + (fd-in + y + (list + 1 + 2 + 3 + 4 + 5 + 6)) + (fd-times x y 12) + (fd-label (list x y)) + (== q (list x y)))) + (list + (list 2 6) + (list 3 4) + (list 4 3) + (list 6 2))) + +(mk-test + "fd-times-square-of-each" + (run* + q + (fresh + (x z) + (fd-in x (list 1 2 3 4 5)) + (fd-times x x z) + (fd-label (list x)) + (== q (list x z)))) + (list + (list 1 1) + (list 2 4) + (list 3 9) + (list 4 16) + (list 5 25))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/conda.sx b/lib/minikanren/tests/conda.sx new file mode 100644 index 00000000..0f6ed1e6 --- /dev/null +++ b/lib/minikanren/tests/conda.sx @@ -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!) diff --git a/lib/minikanren/tests/conde.sx b/lib/minikanren/tests/conde.sx new file mode 100644 index 00000000..681f372b --- /dev/null +++ b/lib/minikanren/tests/conde.sx @@ -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!) diff --git a/lib/minikanren/tests/condu.sx b/lib/minikanren/tests/condu.sx new file mode 100644 index 00000000..f19deb07 --- /dev/null +++ b/lib/minikanren/tests/condu.sx @@ -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!) diff --git a/lib/minikanren/tests/counto.sx b/lib/minikanren/tests/counto.sx new file mode 100644 index 00000000..0c9248fc --- /dev/null +++ b/lib/minikanren/tests/counto.sx @@ -0,0 +1,35 @@ +;; lib/minikanren/tests/counto.sx — count occurrences of x in l (intarith). + +(mk-test + "counto-empty" + (run* q (counto 1 (list) q)) + (list 0)) +(mk-test + "counto-not-found" + (run* q (counto 99 (list 1 2 3) q)) + (list 0)) +(mk-test + "counto-once" + (run* q (counto 2 (list 1 2 3) q)) + (list 1)) +(mk-test + "counto-thrice" + (run* + q + (counto + 1 + (list 1 2 1 3 1) + q)) + (list 3)) +(mk-test + "counto-all-same" + (run* + q + (counto 7 (list 7 7 7 7) q)) + (list 4)) +(mk-test + "counto-string" + (run* q (counto "x" (list "x" "y" "x") q)) + (list 2)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/cyclic-graph.sx b/lib/minikanren/tests/cyclic-graph.sx new file mode 100644 index 00000000..f40675d2 --- /dev/null +++ b/lib/minikanren/tests/cyclic-graph.sx @@ -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!) diff --git a/lib/minikanren/tests/defrel.sx b/lib/minikanren/tests/defrel.sx new file mode 100644 index 00000000..9456bde7 --- /dev/null +++ b/lib/minikanren/tests/defrel.sx @@ -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!) diff --git a/lib/minikanren/tests/enumerate.sx b/lib/minikanren/tests/enumerate.sx new file mode 100644 index 00000000..bc1dd74a --- /dev/null +++ b/lib/minikanren/tests/enumerate.sx @@ -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!) diff --git a/lib/minikanren/tests/fd.sx b/lib/minikanren/tests/fd.sx new file mode 100644 index 00000000..4954d777 --- /dev/null +++ b/lib/minikanren/tests/fd.sx @@ -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!) diff --git a/lib/minikanren/tests/flat-mapo.sx b/lib/minikanren/tests/flat-mapo.sx new file mode 100644 index 00000000..fd98f3f3 --- /dev/null +++ b/lib/minikanren/tests/flat-mapo.sx @@ -0,0 +1,39 @@ +;; lib/minikanren/tests/flat-mapo.sx — concatMap-style relation. + +(mk-test + "flat-mapo-empty" + (run* q (flat-mapo (fn (x r) (== r (list x x))) (list) q)) + (list (list))) + +(mk-test + "flat-mapo-duplicate-each" + (run* + q + (flat-mapo + (fn (x r) (== r (list x x))) + (list 1 2 3) + q)) + (list + (list 1 1 2 2 3 3))) + +(mk-test + "flat-mapo-empty-from-each" + (run* q (flat-mapo (fn (x r) (== r (list))) (list :a :b :c) q)) + (list (list))) + +(mk-test + "flat-mapo-singleton-from-each-is-identity" + (run* q (flat-mapo (fn (x r) (== r (list x))) (list :a :b :c) q)) + (list (list :a :b :c))) + +(mk-test + "flat-mapo-tag-each" + (run* + q + (flat-mapo + (fn (x r) (== r (list :tag x))) + (list 1 2) + q)) + (list (list :tag 1 :tag 2))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/flatteno.sx b/lib/minikanren/tests/flatteno.sx new file mode 100644 index 00000000..4a01780a --- /dev/null +++ b/lib/minikanren/tests/flatteno.sx @@ -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!) diff --git a/lib/minikanren/tests/foldl-o.sx b/lib/minikanren/tests/foldl-o.sx new file mode 100644 index 00000000..2e196e43 --- /dev/null +++ b/lib/minikanren/tests/foldl-o.sx @@ -0,0 +1,48 @@ +;; lib/minikanren/tests/foldl-o.sx — relational left fold. + +(mk-test + "foldl-o-empty" + (run* q (foldl-o pluso-i (list) 42 q)) + (list 42)) + +(mk-test + "foldl-o-sum" + (run* + q + (foldl-o + pluso-i + (list 1 2 3 4 5) + 0 + q)) + (list 15)) + +(mk-test + "foldl-o-product" + (run* + q + (foldl-o + *o-i + (list 1 2 3 4) + 1 + q)) + (list 24)) + +(mk-test + "foldl-o-reverse-via-flip-conso" + (run* + q + (foldl-o + (fn (acc x r) (conso x acc r)) + (list 1 2 3 4) + (list) + q)) + (list (list 4 3 2 1))) + +(mk-test + "foldl-o-with-init" + (run* + q + (foldl-o pluso-i (list 1 2 3) 100 q)) + (list 106)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/foldr-o.sx b/lib/minikanren/tests/foldr-o.sx new file mode 100644 index 00000000..7a24ca5e --- /dev/null +++ b/lib/minikanren/tests/foldr-o.sx @@ -0,0 +1,38 @@ +;; lib/minikanren/tests/foldr-o.sx — relational right fold. + +(mk-test + "foldr-o-empty" + (run* q (foldr-o conso (list) (list 99) q)) + (list (list 99))) + +(mk-test + "foldr-o-conso-rebuilds-list" + (run* q (foldr-o conso (list 1 2 3) (list) q)) + (list (list 1 2 3))) + +(mk-test + "foldr-o-appendo-flattens" + (run* + q + (foldr-o + appendo + (list + (list 1 2) + (list 3) + (list 4 5)) + (list) + q)) + (list (list 1 2 3 4 5))) + +(mk-test + "foldr-o-with-acc-init" + (run* + q + (foldr-o + conso + (list 1 2) + (list 9 9) + q)) + (list (list 1 2 9 9))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/fresh.sx b/lib/minikanren/tests/fresh.sx new file mode 100644 index 00000000..fd912c55 --- /dev/null +++ b/lib/minikanren/tests/fresh.sx @@ -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!) diff --git a/lib/minikanren/tests/goals.sx b/lib/minikanren/tests/goals.sx new file mode 100644 index 00000000..150b0650 --- /dev/null +++ b/lib/minikanren/tests/goals.sx @@ -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!) diff --git a/lib/minikanren/tests/graph.sx b/lib/minikanren/tests/graph.sx new file mode 100644 index 00000000..a1b3e989 --- /dev/null +++ b/lib/minikanren/tests/graph.sx @@ -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!) diff --git a/lib/minikanren/tests/intarith.sx b/lib/minikanren/tests/intarith.sx new file mode 100644 index 00000000..baab8fe2 --- /dev/null +++ b/lib/minikanren/tests/intarith.sx @@ -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!) + diff --git a/lib/minikanren/tests/iterate-no.sx b/lib/minikanren/tests/iterate-no.sx new file mode 100644 index 00000000..56405e52 --- /dev/null +++ b/lib/minikanren/tests/iterate-no.sx @@ -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!) diff --git a/lib/minikanren/tests/lasto.sx b/lib/minikanren/tests/lasto.sx new file mode 100644 index 00000000..110f8019 --- /dev/null +++ b/lib/minikanren/tests/lasto.sx @@ -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!) diff --git a/lib/minikanren/tests/latin.sx b/lib/minikanren/tests/latin.sx new file mode 100644 index 00000000..8a0afabd --- /dev/null +++ b/lib/minikanren/tests/latin.sx @@ -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!) diff --git a/lib/minikanren/tests/laziness.sx b/lib/minikanren/tests/laziness.sx new file mode 100644 index 00000000..d3440ac4 --- /dev/null +++ b/lib/minikanren/tests/laziness.sx @@ -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!) diff --git a/lib/minikanren/tests/lengtho-i.sx b/lib/minikanren/tests/lengtho-i.sx new file mode 100644 index 00000000..6759e24e --- /dev/null +++ b/lib/minikanren/tests/lengtho-i.sx @@ -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!) diff --git a/lib/minikanren/tests/list-relations.sx b/lib/minikanren/tests/list-relations.sx new file mode 100644 index 00000000..0a9582d3 --- /dev/null +++ b/lib/minikanren/tests/list-relations.sx @@ -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!) diff --git a/lib/minikanren/tests/mapo.sx b/lib/minikanren/tests/mapo.sx new file mode 100644 index 00000000..3afbdd04 --- /dev/null +++ b/lib/minikanren/tests/mapo.sx @@ -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!) diff --git a/lib/minikanren/tests/matche.sx b/lib/minikanren/tests/matche.sx new file mode 100644 index 00000000..8309cfbf --- /dev/null +++ b/lib/minikanren/tests/matche.sx @@ -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!) diff --git a/lib/minikanren/tests/minmax.sx b/lib/minikanren/tests/minmax.sx new file mode 100644 index 00000000..76ea3dd5 --- /dev/null +++ b/lib/minikanren/tests/minmax.sx @@ -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!) diff --git a/lib/minikanren/tests/nafc.sx b/lib/minikanren/tests/nafc.sx new file mode 100644 index 00000000..cec8eaa6 --- /dev/null +++ b/lib/minikanren/tests/nafc.sx @@ -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!) diff --git a/lib/minikanren/tests/not-membero.sx b/lib/minikanren/tests/not-membero.sx new file mode 100644 index 00000000..8952f79e --- /dev/null +++ b/lib/minikanren/tests/not-membero.sx @@ -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!) diff --git a/lib/minikanren/tests/nub-o.sx b/lib/minikanren/tests/nub-o.sx new file mode 100644 index 00000000..cffa5159 --- /dev/null +++ b/lib/minikanren/tests/nub-o.sx @@ -0,0 +1,31 @@ +;; lib/minikanren/tests/nub-o.sx — relational dedupe (keep last occurrence). + +(mk-test "nub-o-empty" (run* q (nub-o (list) q)) (list (list))) + +(mk-test + "nub-o-no-duplicates" + (run* q (nub-o (list 1 2 3) q)) + (list (list 1 2 3))) + +(mk-test + "nub-o-with-duplicates" + (run* + q + (nub-o + (list 1 2 1 3 2 4) + q)) + (list (list 1 3 2 4))) + +(mk-test + "nub-o-all-same" + (let + ((res (run* q (nub-o (list 1 1 1) q)))) + (every? (fn (r) (= r (list 1))) res)) + true) + +(mk-test + "nub-o-keeps-last" + (run* q (nub-o (list 1 2 1) q)) + (list (list 2 1))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/pairlisto.sx b/lib/minikanren/tests/pairlisto.sx new file mode 100644 index 00000000..5406d37b --- /dev/null +++ b/lib/minikanren/tests/pairlisto.sx @@ -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!) diff --git a/lib/minikanren/tests/palindromeo.sx b/lib/minikanren/tests/palindromeo.sx new file mode 100644 index 00000000..0d28773f --- /dev/null +++ b/lib/minikanren/tests/palindromeo.sx @@ -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!) diff --git a/lib/minikanren/tests/parity.sx b/lib/minikanren/tests/parity.sx new file mode 100644 index 00000000..fc445558 --- /dev/null +++ b/lib/minikanren/tests/parity.sx @@ -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!) diff --git a/lib/minikanren/tests/partitiono.sx b/lib/minikanren/tests/partitiono.sx new file mode 100644 index 00000000..282d1bda --- /dev/null +++ b/lib/minikanren/tests/partitiono.sx @@ -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!) diff --git a/lib/minikanren/tests/path-cycle-free.sx b/lib/minikanren/tests/path-cycle-free.sx new file mode 100644 index 00000000..2c46e407 --- /dev/null +++ b/lib/minikanren/tests/path-cycle-free.sx @@ -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!) diff --git a/lib/minikanren/tests/peano.sx b/lib/minikanren/tests/peano.sx new file mode 100644 index 00000000..682a3dd4 --- /dev/null +++ b/lib/minikanren/tests/peano.sx @@ -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!) diff --git a/lib/minikanren/tests/predicates.sx b/lib/minikanren/tests/predicates.sx new file mode 100644 index 00000000..7242b278 --- /dev/null +++ b/lib/minikanren/tests/predicates.sx @@ -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!) diff --git a/lib/minikanren/tests/prefix-suffix.sx b/lib/minikanren/tests/prefix-suffix.sx new file mode 100644 index 00000000..7237ef1d --- /dev/null +++ b/lib/minikanren/tests/prefix-suffix.sx @@ -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!) diff --git a/lib/minikanren/tests/project.sx b/lib/minikanren/tests/project.sx new file mode 100644 index 00000000..b58c71ab --- /dev/null +++ b/lib/minikanren/tests/project.sx @@ -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!) diff --git a/lib/minikanren/tests/pythag.sx b/lib/minikanren/tests/pythag.sx new file mode 100644 index 00000000..c8015ea6 --- /dev/null +++ b/lib/minikanren/tests/pythag.sx @@ -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!) diff --git a/lib/minikanren/tests/queens-fd.sx b/lib/minikanren/tests/queens-fd.sx new file mode 100644 index 00000000..7457abd0 --- /dev/null +++ b/lib/minikanren/tests/queens-fd.sx @@ -0,0 +1,97 @@ +;; lib/minikanren/tests/queens-fd.sx — N-queens via CLP(FD). +;; +;; Native FD propagation makes N-queens tractable: 4-queens finds both +;; solutions instantly; 5-queens finds all 10 in seconds. Compare with +;; the naive enumerate-then-filter version in queens.sx, which struggles +;; past N=4. + +(define + fd-no-diag + (fn + (ci cj k) + (fresh + (a b) + (fd-plus cj k a) + (fd-plus ci k b) + (fd-neq ci a) + (fd-neq cj b)))) + +(define + n-queens-4-fd + (fn + (cs) + (let + ((c1 (nth cs 0)) + (c2 (nth cs 1)) + (c3 (nth cs 2)) + (c4 (nth cs 3))) + (mk-conj + (fd-in c1 (list 1 2 3 4)) + (fd-in c2 (list 1 2 3 4)) + (fd-in c3 (list 1 2 3 4)) + (fd-in c4 (list 1 2 3 4)) + (fd-distinct cs) + (fd-no-diag c1 c2 1) + (fd-no-diag c1 c3 2) + (fd-no-diag c1 c4 3) + (fd-no-diag c2 c3 1) + (fd-no-diag c2 c4 2) + (fd-no-diag c3 c4 1) + (fd-label cs))))) + +(define + n-queens-5-fd + (fn + (cs) + (let + ((c1 (nth cs 0)) + (c2 (nth cs 1)) + (c3 (nth cs 2)) + (c4 (nth cs 3)) + (c5 (nth cs 4))) + (mk-conj + (fd-in + c1 + (list 1 2 3 4 5)) + (fd-in + c2 + (list 1 2 3 4 5)) + (fd-in + c3 + (list 1 2 3 4 5)) + (fd-in + c4 + (list 1 2 3 4 5)) + (fd-in + c5 + (list 1 2 3 4 5)) + (fd-distinct cs) + (fd-no-diag c1 c2 1) + (fd-no-diag c1 c3 2) + (fd-no-diag c1 c4 3) + (fd-no-diag c1 c5 4) + (fd-no-diag c2 c3 1) + (fd-no-diag c2 c4 2) + (fd-no-diag c2 c5 3) + (fd-no-diag c3 c4 1) + (fd-no-diag c3 c5 2) + (fd-no-diag c4 c5 1) + (fd-label cs))))) + +(mk-test + "n-queens-4-fd-two-solutions" + (run* + q + (fresh (a b c d) (== q (list a b c d)) (n-queens-4-fd (list a b c d)))) + (list + (list 2 4 1 3) + (list 3 1 4 2))) + +(mk-test + "n-queens-5-fd-ten-solutions" + (let + ((sols (run* q (fresh (a b c d e) (== q (list a b c d e)) (n-queens-5-fd (list a b c d e)))))) + (= (len sols) 10)) + true) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/queens.sx b/lib/minikanren/tests/queens.sx new file mode 100644 index 00000000..2f85bdd8 --- /dev/null +++ b/lib/minikanren/tests/queens.sx @@ -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!) diff --git a/lib/minikanren/tests/rdb.sx b/lib/minikanren/tests/rdb.sx new file mode 100644 index 00000000..96514058 --- /dev/null +++ b/lib/minikanren/tests/rdb.sx @@ -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!) diff --git a/lib/minikanren/tests/relations.sx b/lib/minikanren/tests/relations.sx new file mode 100644 index 00000000..ffbdfcf6 --- /dev/null +++ b/lib/minikanren/tests/relations.sx @@ -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!) diff --git a/lib/minikanren/tests/removeo-allo.sx b/lib/minikanren/tests/removeo-allo.sx new file mode 100644 index 00000000..b7dd8a31 --- /dev/null +++ b/lib/minikanren/tests/removeo-allo.sx @@ -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!) diff --git a/lib/minikanren/tests/repeato-concato.sx b/lib/minikanren/tests/repeato-concato.sx new file mode 100644 index 00000000..ff730413 --- /dev/null +++ b/lib/minikanren/tests/repeato-concato.sx @@ -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!) diff --git a/lib/minikanren/tests/rev-acco.sx b/lib/minikanren/tests/rev-acco.sx new file mode 100644 index 00000000..6733fe9a --- /dev/null +++ b/lib/minikanren/tests/rev-acco.sx @@ -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!) diff --git a/lib/minikanren/tests/run.sx b/lib/minikanren/tests/run.sx new file mode 100644 index 00000000..c25a49e4 --- /dev/null +++ b/lib/minikanren/tests/run.sx @@ -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!) diff --git a/lib/minikanren/tests/selecto.sx b/lib/minikanren/tests/selecto.sx new file mode 100644 index 00000000..ba34a86b --- /dev/null +++ b/lib/minikanren/tests/selecto.sx @@ -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!) diff --git a/lib/minikanren/tests/simplifyo.sx b/lib/minikanren/tests/simplifyo.sx new file mode 100644 index 00000000..02a56e0b --- /dev/null +++ b/lib/minikanren/tests/simplifyo.sx @@ -0,0 +1,47 @@ +;; lib/minikanren/tests/simplifyo.sx — algebraic expression simplifier +;; demo using conda for first-match-wins dispatch. + +(define + simplify-step-o + (fn + (expr result) + (conda + ((fresh (x) (== expr (list :+ 0 x)) (== result x))) + ((fresh (x) (== expr (list :+ x 0)) (== result x))) + ((fresh (y) (== expr (list :* 0 y)) (== result 0))) + ((fresh (x) (== expr (list :* x 0)) (== result 0))) + ((fresh (x) (== expr (list :* 1 x)) (== result x))) + ((fresh (x) (== expr (list :* x 1)) (== result x))) + ((== result expr))))) ;; default: unchanged + +(mk-test + "simplify-zero-plus" + (run* q (simplify-step-o (list :+ 0 :y) q)) + (list :y)) + +(mk-test + "simplify-plus-zero" + (run* q (simplify-step-o (list :+ :x 0) q)) + (list :x)) + +(mk-test + "simplify-zero-times" + (run* q (simplify-step-o (list :* 0 :y) q)) + (list 0)) + +(mk-test + "simplify-one-times" + (run* q (simplify-step-o (list :* 1 :y) q)) + (list :y)) + +(mk-test + "simplify-no-rule-applies" + (run* q (simplify-step-o (list :+ :x :y) q)) + (list (list :+ :x :y))) + +(mk-test + "simplify-non-identity-form" + (run* q (simplify-step-o (list :+ 5 7) q)) + (list (list :+ 5 7))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/sortedo.sx b/lib/minikanren/tests/sortedo.sx new file mode 100644 index 00000000..6137da0c --- /dev/null +++ b/lib/minikanren/tests/sortedo.sx @@ -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!) diff --git a/lib/minikanren/tests/subo.sx b/lib/minikanren/tests/subo.sx new file mode 100644 index 00000000..a48c645a --- /dev/null +++ b/lib/minikanren/tests/subo.sx @@ -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!) diff --git a/lib/minikanren/tests/subseto.sx b/lib/minikanren/tests/subseto.sx new file mode 100644 index 00000000..68c4cf82 --- /dev/null +++ b/lib/minikanren/tests/subseto.sx @@ -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!) diff --git a/lib/minikanren/tests/sum-product.sx b/lib/minikanren/tests/sum-product.sx new file mode 100644 index 00000000..6eddd96c --- /dev/null +++ b/lib/minikanren/tests/sum-product.sx @@ -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!) diff --git a/lib/minikanren/tests/swap-firsto.sx b/lib/minikanren/tests/swap-firsto.sx new file mode 100644 index 00000000..773a57c2 --- /dev/null +++ b/lib/minikanren/tests/swap-firsto.sx @@ -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!) diff --git a/lib/minikanren/tests/tabling-more.sx b/lib/minikanren/tests/tabling-more.sx new file mode 100644 index 00000000..332c1177 --- /dev/null +++ b/lib/minikanren/tests/tabling-more.sx @@ -0,0 +1,55 @@ +;; lib/minikanren/tests/tabling-more.sx — table-1 + table-3. + +;; --- table-1 (predicate caching) --- + +(define + tab-in-list + (table-1 + "in-list" + (fn + (x) + (membero + x + (list 1 2 3 4 5))))) + +(mk-tab-clear!) +(mk-test + "table-1-hit" + (run* q (tab-in-list 3)) + (list (make-symbol "_.0"))) +(mk-test "table-1-miss-no" (run* q (tab-in-list 99)) (list)) +(mk-test + "table-1-replay" + (run* q (tab-in-list 3)) + (list (make-symbol "_.0"))) + +;; --- table-3 (Ackermann) --- + +(define + ack-o + (table-3 + "ack" + (fn + (m n result) + (conde + ((== m 0) (pluso-i n 1 result)) + ((fresh (m-1) (lto-i 0 m) (== n 0) (minuso-i m 1 m-1) (ack-o m-1 1 result))) + ((fresh (m-1 n-1 inner) (lto-i 0 m) (lto-i 0 n) (minuso-i m 1 m-1) (minuso-i n 1 n-1) (ack-o m n-1 inner) (ack-o m-1 inner result))))))) + +(mk-tab-clear!) +(mk-test + "ack-0-0" + (run* q (ack-o 0 0 q)) + (list 1)) +(mk-tab-clear!) +(mk-test + "ack-2-3" + (run* q (ack-o 2 3 q)) + (list 9)) +(mk-tab-clear!) +(mk-test + "ack-3-3" + (run* q (ack-o 3 3 q)) + (list 61)) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/tabling.sx b/lib/minikanren/tests/tabling.sx new file mode 100644 index 00000000..031d2f35 --- /dev/null +++ b/lib/minikanren/tests/tabling.sx @@ -0,0 +1,60 @@ +;; lib/minikanren/tests/tabling.sx — Phase 7 piece A: naive memoization. + +;; --- Fibonacci canary: tabled vs naive -- + +(define + tab-fib-o + (table-2 + "fib" + (fn + (n result) + (conde + ((== n 0) (== result 0)) + ((== n 1) (== result 1)) + ((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (tab-fib-o n-1 r-1) (tab-fib-o n-2 r-2) (pluso-i r-1 r-2 result))))))) + +(mk-tab-clear!) + +(mk-test "tab-fib-zero" (run* q (tab-fib-o 0 q)) (list 0)) +(mk-tab-clear!) +(mk-test "tab-fib-one" (run* q (tab-fib-o 1 q)) (list 1)) +(mk-tab-clear!) +(mk-test "tab-fib-two" (run* q (tab-fib-o 2 q)) (list 1)) +(mk-tab-clear!) +(mk-test "tab-fib-five" (run* q (tab-fib-o 5 q)) (list 5)) +(mk-tab-clear!) +(mk-test "tab-fib-ten" (run* q (tab-fib-o 10 q)) (list 55)) +(mk-tab-clear!) +(mk-test + "tab-fib-twenty" + (run* q (tab-fib-o 20 q)) + (list 6765)) + +;; --- ground-term predicate --- + +(mk-test "tab-ground-term-num" (mk-tab-ground-term? 5) true) +(mk-test "tab-ground-term-str" (mk-tab-ground-term? "hi") true) +(mk-test + "tab-ground-term-list" + (mk-tab-ground-term? (list 1 2 3)) + true) +(mk-test "tab-ground-term-var" (mk-tab-ground-term? (mk-var "x")) false) +(mk-test + "tab-ground-term-nested" + (mk-tab-ground-term? + (list 1 (list 2 (mk-var "y")) 3)) + false) + +;; --- caching reduces work — count cache hits via repeated query --- + +(mk-test + "tab-cache-replay" + (begin + (mk-tab-clear!) + (let + ((first (run* q (tab-fib-o 10 q))) + (second (run* q (tab-fib-o 10 q)))) + (and (= first (list 55)) (= second (list 55))))) + true) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/take-drop.sx b/lib/minikanren/tests/take-drop.sx new file mode 100644 index 00000000..c8c2959d --- /dev/null +++ b/lib/minikanren/tests/take-drop.sx @@ -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!) diff --git a/lib/minikanren/tests/take-while-drop-while.sx b/lib/minikanren/tests/take-while-drop-while.sx new file mode 100644 index 00000000..99cd69cd --- /dev/null +++ b/lib/minikanren/tests/take-while-drop-while.sx @@ -0,0 +1,80 @@ +;; lib/minikanren/tests/take-while-drop-while.sx — prefix/suffix by predicate. + +(mk-test + "take-while-o-empty" + (run* q (take-while-o (fn (x) (== x 1)) (list) q)) + (list (list))) + +(mk-test + "take-while-o-while-lt-5" + (run* + q + (take-while-o + (fn (x) (lto-i x 5)) + (list 1 3 7 2 9) + q)) + (list (list 1 3))) + +(mk-test + "take-while-o-all-match" + (run* + q + (take-while-o + (fn (x) (lto-i x 100)) + (list 1 2 3) + q)) + (list (list 1 2 3))) + +(mk-test + "take-while-o-none-match" + (run* + q + (take-while-o + (fn (x) (lto-i 100 x)) + (list 1 2 3) + q)) + (list (list))) + +(mk-test + "drop-while-o-empty" + (run* q (drop-while-o (fn (x) (== x 1)) (list) q)) + (list (list))) + +(mk-test + "drop-while-o-while-lt-5" + (run* + q + (drop-while-o + (fn (x) (lto-i x 5)) + (list 1 3 7 2 9) + q)) + (list (list 7 2 9))) + +(mk-test + "drop-while-o-all-match" + (run* + q + (drop-while-o + (fn (x) (lto-i x 100)) + (list 1 2 3) + q)) + (list (list))) + +(mk-test + "take-drop-roundtrip" + (run* + q + (fresh + (p s) + (take-while-o + (fn (x) (lto-i x 5)) + (list 1 3 7 2 9) + p) + (drop-while-o + (fn (x) (lto-i x 5)) + (list 1 3 7 2 9) + s) + (appendo p s q))) + (list (list 1 3 7 2 9))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/types.sx b/lib/minikanren/tests/types.sx new file mode 100644 index 00000000..5eb50e6f --- /dev/null +++ b/lib/minikanren/tests/types.sx @@ -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!) diff --git a/lib/minikanren/tests/unify.sx b/lib/minikanren/tests/unify.sx new file mode 100644 index 00000000..3bec755b --- /dev/null +++ b/lib/minikanren/tests/unify.sx @@ -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!) diff --git a/lib/minikanren/tests/zip-with-o.sx b/lib/minikanren/tests/zip-with-o.sx new file mode 100644 index 00000000..c3cea9ab --- /dev/null +++ b/lib/minikanren/tests/zip-with-o.sx @@ -0,0 +1,52 @@ +;; lib/minikanren/tests/zip-with-o.sx — element-wise combine of two lists. + +(mk-test + "zip-with-o-empty" + (run* q (zip-with-o pluso-i (list) (list) q)) + (list (list))) + +(mk-test + "zip-with-o-pluso-i" + (run* + q + (zip-with-o + pluso-i + (list 1 2 3) + (list 10 20 30) + q)) + (list (list 11 22 33))) + +(mk-test + "zip-with-o-times-i" + (run* + q + (zip-with-o + *o-i + (list 2 3 4) + (list 5 6 7) + q)) + (list (list 10 18 28))) + +(mk-test + "zip-with-o-different-length-fails" + (run* + q + (zip-with-o + pluso-i + (list 1 2) + (list 1 2 3) + q)) + (list)) + +(mk-test + "zip-with-o-non-arith-rel" + (run* + q + (zip-with-o + (fn (a b r) (== r (list a b))) + (list :x :y) + (list 1 2) + q)) + (list (list (list :x 1) (list :y 2)))) + +(mk-tests-run!) diff --git a/lib/minikanren/unify.sx b/lib/minikanren/unify.sx new file mode 100644 index 00000000..89f00ab4 --- /dev/null +++ b/lib/minikanren/unify.sx @@ -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))) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 734a8a2c..16816005 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -50,68 +50,126 @@ Key semantic mappings: ## Roadmap ### Phase 1 — variables + unification -- [ ] `make-var` → fresh logic variable (unique mutable box) -- [ ] `var?` `v` → bool — is this a logic variable? -- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var -- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts) -- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure) +- [x] `make-var` → fresh logic variable (unique mutable box) +- [x] `var?` `v` → bool — is this a logic variable? +- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var +- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts) +- [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure) 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. -- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list) -- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs +- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it) +- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs ### Phase 2 — streams + goals -- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`), - `mplus` (interleave two streams), `bind` (apply goal to stream) -- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy -- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))` -- [ ] `succeed` / `fail` — trivial goals -- [ ] `fresh` — `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many -- [ ] `conde` — interleaving disjunction of goal lists -- [ ] `condu` — committed choice (soft-cut): only explores first successful clause -- [ ] `onceo` — succeeds at most once -- [ ] Tests: basic goal composition, backtracking, interleaving +- [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave), + `mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host + `bind` primitive that silently shadows user defines. +- [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends + and swaps when its left operand is paused, giving fair interleaving. +- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))` +- [x] `==-check` — opt-in occurs-checked equality goal +- [x] `succeed` / `fail` — trivial goals +- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction +- [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 -- [ ] `run*` `goal` → list of all answers (reified) -- [ ] `run n` `goal` → list of first n answers -- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names -- [ ] `reify-s` → builds reification substitution for naming unbound vars consistently -- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar -- [ ] Query variable conventions: `q` as canonical query variable -- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`, +- [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as + fresh var, conj goals, take all from stream, reify each. +- [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all) +- [x] `reify` `term` `subst` → walk* + build reification subst + walk* again +- [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a + `_.N` symbol via `(make-symbol (str "_." n))` +- [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)`, - 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 -- [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards -- [ ] `membero` `x` `l` — x is a member of l -- [ ] `listo` `l` — l is a proper list -- [ ] `nullo` `l` — l is empty -- [ ] `pairo` `p` — p is a pair (cons cell) -- [ ] `caro` `p` `a` — car of pair -- [ ] `cdro` `p` `d` — cdr of pair -- [ ] `conso` `a` `d` `p` — cons -- [ ] `firsto` / `resto` — aliases for caro/cdro -- [ ] `reverseo` `l` `r` — reverse of list -- [ ] `flatteno` `l` `f` — flatten nested lists -- [ ] `permuteo` `l` `p` — permutation of list -- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer) -- [ ] Tests: run each relation forwards and backwards; generate from partial inputs +- [x] `appendo` `l` `s` `ls` — list append, runs forwards AND backwards. + Canary green: `(run* q (appendo (1 2) (3 4) q))` → `((1 2 3 4))`; + `(run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s))))` → + all four splits. +- [x] `membero` `x` `l` — enumerates: `(run* q (membero q (a b c)))` → `(a b c)` +- [x] `listo` `l` — l is a proper list; enumerates list shapes with laziness +- [x] `nullo` `l` — l is empty +- [x] `pairo` `p` — p is a (non-empty) cons-cell / list +- [x] `caro` / `cdro` / `conso` / `firsto` / `resto` +- [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean, + `run*` diverges due to interleaved unbounded list search (canonical TRS issue). +- [x] `flatteno` `l` `f` — flatten nested lists. Three conde clauses: + empty → empty; pair → recurse on car & cdr + appendo; otherwise atom → + `(== 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 -- [ ] `project` `(x ...) body` — access reified values of logic vars inside a goal; - escapes to ground values for arithmetic or string ops -- [ ] `matche` — pattern matching over logic terms (extension from core.logic) - `(matche l ((head . tail) goal) (() goal))` -- [ ] `conda` — soft-cut disjunction (like Prolog `->`) -- [ ] `condu` — committed choice (already in phase 2; refine semantics here) -- [ ] `nafc` — negation as finite failure with constraint +- [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)` + in the body's lexical scope, then runs `(mk-conj body...)` on the same + substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`) +- [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` / + symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes + `(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol + 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` ### Phase 6 — arithmetic constraints CLP(FD) -- [ ] Finite domain variables: `fd-var` with domain `[lo..hi]` -- [ ] `in` `x` `domain` — constrain x to domain +- [x] Finite domain variables: domain stored under reserved key `_fd` in + the substitution dict; ascending sorted-int-list representation; + domain primitives `fd-dom-from-list`, `fd-dom-intersect`, + `fd-dom-without`, `fd-dom-range`, `fd-dom-min/max/empty?/singleton?`. +- [x] `fd-in x dom` — narrows x's domain by intersection. +- [x] `fd-eq x y`, `fd-neq x y`, `fd-lt`, `fd-lte` — propagator-store + goals. Each adds a closure to the constraints field and runs it + on post; closures re-fire after every label step via fd-fire-store. +- [x] `fd-plus x y z`, `fd-times x y z` — ground-cases propagators + (when 2 of 3 walk to numbers, the third is derived). +- [x] `fd-distinct vars` — pairwise alldifferent via fd-neq folds. +- [x] Constraint reactivation: `fd-fire-store` iterates to fixed point + using a domain+bindings signature comparison; ensures multi-step + propagation chains (e.g. fd-plus binds a fresh var, which then + lets a downstream fd-neq fire). +- [x] Labelling: `fd-label vars` enumerates each var's domain via + mk-mplus over singleton bindings; constraint store re-fires after + each binding. +- [x] Tests: N-queens via FD — 4-queens finds both solutions, 5-queens + finds all 10 in seconds (vs the naive enumerate-then-filter + version which times out past N=4). +- [x] `ino` `x` `domain` — alias for `(membero x domain)` (kept for + the simple enumerate-then-filter pattern alongside fd-in). +- [x] `all-distincto` `l` — original membero-based version (kept alongside + the newer fd-distinct). - [ ] `fd-eq` `x` `y` — x = y (constraint propagation) - [ ] `fd-neq` `x` `y` — x ≠ y - [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints @@ -122,10 +180,22 @@ Key semantic mappings: - [ ] Tests: send-more-money, N-queens with CLP(FD), map coloring, cryptarithmetic ### Phase 7 — tabling (memoization of relations) -- [ ] `tabled` annotation: memoize calls to a relation using a hash table -- [ ] Prevents infinite loops in recursive relations like `patho` on cyclic graphs -- [ ] Producer/consumer scheduling for tabled relations (variant of SLG resolution) -- [ ] Tests: cyclic graph reachability, mutual recursion, Fibonacci via tabling +- [x] `table-1`, `table-2`, `table-3` wrappers: ground-arg memoization + for 1-, 2-, and 3-argument relations. +- [x] `table-2` wrapper: ground-arg memoization for 2-arg relations. + Cache keyed by walked input; on miss runs underlying relation, + collects all output values from the answer stream, stores, and + replays. Subsequent calls with the same ground input replay the + cached values (no recomputation). +- [x] Fibonacci canary green: tabled `fib(25) = 75025` in seconds; + naive `fib(25)` times out at 60s. Memoization turns exponential + recursion into linear. +- [x] Ackermann canary green via `table-3`: `A(3, 3) = 61`. +- [ ] Producer/consumer SLG scheduling — required to handle recursive + tabled calls with the SAME ground key (e.g. cyclic `patho` with a + shared key); naive memoization deferred to a future iteration. +- [ ] Tests: cyclic graph reachability via tabled patho (deferred — + requires SLG); mutual recursion (deferred). ## Blockers @@ -135,4 +205,242 @@ _(none yet)_ _Newest first._ -_(awaiting phase 1)_ +- **2026-05-08** — **Session snapshot**: 17 lib files, 61 test files, 1229 + library LOC + 4360 test LOC, **551/551 tests cumulative**. Library covers + Phases 1–5 fully, Phase 6 partial (FD helpers + intarith escape), Phase 7 + documented via cyclic-graph divergence test. lib-guest validation + completed: `lib/minikanren/unify.sx` ≈ 50 LOC of local logic over + `lib/guest/match.sx`'s ≈100 LOC kit (kit earns ~3× by line count). Major + classic miniKanren tests green: appendo forwards/backwards, Peano + arithmetic, 4-queens, Pythagorean triples, family-relations / pet + puzzle / symbolic differentiation, 2x2 Latin square. Ready for Phase 6 + (native FD with arc-consistency) and Phase 7 (tabling) as future work. +- **2026-05-08** — **zip-with-o**: element-wise relational combine over two + lists with a 3-arg combiner. Ground-only by composition. 5 new tests. +- **2026-05-08** — **take-while-o + drop-while-o**: predicate-driven + prefix/suffix split. Roundtrip property verified. 8 new tests. +- **2026-05-08** — **arith-progo**: arithmetic-progression list generator + via project. 6 new tests. +- **2026-05-08** — **counto**: count occurrences of x in l (intarith). + 6 new tests. +- **2026-05-08** — **nub-o**: dedupe via membero-on-tail. Multiplicity + caveat documented in tests. 5 new tests. +- **2026-05-08** — **simplify-step-o**: algebraic identity simplifier + (conda demo). 6 new tests. +- **2026-05-08** — **flat-mapo**: concatMap-style relation. 5 new tests. +- **2026-05-08** — **foldl-o (relational left fold)**: complement to foldr-o. Combiner has args (acc, head) -> new-acc. (foldl-o pluso-i (1 2 3 4 5) 0 q) -> 15; (foldl-o flipped-conso l () q) reverses l. 5 new tests, 510/510 cumulative. +- **2026-05-08** — **foldr-o (relational right fold)**: takes a 3-arg combiner relation rel, a list, an initial accumulator, produces the result. (foldr-o appendo lists () q) is a flatten; (foldr-o conso l () q) rebuilds l. 4 new tests, 505/505 cumulative. +- **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.