Compare commits
56 Commits
architectu
...
loops/mini
| Author | SHA1 | Date | |
|---|---|---|---|
| 08f4a7babd | |||
| 221c7fef35 | |||
| 363ebc8f04 | |||
| 7ff72cefb2 | |||
| 064ab2900b | |||
| 4f5f8015fb | |||
| c4b6f1fa0f | |||
| 6454603568 | |||
| 4df277803d | |||
| 58d78de32a | |||
| 6bc3c14dac | |||
| eb69039935 | |||
| c04ddd105b | |||
| 136cacbd3f | |||
| 6fc155ddd8 | |||
| d992788a03 | |||
| 4d861575df | |||
| e202c81a0d | |||
| fc14a8063b | |||
| 6ee02db2ab | |||
| 7b6cb64548 | |||
| c2b238635f | |||
| 8c48a0be63 | |||
| 54a58c704e | |||
| ada405b37b | |||
| 99066430fd | |||
| 48835f2d4f | |||
| 16fe22669a | |||
| 2d51a8c4ea | |||
| b4c1253891 | |||
| e7dca2675c | |||
| f00054309d | |||
| cfb43a3cdf | |||
| 186171fec3 | |||
| 9795532f7d | |||
| b89b0def93 | |||
| 428ca79f61 | |||
| bf9fe8b365 | |||
| 2ae848dfe7 | |||
| 33693fc957 | |||
| 3d2a5b1814 | |||
| bc9261e90a | |||
| fd73f3c51b | |||
| b8a0c504bc | |||
| a038d41815 | |||
| d61b355413 | |||
| 43d58e6ca9 | |||
| 240ed90b20 | |||
| f4ab7f2534 | |||
| cae87c1e2c | |||
| 52070e07fc | |||
| 2de6727e83 | |||
| c754a8ee05 | |||
| f43ad04f91 | |||
| 0ba60d6a25 | |||
| f13e03e625 |
42
lib/minikanren/conda.sx
Normal file
42
lib/minikanren/conda.sx
Normal file
@@ -0,0 +1,42 @@
|
|||||||
|
;; lib/minikanren/conda.sx — Phase 5 piece A: `conda`, the soft-cut.
|
||||||
|
;;
|
||||||
|
;; (conda (g0 g ...) (h0 h ...) ...)
|
||||||
|
;; — first clause whose head g0 produces ANY answer wins; ALL of g0's
|
||||||
|
;; answers are then conj'd with the rest of that clause; later
|
||||||
|
;; clauses are NOT tried.
|
||||||
|
;; — differs from condu only in not wrapping g0 in onceo: condu
|
||||||
|
;; commits to the SINGLE first answer, conda lets the head's full
|
||||||
|
;; answer-set flow into the rest of the clause.
|
||||||
|
;; (Reasoned Schemer chapter 10; Byrd 5.3.)
|
||||||
|
|
||||||
|
(define
|
||||||
|
conda-try
|
||||||
|
(fn
|
||||||
|
(clauses s)
|
||||||
|
(cond
|
||||||
|
((empty? clauses) mzero)
|
||||||
|
(:else
|
||||||
|
(let
|
||||||
|
((cl (first clauses)))
|
||||||
|
(let
|
||||||
|
((head-goal (first cl)) (rest-goals (rest cl)))
|
||||||
|
(let
|
||||||
|
((peek (stream-take 1 (head-goal s))))
|
||||||
|
(if
|
||||||
|
(empty? peek)
|
||||||
|
(conda-try (rest clauses) s)
|
||||||
|
(mk-bind (head-goal s) (mk-conj-list rest-goals))))))))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
conda
|
||||||
|
(&rest clauses)
|
||||||
|
(quasiquote
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(conda-try
|
||||||
|
(list
|
||||||
|
(splice-unquote
|
||||||
|
(map
|
||||||
|
(fn (cl) (quasiquote (list (splice-unquote cl))))
|
||||||
|
clauses)))
|
||||||
|
s))))
|
||||||
39
lib/minikanren/conde.sx
Normal file
39
lib/minikanren/conde.sx
Normal file
@@ -0,0 +1,39 @@
|
|||||||
|
;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
|
||||||
|
;; miniKanren and-or form, with implicit Zzz inverse-eta delay so recursive
|
||||||
|
;; relations like appendo terminate.
|
||||||
|
;;
|
||||||
|
;; (conde (g1a g1b ...) (g2a g2b ...) ...)
|
||||||
|
;; ≡ (mk-disj (Zzz (mk-conj g1a g1b ...))
|
||||||
|
;; (Zzz (mk-conj g2a g2b ...)) ...)
|
||||||
|
;;
|
||||||
|
;; `Zzz g` wraps a goal expression in (fn (S) (fn () (g S))) so that
|
||||||
|
;; `g`'s body isn't constructed until the surrounding fn is applied to a
|
||||||
|
;; substitution AND the returned thunk is forced. This is what gives
|
||||||
|
;; miniKanren its laziness — recursive goal definitions can be `(conde
|
||||||
|
;; ... (... (recur ...)))` without infinite descent at construction time.
|
||||||
|
;;
|
||||||
|
;; Hygiene: the substitution parameter is gensym'd so that user goal
|
||||||
|
;; expressions which themselves bind `s` (e.g. `(appendo l s ls)`) keep
|
||||||
|
;; their lexical `s` and don't accidentally reference the wrapper's
|
||||||
|
;; substitution. Without gensym, miniKanren relations that follow the
|
||||||
|
;; common (l s ls) parameter convention are silently miscompiled.
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
Zzz
|
||||||
|
(g)
|
||||||
|
(let
|
||||||
|
((s-sym (gensym "zzz-s-")))
|
||||||
|
(quasiquote
|
||||||
|
(fn ((unquote s-sym)) (fn () ((unquote g) (unquote s-sym)))))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
conde
|
||||||
|
(&rest clauses)
|
||||||
|
(quasiquote
|
||||||
|
(mk-disj
|
||||||
|
(splice-unquote
|
||||||
|
(map
|
||||||
|
(fn
|
||||||
|
(clause)
|
||||||
|
(quasiquote (Zzz (mk-conj (splice-unquote clause)))))
|
||||||
|
clauses)))))
|
||||||
58
lib/minikanren/condu.sx
Normal file
58
lib/minikanren/condu.sx
Normal file
@@ -0,0 +1,58 @@
|
|||||||
|
;; lib/minikanren/condu.sx — Phase 2 piece D: `condu` and `onceo`.
|
||||||
|
;;
|
||||||
|
;; Both are commitment forms (no backtracking into discarded options):
|
||||||
|
;;
|
||||||
|
;; (onceo g) — succeeds at most once: takes the first answer
|
||||||
|
;; stream-take produces from (g s).
|
||||||
|
;;
|
||||||
|
;; (condu (g0 g ...) (h0 h ...) ...)
|
||||||
|
;; — first clause whose head goal succeeds wins; only
|
||||||
|
;; the first answer of the head is propagated to the
|
||||||
|
;; rest of that clause; later clauses are not tried.
|
||||||
|
;; (Reasoned Schemer chapter 10; Byrd 5.4.)
|
||||||
|
|
||||||
|
(define
|
||||||
|
onceo
|
||||||
|
(fn
|
||||||
|
(g)
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(let
|
||||||
|
((peek (stream-take 1 (g s))))
|
||||||
|
(if (empty? peek) mzero (unit (first peek)))))))
|
||||||
|
|
||||||
|
;; condu-try — runtime walker over a list of clauses (each clause a list of
|
||||||
|
;; goals). Forces the head with stream-take 1; if head fails, recurse to
|
||||||
|
;; the next clause; if head succeeds, commits its single answer through
|
||||||
|
;; the rest of the clause.
|
||||||
|
(define
|
||||||
|
condu-try
|
||||||
|
(fn
|
||||||
|
(clauses s)
|
||||||
|
(cond
|
||||||
|
((empty? clauses) mzero)
|
||||||
|
(:else
|
||||||
|
(let
|
||||||
|
((cl (first clauses)))
|
||||||
|
(let
|
||||||
|
((head-goal (first cl)) (rest-goals (rest cl)))
|
||||||
|
(let
|
||||||
|
((peek (stream-take 1 (head-goal s))))
|
||||||
|
(if
|
||||||
|
(empty? peek)
|
||||||
|
(condu-try (rest clauses) s)
|
||||||
|
((mk-conj-list rest-goals) (first peek))))))))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
condu
|
||||||
|
(&rest clauses)
|
||||||
|
(quasiquote
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(condu-try
|
||||||
|
(list
|
||||||
|
(splice-unquote
|
||||||
|
(map
|
||||||
|
(fn (cl) (quasiquote (list (splice-unquote cl))))
|
||||||
|
clauses)))
|
||||||
|
s))))
|
||||||
25
lib/minikanren/defrel.sx
Normal file
25
lib/minikanren/defrel.sx
Normal file
@@ -0,0 +1,25 @@
|
|||||||
|
;; lib/minikanren/defrel.sx — Prolog-style defrel macro.
|
||||||
|
;;
|
||||||
|
;; (defrel (NAME ARG1 ARG2 ...)
|
||||||
|
;; (CLAUSE1 ...)
|
||||||
|
;; (CLAUSE2 ...)
|
||||||
|
;; ...)
|
||||||
|
;;
|
||||||
|
;; expands to
|
||||||
|
;;
|
||||||
|
;; (define NAME (fn (ARG1 ARG2 ...) (conde (CLAUSE1 ...) (CLAUSE2 ...))))
|
||||||
|
;;
|
||||||
|
;; This puts each clause's goals immediately after the head, mirroring
|
||||||
|
;; Prolog's `name(Args) :- goals.` shape. Clauses are conde-conjoined
|
||||||
|
;; goals — `Zzz`-wrapping is automatic via `conde`, so recursive
|
||||||
|
;; relations terminate on partial answers.
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
defrel
|
||||||
|
(head &rest clauses)
|
||||||
|
(let
|
||||||
|
((name (first head)) (args (rest head)))
|
||||||
|
(list
|
||||||
|
(quote define)
|
||||||
|
name
|
||||||
|
(list (quote fn) args (cons (quote conde) clauses)))))
|
||||||
25
lib/minikanren/fd.sx
Normal file
25
lib/minikanren/fd.sx
Normal file
@@ -0,0 +1,25 @@
|
|||||||
|
;; lib/minikanren/fd.sx — Phase 6 piece A: minimal finite-domain helpers.
|
||||||
|
;;
|
||||||
|
;; A full CLP(FD) engine (arc consistency, native integer domains, fd-plus
|
||||||
|
;; etc.) is Phase 6 proper. For now we expose two small relations layered
|
||||||
|
;; on the existing list machinery — they're sufficient for permutation
|
||||||
|
;; puzzles, the N-queens-style core of constraint solving:
|
||||||
|
;;
|
||||||
|
;; (ino x dom) — x is a member of dom (alias for membero with the
|
||||||
|
;; constraint-store-friendly argument order).
|
||||||
|
;; (all-distincto l) — all elements of l are pairwise distinct.
|
||||||
|
;;
|
||||||
|
;; all-distincto uses nafc + membero on the tail — it requires the head
|
||||||
|
;; element of each recursive step to be ground enough for membero to be
|
||||||
|
;; finitary, so order matters: prefer (in x dom) goals BEFORE
|
||||||
|
;; (all-distincto (list x ...)) so values get committed first.
|
||||||
|
|
||||||
|
(define ino (fn (x dom) (membero x dom)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
all-distincto
|
||||||
|
(fn
|
||||||
|
(l)
|
||||||
|
(conde
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (nafc (membero a d)) (all-distincto d))))))
|
||||||
23
lib/minikanren/fresh.sx
Normal file
23
lib/minikanren/fresh.sx
Normal file
@@ -0,0 +1,23 @@
|
|||||||
|
;; lib/minikanren/fresh.sx — Phase 2 piece B: `fresh` for introducing
|
||||||
|
;; logic variables inside a goal body.
|
||||||
|
;;
|
||||||
|
;; (fresh (x y z) goal1 goal2 ...)
|
||||||
|
;; ≡ (let ((x (make-var)) (y (make-var)) (z (make-var)))
|
||||||
|
;; (mk-conj goal1 goal2 ...))
|
||||||
|
;;
|
||||||
|
;; A macro rather than a function so user-named vars are real lexical
|
||||||
|
;; bindings — which is also what miniKanren convention expects.
|
||||||
|
;; The empty-vars form (fresh () goal ...) is just a goal grouping.
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
fresh
|
||||||
|
(vars &rest goals)
|
||||||
|
(quasiquote
|
||||||
|
(let
|
||||||
|
(unquote (map (fn (v) (list v (list (quote make-var)))) vars))
|
||||||
|
(mk-conj (splice-unquote goals)))))
|
||||||
|
|
||||||
|
;; call-fresh — functional alternative for code that builds goals
|
||||||
|
;; programmatically:
|
||||||
|
;; ((call-fresh (fn (x) (== x 7))) empty-s) → ({:_.N 7})
|
||||||
|
(define call-fresh (fn (f) (fn (s) ((f (make-var)) s))))
|
||||||
58
lib/minikanren/goals.sx
Normal file
58
lib/minikanren/goals.sx
Normal file
@@ -0,0 +1,58 @@
|
|||||||
|
;; lib/minikanren/goals.sx — Phase 2 piece B: core goals.
|
||||||
|
;;
|
||||||
|
;; A goal is a function (fn (s) → stream-of-substitutions).
|
||||||
|
;; Goals built here:
|
||||||
|
;; succeed — always returns (unit s)
|
||||||
|
;; fail — always returns mzero
|
||||||
|
;; == — unifies two terms; succeeds with a singleton, else fails
|
||||||
|
;; ==-check — opt-in occurs-checked equality
|
||||||
|
;; conj2 / mk-conj — sequential conjunction of goals
|
||||||
|
;; disj2 / mk-disj — interleaved disjunction of goals (raw — `conde` adds
|
||||||
|
;; the implicit-conj-per-clause sugar in a later commit)
|
||||||
|
|
||||||
|
(define succeed (fn (s) (unit s)))
|
||||||
|
|
||||||
|
(define fail (fn (s) mzero))
|
||||||
|
|
||||||
|
(define
|
||||||
|
==
|
||||||
|
(fn
|
||||||
|
(u v)
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(let ((s2 (mk-unify u v s))) (if (= s2 nil) mzero (unit s2))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
==-check
|
||||||
|
(fn
|
||||||
|
(u v)
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(let ((s2 (mk-unify-check u v s))) (if (= s2 nil) mzero (unit s2))))))
|
||||||
|
|
||||||
|
(define conj2 (fn (g1 g2) (fn (s) (mk-bind (g1 s) g2))))
|
||||||
|
|
||||||
|
(define disj2 (fn (g1 g2) (fn (s) (mk-mplus (g1 s) (g2 s)))))
|
||||||
|
|
||||||
|
;; Fold goals in a list. (mk-conj-list ()) ≡ succeed; (mk-disj-list ()) ≡ fail.
|
||||||
|
(define
|
||||||
|
mk-conj-list
|
||||||
|
(fn
|
||||||
|
(gs)
|
||||||
|
(cond
|
||||||
|
((empty? gs) succeed)
|
||||||
|
((empty? (rest gs)) (first gs))
|
||||||
|
(:else (conj2 (first gs) (mk-conj-list (rest gs)))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-disj-list
|
||||||
|
(fn
|
||||||
|
(gs)
|
||||||
|
(cond
|
||||||
|
((empty? gs) fail)
|
||||||
|
((empty? (rest gs)) (first gs))
|
||||||
|
(:else (disj2 (first gs) (mk-disj-list (rest gs)))))))
|
||||||
|
|
||||||
|
(define mk-conj (fn (&rest gs) (mk-conj-list gs)))
|
||||||
|
|
||||||
|
(define mk-disj (fn (&rest gs) (mk-disj-list gs)))
|
||||||
129
lib/minikanren/intarith.sx
Normal file
129
lib/minikanren/intarith.sx
Normal file
@@ -0,0 +1,129 @@
|
|||||||
|
;; lib/minikanren/intarith.sx — fast integer arithmetic via project.
|
||||||
|
;;
|
||||||
|
;; These are ground-only escapes into host arithmetic. They run at native
|
||||||
|
;; speed (host ints) but require their arguments to walk to actual numbers
|
||||||
|
;; — they are not relational the way `pluso` (Peano) is. Use them when
|
||||||
|
;; the puzzle size makes Peano impractical.
|
||||||
|
;;
|
||||||
|
;; Naming: `-i` suffix marks "integer-only" goals.
|
||||||
|
|
||||||
|
(define
|
||||||
|
pluso-i
|
||||||
|
(fn
|
||||||
|
(a b c)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (number? b)) (== c (+ a b)) fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
minuso-i
|
||||||
|
(fn
|
||||||
|
(a b c)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (number? b)) (== c (- a b)) fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
*o-i
|
||||||
|
(fn
|
||||||
|
(a b c)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (number? b)) (== c (* a b)) fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
lto-i
|
||||||
|
(fn
|
||||||
|
(a b)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (and (number? b) (< a b))) succeed fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
lteo-i
|
||||||
|
(fn
|
||||||
|
(a b)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (and (number? b) (<= a b))) succeed fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
neqo-i
|
||||||
|
(fn
|
||||||
|
(a b)
|
||||||
|
(project
|
||||||
|
(a b)
|
||||||
|
(if (and (number? a) (and (number? b) (not (= a b)))) succeed fail))))
|
||||||
|
|
||||||
|
(define numbero (fn (x) (project (x) (if (number? x) succeed fail))))
|
||||||
|
|
||||||
|
(define stringo (fn (x) (project (x) (if (string? x) succeed fail))))
|
||||||
|
|
||||||
|
(define symbolo (fn (x) (project (x) (if (symbol? x) succeed fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
even-i
|
||||||
|
(fn (n) (project (n) (if (and (number? n) (even? n)) succeed fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
odd-i
|
||||||
|
(fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
sortedo
|
||||||
|
(fn
|
||||||
|
(l)
|
||||||
|
(conde
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a) (== l (list a))))
|
||||||
|
((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mino
|
||||||
|
(fn
|
||||||
|
(l m)
|
||||||
|
(conde
|
||||||
|
((fresh (a) (== l (list a)) (== m a)))
|
||||||
|
((fresh (a d rest-min) (conso a d l) (mino d rest-min) (conde ((lteo-i a rest-min) (== m a)) ((lto-i rest-min a) (== m rest-min))))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
maxo
|
||||||
|
(fn
|
||||||
|
(l m)
|
||||||
|
(conde
|
||||||
|
((fresh (a) (== l (list a)) (== m a)))
|
||||||
|
((fresh (a d rest-max) (conso a d l) (maxo d rest-max) (conde ((lteo-i rest-max a) (== m a)) ((lto-i a rest-max) (== m rest-max))))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
sumo
|
||||||
|
(fn
|
||||||
|
(l total)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== total 0))
|
||||||
|
((fresh (a d rest-sum) (conso a d l) (sumo d rest-sum) (pluso-i a rest-sum total))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
producto
|
||||||
|
(fn
|
||||||
|
(l total)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== total 1))
|
||||||
|
((fresh (a d rest-prod) (conso a d l) (producto d rest-prod) (*o-i a rest-prod total))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
lengtho-i
|
||||||
|
(fn
|
||||||
|
(l n)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== n 0))
|
||||||
|
((fresh (a d n-1) (conso a d l) (lengtho-i d n-1) (pluso-i 1 n-1 n))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
enumerate-from-i
|
||||||
|
(fn
|
||||||
|
(start l result)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo result))
|
||||||
|
((fresh (a d r-rest start-prime) (conso a d l) (conso (list start a) r-rest result) (pluso-i 1 start start-prime) (enumerate-from-i start-prime d r-rest))))))
|
||||||
|
|
||||||
|
(define enumerate-i (fn (l result) (enumerate-from-i 0 l result)))
|
||||||
76
lib/minikanren/matche.sx
Normal file
76
lib/minikanren/matche.sx
Normal file
@@ -0,0 +1,76 @@
|
|||||||
|
;; lib/minikanren/matche.sx — Phase 5 piece D: pattern matching over terms.
|
||||||
|
;;
|
||||||
|
;; (matche TARGET
|
||||||
|
;; (PATTERN1 g1 g2 ...)
|
||||||
|
;; (PATTERN2 g1 ...)
|
||||||
|
;; ...)
|
||||||
|
;;
|
||||||
|
;; Pattern grammar:
|
||||||
|
;; _ wildcard — fresh anonymous var
|
||||||
|
;; x plain symbol — fresh var, bind by name
|
||||||
|
;; ATOM literal (number, string, boolean) — must equal
|
||||||
|
;; :keyword keyword literal — emitted bare (keywords self-evaluate
|
||||||
|
;; to their string name in SX, so quoting them changes
|
||||||
|
;; their type from string to keyword)
|
||||||
|
;; () empty list — must equal
|
||||||
|
;; (p1 p2 ... pn) list pattern — recurse on each element
|
||||||
|
;;
|
||||||
|
;; The macro expands to a `conde` whose clauses are
|
||||||
|
;; `((fresh (vars-in-pat) (== target pat-expr) body...))`.
|
||||||
|
;;
|
||||||
|
;; Repeated symbol names within a pattern produce the same fresh var, so
|
||||||
|
;; they unify by `==`. Fixed-length list patterns only — head/tail
|
||||||
|
;; destructuring uses `(fresh (a d) (conso a d target) body)` directly.
|
||||||
|
;;
|
||||||
|
;; Note: the macro builds the expansion via `cons` / `list` rather than a
|
||||||
|
;; quasiquote — quasiquote does not recurse into nested lambda bodies in
|
||||||
|
;; SX, so `\`(matche-clause (quote ,target) cl)` left literal
|
||||||
|
;; `(unquote target)` in the output.
|
||||||
|
|
||||||
|
(define matche-symbol-var? (fn (s) (symbol? s)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
matche-collect-vars-acc
|
||||||
|
(fn
|
||||||
|
(pat acc)
|
||||||
|
(cond
|
||||||
|
((matche-symbol-var? pat)
|
||||||
|
(if (some (fn (s) (= s pat)) acc) acc (append acc (list pat))))
|
||||||
|
((and (list? pat) (not (empty? pat)))
|
||||||
|
(reduce (fn (a p) (matche-collect-vars-acc p a)) acc pat))
|
||||||
|
(:else acc))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
matche-collect-vars
|
||||||
|
(fn (pat) (matche-collect-vars-acc pat (list))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
matche-pattern->expr
|
||||||
|
(fn
|
||||||
|
(pat)
|
||||||
|
(cond
|
||||||
|
((matche-symbol-var? pat) pat)
|
||||||
|
((and (list? pat) (empty? pat)) (list (quote list)))
|
||||||
|
((list? pat) (cons (quote list) (map matche-pattern->expr pat)))
|
||||||
|
((keyword? pat) pat)
|
||||||
|
(:else (list (quote quote) pat)))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
matche-clause
|
||||||
|
(fn
|
||||||
|
(target cl)
|
||||||
|
(let
|
||||||
|
((pat (first cl)) (body (rest cl)))
|
||||||
|
(let
|
||||||
|
((vars (matche-collect-vars pat)))
|
||||||
|
(let
|
||||||
|
((pat-expr (matche-pattern->expr pat)))
|
||||||
|
(list
|
||||||
|
(cons
|
||||||
|
(quote fresh)
|
||||||
|
(cons vars (cons (list (quote ==) target pat-expr) body)))))))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
matche
|
||||||
|
(target &rest clauses)
|
||||||
|
(cons (quote conde) (map (fn (cl) (matche-clause target cl)) clauses)))
|
||||||
24
lib/minikanren/nafc.sx
Normal file
24
lib/minikanren/nafc.sx
Normal file
@@ -0,0 +1,24 @@
|
|||||||
|
;; lib/minikanren/nafc.sx — Phase 5 piece C: negation as finite failure.
|
||||||
|
;;
|
||||||
|
;; (nafc g)
|
||||||
|
;; succeeds (yields the input substitution) if g has zero answers
|
||||||
|
;; against that substitution; fails (mzero) if g has at least one.
|
||||||
|
;;
|
||||||
|
;; Caveat: `nafc` is unsound under the open-world assumption. It only
|
||||||
|
;; makes sense for goals over fully-ground terms, or with the explicit
|
||||||
|
;; understanding that adding more facts could flip the answer. Use
|
||||||
|
;; `(project (...) ...)` to ensure the relevant vars are ground first.
|
||||||
|
;;
|
||||||
|
;; Caveat 2: stream-take forces g for at least one answer; if g is
|
||||||
|
;; infinitely-ground (say, a divergent search over an unbound list),
|
||||||
|
;; nafc itself will diverge. Standard miniKanren limitation.
|
||||||
|
|
||||||
|
(define
|
||||||
|
nafc
|
||||||
|
(fn
|
||||||
|
(g)
|
||||||
|
(fn
|
||||||
|
(s)
|
||||||
|
(let
|
||||||
|
((peek (stream-take 1 (g s))))
|
||||||
|
(if (empty? peek) (unit s) mzero)))))
|
||||||
51
lib/minikanren/peano.sx
Normal file
51
lib/minikanren/peano.sx
Normal file
@@ -0,0 +1,51 @@
|
|||||||
|
;; lib/minikanren/peano.sx — Peano-encoded natural-number relations.
|
||||||
|
;;
|
||||||
|
;; Same encoding as `lengtho`: zero is the keyword `:z`; successors are
|
||||||
|
;; `(:s n)`. So 3 = `(:s (:s (:s :z)))`. `(:z)` and `(:s ...)` are normal
|
||||||
|
;; SX values that unify positionally — no special primitives needed.
|
||||||
|
;;
|
||||||
|
;; Peano arithmetic is the canonical miniKanren way to test addition /
|
||||||
|
;; multiplication / less-than relationally without an FD constraint store.
|
||||||
|
;; (CLP(FD) integers come in Phase 6.)
|
||||||
|
|
||||||
|
(define zeroo (fn (n) (== n :z)))
|
||||||
|
|
||||||
|
(define succ-of (fn (n m) (== m (list :s n))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
pluso
|
||||||
|
(fn
|
||||||
|
(a b c)
|
||||||
|
(conde
|
||||||
|
((== a :z) (== b c))
|
||||||
|
((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (pluso a-1 b c-1))))))
|
||||||
|
|
||||||
|
(define minuso (fn (a b c) (pluso b c a)))
|
||||||
|
|
||||||
|
(define lteo (fn (a b) (fresh (k) (pluso a k b))))
|
||||||
|
|
||||||
|
(define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
eveno
|
||||||
|
(fn
|
||||||
|
(n)
|
||||||
|
(conde
|
||||||
|
((== n :z))
|
||||||
|
((fresh (m) (== n (list :s (list :s m))) (eveno m))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
oddo
|
||||||
|
(fn
|
||||||
|
(n)
|
||||||
|
(conde
|
||||||
|
((== n (list :s :z)))
|
||||||
|
((fresh (m) (== n (list :s (list :s m))) (oddo m))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
*o
|
||||||
|
(fn
|
||||||
|
(a b c)
|
||||||
|
(conde
|
||||||
|
((== a :z) (== c :z))
|
||||||
|
((fresh (a-1 ab-1) (== a (list :s a-1)) (*o a-1 b ab-1) (pluso b ab-1 c))))))
|
||||||
25
lib/minikanren/project.sx
Normal file
25
lib/minikanren/project.sx
Normal file
@@ -0,0 +1,25 @@
|
|||||||
|
;; lib/minikanren/project.sx — Phase 5 piece B: `project`.
|
||||||
|
;;
|
||||||
|
;; (project (x y) g1 g2 ...)
|
||||||
|
;; — rebinds each named var to (mk-walk* var s) within the body's
|
||||||
|
;; lexical scope, then runs the conjunction of the body goals on
|
||||||
|
;; the same substitution. Use to escape into regular SX (arithmetic,
|
||||||
|
;; string ops, host predicates) when you need a ground value.
|
||||||
|
;;
|
||||||
|
;; If any of the projected vars is still unbound at this point, the body
|
||||||
|
;; sees the raw `(:var NAME)` term — that is intentional and lets you
|
||||||
|
;; mix project with `(== ground? var)` patterns or with conda guards.
|
||||||
|
;;
|
||||||
|
;; Hygiene: substitution parameter is gensym'd so it doesn't capture user
|
||||||
|
;; vars (`s` is a popular relation parameter name).
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
project
|
||||||
|
(vars &rest goals)
|
||||||
|
(let
|
||||||
|
((s-sym (gensym "proj-s-")))
|
||||||
|
(quasiquote
|
||||||
|
(fn
|
||||||
|
((unquote s-sym))
|
||||||
|
((let (unquote (map (fn (v) (list v (list (quote mk-walk*) v s-sym))) vars)) (mk-conj (splice-unquote goals)))
|
||||||
|
(unquote s-sym))))))
|
||||||
67
lib/minikanren/queens.sx
Normal file
67
lib/minikanren/queens.sx
Normal file
@@ -0,0 +1,67 @@
|
|||||||
|
;; lib/minikanren/queens.sx — N-queens via ino + all-distincto + project.
|
||||||
|
;;
|
||||||
|
;; Encoding: q = (c1 c2 ... cn) where ci is the column of the queen in
|
||||||
|
;; row i. Each ci ∈ {1..n}; all distinct (no two queens share a column);
|
||||||
|
;; no two queens on the same diagonal (|ci - cj| ≠ |i - j| for i ≠ j).
|
||||||
|
;;
|
||||||
|
;; The diagonal check uses `project` to escape into host arithmetic
|
||||||
|
;; once both column values are ground.
|
||||||
|
|
||||||
|
(define
|
||||||
|
safe-diag
|
||||||
|
(fn
|
||||||
|
(a b dist)
|
||||||
|
(project (a b) (if (= (abs (- a b)) dist) fail succeed))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
safe-cell-vs-rest
|
||||||
|
(fn
|
||||||
|
(c c-row others next-row)
|
||||||
|
(cond
|
||||||
|
((empty? others) succeed)
|
||||||
|
(:else
|
||||||
|
(mk-conj
|
||||||
|
(safe-diag c (first others) (- next-row c-row))
|
||||||
|
(safe-cell-vs-rest c c-row (rest others) (+ next-row 1)))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
all-cells-safe
|
||||||
|
(fn
|
||||||
|
(cols start-row)
|
||||||
|
(cond
|
||||||
|
((empty? cols) succeed)
|
||||||
|
(:else
|
||||||
|
(mk-conj
|
||||||
|
(safe-cell-vs-rest
|
||||||
|
(first cols)
|
||||||
|
start-row
|
||||||
|
(rest cols)
|
||||||
|
(+ start-row 1))
|
||||||
|
(all-cells-safe (rest cols) (+ start-row 1)))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
range-1-to-n
|
||||||
|
(fn
|
||||||
|
(n)
|
||||||
|
(cond
|
||||||
|
((= n 0) (list))
|
||||||
|
(:else (append (range-1-to-n (- n 1)) (list n))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
ino-each
|
||||||
|
(fn
|
||||||
|
(cols dom)
|
||||||
|
(cond
|
||||||
|
((empty? cols) succeed)
|
||||||
|
(:else (mk-conj (ino (first cols) dom) (ino-each (rest cols) dom))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
queens-cols
|
||||||
|
(fn
|
||||||
|
(cols n)
|
||||||
|
(let
|
||||||
|
((dom (range-1-to-n n)))
|
||||||
|
(mk-conj
|
||||||
|
(ino-each cols dom)
|
||||||
|
(all-distincto cols)
|
||||||
|
(all-cells-safe cols 1)))))
|
||||||
305
lib/minikanren/relations.sx
Normal file
305
lib/minikanren/relations.sx
Normal file
@@ -0,0 +1,305 @@
|
|||||||
|
;; lib/minikanren/relations.sx — Phase 4 standard relations.
|
||||||
|
;;
|
||||||
|
;; Programs use native SX lists as data. Relations decompose lists via the
|
||||||
|
;; tagged cons-cell shape `(:cons h t)` because SX has no improper pairs;
|
||||||
|
;; the unifier treats `(:cons h t)` and the native list `(h . t)` as
|
||||||
|
;; equivalent, and `mk-walk*` flattens cons cells back to flat lists for
|
||||||
|
;; reification.
|
||||||
|
|
||||||
|
;; --- pair / list shape relations ---
|
||||||
|
|
||||||
|
(define nullo (fn (l) (== l (list))))
|
||||||
|
|
||||||
|
(define pairo (fn (p) (fresh (a d) (== p (mk-cons a d)))))
|
||||||
|
|
||||||
|
(define caro (fn (p a) (fresh (d) (== p (mk-cons a d)))))
|
||||||
|
|
||||||
|
(define cdro (fn (p d) (fresh (a) (== p (mk-cons a d)))))
|
||||||
|
|
||||||
|
(define conso (fn (a d p) (== p (mk-cons a d))))
|
||||||
|
|
||||||
|
(define firsto caro)
|
||||||
|
(define resto cdro)
|
||||||
|
|
||||||
|
(define
|
||||||
|
listo
|
||||||
|
(fn (l) (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo d))))))
|
||||||
|
|
||||||
|
;; --- appendo: the canary ---
|
||||||
|
;;
|
||||||
|
;; (appendo l s ls) — `ls` is the concatenation of `l` and `s`.
|
||||||
|
;; Runs forwards (l, s known → ls), backwards (ls known → all (l, s) pairs),
|
||||||
|
;; and bidirectionally (mix of bound + unbound).
|
||||||
|
|
||||||
|
(define
|
||||||
|
appendo
|
||||||
|
(fn
|
||||||
|
(l s ls)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== s ls))
|
||||||
|
((fresh (a d res) (conso a d l) (conso a res ls) (appendo d s res))))))
|
||||||
|
|
||||||
|
;; --- membero ---
|
||||||
|
;; (membero x l) — x appears (at least once) in l.
|
||||||
|
|
||||||
|
(define
|
||||||
|
appendo3
|
||||||
|
(fn
|
||||||
|
(l1 l2 l3 result)
|
||||||
|
(fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
partitiono
|
||||||
|
(fn
|
||||||
|
(pred l yes no)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo yes) (nullo no))
|
||||||
|
((fresh (a d y-rest n-rest) (conso a d l) (conde ((pred a) (conso a y-rest yes) (== no n-rest) (partitiono pred d y-rest n-rest)) ((nafc (pred a)) (== yes y-rest) (conso a n-rest no) (partitiono pred d y-rest n-rest))))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
membero
|
||||||
|
(fn
|
||||||
|
(x l)
|
||||||
|
(conde
|
||||||
|
((fresh (d) (conso x d l)))
|
||||||
|
((fresh (a d) (conso a d l) (membero x d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
not-membero
|
||||||
|
(fn
|
||||||
|
(x l)
|
||||||
|
(conde
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
subseto
|
||||||
|
(fn
|
||||||
|
(l1 l2)
|
||||||
|
(conde
|
||||||
|
((nullo l1))
|
||||||
|
((fresh (a d) (conso a d l1) (membero a l2) (subseto d l2))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
reverseo
|
||||||
|
(fn
|
||||||
|
(l r)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo r))
|
||||||
|
((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
|
||||||
|
|
||||||
|
|
||||||
|
(define
|
||||||
|
rev-acco
|
||||||
|
(fn
|
||||||
|
(l acc result)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== result acc))
|
||||||
|
((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result))))))
|
||||||
|
|
||||||
|
(define rev-2o (fn (l result) (rev-acco l (list) result)))
|
||||||
|
|
||||||
|
(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
|
||||||
|
|
||||||
|
(define prefixo (fn (p l) (fresh (rest) (appendo p rest l))))
|
||||||
|
|
||||||
|
(define suffixo (fn (s l) (fresh (front) (appendo front s l))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
subo
|
||||||
|
(fn
|
||||||
|
(s l)
|
||||||
|
(fresh
|
||||||
|
(front-and-s back front)
|
||||||
|
(appendo front-and-s back l)
|
||||||
|
(appendo front s front-and-s))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
selecto
|
||||||
|
(fn
|
||||||
|
(x rest l)
|
||||||
|
(conde
|
||||||
|
((conso x rest l))
|
||||||
|
((fresh (a d r) (conso a d l) (conso a r rest) (selecto x r d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
lengtho
|
||||||
|
(fn
|
||||||
|
(l n)
|
||||||
|
(conde
|
||||||
|
((nullo l) (== n :z))
|
||||||
|
((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
inserto
|
||||||
|
(fn
|
||||||
|
(a l p)
|
||||||
|
(conde
|
||||||
|
((conso a l p))
|
||||||
|
((fresh (h t pt) (conso h t l) (conso h pt p) (inserto a t pt))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
permuteo
|
||||||
|
(fn
|
||||||
|
(l p)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo p))
|
||||||
|
((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
flatteno
|
||||||
|
(fn
|
||||||
|
(tree flat)
|
||||||
|
(conde
|
||||||
|
((nullo tree) (nullo flat))
|
||||||
|
((pairo tree)
|
||||||
|
(fresh
|
||||||
|
(h t hf tf)
|
||||||
|
(conso h t tree)
|
||||||
|
(flatteno h hf)
|
||||||
|
(flatteno t tf)
|
||||||
|
(appendo hf tf flat)))
|
||||||
|
((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
rembero
|
||||||
|
(fn
|
||||||
|
(x l out)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo out))
|
||||||
|
((fresh (a d) (conso a d l) (== a x) (== out d)))
|
||||||
|
((fresh (a d res) (conso a d l) (nafc (== a x)) (conso a res out) (rembero x d res))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
removeo-allo
|
||||||
|
(fn
|
||||||
|
(x l result)
|
||||||
|
(conde
|
||||||
|
((nullo l) (nullo result))
|
||||||
|
((fresh (a d) (conso a d l) (== a x) (removeo-allo x d result)))
|
||||||
|
((fresh (a d r-rest) (conso a d l) (nafc (== a x)) (conso a r-rest result) (removeo-allo x d r-rest))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
assoco
|
||||||
|
(fn
|
||||||
|
(key pairs val)
|
||||||
|
(fresh
|
||||||
|
(rest)
|
||||||
|
(conde
|
||||||
|
((conso (list key val) rest pairs))
|
||||||
|
((fresh (other) (conso other rest pairs) (assoco key rest val)))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
nth-o
|
||||||
|
(fn
|
||||||
|
(n l elem)
|
||||||
|
(conde
|
||||||
|
((== n :z) (fresh (d) (conso elem d l)))
|
||||||
|
((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (nth-o n-1 d elem))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
samelengtho
|
||||||
|
(fn
|
||||||
|
(l1 l2)
|
||||||
|
(conde
|
||||||
|
((nullo l1) (nullo l2))
|
||||||
|
((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (samelengtho d d-prime))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mapo
|
||||||
|
(fn
|
||||||
|
(rel l1 l2)
|
||||||
|
(conde
|
||||||
|
((nullo l1) (nullo l2))
|
||||||
|
((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (rel a a-prime) (mapo rel d d-prime))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
iterate-no
|
||||||
|
(fn
|
||||||
|
(rel n x result)
|
||||||
|
(conde
|
||||||
|
((== n :z) (== result x))
|
||||||
|
((fresh (n-1 mid) (== n (list :s n-1)) (rel x mid) (iterate-no rel n-1 mid result))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
pairlisto
|
||||||
|
(fn
|
||||||
|
(l1 l2 pairs)
|
||||||
|
(conde
|
||||||
|
((nullo l1) (nullo l2) (nullo pairs))
|
||||||
|
((fresh (a1 d1 a2 d2 d-pairs) (conso a1 d1 l1) (conso a2 d2 l2) (conso (list a1 a2) d-pairs pairs) (pairlisto d1 d2 d-pairs))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
swap-firsto
|
||||||
|
(fn
|
||||||
|
(l result)
|
||||||
|
(fresh
|
||||||
|
(a b rest mid-l mid-r)
|
||||||
|
(conso a mid-l l)
|
||||||
|
(conso b rest mid-l)
|
||||||
|
(conso b mid-r result)
|
||||||
|
(conso a rest mid-r))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
everyo
|
||||||
|
(fn
|
||||||
|
(rel l)
|
||||||
|
(conde
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (rel a) (everyo rel d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
someo
|
||||||
|
(fn
|
||||||
|
(rel l)
|
||||||
|
(conde
|
||||||
|
((fresh (a d) (conso a d l) (rel a)))
|
||||||
|
((fresh (a d) (conso a d l) (someo rel d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
lasto
|
||||||
|
(fn
|
||||||
|
(l x)
|
||||||
|
(conde
|
||||||
|
((conso x (list) l))
|
||||||
|
((fresh (a d) (conso a d l) (lasto d x))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
init-o
|
||||||
|
(fn
|
||||||
|
(l init)
|
||||||
|
(conde
|
||||||
|
((fresh (x) (conso x (list) l) (== init (list))))
|
||||||
|
((fresh (a d d-init) (conso a d l) (conso a d-init init) (init-o d d-init))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
tako
|
||||||
|
(fn
|
||||||
|
(n l prefix)
|
||||||
|
(conde
|
||||||
|
((== n :z) (== prefix (list)))
|
||||||
|
((fresh (n-1 a d p-rest) (== n (list :s n-1)) (conso a d l) (conso a p-rest prefix) (tako n-1 d p-rest))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
dropo
|
||||||
|
(fn
|
||||||
|
(n l suffix)
|
||||||
|
(conde
|
||||||
|
((== n :z) (== suffix l))
|
||||||
|
((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (dropo n-1 d suffix))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
repeato
|
||||||
|
(fn
|
||||||
|
(x n result)
|
||||||
|
(conde
|
||||||
|
((== n :z) (== result (list)))
|
||||||
|
((fresh (n-1 r-rest) (== n (list :s n-1)) (conso x r-rest result) (repeato x n-1 r-rest))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
concato
|
||||||
|
(fn
|
||||||
|
(lists result)
|
||||||
|
(conde
|
||||||
|
((nullo lists) (nullo result))
|
||||||
|
((fresh (h t r-rest) (conso h t lists) (appendo h r-rest result) (concato t r-rest))))))
|
||||||
56
lib/minikanren/run.sx
Normal file
56
lib/minikanren/run.sx
Normal file
@@ -0,0 +1,56 @@
|
|||||||
|
;; lib/minikanren/run.sx — Phase 3: drive a goal + reify the query var.
|
||||||
|
;;
|
||||||
|
;; reify-name N — make the canonical "_.N" reified symbol.
|
||||||
|
;; reify-s term rs — walk term in rs, add a mapping from each fresh
|
||||||
|
;; unbound var to its _.N name (left-to-right order).
|
||||||
|
;; reify q s — walk* q in s, build reify-s, walk* again to
|
||||||
|
;; substitute reified names in.
|
||||||
|
;; run-n n q-name g... — defmacro: bind q-name to a fresh var, conj goals,
|
||||||
|
;; take ≤ n answers from the stream, reify each
|
||||||
|
;; through q-name. n = -1 takes all (used by run*).
|
||||||
|
;; run* — defmacro: (run* q g...) ≡ (run-n -1 q g...)
|
||||||
|
;; run — defmacro: (run n q g...) ≡ (run-n n q g...)
|
||||||
|
;; The two-segment form is the standard TRS API.
|
||||||
|
|
||||||
|
(define reify-name (fn (n) (make-symbol (str "_." n))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
reify-s
|
||||||
|
(fn
|
||||||
|
(term rs)
|
||||||
|
(let
|
||||||
|
((w (mk-walk term rs)))
|
||||||
|
(cond
|
||||||
|
((is-var? w) (extend (var-name w) (reify-name (len rs)) rs))
|
||||||
|
((mk-list-pair? w) (reduce (fn (acc a) (reify-s a acc)) rs w))
|
||||||
|
(:else rs)))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
reify
|
||||||
|
(fn
|
||||||
|
(term s)
|
||||||
|
(let
|
||||||
|
((w (mk-walk* term s)))
|
||||||
|
(let ((rs (reify-s w (empty-subst)))) (mk-walk* w rs)))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
run-n
|
||||||
|
(n q-name &rest goals)
|
||||||
|
(quasiquote
|
||||||
|
(let
|
||||||
|
(((unquote q-name) (make-var)))
|
||||||
|
(map
|
||||||
|
(fn (s) (reify (unquote q-name) s))
|
||||||
|
(stream-take
|
||||||
|
(unquote n)
|
||||||
|
((mk-conj (splice-unquote goals)) empty-s))))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
run*
|
||||||
|
(q-name &rest goals)
|
||||||
|
(quasiquote (run-n -1 (unquote q-name) (splice-unquote goals))))
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
run
|
||||||
|
(n q-name &rest goals)
|
||||||
|
(quasiquote (run-n (unquote n) (unquote q-name) (splice-unquote goals))))
|
||||||
66
lib/minikanren/stream.sx
Normal file
66
lib/minikanren/stream.sx
Normal file
@@ -0,0 +1,66 @@
|
|||||||
|
;; lib/minikanren/stream.sx — Phase 2 piece A: lazy streams of substitutions.
|
||||||
|
;;
|
||||||
|
;; SX has no improper pairs (cons requires a list cdr), so we use a
|
||||||
|
;; tagged stream-cell shape for mature stream elements:
|
||||||
|
;;
|
||||||
|
;; stream ::= mzero empty (the SX empty list)
|
||||||
|
;; | (:s HEAD TAIL) mature cell, TAIL is a stream
|
||||||
|
;; | thunk (fn () ...) → stream when forced
|
||||||
|
;;
|
||||||
|
;; HEAD is a substitution dict. TAIL is again a stream (possibly a thunk),
|
||||||
|
;; which is what gives us laziness — mk-mplus can return a mature head with
|
||||||
|
;; a thunk in the tail, deferring the rest of the search.
|
||||||
|
|
||||||
|
(define mzero (list))
|
||||||
|
|
||||||
|
(define s-cons (fn (h t) (list :s h t)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
s-cons?
|
||||||
|
(fn (s) (and (list? s) (not (empty? s)) (= (first s) :s))))
|
||||||
|
|
||||||
|
(define s-car (fn (s) (nth s 1)))
|
||||||
|
(define s-cdr (fn (s) (nth s 2)))
|
||||||
|
|
||||||
|
(define unit (fn (s) (s-cons s mzero)))
|
||||||
|
|
||||||
|
(define stream-pause? (fn (s) (and (not (list? s)) (callable? s))))
|
||||||
|
|
||||||
|
;; mk-mplus — interleave two streams. If s1 is paused we suspend and
|
||||||
|
;; swap (Reasoned Schemer "interleave"); otherwise mature-cons head with
|
||||||
|
;; mk-mplus of the rest.
|
||||||
|
(define
|
||||||
|
mk-mplus
|
||||||
|
(fn
|
||||||
|
(s1 s2)
|
||||||
|
(cond
|
||||||
|
((empty? s1) s2)
|
||||||
|
((stream-pause? s1) (fn () (mk-mplus s2 (s1))))
|
||||||
|
(:else (s-cons (s-car s1) (mk-mplus (s-cdr s1) s2))))))
|
||||||
|
|
||||||
|
;; mk-bind — apply goal g to every substitution in stream s, mk-mplus-ing.
|
||||||
|
(define
|
||||||
|
mk-bind
|
||||||
|
(fn
|
||||||
|
(s g)
|
||||||
|
(cond
|
||||||
|
((empty? s) mzero)
|
||||||
|
((stream-pause? s) (fn () (mk-bind (s) g)))
|
||||||
|
(:else (mk-mplus (g (s-car s)) (mk-bind (s-cdr s) g))))))
|
||||||
|
|
||||||
|
;; stream-take — force up to n results out of a (possibly lazy) stream
|
||||||
|
;; into a flat SX list of substitutions. n = -1 means take all.
|
||||||
|
(define
|
||||||
|
stream-take
|
||||||
|
(fn
|
||||||
|
(n s)
|
||||||
|
(cond
|
||||||
|
((= n 0) (list))
|
||||||
|
((empty? s) (list))
|
||||||
|
((stream-pause? s) (stream-take n (s)))
|
||||||
|
(:else
|
||||||
|
(cons
|
||||||
|
(s-car s)
|
||||||
|
(stream-take
|
||||||
|
(if (= n -1) -1 (- n 1))
|
||||||
|
(s-cdr s)))))))
|
||||||
49
lib/minikanren/tests/appendo3.sx
Normal file
49
lib/minikanren/tests/appendo3.sx
Normal file
@@ -0,0 +1,49 @@
|
|||||||
|
;; lib/minikanren/tests/appendo3.sx — 3-list append.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-forward"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
(list 3 4)
|
||||||
|
(list 5 6)
|
||||||
|
q))
|
||||||
|
(list
|
||||||
|
(list 1 2 3 4 5 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-everything"
|
||||||
|
(run* q (appendo3 (list) (list) (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-recover-middle"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
q
|
||||||
|
(list 5 6)
|
||||||
|
(list 1 2 3 4 5 6)))
|
||||||
|
(list (list 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-middle"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
(list)
|
||||||
|
(list 3 4)
|
||||||
|
q))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-first-and-last"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3 (list) (list 1 2 3) (list) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
54
lib/minikanren/tests/btree-walko.sx
Normal file
54
lib/minikanren/tests/btree-walko.sx
Normal file
@@ -0,0 +1,54 @@
|
|||||||
|
;; lib/minikanren/tests/btree-walko.sx — walk a leaves-of-binary-tree relation
|
||||||
|
;; using matche dispatch on (:leaf v) and (:node left right) patterns.
|
||||||
|
|
||||||
|
(define
|
||||||
|
btree-walko
|
||||||
|
(fn
|
||||||
|
(tree v)
|
||||||
|
(matche
|
||||||
|
tree
|
||||||
|
((:leaf x) (== v x))
|
||||||
|
((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))))
|
||||||
|
|
||||||
|
;; A small test tree: ((1 2) (3 (4 5))).
|
||||||
|
(define
|
||||||
|
test-btree
|
||||||
|
(list
|
||||||
|
:node (list :node (list :leaf 1) (list :leaf 2))
|
||||||
|
(list
|
||||||
|
:node (list :leaf 3)
|
||||||
|
(list :node (list :leaf 4) (list :leaf 5)))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"btree-walko-enumerates-all-leaves"
|
||||||
|
(let
|
||||||
|
((leaves (run* q (btree-walko test-btree q))))
|
||||||
|
(and
|
||||||
|
(= (len leaves) 5)
|
||||||
|
(and
|
||||||
|
(some (fn (l) (= l 1)) leaves)
|
||||||
|
(and
|
||||||
|
(some (fn (l) (= l 2)) leaves)
|
||||||
|
(and
|
||||||
|
(some (fn (l) (= l 3)) leaves)
|
||||||
|
(and
|
||||||
|
(some (fn (l) (= l 4)) leaves)
|
||||||
|
(some (fn (l) (= l 5)) leaves)))))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"btree-walko-find-3-membership"
|
||||||
|
(run 1 q (btree-walko test-btree 3))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"btree-walko-find-99-not-present"
|
||||||
|
(run* q (btree-walko test-btree 99))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"btree-walko-leaf-only"
|
||||||
|
(run* q (btree-walko (list :leaf 42) q))
|
||||||
|
(list 42))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
87
lib/minikanren/tests/classics.sx
Normal file
87
lib/minikanren/tests/classics.sx
Normal file
@@ -0,0 +1,87 @@
|
|||||||
|
;; lib/minikanren/tests/classics.sx — small classic-style puzzles that
|
||||||
|
;; exercise the full system end to end (relations + conde + matche +
|
||||||
|
;; fresh + run*). Each test is a self-contained miniKanren program.
|
||||||
|
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
;; Pet puzzle (3 friends, 3 pets, 1-each).
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"classics-pet-puzzle"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(a b c)
|
||||||
|
(== q (list a b c))
|
||||||
|
(permuteo (list :dog :cat :fish) (list a b c))
|
||||||
|
(== b :fish)
|
||||||
|
(conde ((== a :cat)) ((== a :fish)))))
|
||||||
|
(list (list :cat :fish :dog)))
|
||||||
|
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
;; Family-relations puzzle (uses membero on a fact list).
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
|
||||||
|
(define
|
||||||
|
parent-facts
|
||||||
|
(list
|
||||||
|
(list "alice" "bob")
|
||||||
|
(list "alice" "carol")
|
||||||
|
(list "bob" "dave")
|
||||||
|
(list "carol" "eve")
|
||||||
|
(list "dave" "frank")))
|
||||||
|
|
||||||
|
(define parento (fn (x y) (membero (list x y) parent-facts)))
|
||||||
|
|
||||||
|
(define grandparento (fn (x z) (fresh (y) (parento x y) (parento y z))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"classics-grandparents-of-frank"
|
||||||
|
(run* q (grandparento q "frank"))
|
||||||
|
(list "bob"))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"classics-grandchildren-of-alice"
|
||||||
|
(run* q (grandparento "alice" q))
|
||||||
|
(list "dave" "eve"))
|
||||||
|
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
;; Symbolic differentiation, matche-driven.
|
||||||
|
;; Variable :x: d/dx x = 1
|
||||||
|
;; Sum (:+ a b): d/dx (a+b) = (da + db)
|
||||||
|
;; Product (:* a b): d/dx (a*b) = (da*b + a*db)
|
||||||
|
;; -----------------------------------------------------------------------
|
||||||
|
|
||||||
|
(define
|
||||||
|
diffo
|
||||||
|
(fn
|
||||||
|
(expr var d)
|
||||||
|
(matche
|
||||||
|
expr
|
||||||
|
(:x (== d 1))
|
||||||
|
((:+ a b)
|
||||||
|
(fresh
|
||||||
|
(da db)
|
||||||
|
(== d (list :+ da db))
|
||||||
|
(diffo a var da)
|
||||||
|
(diffo b var db)))
|
||||||
|
((:* a b)
|
||||||
|
(fresh
|
||||||
|
(da db)
|
||||||
|
(== d (list :+ (list :* da b) (list :* a db)))
|
||||||
|
(diffo a var da)
|
||||||
|
(diffo b var db))))))
|
||||||
|
|
||||||
|
(mk-test "classics-diff-of-x" (run* q (diffo :x :x q)) (list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"classics-diff-of-x-plus-x"
|
||||||
|
(run* q (diffo (list :+ :x :x) :x q))
|
||||||
|
(list (list :+ 1 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"classics-diff-of-x-times-x"
|
||||||
|
(run* q (diffo (list :* :x :x) :x q))
|
||||||
|
(list (list :+ (list :* 1 :x) (list :* :x 1))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
75
lib/minikanren/tests/conda.sx
Normal file
75
lib/minikanren/tests/conda.sx
Normal file
@@ -0,0 +1,75 @@
|
|||||||
|
;; lib/minikanren/tests/conda.sx — Phase 5 piece A tests for `conda`.
|
||||||
|
|
||||||
|
;; --- conda commits to first non-failing head, keeps ALL its answers ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-first-clause-keeps-all"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conda
|
||||||
|
((mk-disj (== q 1) (== q 2)))
|
||||||
|
((== q 100))))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-skips-failing-head"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conda
|
||||||
|
((== 1 2))
|
||||||
|
((mk-disj (== q 10) (== q 20)))))
|
||||||
|
(list 10 20))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-all-fail"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conda ((== 1 2)) ((== 3 4))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test "conda-no-clauses" (run* q (conda)) (list))
|
||||||
|
|
||||||
|
;; --- conda DIFFERS from condu: conda keeps all head answers ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-vs-condu-divergence"
|
||||||
|
(list
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conda
|
||||||
|
((mk-disj (== q 1) (== q 2)))
|
||||||
|
((== q 100))))
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(condu
|
||||||
|
((mk-disj (== q 1) (== q 2)))
|
||||||
|
((== q 100)))))
|
||||||
|
(list (list 1 2) (list 1)))
|
||||||
|
|
||||||
|
;; --- conda head's rest-goals run on every head answer ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-rest-goals-run-on-all-answers"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x r)
|
||||||
|
(conda
|
||||||
|
((mk-disj (== x 1) (== x 2))
|
||||||
|
(== r (list :tag x))))
|
||||||
|
(== q r)))
|
||||||
|
(list (list :tag 1) (list :tag 2)))
|
||||||
|
|
||||||
|
;; --- if rest-goals fail on a head answer, that head answer is filtered;
|
||||||
|
;; the clause does not fall through to next clauses (per soft-cut). ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conda-rest-fails-no-fallthrough"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conda
|
||||||
|
((mk-disj (== q 1) (== q 2)) (== q 99))
|
||||||
|
((== q 200))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
89
lib/minikanren/tests/conde.sx
Normal file
89
lib/minikanren/tests/conde.sx
Normal file
@@ -0,0 +1,89 @@
|
|||||||
|
;; lib/minikanren/tests/conde.sx — Phase 2 piece C tests for `conde`.
|
||||||
|
;;
|
||||||
|
;; Note on ordering: conde clauses are wrapped in Zzz (inverse-eta delay),
|
||||||
|
;; so applying the conde goal to a substitution returns thunks. mk-mplus
|
||||||
|
;; suspends-and-swaps when its left operand is paused, giving fair
|
||||||
|
;; interleaving — this is exactly what makes recursive relations work,
|
||||||
|
;; but it does mean conde answers can interleave rather than appear in
|
||||||
|
;; strict left-to-right clause order.
|
||||||
|
|
||||||
|
;; --- single-clause conde ≡ conj of clause body ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-one-clause"
|
||||||
|
(let ((q (mk-var "q"))) (run* q (conde ((== q 7)))))
|
||||||
|
(list 7))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-one-clause-multi-goals"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(run* q (conde ((fresh (x) (== x 5) (== q (list x x)))))))
|
||||||
|
(list (list 5 5)))
|
||||||
|
|
||||||
|
;; --- multi-clause: produces one row per clause (interleaved) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-three-clauses-as-set"
|
||||||
|
(let
|
||||||
|
((qs (run* q (conde ((== q 1)) ((== q 2)) ((== q 3))))))
|
||||||
|
(and
|
||||||
|
(= (len qs) 3)
|
||||||
|
(and
|
||||||
|
(some (fn (x) (= x 1)) qs)
|
||||||
|
(and
|
||||||
|
(some (fn (x) (= x 2)) qs)
|
||||||
|
(some (fn (x) (= x 3)) qs)))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-mixed-success-failure-as-set"
|
||||||
|
(let
|
||||||
|
((qs (run* q (conde ((== q "a")) ((== 1 2)) ((== q "b"))))))
|
||||||
|
(and
|
||||||
|
(= (len qs) 2)
|
||||||
|
(and (some (fn (x) (= x "a")) qs) (some (fn (x) (= x "b")) qs))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- conde with conjuncts inside clauses ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-clause-conj-as-set"
|
||||||
|
(let
|
||||||
|
((rows (run* q (fresh (x y) (conde ((== x 1) (== y 10)) ((== x 2) (== y 20))) (== q (list x y))))))
|
||||||
|
(and
|
||||||
|
(= (len rows) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (r) (= r (list 1 10))) rows)
|
||||||
|
(some (fn (r) (= r (list 2 20))) rows))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- nested conde ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-nested-yields-three"
|
||||||
|
(let
|
||||||
|
((qs (run* q (conde ((conde ((== q 1)) ((== q 2)))) ((== q 3))))))
|
||||||
|
(and
|
||||||
|
(= (len qs) 3)
|
||||||
|
(and
|
||||||
|
(some (fn (x) (= x 1)) qs)
|
||||||
|
(and
|
||||||
|
(some (fn (x) (= x 2)) qs)
|
||||||
|
(some (fn (x) (= x 3)) qs)))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- conde all clauses fail → empty stream ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conde-all-fail"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conde ((== 1 2)) ((== 3 4))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- empty conde: no clauses ⇒ fail ---
|
||||||
|
|
||||||
|
(mk-test "conde-no-clauses" (run* q (conde)) (list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
86
lib/minikanren/tests/condu.sx
Normal file
86
lib/minikanren/tests/condu.sx
Normal file
@@ -0,0 +1,86 @@
|
|||||||
|
;; lib/minikanren/tests/condu.sx — Phase 2 piece D tests for `onceo` and `condu`.
|
||||||
|
|
||||||
|
;; --- onceo: at most one answer ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"onceo-single-success-passes-through"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((onceo (== q 7)) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 7))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"onceo-multi-success-trimmed-to-one"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((onceo (mk-disj (== q 1) (== q 2) (== q 3))) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"onceo-failure-stays-failure"
|
||||||
|
((onceo (== 1 2)) empty-s)
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"onceo-conde-trimmed"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((onceo (conde ((== q "a")) ((== q "b")))) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list "a"))
|
||||||
|
|
||||||
|
;; --- condu: first clause with successful head wins ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"condu-first-clause-wins"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 10 ((condu ((== q 1)) ((== q 2))) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"condu-skips-failing-head"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 10 ((condu ((== 1 2)) ((== q 100)) ((== q 200))) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 100))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"condu-all-fail-empty"
|
||||||
|
((condu ((== 1 2)) ((== 3 4)))
|
||||||
|
empty-s)
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test "condu-empty-clauses-fail" ((condu) empty-s) (list))
|
||||||
|
|
||||||
|
;; --- condu commits head's first answer; rest-goals can still backtrack
|
||||||
|
;; within that committed substitution but cannot revisit other heads. ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"condu-head-onceo-rest-runs"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")) (r (mk-var "r")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 10 ((condu ((mk-disj (== q 1) (== q 2)) (== r 99))) empty-s))))
|
||||||
|
(map (fn (s) (list (mk-walk q s) (mk-walk r s))) res)))
|
||||||
|
(list (list 1 99)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"condu-rest-goals-can-fail-the-clause"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 10 ((condu ((== q 1) (== 2 3)) ((== q 99))) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
48
lib/minikanren/tests/cyclic-graph.sx
Normal file
48
lib/minikanren/tests/cyclic-graph.sx
Normal file
@@ -0,0 +1,48 @@
|
|||||||
|
;; lib/minikanren/tests/cyclic-graph.sx — demonstrates the naive-patho
|
||||||
|
;; behaviour on a cyclic graph. Without Phase-7 tabling/SLG, the search
|
||||||
|
;; produces ever-longer paths revisiting the cycle. `run n` truncates;
|
||||||
|
;; `run*` would diverge.
|
||||||
|
|
||||||
|
(define cyclic-edges (list (list :a :b) (list :b :a) (list :b :c)))
|
||||||
|
|
||||||
|
(define cyclic-edgeo (fn (x y) (membero (list x y) cyclic-edges)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
cyclic-patho
|
||||||
|
(fn
|
||||||
|
(x y path)
|
||||||
|
(conde
|
||||||
|
((cyclic-edgeo x y) (== path (list x y)))
|
||||||
|
((fresh (z mid) (cyclic-edgeo x z) (cyclic-patho z y mid) (conso x mid path))))))
|
||||||
|
|
||||||
|
;; --- direct edge ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cyclic-direct"
|
||||||
|
(run 1 q (cyclic-patho :a :b q))
|
||||||
|
(list (list :a :b)))
|
||||||
|
|
||||||
|
;; --- runs first 5 paths from a to b: bare edge, then increasing
|
||||||
|
;; numbers of cycle traversals (a->b->a->b, etc.) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cyclic-enumerates-prefix-via-run-n"
|
||||||
|
(let
|
||||||
|
((paths (run 5 q (cyclic-patho :a :b q))))
|
||||||
|
(and
|
||||||
|
(= (len paths) 5)
|
||||||
|
(and
|
||||||
|
(every? (fn (p) (= (first p) :a)) paths)
|
||||||
|
(every? (fn (p) (= (last p) :b)) paths))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cyclic-finds-c-via-cycle-or-direct"
|
||||||
|
(let
|
||||||
|
((paths (run 3 q (cyclic-patho :a :c q))))
|
||||||
|
(and
|
||||||
|
(>= (len paths) 1)
|
||||||
|
(some (fn (p) (= p (list :a :b :c))) paths)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
40
lib/minikanren/tests/defrel.sx
Normal file
40
lib/minikanren/tests/defrel.sx
Normal file
@@ -0,0 +1,40 @@
|
|||||||
|
;; lib/minikanren/tests/defrel.sx — Prolog-style relation definition macro.
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-membero x l)
|
||||||
|
((fresh (d) (conso x d l)))
|
||||||
|
((fresh (a d) (conso a d l) (my-membero x d))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-defines-membero"
|
||||||
|
(run* q (my-membero q (list 1 2 3)))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-listo l)
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (my-listo d))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-listo-bounded"
|
||||||
|
(run 3 q (my-listo q))
|
||||||
|
(list
|
||||||
|
(list)
|
||||||
|
(list (make-symbol "_.0"))
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; Multi-arg relation with arithmetic.
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-pluso a b c)
|
||||||
|
((== a :z) (== b c))
|
||||||
|
((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (my-pluso a-1 b c-1))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-pluso-2-3"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(my-pluso (list :s (list :s :z)) (list :s (list :s (list :s :z))) q))
|
||||||
|
(list (list :s (list :s (list :s (list :s (list :s :z)))))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
31
lib/minikanren/tests/enumerate.sx
Normal file
31
lib/minikanren/tests/enumerate.sx
Normal file
@@ -0,0 +1,31 @@
|
|||||||
|
;; lib/minikanren/tests/enumerate.sx — index-each-element relation.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"enumerate-i-empty"
|
||||||
|
(run* q (enumerate-i (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"enumerate-i-three"
|
||||||
|
(run* q (enumerate-i (list :a :b :c) q))
|
||||||
|
(list
|
||||||
|
(list (list 0 :a) (list 1 :b) (list 2 :c))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"enumerate-i-strings"
|
||||||
|
(run* q (enumerate-i (list "x" "y" "z") q))
|
||||||
|
(list
|
||||||
|
(list (list 0 "x") (list 1 "y") (list 2 "z"))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"enumerate-from-i-100"
|
||||||
|
(run* q (enumerate-from-i 100 (list :x :y :z) q))
|
||||||
|
(list
|
||||||
|
(list (list 100 :x) (list 101 :y) (list 102 :z))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"enumerate-from-i-singleton"
|
||||||
|
(run* q (enumerate-from-i 0 (list :only) q))
|
||||||
|
(list (list (list 0 :only))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
75
lib/minikanren/tests/fd.sx
Normal file
75
lib/minikanren/tests/fd.sx
Normal file
@@ -0,0 +1,75 @@
|
|||||||
|
;; lib/minikanren/tests/fd.sx — Phase 6 piece A: ino + all-distincto.
|
||||||
|
|
||||||
|
;; --- ino ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"ino-element-in-domain"
|
||||||
|
(run* q (ino q (list 1 2 3)))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(mk-test "ino-empty-domain" (run* q (ino q (list))) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"ino-singleton-domain"
|
||||||
|
(run* q (ino q (list 42)))
|
||||||
|
(list 42))
|
||||||
|
|
||||||
|
;; --- all-distincto ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"all-distincto-empty"
|
||||||
|
(run* q (all-distincto (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"all-distincto-singleton"
|
||||||
|
(run* q (all-distincto (list 1)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"all-distincto-distinct-three"
|
||||||
|
(run* q (all-distincto (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"all-distincto-duplicate-fails"
|
||||||
|
(run* q (all-distincto (list 1 2 1)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"all-distincto-adjacent-duplicate-fails"
|
||||||
|
(run* q (all-distincto (list 1 1 2)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- ino + all-distincto: classic enumerate-all-permutations ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fd-puzzle-three-distinct-from-domain"
|
||||||
|
(let
|
||||||
|
((perms (run* q (fresh (a b c) (== q (list a b c)) (ino a (list 1 2 3)) (ino b (list 1 2 3)) (ino c (list 1 2 3)) (all-distincto (list a b c))))))
|
||||||
|
(and
|
||||||
|
(= (len perms) 6)
|
||||||
|
(and
|
||||||
|
(some (fn (p) (= p (list 1 2 3))) perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 1 3 2)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 2 1 3)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 2 3 1)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 3 1 2)))
|
||||||
|
perms)
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 3 2 1)))
|
||||||
|
perms))))))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
42
lib/minikanren/tests/flatteno.sx
Normal file
42
lib/minikanren/tests/flatteno.sx
Normal file
@@ -0,0 +1,42 @@
|
|||||||
|
(mk-test "flatteno-empty" (run* q (flatteno (list) q)) (list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-atom"
|
||||||
|
(run* q (flatteno 5 q))
|
||||||
|
(list (list 5)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-flat-list"
|
||||||
|
(run* q (flatteno (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-singleton"
|
||||||
|
(run* q (flatteno (list 1) q))
|
||||||
|
(list (list 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-nested-once"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(flatteno (list 1 (list 2 3) 4) q))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-nested-twice"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(flatteno
|
||||||
|
(list
|
||||||
|
1
|
||||||
|
(list 2 (list 3 4))
|
||||||
|
5)
|
||||||
|
q))
|
||||||
|
(list (list 1 2 3 4 5)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"flatteno-keywords"
|
||||||
|
(run* q (flatteno (list :a (list :b :c) :d) q))
|
||||||
|
(list (list :a :b :c :d)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
101
lib/minikanren/tests/fresh.sx
Normal file
101
lib/minikanren/tests/fresh.sx
Normal file
@@ -0,0 +1,101 @@
|
|||||||
|
;; lib/minikanren/tests/fresh.sx — Phase 2 piece B tests for `fresh`.
|
||||||
|
|
||||||
|
;; --- empty fresh: pure goal grouping ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-empty-vars-equiv-conj"
|
||||||
|
(stream-take 5 ((fresh () (== 1 1)) empty-s))
|
||||||
|
(list empty-s))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-empty-vars-no-goals-is-succeed"
|
||||||
|
(stream-take 5 ((fresh ()) empty-s))
|
||||||
|
(list empty-s))
|
||||||
|
|
||||||
|
;; --- single var ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-one-var-bound"
|
||||||
|
(let
|
||||||
|
((s (first (stream-take 5 ((fresh (x) (== x 7)) empty-s)))))
|
||||||
|
(first (vals s)))
|
||||||
|
7)
|
||||||
|
|
||||||
|
;; --- multiple vars + multiple goals ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-two-vars-three-goals"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q"))
|
||||||
|
(g
|
||||||
|
(fresh
|
||||||
|
(x y)
|
||||||
|
(== x 10)
|
||||||
|
(== y 20)
|
||||||
|
(== q (list x y)))))
|
||||||
|
(mk-walk* q (first (stream-take 5 (g empty-s)))))
|
||||||
|
(list 10 20))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-three-vars"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q"))
|
||||||
|
(g
|
||||||
|
(fresh
|
||||||
|
(a b c)
|
||||||
|
(== a 1)
|
||||||
|
(== b 2)
|
||||||
|
(== c 3)
|
||||||
|
(== q (list a b c)))))
|
||||||
|
(mk-walk* q (first (stream-take 5 (g empty-s)))))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
;; --- fresh interacts with disj ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-with-disj"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((g (fresh (x) (mk-disj (== x 1) (== x 2)) (== q x))))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 (g empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res))))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
;; --- nested fresh ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"fresh-nested"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q"))
|
||||||
|
(g
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(fresh
|
||||||
|
(y)
|
||||||
|
(== x 1)
|
||||||
|
(== y 2)
|
||||||
|
(== q (list x y))))))
|
||||||
|
(mk-walk* q (first (stream-take 5 (g empty-s)))))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
;; --- call-fresh (functional alternative) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"call-fresh-binds-and-walks"
|
||||||
|
(let
|
||||||
|
((s (first (stream-take 5 ((call-fresh (fn (x) (== x 99))) empty-s)))))
|
||||||
|
(first (vals s)))
|
||||||
|
99)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"call-fresh-distinct-from-outer-vars"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((g (call-fresh (fn (x) (mk-conj (== x 5) (== q (list x x)))))))
|
||||||
|
(mk-walk* q (first (stream-take 5 (g empty-s))))))
|
||||||
|
(list 5 5))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
260
lib/minikanren/tests/goals.sx
Normal file
260
lib/minikanren/tests/goals.sx
Normal file
@@ -0,0 +1,260 @@
|
|||||||
|
;; lib/minikanren/tests/goals.sx — Phase 2 tests for stream.sx + goals.sx.
|
||||||
|
;;
|
||||||
|
;; Streams use a tagged shape internally (`(:s head tail)`) so that mature
|
||||||
|
;; cells can have thunk tails — SX has no improper pairs. Test assertions
|
||||||
|
;; therefore stream-take into a plain SX list, or check goal effects via
|
||||||
|
;; mk-walk on the resulting subst, instead of inspecting raw streams.
|
||||||
|
|
||||||
|
;; --- stream-take base cases (input streams use s-cons / mzero) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-zero-from-mature"
|
||||||
|
(stream-take 0 (s-cons (empty-subst) mzero))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test "stream-take-from-mzero" (stream-take 5 mzero) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-mature-pair"
|
||||||
|
(stream-take 5 (s-cons :a (s-cons :b mzero)))
|
||||||
|
(list :a :b))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-fewer-than-available"
|
||||||
|
(stream-take 1 (s-cons :a (s-cons :b mzero)))
|
||||||
|
(list :a))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-all-with-neg-1"
|
||||||
|
(stream-take -1 (s-cons :a (s-cons :b (s-cons :c mzero))))
|
||||||
|
(list :a :b :c))
|
||||||
|
|
||||||
|
;; --- stream-take forces immature thunks ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-forces-thunk"
|
||||||
|
(stream-take 5 (fn () (s-cons :x mzero)))
|
||||||
|
(list :x))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stream-take-forces-nested-thunks"
|
||||||
|
(stream-take 5 (fn () (fn () (s-cons :y mzero))))
|
||||||
|
(list :y))
|
||||||
|
|
||||||
|
;; --- mk-mplus interleaves ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mplus-empty-left"
|
||||||
|
(stream-take 5 (mk-mplus mzero (s-cons :r mzero)))
|
||||||
|
(list :r))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mplus-empty-right"
|
||||||
|
(stream-take 5 (mk-mplus (s-cons :l mzero) mzero))
|
||||||
|
(list :l))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mplus-mature-mature"
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
(mk-mplus (s-cons :a (s-cons :b mzero)) (s-cons :c (s-cons :d mzero))))
|
||||||
|
(list :a :b :c :d))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mplus-with-paused-left-swaps"
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
(mk-mplus
|
||||||
|
(fn () (s-cons :a (s-cons :b mzero)))
|
||||||
|
(s-cons :c (s-cons :d mzero))))
|
||||||
|
(list :c :d :a :b))
|
||||||
|
|
||||||
|
;; --- mk-bind ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"bind-empty-stream"
|
||||||
|
(stream-take 5 (mk-bind mzero (fn (s) (unit s))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"bind-singleton-identity"
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
(mk-bind (s-cons 5 mzero) (fn (x) (unit x))))
|
||||||
|
(list 5))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"bind-flat-multi"
|
||||||
|
(stream-take
|
||||||
|
10
|
||||||
|
(mk-bind
|
||||||
|
(s-cons 1 (s-cons 2 mzero))
|
||||||
|
(fn (x) (s-cons x (s-cons (* x 10) mzero)))))
|
||||||
|
(list 1 10 2 20))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"bind-fail-prunes-some"
|
||||||
|
(stream-take
|
||||||
|
10
|
||||||
|
(mk-bind
|
||||||
|
(s-cons 1 (s-cons 2 (s-cons 3 mzero)))
|
||||||
|
(fn (x) (if (= x 2) mzero (unit x)))))
|
||||||
|
(list 1 3))
|
||||||
|
|
||||||
|
;; --- core goals: succeed / fail ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"succeed-yields-singleton"
|
||||||
|
(stream-take 5 (succeed empty-s))
|
||||||
|
(list empty-s))
|
||||||
|
|
||||||
|
(mk-test "fail-yields-mzero" (stream-take 5 (fail empty-s)) (list))
|
||||||
|
|
||||||
|
;; --- == ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-ground-success"
|
||||||
|
(stream-take 5 ((== 1 1) empty-s))
|
||||||
|
(list empty-s))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-ground-failure"
|
||||||
|
(stream-take 5 ((== 1 2) empty-s))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-binds-var"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-walk
|
||||||
|
x
|
||||||
|
(first (stream-take 5 ((== x 7) empty-s)))))
|
||||||
|
7)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-list-success"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-walk
|
||||||
|
x
|
||||||
|
(first
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
((== x (list 1 2)) empty-s)))))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-list-mismatch-fails"
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
((== (list 1 2) (list 1 3)) empty-s))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- conj2 / mk-conj ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conj2-both-bind"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")) (y (mk-var "y")))
|
||||||
|
(let
|
||||||
|
((s (first (stream-take 5 ((conj2 (== x 1) (== y 2)) empty-s)))))
|
||||||
|
(list (mk-walk x s) (mk-walk y s))))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conj2-conflict-empty"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(stream-take
|
||||||
|
5
|
||||||
|
((conj2 (== x 1) (== x 2)) empty-s)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conj-empty-is-succeed"
|
||||||
|
(stream-take 5 ((mk-conj) empty-s))
|
||||||
|
(list empty-s))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conj-single-is-goal"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-walk
|
||||||
|
x
|
||||||
|
(first
|
||||||
|
(stream-take 5 ((mk-conj (== x 99)) empty-s)))))
|
||||||
|
99)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conj-three-bindings"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
|
||||||
|
(let
|
||||||
|
((s (first (stream-take 5 ((mk-conj (== x 1) (== y 2) (== z 3)) empty-s)))))
|
||||||
|
(list (mk-walk x s) (mk-walk y s) (mk-walk z s))))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
;; --- disj2 / mk-disj ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"disj2-both-succeed"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((disj2 (== q 1) (== q 2)) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"disj2-fail-or-succeed"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((disj2 fail (== q 5)) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list 5))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"disj-empty-is-fail"
|
||||||
|
(stream-take 5 ((mk-disj) empty-s))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"disj-three-clauses"
|
||||||
|
(let
|
||||||
|
((q (mk-var "q")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((mk-disj (== q "a") (== q "b") (== q "c")) empty-s))))
|
||||||
|
(map (fn (s) (mk-walk q s)) res)))
|
||||||
|
(list "a" "b" "c"))
|
||||||
|
|
||||||
|
;; --- conj/disj nesting ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"disj-of-conj"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")) (y (mk-var "y")))
|
||||||
|
(let
|
||||||
|
((res (stream-take 5 ((mk-disj (mk-conj (== x 1) (== y 2)) (mk-conj (== x 3) (== y 4))) empty-s))))
|
||||||
|
(map (fn (s) (list (mk-walk x s) (mk-walk y s))) res)))
|
||||||
|
(list (list 1 2) (list 3 4)))
|
||||||
|
|
||||||
|
;; --- ==-check ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-check-no-occurs-fails"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(stream-take 5 ((==-check x (list 1 x)) empty-s)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"eq-check-no-occurs-non-occurring-succeeds"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-walk
|
||||||
|
x
|
||||||
|
(first (stream-take 5 ((==-check x 5) empty-s)))))
|
||||||
|
5)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
70
lib/minikanren/tests/graph.sx
Normal file
70
lib/minikanren/tests/graph.sx
Normal file
@@ -0,0 +1,70 @@
|
|||||||
|
;; lib/minikanren/tests/graph.sx — directed-graph reachability via patho.
|
||||||
|
|
||||||
|
(define
|
||||||
|
test-edges
|
||||||
|
(list (list :a :b) (list :b :c) (list :c :d) (list :a :c) (list :d :e)))
|
||||||
|
|
||||||
|
(define edgeo (fn (from to) (membero (list from to) test-edges)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
patho
|
||||||
|
(fn
|
||||||
|
(x y path)
|
||||||
|
(conde
|
||||||
|
((edgeo x y) (== path (list x y)))
|
||||||
|
((fresh (z mid-path) (edgeo x z) (patho z y mid-path) (conso x mid-path path))))))
|
||||||
|
|
||||||
|
;; --- direct edges ---
|
||||||
|
|
||||||
|
(mk-test "patho-direct" (run* q (patho :a :b q)) (list (list :a :b)))
|
||||||
|
|
||||||
|
(mk-test "patho-no-direct-edge" (run* q (patho :e :a q)) (list))
|
||||||
|
|
||||||
|
;; --- indirect ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"patho-multi-hop"
|
||||||
|
(let
|
||||||
|
((paths (run* q (patho :a :d q))))
|
||||||
|
(and
|
||||||
|
(= (len paths) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (p) (= p (list :a :b :c :d))) paths)
|
||||||
|
(some (fn (p) (= p (list :a :c :d))) paths))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"patho-to-leaf"
|
||||||
|
(let
|
||||||
|
((paths (run* q (patho :a :e q))))
|
||||||
|
(and
|
||||||
|
(= (len paths) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (p) (= p (list :a :b :c :d :e))) paths)
|
||||||
|
(some (fn (p) (= p (list :a :c :d :e))) paths))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- enumeration with multiplicity ---
|
||||||
|
;; Each path contributes one tuple, so reachable nodes can repeat. Here
|
||||||
|
;; targets are: b (1 path), c (2 paths), d (2 paths), e (2 paths) = 7.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"patho-enumerate-from-a-with-multiplicity"
|
||||||
|
(let
|
||||||
|
((targets (run* q (fresh (path) (patho :a q path)))))
|
||||||
|
(and
|
||||||
|
(= (len targets) 7)
|
||||||
|
(and
|
||||||
|
(some (fn (t) (= t :b)) targets)
|
||||||
|
(and
|
||||||
|
(some (fn (t) (= t :c)) targets)
|
||||||
|
(and
|
||||||
|
(some (fn (t) (= t :d)) targets)
|
||||||
|
(some (fn (t) (= t :e)) targets))))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- unreachable target ---
|
||||||
|
|
||||||
|
(mk-test "patho-unreachable" (run* q (patho :a :z q)) (list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
103
lib/minikanren/tests/intarith.sx
Normal file
103
lib/minikanren/tests/intarith.sx
Normal file
@@ -0,0 +1,103 @@
|
|||||||
|
;; lib/minikanren/tests/intarith.sx — ground-only integer arithmetic
|
||||||
|
;; goals that escape into host operations via project.
|
||||||
|
|
||||||
|
;; --- pluso-i ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-i-forward"
|
||||||
|
(run* q (pluso-i 7 8 q))
|
||||||
|
(list 15))
|
||||||
|
(mk-test
|
||||||
|
"pluso-i-zero"
|
||||||
|
(run* q (pluso-i 0 0 q))
|
||||||
|
(list 0))
|
||||||
|
(mk-test
|
||||||
|
"pluso-i-negatives"
|
||||||
|
(run* q (pluso-i -5 3 q))
|
||||||
|
(list -2))
|
||||||
|
(mk-test
|
||||||
|
"pluso-i-non-ground-fails"
|
||||||
|
(run* q (fresh (a) (pluso-i a 3 5)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- minuso-i ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"minuso-i-forward"
|
||||||
|
(run* q (minuso-i 10 4 q))
|
||||||
|
(list 6))
|
||||||
|
(mk-test
|
||||||
|
"minuso-i-zero"
|
||||||
|
(run* q (minuso-i 5 5 q))
|
||||||
|
(list 0))
|
||||||
|
|
||||||
|
;; --- *o-i ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"times-i-forward"
|
||||||
|
(run* q (*o-i 6 7 q))
|
||||||
|
(list 42))
|
||||||
|
(mk-test
|
||||||
|
"times-i-by-zero"
|
||||||
|
(run* q (*o-i 0 99 q))
|
||||||
|
(list 0))
|
||||||
|
(mk-test
|
||||||
|
"times-i-by-one"
|
||||||
|
(run* q (*o-i 1 17 q))
|
||||||
|
(list 17))
|
||||||
|
|
||||||
|
;; --- comparisons ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lto-i-true"
|
||||||
|
(run 1 q (lto-i 2 5))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "lto-i-false" (run* q (lto-i 5 2)) (list))
|
||||||
|
(mk-test "lto-i-equal-false" (run* q (lto-i 3 3)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lteo-i-equal"
|
||||||
|
(run 1 q (lteo-i 4 4))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"lteo-i-less"
|
||||||
|
(run 1 q (lteo-i 1 4))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "lteo-i-more" (run* q (lteo-i 9 4)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"neqo-i-different"
|
||||||
|
(run 1 q (neqo-i 3 5))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "neqo-i-same" (run* q (neqo-i 3 3)) (list))
|
||||||
|
|
||||||
|
;; --- composition with relational vars ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"intarith-with-membero"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(membero
|
||||||
|
x
|
||||||
|
(list 1 2 3 4 5))
|
||||||
|
(lto-i x 3)
|
||||||
|
(== q x)))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test "even-i-pos" (run* q (even-i 4)) (list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test "even-i-neg" (run* q (even-i 5)) (list))
|
||||||
|
|
||||||
|
(mk-test "odd-i-pos" (run* q (odd-i 7)) (list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test "odd-i-neg" (run* q (odd-i 4)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"even-i-filter"
|
||||||
|
(run* q (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x)))
|
||||||
|
(list 2 4 6))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
|
|
||||||
38
lib/minikanren/tests/iterate-no.sx
Normal file
38
lib/minikanren/tests/iterate-no.sx
Normal file
@@ -0,0 +1,38 @@
|
|||||||
|
;; lib/minikanren/tests/iterate-no.sx — iterated relation application.
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-nat
|
||||||
|
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"iterate-no-zero"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(iterate-no
|
||||||
|
(fn (a b) (== b (list :wrap a)))
|
||||||
|
(mk-nat 0)
|
||||||
|
:seed q))
|
||||||
|
(list :seed))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"iterate-no-three-wraps"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(iterate-no (fn (a b) (== b (list :wrap a))) (mk-nat 3) :x q))
|
||||||
|
(list (list :wrap (list :wrap (list :wrap :x)))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"iterate-no-succ-three-times"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(iterate-no (fn (a b) (== b (list :s a))) (mk-nat 3) :z q))
|
||||||
|
(list (mk-nat 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"iterate-no-with-list-cons"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(iterate-no (fn (a b) (conso :a a b)) (mk-nat 4) (list) q))
|
||||||
|
(list (list :a :a :a :a)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
38
lib/minikanren/tests/lasto.sx
Normal file
38
lib/minikanren/tests/lasto.sx
Normal file
@@ -0,0 +1,38 @@
|
|||||||
|
;; lib/minikanren/tests/lasto.sx — last-element + init-without-last.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lasto-singleton"
|
||||||
|
(run* q (lasto (list 5) q))
|
||||||
|
(list 5))
|
||||||
|
(mk-test
|
||||||
|
"lasto-multi"
|
||||||
|
(run* q (lasto (list 1 2 3 4) q))
|
||||||
|
(list 4))
|
||||||
|
(mk-test "lasto-empty" (run* q (lasto (list) q)) (list))
|
||||||
|
|
||||||
|
(mk-test "lasto-strings" (run* q (lasto (list "a" "b" "c") q)) (list "c"))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"init-o-multi"
|
||||||
|
(run* q (init-o (list 1 2 3 4) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"init-o-singleton"
|
||||||
|
(run* q (init-o (list 7) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test "init-o-empty" (run* q (init-o (list) q)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lasto-init-o-roundtrip"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(init last)
|
||||||
|
(lasto (list 1 2 3 4) last)
|
||||||
|
(init-o (list 1 2 3 4) init)
|
||||||
|
(appendo init (list last) q)))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
61
lib/minikanren/tests/latin.sx
Normal file
61
lib/minikanren/tests/latin.sx
Normal file
@@ -0,0 +1,61 @@
|
|||||||
|
;; lib/minikanren/tests/latin.sx — 2x2 Latin square via ino + all-distincto.
|
||||||
|
;;
|
||||||
|
;; A 2x2 Latin square has 2 distinct fillings:
|
||||||
|
;; ((1 2) (2 1)) and ((2 1) (1 2)).
|
||||||
|
;; The 3x3 version has 12 fillings but takes minutes under naive search;
|
||||||
|
;; full CLP(FD) (Phase 6 proper) would handle it in milliseconds.
|
||||||
|
|
||||||
|
(define
|
||||||
|
latin-2x2
|
||||||
|
(fn
|
||||||
|
(cells)
|
||||||
|
(let
|
||||||
|
((c11 (nth cells 0))
|
||||||
|
(c12 (nth cells 1))
|
||||||
|
(c21 (nth cells 2))
|
||||||
|
(c22 (nth cells 3))
|
||||||
|
(dom (list 1 2)))
|
||||||
|
(mk-conj
|
||||||
|
(ino c11 dom)
|
||||||
|
(ino c12 dom)
|
||||||
|
(ino c21 dom)
|
||||||
|
(ino c22 dom)
|
||||||
|
(all-distincto (list c11 c12))
|
||||||
|
(all-distincto (list c21 c22))
|
||||||
|
(all-distincto (list c11 c21))
|
||||||
|
(all-distincto (list c12 c22)))))) ;; col 2
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"latin-2x2-count"
|
||||||
|
(let
|
||||||
|
((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
|
||||||
|
(len squares))
|
||||||
|
2)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"latin-2x2-as-set"
|
||||||
|
(let
|
||||||
|
((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
|
||||||
|
(and
|
||||||
|
(= (len squares) 2)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (s) (= s (list 1 2 2 1)))
|
||||||
|
squares)
|
||||||
|
(some
|
||||||
|
(fn (s) (= s (list 2 1 1 2)))
|
||||||
|
squares))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"latin-2x2-with-clue"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(a b c d)
|
||||||
|
(== a 1)
|
||||||
|
(== q (list a b c d))
|
||||||
|
(latin-2x2 (list a b c d))))
|
||||||
|
(list (list 1 2 2 1)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
77
lib/minikanren/tests/laziness.sx
Normal file
77
lib/minikanren/tests/laziness.sx
Normal file
@@ -0,0 +1,77 @@
|
|||||||
|
;; lib/minikanren/tests/laziness.sx — verify Zzz wrapping (in conde)
|
||||||
|
;; lets infinitely-recursive relations produce finite prefixes via run-n.
|
||||||
|
|
||||||
|
;; --- a relation that has no base case but conde-protects via Zzz ---
|
||||||
|
|
||||||
|
(define
|
||||||
|
listo-aux
|
||||||
|
(fn
|
||||||
|
(l)
|
||||||
|
(conde ((nullo l)) ((fresh (a d) (conso a d l) (listo-aux d))))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"infinite-relation-truncates-via-run-n"
|
||||||
|
(run 4 q (listo-aux q))
|
||||||
|
(list
|
||||||
|
(list)
|
||||||
|
(list (make-symbol "_.0"))
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1"))
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
|
||||||
|
|
||||||
|
;; --- two infinite generators interleaved via mk-disj must both produce
|
||||||
|
;; answers (no starvation) — the fairness test ---
|
||||||
|
|
||||||
|
(define
|
||||||
|
ones-gen
|
||||||
|
(fn
|
||||||
|
(l)
|
||||||
|
(conde
|
||||||
|
((== l (list)))
|
||||||
|
((fresh (d) (conso 1 d l) (ones-gen d))))))
|
||||||
|
|
||||||
|
(define
|
||||||
|
twos-gen
|
||||||
|
(fn
|
||||||
|
(l)
|
||||||
|
(conde
|
||||||
|
((== l (list)))
|
||||||
|
((fresh (d) (conso 2 d l) (twos-gen d))))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"interleaving-keeps-both-streams-alive"
|
||||||
|
(let
|
||||||
|
((res (run 4 q (mk-disj (ones-gen q) (twos-gen q)))))
|
||||||
|
(and
|
||||||
|
(= (len res) 4)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn
|
||||||
|
(x)
|
||||||
|
(and
|
||||||
|
(list? x)
|
||||||
|
(and (not (empty? x)) (= (first x) 1))))
|
||||||
|
res)
|
||||||
|
(some
|
||||||
|
(fn
|
||||||
|
(x)
|
||||||
|
(and
|
||||||
|
(list? x)
|
||||||
|
(and (not (empty? x)) (= (first x) 2))))
|
||||||
|
res))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- run* terminates on a relation whose conde has finite base case
|
||||||
|
;; reached from any starting point ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run-star-terminates-on-bounded-relation"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(l)
|
||||||
|
(== l (list 1 2 3))
|
||||||
|
(listo l)
|
||||||
|
(== q :ok)))
|
||||||
|
(list :ok))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
28
lib/minikanren/tests/lengtho-i.sx
Normal file
28
lib/minikanren/tests/lengtho-i.sx
Normal file
@@ -0,0 +1,28 @@
|
|||||||
|
;; lib/minikanren/tests/lengtho-i.sx — integer-indexed length (fast).
|
||||||
|
|
||||||
|
(mk-test "lengtho-i-empty" (run* q (lengtho-i (list) q)) (list 0))
|
||||||
|
(mk-test
|
||||||
|
"lengtho-i-singleton"
|
||||||
|
(run* q (lengtho-i (list :a) q))
|
||||||
|
(list 1))
|
||||||
|
(mk-test
|
||||||
|
"lengtho-i-three"
|
||||||
|
(run* q (lengtho-i (list 1 2 3) q))
|
||||||
|
(list 3))
|
||||||
|
(mk-test
|
||||||
|
"lengtho-i-five"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(lengtho-i
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
q))
|
||||||
|
(list 5))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lengtho-i-mixed-types"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(lengtho-i (list 1 "two" :three (list 4 5)) q))
|
||||||
|
(list 4))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
126
lib/minikanren/tests/list-relations.sx
Normal file
126
lib/minikanren/tests/list-relations.sx
Normal file
@@ -0,0 +1,126 @@
|
|||||||
|
;; lib/minikanren/tests/list-relations.sx — rembero, assoco, nth-o, samelengtho.
|
||||||
|
|
||||||
|
;; --- rembero (remove first occurrence) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rembero-element-present"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(rembero 2 (list 1 2 3 2) q))
|
||||||
|
(list (list 1 3 2)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rembero-element-not-present"
|
||||||
|
(run* q (rembero 99 (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rembero-empty"
|
||||||
|
(run* q (rembero 1 (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rembero-only-element"
|
||||||
|
(run* q (rembero 5 (list 5) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rembero-first-of-many"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(rembero 1 (list 1 2 3 4) q))
|
||||||
|
(list (list 2 3 4)))
|
||||||
|
|
||||||
|
;; --- assoco (alist lookup) ---
|
||||||
|
|
||||||
|
(define
|
||||||
|
test-pairs
|
||||||
|
(list
|
||||||
|
(list "alice" 30)
|
||||||
|
(list "bob" 25)
|
||||||
|
(list "carol" 35)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"assoco-found"
|
||||||
|
(run* q (assoco "bob" test-pairs q))
|
||||||
|
(list 25))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"assoco-first"
|
||||||
|
(run* q (assoco "alice" test-pairs q))
|
||||||
|
(list 30))
|
||||||
|
|
||||||
|
(mk-test "assoco-missing" (run* q (assoco "dave" test-pairs q)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"assoco-find-keys-with-value"
|
||||||
|
(run* q (assoco q test-pairs 25))
|
||||||
|
(list "bob"))
|
||||||
|
|
||||||
|
;; --- nth-o (Peano-indexed access) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nth-o-zero"
|
||||||
|
(run* q (nth-o :z (list 10 20 30) q))
|
||||||
|
(list 10))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nth-o-one"
|
||||||
|
(run* q (nth-o (list :s :z) (list 10 20 30) q))
|
||||||
|
(list 20))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nth-o-two"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(nth-o (list :s (list :s :z)) (list 10 20 30) q))
|
||||||
|
(list 30))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nth-o-out-of-range"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(nth-o
|
||||||
|
(list :s (list :s (list :s :z)))
|
||||||
|
(list 10 20 30)
|
||||||
|
q))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- samelengtho ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"samelengtho-equal"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(samelengtho (list 1 2 3) (list :a :b :c)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"samelengtho-different-fails"
|
||||||
|
(run* q (samelengtho (list 1 2) (list :a :b :c)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"samelengtho-empty-equal"
|
||||||
|
(run* q (samelengtho (list) (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"samelengtho-builds-vars"
|
||||||
|
(run 1 q (samelengtho (list 1 2 3) q))
|
||||||
|
(list (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"samelengtho-enumerates-pairs"
|
||||||
|
(run
|
||||||
|
3
|
||||||
|
q
|
||||||
|
(fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2))))
|
||||||
|
(list
|
||||||
|
(list (list) (list))
|
||||||
|
(list (list (make-symbol "_.0")) (list (make-symbol "_.1")))
|
||||||
|
(list
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1"))
|
||||||
|
(list (make-symbol "_.2") (make-symbol "_.3")))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
62
lib/minikanren/tests/mapo.sx
Normal file
62
lib/minikanren/tests/mapo.sx
Normal file
@@ -0,0 +1,62 @@
|
|||||||
|
;; lib/minikanren/tests/mapo.sx — relational map.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-identity"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mapo (fn (a b) (== a b)) (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-tag-each"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mapo
|
||||||
|
(fn (a b) (== b (list :tag a)))
|
||||||
|
(list 1 2 3)
|
||||||
|
q))
|
||||||
|
(list
|
||||||
|
(list
|
||||||
|
(list :tag 1)
|
||||||
|
(list :tag 2)
|
||||||
|
(list :tag 3))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-backward"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mapo (fn (a b) (== a b)) q (list 1 2 3)))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-empty"
|
||||||
|
(run* q (mapo (fn (a b) (== a b)) (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-duplicate"
|
||||||
|
(run* q (mapo (fn (a b) (== b (list a a))) (list :x :y) q))
|
||||||
|
(list (list (list :x :x) (list :y :y))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mapo-different-length-fails"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mapo
|
||||||
|
(fn (a b) (== a b))
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; mapo + arithmetic via intarith
|
||||||
|
(mk-test
|
||||||
|
"mapo-square-each"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mapo
|
||||||
|
(fn (a b) (*o-i a a b))
|
||||||
|
(list 1 2 3 4)
|
||||||
|
q))
|
||||||
|
(list (list 1 4 9 16)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
138
lib/minikanren/tests/matche.sx
Normal file
138
lib/minikanren/tests/matche.sx
Normal file
@@ -0,0 +1,138 @@
|
|||||||
|
;; lib/minikanren/tests/matche.sx — Phase 5 piece D tests for `matche`.
|
||||||
|
|
||||||
|
;; --- literal patterns ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-literal-number"
|
||||||
|
(run* q (matche q (1 (== q 1))))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-literal-string"
|
||||||
|
(run* q (matche q ("hello" (== q "hello"))))
|
||||||
|
(list "hello"))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-literal-no-clause-matches"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(matche 7 (1 (== q :a)) (2 (== q :b))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- variable patterns ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-symbol-pattern"
|
||||||
|
(run* q (fresh (x) (== x 99) (matche x (a (== q a)))))
|
||||||
|
(list 99))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-wildcard"
|
||||||
|
(run* q (fresh (x) (== x 7) (matche x (_ (== q :any)))))
|
||||||
|
(list :any))
|
||||||
|
|
||||||
|
;; --- list patterns ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-empty-list"
|
||||||
|
(run* q (matche (list) (() (== q :ok))))
|
||||||
|
(list :ok))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-pair-binds"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 1 2))
|
||||||
|
(matche x ((a b) (== q (list b a))))))
|
||||||
|
(list (list 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-triple-binds"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 1 2 3))
|
||||||
|
(matche x ((a b c) (== q (list :sum a b c))))))
|
||||||
|
(list (list :sum 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-mixed-literal-and-var"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 1 99 3))
|
||||||
|
(matche x ((1 m 3) (== q m)))))
|
||||||
|
(list 99))
|
||||||
|
|
||||||
|
;; --- multi-clause dispatch ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-multi-clause-shape"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 5 6))
|
||||||
|
(matche
|
||||||
|
x
|
||||||
|
(() (== q :empty))
|
||||||
|
((a) (== q (list :one a)))
|
||||||
|
((a b) (== q (list :two a b))))))
|
||||||
|
(list (list :two 5 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-three-shapes-via-fresh"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(matche
|
||||||
|
x
|
||||||
|
(() (== q :empty))
|
||||||
|
((a) (== q (list :one a)))
|
||||||
|
((a b) (== q (list :two a b))))))
|
||||||
|
(list
|
||||||
|
:empty (list :one (make-symbol "_.0"))
|
||||||
|
(list :two (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; --- nested patterns ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-nested"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(==
|
||||||
|
x
|
||||||
|
(list (list 1 2) (list 3 4)))
|
||||||
|
(matche x (((a b) (c d)) (== q (list a b c d))))))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
;; --- repeated var names create the same fresh var → must unify ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-repeated-var-implies-equality"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 7 7))
|
||||||
|
(matche x ((a a) (== q a)))))
|
||||||
|
(list 7))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"matche-repeated-var-mismatch-fails"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(== x (list 7 8))
|
||||||
|
(matche x ((a a) (== q a)))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
49
lib/minikanren/tests/minmax.sx
Normal file
49
lib/minikanren/tests/minmax.sx
Normal file
@@ -0,0 +1,49 @@
|
|||||||
|
;; lib/minikanren/tests/minmax.sx — mino + maxo via intarith.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"mino-singleton"
|
||||||
|
(run* q (mino (list 7) q))
|
||||||
|
(list 7))
|
||||||
|
(mk-test
|
||||||
|
"mino-of-3"
|
||||||
|
(run* q (mino (list 5 1 3) q))
|
||||||
|
(list 1))
|
||||||
|
(mk-test
|
||||||
|
"mino-of-5"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mino (list 5 1 3 2 4) q))
|
||||||
|
(list 1))
|
||||||
|
(mk-test
|
||||||
|
"mino-with-dups"
|
||||||
|
(run* q (mino (list 3 3 3) q))
|
||||||
|
(list 3))
|
||||||
|
(mk-test "mino-empty-fails" (run* q (mino (list) q)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"maxo-singleton"
|
||||||
|
(run* q (maxo (list 7) q))
|
||||||
|
(list 7))
|
||||||
|
(mk-test
|
||||||
|
"maxo-of-5"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(maxo (list 5 1 3 2 4) q))
|
||||||
|
(list 5))
|
||||||
|
(mk-test
|
||||||
|
"maxo-of-negs"
|
||||||
|
(run* q (maxo (list -5 -1 -3) q))
|
||||||
|
(list -1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"min-and-max-of-list"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(mn mx)
|
||||||
|
(mino (list 5 1 3 2 4) mn)
|
||||||
|
(maxo (list 5 1 3 2 4) mx)
|
||||||
|
(== q (list mn mx))))
|
||||||
|
(list (list 1 5)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
50
lib/minikanren/tests/nafc.sx
Normal file
50
lib/minikanren/tests/nafc.sx
Normal file
@@ -0,0 +1,50 @@
|
|||||||
|
;; lib/minikanren/tests/nafc.sx — Phase 5 piece C tests for `nafc`.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-failed-goal-succeeds"
|
||||||
|
(run* q (nafc (== 1 2)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-successful-goal-fails"
|
||||||
|
(run* q (nafc (== 1 1)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-double-negation"
|
||||||
|
(run* q (nafc (nafc (== 1 1))))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-with-conde-no-clauses-succeed"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(nafc
|
||||||
|
(conde ((== 1 2)) ((== 3 4)))))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-with-conde-some-clause-succeeds-fails"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(nafc
|
||||||
|
(conde ((== 1 1)) ((== 3 4)))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- composing nafc with == as a guard ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-as-guard"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh (x) (== x 5) (nafc (== x 99)) (== q x)))
|
||||||
|
(list 5))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nafc-guard-blocking"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh (x) (== x 5) (nafc (== x 5)) (== q x)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
29
lib/minikanren/tests/not-membero.sx
Normal file
29
lib/minikanren/tests/not-membero.sx
Normal file
@@ -0,0 +1,29 @@
|
|||||||
|
;; lib/minikanren/tests/not-membero.sx — relational "not in list".
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"not-membero-absent"
|
||||||
|
(run* q (not-membero 99 (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"not-membero-present"
|
||||||
|
(run* q (not-membero 2 (list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
(mk-test
|
||||||
|
"not-membero-empty"
|
||||||
|
(run* q (not-membero 1 (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"not-membero-as-filter"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(membero
|
||||||
|
x
|
||||||
|
(list 1 2 3 4 5))
|
||||||
|
(not-membero x (list 2 4))
|
||||||
|
(== q x)))
|
||||||
|
(list 1 3 5))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
41
lib/minikanren/tests/pairlisto.sx
Normal file
41
lib/minikanren/tests/pairlisto.sx
Normal file
@@ -0,0 +1,41 @@
|
|||||||
|
;; lib/minikanren/tests/pairlisto.sx — zip two lists into pair list.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairlisto-empty"
|
||||||
|
(run* q (pairlisto (list) (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairlisto-equal-lengths"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(pairlisto (list 1 2 3) (list :a :b :c) q))
|
||||||
|
(list
|
||||||
|
(list (list 1 :a) (list 2 :b) (list 3 :c))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairlisto-recover-l1"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(pairlisto
|
||||||
|
q
|
||||||
|
(list :a :b :c)
|
||||||
|
(list (list 10 :a) (list 20 :b) (list 30 :c))))
|
||||||
|
(list (list 10 20 30)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairlisto-recover-l2"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(pairlisto
|
||||||
|
(list 1 2 3)
|
||||||
|
q
|
||||||
|
(list (list 1 :x) (list 2 :y) (list 3 :z))))
|
||||||
|
(list (list :x :y :z)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairlisto-different-lengths-fails"
|
||||||
|
(run* q (pairlisto (list 1 2) (list :a :b :c) q))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
44
lib/minikanren/tests/palindromeo.sx
Normal file
44
lib/minikanren/tests/palindromeo.sx
Normal file
@@ -0,0 +1,44 @@
|
|||||||
|
;; lib/minikanren/tests/palindromeo.sx — palindromic list relation.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-empty"
|
||||||
|
(run* q (palindromeo (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-singleton"
|
||||||
|
(run* q (palindromeo (list :a)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-pair-equal"
|
||||||
|
(run* q (palindromeo (list 1 1)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-pair-unequal-fails"
|
||||||
|
(run* q (palindromeo (list 1 2)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-five-yes"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(palindromeo
|
||||||
|
(list 1 2 3 2 1)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-five-no"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(palindromeo
|
||||||
|
(list 1 2 3 4 5)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"palindromeo-strings"
|
||||||
|
(run* q (palindromeo (list "a" "b" "a")))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
58
lib/minikanren/tests/parity.sx
Normal file
58
lib/minikanren/tests/parity.sx
Normal file
@@ -0,0 +1,58 @@
|
|||||||
|
;; lib/minikanren/tests/parity.sx — eveno + oddo Peano predicates.
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-nat
|
||||||
|
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
|
||||||
|
|
||||||
|
(mk-test "eveno-zero" (run* q (eveno :z)) (list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"eveno-2"
|
||||||
|
(run* q (eveno (mk-nat 2)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"eveno-4"
|
||||||
|
(run* q (eveno (mk-nat 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "eveno-1-fails" (run* q (eveno (mk-nat 1))) (list))
|
||||||
|
(mk-test "eveno-3-fails" (run* q (eveno (mk-nat 3))) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"oddo-1"
|
||||||
|
(run* q (oddo (mk-nat 1)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"oddo-3"
|
||||||
|
(run* q (oddo (mk-nat 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "oddo-zero-fails" (run* q (oddo :z)) (list))
|
||||||
|
(mk-test "oddo-2-fails" (run* q (oddo (mk-nat 2))) (list))
|
||||||
|
|
||||||
|
;; Enumerate small evens.
|
||||||
|
(mk-test
|
||||||
|
"eveno-enumerates"
|
||||||
|
(run 4 q (eveno q))
|
||||||
|
(list
|
||||||
|
(mk-nat 0)
|
||||||
|
(mk-nat 2)
|
||||||
|
(mk-nat 4)
|
||||||
|
(mk-nat 6)))
|
||||||
|
|
||||||
|
;; Enumerate small odds.
|
||||||
|
(mk-test
|
||||||
|
"oddo-enumerates"
|
||||||
|
(run 4 q (oddo q))
|
||||||
|
(list
|
||||||
|
(mk-nat 1)
|
||||||
|
(mk-nat 3)
|
||||||
|
(mk-nat 5)
|
||||||
|
(mk-nat 7)))
|
||||||
|
|
||||||
|
;; A number is even XOR odd (no overlap).
|
||||||
|
(mk-test
|
||||||
|
"even-odd-no-overlap"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(mk-conj (eveno (mk-nat 4)) (oddo (mk-nat 4))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
75
lib/minikanren/tests/partitiono.sx
Normal file
75
lib/minikanren/tests/partitiono.sx
Normal file
@@ -0,0 +1,75 @@
|
|||||||
|
;; lib/minikanren/tests/partitiono.sx — partition list by predicate.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"partitiono-empty"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(yes no)
|
||||||
|
(partitiono (fn (x) (== x 1)) (list) yes no)
|
||||||
|
(== q (list yes no))))
|
||||||
|
(list (list (list) (list))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"partitiono-by-equality"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(yes no)
|
||||||
|
(partitiono
|
||||||
|
(fn (x) (== x 2))
|
||||||
|
(list 1 2 3 2 4)
|
||||||
|
yes
|
||||||
|
no)
|
||||||
|
(== q (list yes no))))
|
||||||
|
(list
|
||||||
|
(list
|
||||||
|
(list 2 2)
|
||||||
|
(list 1 3 4))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"partitiono-by-numeric-pred"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(yes no)
|
||||||
|
(partitiono
|
||||||
|
(fn (x) (lto-i x 5))
|
||||||
|
(list 1 7 2 8 3)
|
||||||
|
yes
|
||||||
|
no)
|
||||||
|
(== q (list yes no))))
|
||||||
|
(list
|
||||||
|
(list
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 7 8))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"partitiono-all-yes"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(yes no)
|
||||||
|
(partitiono
|
||||||
|
(fn (x) (lto-i x 100))
|
||||||
|
(list 1 2 3)
|
||||||
|
yes
|
||||||
|
no)
|
||||||
|
(== q (list yes no))))
|
||||||
|
(list (list (list 1 2 3) (list))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"partitiono-all-no"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(yes no)
|
||||||
|
(partitiono
|
||||||
|
(fn (x) (lto-i 100 x))
|
||||||
|
(list 1 2 3)
|
||||||
|
yes
|
||||||
|
no)
|
||||||
|
(== q (list yes no))))
|
||||||
|
(list (list (list) (list 1 2 3))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
40
lib/minikanren/tests/path-cycle-free.sx
Normal file
40
lib/minikanren/tests/path-cycle-free.sx
Normal file
@@ -0,0 +1,40 @@
|
|||||||
|
;; lib/minikanren/tests/path-cycle-free.sx — cycle-free reachability search.
|
||||||
|
;;
|
||||||
|
;; Threads a "visited" accumulator through the recursion, using nafc +
|
||||||
|
;; membero to prevent revisiting nodes. Demonstrates how to make the
|
||||||
|
;; cyclic-graph divergence problem (see tests/cyclic-graph.sx) tractable
|
||||||
|
;; for graphs with cycles, without invoking Phase-7 tabling.
|
||||||
|
|
||||||
|
(define
|
||||||
|
cf-edges
|
||||||
|
(list (list :a :b) (list :b :a) (list :b :c) (list :c :d) (list :d :a))) ; another cycle
|
||||||
|
|
||||||
|
(define cf-edgeo (fn (from to) (membero (list from to) cf-edges)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
patho-no-cycles
|
||||||
|
(fn
|
||||||
|
(x y visited path)
|
||||||
|
(conde
|
||||||
|
((cf-edgeo x y) (nafc (membero y visited)) (== path (list x y)))
|
||||||
|
((fresh (z mid v-prime) (cf-edgeo x z) (nafc (membero z visited)) (conso z visited v-prime) (patho-no-cycles z y v-prime mid) (conso x mid path))))))
|
||||||
|
|
||||||
|
(define cf-patho (fn (x y path) (patho-no-cycles x y (list x) path)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cycle-free-finds-finitely"
|
||||||
|
(let
|
||||||
|
((paths (run* q (cf-patho :a :d q))))
|
||||||
|
(and
|
||||||
|
(>= (len paths) 1)
|
||||||
|
(every? (fn (p) (and (= (first p) :a) (= (last p) :d))) paths)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cycle-free-direct-edge"
|
||||||
|
(run* q (cf-patho :a :b q))
|
||||||
|
(list (list :a :b)))
|
||||||
|
|
||||||
|
(mk-test "cycle-free-no-self-loop" (run* q (cf-patho :a :a q)) (list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
119
lib/minikanren/tests/peano.sx
Normal file
119
lib/minikanren/tests/peano.sx
Normal file
@@ -0,0 +1,119 @@
|
|||||||
|
;; lib/minikanren/tests/peano.sx — Peano arithmetic.
|
||||||
|
;;
|
||||||
|
;; Builds Peano numbers via a host-side helper so tests stay readable.
|
||||||
|
;; (mk-nat 3) → (:s (:s (:s :z))).
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-nat
|
||||||
|
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
|
||||||
|
|
||||||
|
;; --- zeroo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"zeroo-zero-succeeds"
|
||||||
|
(run* q (zeroo :z))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test
|
||||||
|
"zeroo-non-zero-fails"
|
||||||
|
(run* q (zeroo (mk-nat 1)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- pluso forward ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-forward-2-3"
|
||||||
|
(run* q (pluso (mk-nat 2) (mk-nat 3) q))
|
||||||
|
(list (mk-nat 5)))
|
||||||
|
|
||||||
|
(mk-test "pluso-forward-zero-zero" (run* q (pluso :z :z q)) (list :z))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-forward-zero-n"
|
||||||
|
(run* q (pluso :z (mk-nat 4) q))
|
||||||
|
(list (mk-nat 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-forward-n-zero"
|
||||||
|
(run* q (pluso (mk-nat 4) :z q))
|
||||||
|
(list (mk-nat 4)))
|
||||||
|
|
||||||
|
;; --- pluso backward ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-recover-augend"
|
||||||
|
(run* q (pluso q (mk-nat 2) (mk-nat 5)))
|
||||||
|
(list (mk-nat 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-recover-addend"
|
||||||
|
(run* q (pluso (mk-nat 2) q (mk-nat 5)))
|
||||||
|
(list (mk-nat 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pluso-enumerate-pairs-summing-to-3"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh (a b) (pluso a b (mk-nat 3)) (== q (list a b))))
|
||||||
|
(list
|
||||||
|
(list :z (mk-nat 3))
|
||||||
|
(list (mk-nat 1) (mk-nat 2))
|
||||||
|
(list (mk-nat 2) (mk-nat 1))
|
||||||
|
(list (mk-nat 3) :z)))
|
||||||
|
|
||||||
|
;; --- minuso ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"minuso-5-2-3"
|
||||||
|
(run* q (minuso (mk-nat 5) (mk-nat 2) q))
|
||||||
|
(list (mk-nat 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"minuso-n-n-zero"
|
||||||
|
(run* q (minuso (mk-nat 7) (mk-nat 7) q))
|
||||||
|
(list :z))
|
||||||
|
|
||||||
|
;; --- *o ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"times-2-3"
|
||||||
|
(run* q (*o (mk-nat 2) (mk-nat 3) q))
|
||||||
|
(list (mk-nat 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"times-zero-anything-zero"
|
||||||
|
(run* q (*o :z (mk-nat 99) q))
|
||||||
|
(list :z))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"times-3-4"
|
||||||
|
(run* q (*o (mk-nat 3) (mk-nat 4) q))
|
||||||
|
(list (mk-nat 12)))
|
||||||
|
|
||||||
|
;; --- lteo / lto ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lteo-success"
|
||||||
|
(run 1 q (lteo (mk-nat 2) (mk-nat 5)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lteo-equal-success"
|
||||||
|
(run 1 q (lteo (mk-nat 3) (mk-nat 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lteo-greater-fails"
|
||||||
|
(run* q (lteo (mk-nat 5) (mk-nat 2)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lto-strict-success"
|
||||||
|
(run 1 q (lto (mk-nat 2) (mk-nat 5)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lto-equal-fails"
|
||||||
|
(run* q (lto (mk-nat 3) (mk-nat 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
87
lib/minikanren/tests/predicates.sx
Normal file
87
lib/minikanren/tests/predicates.sx
Normal file
@@ -0,0 +1,87 @@
|
|||||||
|
;; lib/minikanren/tests/predicates.sx — everyo, someo.
|
||||||
|
|
||||||
|
;; --- everyo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"everyo-empty-trivially-true"
|
||||||
|
(run* q (everyo (fn (x) (== x 1)) (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"everyo-all-match"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(everyo
|
||||||
|
(fn (x) (== x 1))
|
||||||
|
(list 1 1 1)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"everyo-some-mismatch"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(everyo
|
||||||
|
(fn (x) (== x 1))
|
||||||
|
(list 1 2 1)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"everyo-with-intarith"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(everyo
|
||||||
|
(fn (x) (lto-i x 10))
|
||||||
|
(list 1 5 9)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"everyo-with-intarith-fail"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(everyo
|
||||||
|
(fn (x) (lto-i x 5))
|
||||||
|
(list 1 5 9)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- someo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"someo-finds-element"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(someo
|
||||||
|
(fn (x) (== x 2))
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"someo-not-found"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(someo
|
||||||
|
(fn (x) (== x 99))
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"someo-empty-fails"
|
||||||
|
(run* q (someo (fn (x) (== x 1)) (list)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"someo-multiple-matches-yields-multiple"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (x) (someo (fn (y) (== y x)) (list 1 2 1)) (== q x)))))
|
||||||
|
(len res))
|
||||||
|
3)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"someo-with-intarith"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(someo
|
||||||
|
(fn (x) (lto-i 100 x))
|
||||||
|
(list 5 50 200)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
76
lib/minikanren/tests/prefix-suffix.sx
Normal file
76
lib/minikanren/tests/prefix-suffix.sx
Normal file
@@ -0,0 +1,76 @@
|
|||||||
|
;; lib/minikanren/tests/prefix-suffix.sx — appendo-derived sublist relations.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"prefixo-empty"
|
||||||
|
(run* q (prefixo (list) (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"prefixo-full"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(prefixo
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"prefixo-partial"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(prefixo
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"prefixo-mismatch-fails"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(prefixo
|
||||||
|
(list 1 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"prefixo-enumerates-all"
|
||||||
|
(run* q (prefixo q (list 1 2 3)))
|
||||||
|
(list
|
||||||
|
(list)
|
||||||
|
(list 1)
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"suffixo-empty"
|
||||||
|
(run* q (suffixo (list) (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"suffixo-full"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(suffixo
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"suffixo-partial"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(suffixo
|
||||||
|
(list 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"suffixo-enumerates-all"
|
||||||
|
(run* q (suffixo q (list 1 2 3)))
|
||||||
|
(list
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 2 3)
|
||||||
|
(list 3)
|
||||||
|
(list)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
60
lib/minikanren/tests/project.sx
Normal file
60
lib/minikanren/tests/project.sx
Normal file
@@ -0,0 +1,60 @@
|
|||||||
|
;; lib/minikanren/tests/project.sx — Phase 5 piece B tests for `project`.
|
||||||
|
|
||||||
|
;; --- project rebinds vars to ground values for SX use ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-square-via-host"
|
||||||
|
(run* q (fresh (n) (== n 5) (project (n) (== q (* n n)))))
|
||||||
|
(list 25))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-multi-vars"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(a b)
|
||||||
|
(== a 3)
|
||||||
|
(== b 4)
|
||||||
|
(project (a b) (== q (+ a b)))))
|
||||||
|
(list 7))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-with-string-host-op"
|
||||||
|
(run* q (fresh (s) (== s "hello") (project (s) (== q (str s "!")))))
|
||||||
|
(list "hello!"))
|
||||||
|
|
||||||
|
;; --- project nested inside conde ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-inside-conde"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(n)
|
||||||
|
(conde ((== n 3)) ((== n 4)))
|
||||||
|
(project (n) (== q (* n 10)))))
|
||||||
|
(list 30 40))
|
||||||
|
|
||||||
|
;; --- project body can be multiple goals (mk-conj'd) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-multi-goal-body"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(n)
|
||||||
|
(== n 7)
|
||||||
|
(project (n) (== q (+ n 1)) (== q (+ n 1)))))
|
||||||
|
(list 8))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"project-multi-goal-body-conflict"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(n)
|
||||||
|
(== n 7)
|
||||||
|
(project (n) (== q (+ n 1)) (== q (+ n 2)))))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
36
lib/minikanren/tests/pythag.sx
Normal file
36
lib/minikanren/tests/pythag.sx
Normal file
@@ -0,0 +1,36 @@
|
|||||||
|
;; lib/minikanren/tests/pythag.sx — Pythagorean triple search.
|
||||||
|
;;
|
||||||
|
;; Uses ino + intarith goals to find triples (a, b, c) with
|
||||||
|
;; a, b, c ∈ [1..N], a ≤ b, a² + b² = c². With intarith escapes
|
||||||
|
;; the search runs at host-arithmetic speed.
|
||||||
|
|
||||||
|
(define
|
||||||
|
digits-1-10
|
||||||
|
(list
|
||||||
|
1
|
||||||
|
2
|
||||||
|
3
|
||||||
|
4
|
||||||
|
5
|
||||||
|
6
|
||||||
|
7
|
||||||
|
8
|
||||||
|
9
|
||||||
|
10))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pythag-triples-1-to-10"
|
||||||
|
(let
|
||||||
|
((triples (run* q (fresh (a b c a-sq b-sq sum c-sq) (ino a digits-1-10) (ino b digits-1-10) (ino c digits-1-10) (lteo-i a b) (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) (pluso-i a-sq b-sq sum) (== sum c-sq) (== q (list a b c))))))
|
||||||
|
(and
|
||||||
|
(= (len triples) 2)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (t) (= t (list 3 4 5)))
|
||||||
|
triples)
|
||||||
|
(some
|
||||||
|
(fn (t) (= t (list 6 8 10)))
|
||||||
|
triples))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
45
lib/minikanren/tests/queens.sx
Normal file
45
lib/minikanren/tests/queens.sx
Normal file
@@ -0,0 +1,45 @@
|
|||||||
|
;; lib/minikanren/tests/queens.sx — N-queens, the classic miniKanren benchmark.
|
||||||
|
|
||||||
|
;; --- safe-diag (helper) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"safe-diag-different-cols-different-distance"
|
||||||
|
(run* q (safe-diag 1 4 2))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"safe-diag-same-distance-fails"
|
||||||
|
(run* q (safe-diag 1 4 3))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"safe-diag-same-distance-other-direction-fails"
|
||||||
|
(run* q (safe-diag 4 1 3))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- ino-each / range ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"range-1-to-4"
|
||||||
|
(range-1-to-n 4)
|
||||||
|
(list 1 2 3 4))
|
||||||
|
(mk-test "range-empty" (range-1-to-n 0) (list))
|
||||||
|
|
||||||
|
;; --- 4-queens: two solutions ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"queens-4"
|
||||||
|
(let
|
||||||
|
((sols (run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols (list a b c d) 4)))))
|
||||||
|
(and
|
||||||
|
(= (len sols) 2)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (s) (= s (list 2 4 1 3)))
|
||||||
|
sols)
|
||||||
|
(some
|
||||||
|
(fn (s) (= s (list 3 1 4 2)))
|
||||||
|
sols))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
90
lib/minikanren/tests/rdb.sx
Normal file
90
lib/minikanren/tests/rdb.sx
Normal file
@@ -0,0 +1,90 @@
|
|||||||
|
;; lib/minikanren/tests/rdb.sx — relational database queries.
|
||||||
|
;;
|
||||||
|
;; Demonstrates how miniKanren can serve as a Datalog-style query engine
|
||||||
|
;; over fact tables. Tables are SX lists of tuples; the relation just
|
||||||
|
;; wraps `membero` over the table.
|
||||||
|
|
||||||
|
(define
|
||||||
|
rdb-employees
|
||||||
|
(list
|
||||||
|
(list "alice" "engineering" 100000)
|
||||||
|
(list "bob" "marketing" 80000)
|
||||||
|
(list "carol" "engineering" 90000)
|
||||||
|
(list "dave" "engineering" 85000)
|
||||||
|
(list "eve" "sales" 75000)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
rdb-projects
|
||||||
|
(list
|
||||||
|
(list "alice" "compiler")
|
||||||
|
(list "carol" "compiler")
|
||||||
|
(list "dave" "runtime")
|
||||||
|
(list "alice" "runtime")
|
||||||
|
(list "eve" "outreach")))
|
||||||
|
|
||||||
|
;; Relation views over the tables.
|
||||||
|
|
||||||
|
(define
|
||||||
|
employees
|
||||||
|
(fn (name dept salary) (membero (list name dept salary) rdb-employees)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
on-project
|
||||||
|
(fn (name project) (membero (list name project) rdb-projects)))
|
||||||
|
|
||||||
|
;; --- queries ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rdb-engineering-staff"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (n s) (employees n "engineering" s) (== q n)))))
|
||||||
|
(and
|
||||||
|
(= (len res) 3)
|
||||||
|
(and
|
||||||
|
(some (fn (n) (= n "alice")) res)
|
||||||
|
(and
|
||||||
|
(some (fn (n) (= n "carol")) res)
|
||||||
|
(some (fn (n) (= n "dave")) res)))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rdb-high-salary"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (n d s) (employees n d s) (lto-i 85000 s) (== q (list n s))))))
|
||||||
|
(and
|
||||||
|
(= (len res) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (r) (= r (list "alice" 100000))) res)
|
||||||
|
(some (fn (r) (= r (list "carol" 90000))) res))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rdb-join-employee-project"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (n d s) (employees n d s) (on-project n "compiler") (== q n)))))
|
||||||
|
(and
|
||||||
|
(= (len res) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (n) (= n "alice")) res)
|
||||||
|
(some (fn (n) (= n "carol")) res))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rdb-engineers-on-runtime"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (n s) (employees n "engineering" s) (on-project n "runtime") (== q n)))))
|
||||||
|
(and
|
||||||
|
(= (len res) 2)
|
||||||
|
(and
|
||||||
|
(some (fn (n) (= n "alice")) res)
|
||||||
|
(some (fn (n) (= n "dave")) res))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rdb-people-on-multiple-projects"
|
||||||
|
(let
|
||||||
|
((res (run* q (fresh (n p1 p2) (on-project n p1) (on-project n p2) (nafc (== p1 p2)) (== q n)))))
|
||||||
|
(some (fn (n) (= n "alice")) res))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
291
lib/minikanren/tests/relations.sx
Normal file
291
lib/minikanren/tests/relations.sx
Normal file
@@ -0,0 +1,291 @@
|
|||||||
|
;; lib/minikanren/tests/relations.sx — Phase 4 standard relations.
|
||||||
|
;;
|
||||||
|
;; Includes the classic miniKanren canaries: appendo forwards / backwards /
|
||||||
|
;; bidirectionally, membero, listo enumeration.
|
||||||
|
|
||||||
|
;; --- nullo / pairo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"nullo-empty-succeeds"
|
||||||
|
(run* q (nullo (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test "nullo-non-empty-fails" (run* q (nullo (list 1))) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"pairo-non-empty-succeeds"
|
||||||
|
(run* q (pairo (list 1 2)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test "pairo-empty-fails" (run* q (pairo (list))) (list))
|
||||||
|
|
||||||
|
;; --- caro / cdro / firsto / resto ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"caro-extracts-head"
|
||||||
|
(run* q (caro (list 1 2 3) q))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"cdro-extracts-tail"
|
||||||
|
(run* q (cdro (list 1 2 3) q))
|
||||||
|
(list (list 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"firsto-alias-of-caro"
|
||||||
|
(run* q (firsto (list 10 20) q))
|
||||||
|
(list 10))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"resto-alias-of-cdro"
|
||||||
|
(run* q (resto (list 10 20) q))
|
||||||
|
(list (list 20)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"caro-cdro-build"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(h t)
|
||||||
|
(caro (list 1 2 3) h)
|
||||||
|
(cdro (list 1 2 3) t)
|
||||||
|
(== q (list h t))))
|
||||||
|
(list (list 1 (list 2 3))))
|
||||||
|
|
||||||
|
;; --- conso ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conso-forward"
|
||||||
|
(run* q (conso 0 (list 1 2 3) q))
|
||||||
|
(list (list 0 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conso-extract-head"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conso
|
||||||
|
q
|
||||||
|
(list 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"conso-extract-tail"
|
||||||
|
(run* q (conso 1 q (list 1 2 3)))
|
||||||
|
(list (list 2 3)))
|
||||||
|
|
||||||
|
;; --- listo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"listo-empty-succeeds"
|
||||||
|
(run* q (listo (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"listo-finite-list-succeeds"
|
||||||
|
(run* q (listo (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"listo-enumerates-shapes"
|
||||||
|
(run 3 q (listo q))
|
||||||
|
(list
|
||||||
|
(list)
|
||||||
|
(list (make-symbol "_.0"))
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; --- appendo: the canary ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-forward-simple"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo (list 1 2) (list 3 4) q))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-forward-empty-l"
|
||||||
|
(run* q (appendo (list) (list 3 4) q))
|
||||||
|
(list (list 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-forward-empty-s"
|
||||||
|
(run* q (appendo (list 1 2) (list) q))
|
||||||
|
(list (list 1 2)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-recovers-tail"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo
|
||||||
|
(list 1 2)
|
||||||
|
q
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (list 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-recovers-prefix"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo
|
||||||
|
q
|
||||||
|
(list 3 4)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (list 1 2)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-backward-all-splits"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(l s)
|
||||||
|
(appendo l s (list 1 2 3))
|
||||||
|
(== q (list l s))))
|
||||||
|
(list
|
||||||
|
(list (list) (list 1 2 3))
|
||||||
|
(list (list 1) (list 2 3))
|
||||||
|
(list (list 1 2) (list 3))
|
||||||
|
(list (list 1 2 3) (list))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo-empty-empty-empty"
|
||||||
|
(run* q (appendo (list) (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
;; --- membero ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"membero-element-present"
|
||||||
|
(run
|
||||||
|
1
|
||||||
|
q
|
||||||
|
(membero 2 (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"membero-element-absent-empty"
|
||||||
|
(run* q (membero 99 (list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"membero-enumerates"
|
||||||
|
(run* q (membero q (list "a" "b" "c")))
|
||||||
|
(list "a" "b" "c"))
|
||||||
|
|
||||||
|
;; --- reverseo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reverseo-forward"
|
||||||
|
(run* q (reverseo (list 1 2 3) q))
|
||||||
|
(list (list 3 2 1)))
|
||||||
|
|
||||||
|
(mk-test "reverseo-empty" (run* q (reverseo (list) q)) (list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reverseo-singleton"
|
||||||
|
(run* q (reverseo (list 42) q))
|
||||||
|
(list (list 42)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reverseo-five"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(reverseo (list 1 2 3 4 5) q))
|
||||||
|
(list (list 5 4 3 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reverseo-backward-one"
|
||||||
|
(run 1 q (reverseo q (list 1 2 3)))
|
||||||
|
(list (list 3 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reverseo-round-trip"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh (mid) (reverseo (list "a" "b" "c") mid) (reverseo mid q)))
|
||||||
|
(list (list "a" "b" "c")))
|
||||||
|
|
||||||
|
;; --- lengtho (Peano-style) ---
|
||||||
|
|
||||||
|
(mk-test "lengtho-empty-is-z" (run* q (lengtho (list) q)) (list :z))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lengtho-of-3"
|
||||||
|
(run* q (lengtho (list "a" "b" "c") q))
|
||||||
|
(list (list :s (list :s (list :s :z)))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lengtho-empty-from-zero"
|
||||||
|
(run 1 q (lengtho q :z))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"lengtho-enumerates-of-length-2"
|
||||||
|
(run 1 q (lengtho q (list :s (list :s :z))))
|
||||||
|
(list (list (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; --- inserto ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"inserto-front"
|
||||||
|
(run* q (inserto 0 (list 1 2 3) q))
|
||||||
|
(list
|
||||||
|
(list 0 1 2 3)
|
||||||
|
(list 1 0 2 3)
|
||||||
|
(list 1 2 0 3)
|
||||||
|
(list 1 2 3 0)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"inserto-empty"
|
||||||
|
(run* q (inserto 0 (list) q))
|
||||||
|
(list (list 0)))
|
||||||
|
|
||||||
|
;; --- permuteo ---
|
||||||
|
|
||||||
|
(mk-test "permuteo-empty" (run* q (permuteo (list) q)) (list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"permuteo-singleton"
|
||||||
|
(run* q (permuteo (list 42) q))
|
||||||
|
(list (list 42)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"permuteo-two"
|
||||||
|
(run* q (permuteo (list 1 2) q))
|
||||||
|
(list (list 1 2) (list 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"permuteo-three-as-set"
|
||||||
|
(let
|
||||||
|
((perms (run* q (permuteo (list 1 2 3) q))))
|
||||||
|
(and
|
||||||
|
(= (len perms) 6)
|
||||||
|
(and
|
||||||
|
(some (fn (p) (= p (list 1 2 3))) perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 2 1 3)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 1 3 2)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 2 3 1)))
|
||||||
|
perms)
|
||||||
|
(and
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 3 1 2)))
|
||||||
|
perms)
|
||||||
|
(some
|
||||||
|
(fn (p) (= p (list 3 2 1)))
|
||||||
|
perms))))))))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"permuteo-backward-finds-input"
|
||||||
|
(run 1 q (permuteo q (list "a" "b" "c")))
|
||||||
|
(list (list "a" "b" "c")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
39
lib/minikanren/tests/removeo-allo.sx
Normal file
39
lib/minikanren/tests/removeo-allo.sx
Normal file
@@ -0,0 +1,39 @@
|
|||||||
|
;; lib/minikanren/tests/removeo-allo.sx — remove every occurrence of x.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"removeo-allo-multi"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(removeo-allo
|
||||||
|
2
|
||||||
|
(list 1 2 3 2 4 2)
|
||||||
|
q))
|
||||||
|
(list (list 1 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"removeo-allo-single"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(removeo-allo 2 (list 1 2 3) q))
|
||||||
|
(list (list 1 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"removeo-allo-no-match"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(removeo-allo 99 (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"removeo-allo-everything"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(removeo-allo 1 (list 1 1 1) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"removeo-allo-empty"
|
||||||
|
(run* q (removeo-allo 1 (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
69
lib/minikanren/tests/repeato-concato.sx
Normal file
69
lib/minikanren/tests/repeato-concato.sx
Normal file
@@ -0,0 +1,69 @@
|
|||||||
|
;; lib/minikanren/tests/repeato-concato.sx — repeat element n times +
|
||||||
|
;; concatenate a list of lists.
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-nat
|
||||||
|
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
|
||||||
|
|
||||||
|
;; --- repeato ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"repeato-zero"
|
||||||
|
(run* q (repeato :a (mk-nat 0) q))
|
||||||
|
(list (list)))
|
||||||
|
(mk-test
|
||||||
|
"repeato-one"
|
||||||
|
(run* q (repeato :a (mk-nat 1) q))
|
||||||
|
(list (list :a)))
|
||||||
|
(mk-test
|
||||||
|
"repeato-three"
|
||||||
|
(run* q (repeato :a (mk-nat 3) q))
|
||||||
|
(list (list :a :a :a)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"repeato-numeric"
|
||||||
|
(run* q (repeato 7 (mk-nat 4) q))
|
||||||
|
(list (list 7 7 7 7)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"repeato-recover-count"
|
||||||
|
(run* q (repeato :x q (list :x :x :x :x)))
|
||||||
|
(list (mk-nat 4)))
|
||||||
|
|
||||||
|
;; --- concato ---
|
||||||
|
|
||||||
|
(mk-test "concato-empty" (run* q (concato (list) q)) (list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"concato-single"
|
||||||
|
(run* q (concato (list (list 1 2 3)) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"concato-multi"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(concato
|
||||||
|
(list
|
||||||
|
(list 1 2)
|
||||||
|
(list 3)
|
||||||
|
(list 4 5 6))
|
||||||
|
q))
|
||||||
|
(list
|
||||||
|
(list 1 2 3 4 5 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"concato-all-empty"
|
||||||
|
(run* q (concato (list (list) (list) (list)) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"concato-mixed-empty"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(concato
|
||||||
|
(list (list 1) (list) (list 2 3))
|
||||||
|
q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
46
lib/minikanren/tests/rev-acco.sx
Normal file
46
lib/minikanren/tests/rev-acco.sx
Normal file
@@ -0,0 +1,46 @@
|
|||||||
|
;; lib/minikanren/tests/rev-acco.sx — accumulator-style reverse.
|
||||||
|
;;
|
||||||
|
;; Faster than reverseo for forward queries (no quadratic appendos).
|
||||||
|
;; Trade-off: rev-acco is asymmetric (acc=initial-empty for the public
|
||||||
|
;; interface), so it does not cleanly run backwards in run* the way
|
||||||
|
;; reverseo does.
|
||||||
|
|
||||||
|
(mk-test "rev-2o-empty" (run* q (rev-2o (list) q)) (list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rev-2o-singleton"
|
||||||
|
(run* q (rev-2o (list 7) q))
|
||||||
|
(list (list 7)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rev-2o-three"
|
||||||
|
(run* q (rev-2o (list 1 2 3) q))
|
||||||
|
(list (list 3 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rev-2o-five"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(rev-2o (list 1 2 3 4 5) q))
|
||||||
|
(list (list 5 4 3 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rev-2o-strings"
|
||||||
|
(run* q (rev-2o (list "a" "b" "c") q))
|
||||||
|
(list (list "c" "b" "a")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"rev-2o-reverseo-agree"
|
||||||
|
(let
|
||||||
|
((via-reverseo (first (run* q (reverseo (list 1 2 3 4 5) q))))
|
||||||
|
(via-rev-2o
|
||||||
|
(first
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(rev-2o
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
q)))))
|
||||||
|
(= via-reverseo via-rev-2o))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
114
lib/minikanren/tests/run.sx
Normal file
114
lib/minikanren/tests/run.sx
Normal file
@@ -0,0 +1,114 @@
|
|||||||
|
;; lib/minikanren/tests/run.sx — Phase 3 tests for run* / run / reify.
|
||||||
|
|
||||||
|
;; --- canonical TRS one-liners ---
|
||||||
|
|
||||||
|
(mk-test "run*-eq-one" (run* q (== q 1)) (list 1))
|
||||||
|
(mk-test "run*-eq-string" (run* q (== q "hello")) (list "hello"))
|
||||||
|
(mk-test "run*-eq-symbol" (run* q (== q (quote sym))) (list (quote sym)))
|
||||||
|
(mk-test "run*-fail-empty" (run* q (== 1 2)) (list))
|
||||||
|
|
||||||
|
;; --- run with a count ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run-3-of-many"
|
||||||
|
(run
|
||||||
|
3
|
||||||
|
q
|
||||||
|
(conde
|
||||||
|
((== q 1))
|
||||||
|
((== q 2))
|
||||||
|
((== q 3))
|
||||||
|
((== q 4))
|
||||||
|
((== q 5))))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(mk-test "run-zero-empty" (run 0 q (== q 1)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run-1-takes-one"
|
||||||
|
(run 1 q (conde ((== q "a")) ((== q "b"))))
|
||||||
|
(list "a"))
|
||||||
|
|
||||||
|
;; --- reification: unbound vars get _.N left-to-right ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reify-single-unbound"
|
||||||
|
(run* q (fresh (x) (== q x)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reify-pair-unbound"
|
||||||
|
(run* q (fresh (x y) (== q (list x y))))
|
||||||
|
(list (list (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reify-mixed-bound-unbound"
|
||||||
|
(run* q (fresh (x y) (== q (list 1 x 2 y))))
|
||||||
|
(list
|
||||||
|
(list 1 (make-symbol "_.0") 2 (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reify-shared-unbound-same-name"
|
||||||
|
(run* q (fresh (x) (== q (list x x))))
|
||||||
|
(list (list (make-symbol "_.0") (make-symbol "_.0"))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"reify-distinct-unbound-distinct-names"
|
||||||
|
(run* q (fresh (x y) (== q (list x y x y))))
|
||||||
|
(list
|
||||||
|
(list
|
||||||
|
(make-symbol "_.0")
|
||||||
|
(make-symbol "_.1")
|
||||||
|
(make-symbol "_.0")
|
||||||
|
(make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; --- conde + run* ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-conde-three"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conde ((== q 1)) ((== q 2)) ((== q 3))))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-conde-fresh-mix"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(conde ((fresh (x) (== q (list 1 x)))) ((== q "ground"))))
|
||||||
|
(list (list 1 (make-symbol "_.0")) "ground"))
|
||||||
|
|
||||||
|
;; --- run* + conjunction ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-conj-binds-q"
|
||||||
|
(run* q (fresh (x) (== x 5) (== q (list x x))))
|
||||||
|
(list (list 5 5)))
|
||||||
|
|
||||||
|
;; --- run* + condu ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-condu-first-wins"
|
||||||
|
(run* q (condu ((== q 1)) ((== q 2))))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-onceo-trim"
|
||||||
|
(run* q (onceo (conde ((== q "a")) ((== q "b")))))
|
||||||
|
(list "a"))
|
||||||
|
|
||||||
|
;; --- multi-goal run ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"run*-three-goals"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x y z)
|
||||||
|
(== x 1)
|
||||||
|
(== y 2)
|
||||||
|
(== z 3)
|
||||||
|
(== q (list x y z))))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
46
lib/minikanren/tests/selecto.sx
Normal file
46
lib/minikanren/tests/selecto.sx
Normal file
@@ -0,0 +1,46 @@
|
|||||||
|
;; lib/minikanren/tests/selecto.sx — choose an element + rest of list.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-enumerate"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x r)
|
||||||
|
(selecto x r (list 1 2 3))
|
||||||
|
(== q (list x r))))
|
||||||
|
(list
|
||||||
|
(list 1 (list 2 3))
|
||||||
|
(list 2 (list 1 3))
|
||||||
|
(list 3 (list 1 2))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-find-rest"
|
||||||
|
(run* q (selecto 2 q (list 1 2 3)))
|
||||||
|
(list (list 1 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-find-element"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(selecto
|
||||||
|
q
|
||||||
|
(list 1 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-element-not-present-fails"
|
||||||
|
(run* q (selecto 99 q (list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-empty-list-fails"
|
||||||
|
(run* q (selecto q (list) (list)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"selecto-singleton"
|
||||||
|
(run* q (fresh (x r) (selecto x r (list :only)) (== q (list x r))))
|
||||||
|
(list (list :only (list))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
40
lib/minikanren/tests/sortedo.sx
Normal file
40
lib/minikanren/tests/sortedo.sx
Normal file
@@ -0,0 +1,40 @@
|
|||||||
|
;; lib/minikanren/tests/sortedo.sx — checks list is non-decreasing.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-empty"
|
||||||
|
(run* q (sortedo (list)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-singleton"
|
||||||
|
(run* q (sortedo (list 42)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-ascending"
|
||||||
|
(run* q (sortedo (list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-with-equal-adjacent"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(sortedo (list 1 1 2 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-out-of-order-fails"
|
||||||
|
(run* q (sortedo (list 1 3 2)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-descending-fails"
|
||||||
|
(run* q (sortedo (list 3 2 1)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sortedo-pair-equal"
|
||||||
|
(run* q (sortedo (list 5 5)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
60
lib/minikanren/tests/subo.sx
Normal file
60
lib/minikanren/tests/subo.sx
Normal file
@@ -0,0 +1,60 @@
|
|||||||
|
;; lib/minikanren/tests/subo.sx — contiguous-sublist relation.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-simple-found"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subo
|
||||||
|
(list 2 3)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-not-contiguous-fails"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subo
|
||||||
|
(list 2 4)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-full-list-found"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subo
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-empty-list-found"
|
||||||
|
(let
|
||||||
|
((res (run* q (subo (list) (list 1 2 3)))))
|
||||||
|
(= (len res) 4))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-prefix"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subo
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-suffix"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subo
|
||||||
|
(list 3 4)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subo-strings"
|
||||||
|
(run* q (subo (list "b" "c") (list "a" "b" "c" "d")))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
62
lib/minikanren/tests/subseto.sx
Normal file
62
lib/minikanren/tests/subseto.sx
Normal file
@@ -0,0 +1,62 @@
|
|||||||
|
;; lib/minikanren/tests/subseto.sx — every element of l1 is in l2.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-empty"
|
||||||
|
(run* q (subseto (list) (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-singleton-yes"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subseto (list 2) (list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-singleton-no"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subseto (list 99) (list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-multi-yes"
|
||||||
|
(run
|
||||||
|
1
|
||||||
|
q
|
||||||
|
(subseto
|
||||||
|
(list 1 3)
|
||||||
|
(list 1 2 3 4)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-multi-no"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(subseto
|
||||||
|
(list 1 99)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"subseto-equal-sets"
|
||||||
|
(run
|
||||||
|
1
|
||||||
|
q
|
||||||
|
(subseto
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
;; allow duplicates in l1 — each just needs membership in l2.
|
||||||
|
(mk-test
|
||||||
|
"subseto-duplicates-allowed"
|
||||||
|
(run
|
||||||
|
1
|
||||||
|
q
|
||||||
|
(subseto
|
||||||
|
(list 1 1 2)
|
||||||
|
(list 1 2 3)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
44
lib/minikanren/tests/sum-product.sx
Normal file
44
lib/minikanren/tests/sum-product.sx
Normal file
@@ -0,0 +1,44 @@
|
|||||||
|
;; lib/minikanren/tests/sum-product.sx — fold list to integer.
|
||||||
|
|
||||||
|
(mk-test "sumo-empty" (run* q (sumo (list) q)) (list 0))
|
||||||
|
(mk-test
|
||||||
|
"sumo-1-to-5"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(sumo (list 1 2 3 4 5) q))
|
||||||
|
(list 15))
|
||||||
|
(mk-test
|
||||||
|
"sumo-zeros"
|
||||||
|
(run* q (sumo (list 0 0 0) q))
|
||||||
|
(list 0))
|
||||||
|
(mk-test
|
||||||
|
"sumo-negs"
|
||||||
|
(run* q (sumo (list 5 -3 8) q))
|
||||||
|
(list 10))
|
||||||
|
|
||||||
|
(mk-test "producto-empty" (run* q (producto (list) q)) (list 1))
|
||||||
|
(mk-test
|
||||||
|
"producto-1-to-4"
|
||||||
|
(run* q (producto (list 1 2 3 4) q))
|
||||||
|
(list 24))
|
||||||
|
(mk-test
|
||||||
|
"producto-with-0"
|
||||||
|
(run* q (producto (list 5 0 7) q))
|
||||||
|
(list 0))
|
||||||
|
(mk-test
|
||||||
|
"producto-of-1s"
|
||||||
|
(run* q (producto (list 1 1 1) q))
|
||||||
|
(list 1))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"sum-product-pythagorean-square"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(s sq2)
|
||||||
|
(sumo (list 3 4 5) s)
|
||||||
|
(producto (list 3 3) sq2)
|
||||||
|
(== q (list s sq2))))
|
||||||
|
(list (list 12 9)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
32
lib/minikanren/tests/swap-firsto.sx
Normal file
32
lib/minikanren/tests/swap-firsto.sx
Normal file
@@ -0,0 +1,32 @@
|
|||||||
|
;; lib/minikanren/tests/swap-firsto.sx — swap first two elements.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"swap-firsto-pair"
|
||||||
|
(run* q (swap-firsto (list 1 2) q))
|
||||||
|
(list (list 2 1)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"swap-firsto-with-tail"
|
||||||
|
(run* q (swap-firsto (list 1 2 3 4) q))
|
||||||
|
(list (list 2 1 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"swap-firsto-singleton-fails"
|
||||||
|
(run* q (swap-firsto (list 1) q))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
(mk-test "swap-firsto-empty-fails" (run* q (swap-firsto (list) q)) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"swap-firsto-self-inverse"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh (mid) (swap-firsto (list :a :b :c :d) mid) (swap-firsto mid q)))
|
||||||
|
(list (list :a :b :c :d)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"swap-firsto-backward"
|
||||||
|
(run* q (swap-firsto q (list :y :x :z)))
|
||||||
|
(list (list :x :y :z)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
92
lib/minikanren/tests/take-drop.sx
Normal file
92
lib/minikanren/tests/take-drop.sx
Normal file
@@ -0,0 +1,92 @@
|
|||||||
|
;; lib/minikanren/tests/take-drop.sx — Peano-indexed prefix/suffix.
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-nat
|
||||||
|
(fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
|
||||||
|
|
||||||
|
;; --- tako ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"tako-zero"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(tako (mk-nat 0) (list 1 2 3) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"tako-two"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(tako
|
||||||
|
(mk-nat 2)
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
q))
|
||||||
|
(list (list 1 2)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"tako-all"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(tako (mk-nat 3) (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"tako-too-many"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(tako (mk-nat 5) (list 1 2 3) q))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- dropo ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"dropo-zero"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(dropo (mk-nat 0) (list 1 2 3) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"dropo-two"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(dropo
|
||||||
|
(mk-nat 2)
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
q))
|
||||||
|
(list (list 3 4 5)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"dropo-all"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(dropo (mk-nat 3) (list 1 2 3) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"dropo-too-many"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(dropo (mk-nat 5) (list 1 2 3) q))
|
||||||
|
(list))
|
||||||
|
|
||||||
|
;; --- take + drop round-trip ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"tako-dropo-roundtrip"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(p s)
|
||||||
|
(tako
|
||||||
|
(mk-nat 2)
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
p)
|
||||||
|
(dropo
|
||||||
|
(mk-nat 2)
|
||||||
|
(list 1 2 3 4 5)
|
||||||
|
s)
|
||||||
|
(appendo p s q)))
|
||||||
|
(list (list 1 2 3 4 5)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
52
lib/minikanren/tests/types.sx
Normal file
52
lib/minikanren/tests/types.sx
Normal file
@@ -0,0 +1,52 @@
|
|||||||
|
;; lib/minikanren/tests/types.sx — type-predicate goals.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"numbero-on-int"
|
||||||
|
(run* q (numbero 5))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "numbero-on-string" (run* q (numbero "5")) (list))
|
||||||
|
(mk-test "numbero-on-symbol" (run* q (numbero (quote x))) (list))
|
||||||
|
(mk-test "numbero-on-list" (run* q (numbero (list 1))) (list))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"stringo-on-string"
|
||||||
|
(run* q (stringo "hi"))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "stringo-on-int" (run* q (stringo 5)) (list))
|
||||||
|
(mk-test
|
||||||
|
"stringo-on-keyword"
|
||||||
|
(run* q (stringo :k))
|
||||||
|
(list (make-symbol "_.0"))) ;; SX keywords ARE strings
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"symbolo-on-symbol"
|
||||||
|
(run* q (symbolo (quote x)))
|
||||||
|
(list (make-symbol "_.0")))
|
||||||
|
(mk-test "symbolo-on-string" (run* q (symbolo "x")) (list))
|
||||||
|
(mk-test "symbolo-on-int" (run* q (symbolo 5)) (list))
|
||||||
|
|
||||||
|
;; --- combine with membero for type-filtered enumeration ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"membero-numbero-filter"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(membero x (list 1 "a" 2 "b" 3))
|
||||||
|
(numbero x)
|
||||||
|
(== q x)))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"membero-stringo-filter"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(fresh
|
||||||
|
(x)
|
||||||
|
(membero x (list 1 "a" 2 "b" 3))
|
||||||
|
(stringo x)
|
||||||
|
(== q x)))
|
||||||
|
(list "a" "b"))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
293
lib/minikanren/tests/unify.sx
Normal file
293
lib/minikanren/tests/unify.sx
Normal file
@@ -0,0 +1,293 @@
|
|||||||
|
;; lib/minikanren/tests/unify.sx — Phase 1 tests for unify.sx.
|
||||||
|
;;
|
||||||
|
;; Loads into a session that already has lib/guest/match.sx and
|
||||||
|
;; lib/minikanren/unify.sx defined. Tests are top-level forms.
|
||||||
|
;; Call (mk-tests-run!) afterwards to get the totals.
|
||||||
|
;;
|
||||||
|
;; Note: SX dict equality is reference-based, so tests check the *effect*
|
||||||
|
;; of a unification (success/failure flag, or walked bindings) rather than
|
||||||
|
;; the raw substitution dict.
|
||||||
|
|
||||||
|
(define mk-test-pass 0)
|
||||||
|
(define mk-test-fail 0)
|
||||||
|
(define mk-test-fails (list))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-test
|
||||||
|
(fn
|
||||||
|
(name actual expected)
|
||||||
|
(if
|
||||||
|
(= actual expected)
|
||||||
|
(set! mk-test-pass (+ mk-test-pass 1))
|
||||||
|
(begin
|
||||||
|
(set! mk-test-fail (+ mk-test-fail 1))
|
||||||
|
(append! mk-test-fails {:name name :expected expected :actual actual})))))
|
||||||
|
|
||||||
|
(define mk-tests-run! (fn () {:total (+ mk-test-pass mk-test-fail) :passed mk-test-pass :failed mk-test-fail :fails mk-test-fails}))
|
||||||
|
|
||||||
|
(define mk-unified? (fn (s) (if (= s nil) false true)))
|
||||||
|
|
||||||
|
;; --- fresh variable construction ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"make-var-distinct"
|
||||||
|
(let ((a (make-var)) (b (make-var))) (= (var-name a) (var-name b)))
|
||||||
|
false)
|
||||||
|
|
||||||
|
(mk-test "make-var-is-var" (mk-var? (make-var)) true)
|
||||||
|
(mk-test "var?-num" (mk-var? 5) false)
|
||||||
|
(mk-test "var?-list" (mk-var? (list 1 2)) false)
|
||||||
|
(mk-test "var?-string" (mk-var? "hi") false)
|
||||||
|
(mk-test "var?-empty" (mk-var? (list)) false)
|
||||||
|
(mk-test "var?-bool" (mk-var? true) false)
|
||||||
|
|
||||||
|
;; --- empty substitution ---
|
||||||
|
|
||||||
|
(mk-test "empty-s-walk-num" (mk-walk 5 empty-s) 5)
|
||||||
|
(mk-test "empty-s-walk-str" (mk-walk "x" empty-s) "x")
|
||||||
|
(mk-test
|
||||||
|
"empty-s-walk-list"
|
||||||
|
(mk-walk (list 1 2) empty-s)
|
||||||
|
(list 1 2))
|
||||||
|
(mk-test
|
||||||
|
"empty-s-walk-unbound-var"
|
||||||
|
(let ((x (make-var))) (= (mk-walk x empty-s) x))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- walk: top-level chain resolution ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk-direct-binding"
|
||||||
|
(mk-walk (mk-var "x") (extend "x" 7 empty-s))
|
||||||
|
7)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk-two-step-chain"
|
||||||
|
(mk-walk
|
||||||
|
(mk-var "x")
|
||||||
|
(extend "x" (mk-var "y") (extend "y" 9 empty-s)))
|
||||||
|
9)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk-three-step-chain"
|
||||||
|
(mk-walk
|
||||||
|
(mk-var "a")
|
||||||
|
(extend
|
||||||
|
"a"
|
||||||
|
(mk-var "b")
|
||||||
|
(extend "b" (mk-var "c") (extend "c" 42 empty-s))))
|
||||||
|
42)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk-stops-at-list"
|
||||||
|
(mk-walk (list 1 (mk-var "x")) (extend "x" 5 empty-s))
|
||||||
|
(list 1 (mk-var "x")))
|
||||||
|
|
||||||
|
;; --- walk*: deep walk into lists ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk*-flat-list-with-vars"
|
||||||
|
(mk-walk*
|
||||||
|
(list (mk-var "x") 2 (mk-var "y"))
|
||||||
|
(extend "x" 1 (extend "y" 3 empty-s)))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk*-nested-list"
|
||||||
|
(mk-walk*
|
||||||
|
(list 1 (mk-var "x") (list 2 (mk-var "y")))
|
||||||
|
(extend "x" 5 (extend "y" 6 empty-s)))
|
||||||
|
(list 1 5 (list 2 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"walk*-unbound-stays-var"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(= (mk-walk* (list 1 x) empty-s) (list 1 x)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test "walk*-atom" (mk-walk* 5 empty-s) 5)
|
||||||
|
|
||||||
|
;; --- unify atoms (success / failure semantics, not dict shape) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-num-eq-succeeds"
|
||||||
|
(mk-unified? (mk-unify 5 5 empty-s))
|
||||||
|
true)
|
||||||
|
(mk-test "unify-num-neq-fails" (mk-unify 5 6 empty-s) nil)
|
||||||
|
(mk-test
|
||||||
|
"unify-str-eq-succeeds"
|
||||||
|
(mk-unified? (mk-unify "a" "a" empty-s))
|
||||||
|
true)
|
||||||
|
(mk-test "unify-str-neq-fails" (mk-unify "a" "b" empty-s) nil)
|
||||||
|
(mk-test
|
||||||
|
"unify-bool-eq-succeeds"
|
||||||
|
(mk-unified? (mk-unify true true empty-s))
|
||||||
|
true)
|
||||||
|
(mk-test "unify-bool-neq-fails" (mk-unify true false empty-s) nil)
|
||||||
|
(mk-test
|
||||||
|
"unify-nil-eq-succeeds"
|
||||||
|
(mk-unified? (mk-unify nil nil empty-s))
|
||||||
|
true)
|
||||||
|
(mk-test
|
||||||
|
"unify-empty-list-succeeds"
|
||||||
|
(mk-unified? (mk-unify (list) (list) empty-s))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- unify var with anything (walk to verify binding) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-var-num-binds"
|
||||||
|
(mk-walk (mk-var "x") (mk-unify (mk-var "x") 5 empty-s))
|
||||||
|
5)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-num-var-binds"
|
||||||
|
(mk-walk (mk-var "x") (mk-unify 5 (mk-var "x") empty-s))
|
||||||
|
5)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-var-list-binds"
|
||||||
|
(mk-walk
|
||||||
|
(mk-var "x")
|
||||||
|
(mk-unify (mk-var "x") (list 1 2) empty-s))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-var-var-same-no-extend"
|
||||||
|
(mk-unified? (mk-unify (mk-var "x") (mk-var "x") empty-s))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-var-var-different-walks-equal"
|
||||||
|
(let
|
||||||
|
((s (mk-unify (mk-var "x") (mk-var "y") empty-s)))
|
||||||
|
(= (mk-walk (mk-var "x") s) (mk-walk (mk-var "y") s)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
;; --- unify lists positionally ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-equal-succeeds"
|
||||||
|
(mk-unified?
|
||||||
|
(mk-unify
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2 3)
|
||||||
|
empty-s))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-different-length-fails-1"
|
||||||
|
(mk-unify
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 2 3)
|
||||||
|
empty-s)
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-different-length-fails-2"
|
||||||
|
(mk-unify
|
||||||
|
(list 1 2 3)
|
||||||
|
(list 1 2)
|
||||||
|
empty-s)
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-mismatch-fails"
|
||||||
|
(mk-unify
|
||||||
|
(list 1 2)
|
||||||
|
(list 1 3)
|
||||||
|
empty-s)
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-vs-atom-fails"
|
||||||
|
(mk-unify (list 1 2) 5 empty-s)
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-empty-vs-non-empty-fails"
|
||||||
|
(mk-unify (list) (list 1) empty-s)
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-list-with-vars-walks"
|
||||||
|
(mk-walk*
|
||||||
|
(list (mk-var "x") (mk-var "y"))
|
||||||
|
(mk-unify
|
||||||
|
(list (mk-var "x") (mk-var "y"))
|
||||||
|
(list 1 2)
|
||||||
|
empty-s))
|
||||||
|
(list 1 2))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-nested-lists-with-vars-walks"
|
||||||
|
(mk-walk*
|
||||||
|
(list (mk-var "x") (list (mk-var "y") 3))
|
||||||
|
(mk-unify
|
||||||
|
(list (mk-var "x") (list (mk-var "y") 3))
|
||||||
|
(list 1 (list 2 3))
|
||||||
|
empty-s))
|
||||||
|
(list 1 (list 2 3)))
|
||||||
|
|
||||||
|
;; --- unify chained substitutions ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-chain-var-var-then-atom"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")) (y (mk-var "y")))
|
||||||
|
(let
|
||||||
|
((s1 (mk-unify x y empty-s)))
|
||||||
|
(mk-walk x (mk-unify y 7 s1))))
|
||||||
|
7)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-already-bound-consistent"
|
||||||
|
(let
|
||||||
|
((s (extend "x" 5 empty-s)))
|
||||||
|
(mk-unified? (mk-unify (mk-var "x") 5 s)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-already-bound-conflict-fails"
|
||||||
|
(let
|
||||||
|
((s (extend "x" 5 empty-s)))
|
||||||
|
(mk-unify (mk-var "x") 6 s))
|
||||||
|
nil)
|
||||||
|
|
||||||
|
;; --- occurs check (opt-in) ---
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-no-occurs-default-succeeds"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-unified? (mk-unify x (list 1 x) empty-s)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-occurs-direct-fails"
|
||||||
|
(let ((x (mk-var "x"))) (mk-unify-check x (list 1 x) empty-s))
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-occurs-nested-fails"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-unify-check x (list 1 (list 2 x)) empty-s))
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-occurs-non-occurring-succeeds"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")))
|
||||||
|
(mk-unified? (mk-unify-check x 5 empty-s)))
|
||||||
|
true)
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"unify-occurs-via-chain-fails"
|
||||||
|
(let
|
||||||
|
((x (mk-var "x")) (y (mk-var "y")))
|
||||||
|
(let ((s (extend "y" (list x) empty-s))) (mk-unify-check x y s)))
|
||||||
|
nil)
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
82
lib/minikanren/unify.sx
Normal file
82
lib/minikanren/unify.sx
Normal file
@@ -0,0 +1,82 @@
|
|||||||
|
;; lib/minikanren/unify.sx — Phase 1 + cons-cell extension.
|
||||||
|
;;
|
||||||
|
;; miniKanren-on-SX, built on lib/guest/match.sx. The kit ships the heavy
|
||||||
|
;; lifting (walk-with, unify-with, occurs-with, extend, empty-subst,
|
||||||
|
;; mk-var/is-var?/var-name); this file supplies a miniKanren-shaped cfg
|
||||||
|
;; and a thin public API.
|
||||||
|
;;
|
||||||
|
;; Term shapes:
|
||||||
|
;; logic var : (:var NAME) — kit's mk-var
|
||||||
|
;; cons cell : (:cons HEAD TAIL) — for relational programming
|
||||||
|
;; (built by mk-cons; lets relations decompose lists by
|
||||||
|
;; head/tail without proper improper pairs in the host)
|
||||||
|
;; native list : SX list (a b c) — also unifies pair-style:
|
||||||
|
;; args = (head, tail) so (1 2 3) ≡ (:cons 1 (:cons 2 (:cons 3 ())))
|
||||||
|
;; atom : number / string / symbol / boolean / nil / ()
|
||||||
|
;;
|
||||||
|
;; Substitution: SX dict mapping VAR-NAME → term. Empty = (empty-subst).
|
||||||
|
|
||||||
|
(define mk-cons (fn (h t) (list :cons h t)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-cons-cell?
|
||||||
|
(fn (t) (and (list? t) (not (empty? t)) (= (first t) :cons))))
|
||||||
|
|
||||||
|
(define mk-cons-head (fn (t) (nth t 1)))
|
||||||
|
(define mk-cons-tail (fn (t) (nth t 2)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-list-pair?
|
||||||
|
(fn (t) (and (list? t) (not (empty? t)) (not (is-var? t)))))
|
||||||
|
|
||||||
|
(define mk-list-pair-head (fn (t) :pair))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-list-pair-args
|
||||||
|
(fn
|
||||||
|
(t)
|
||||||
|
(cond
|
||||||
|
((mk-cons-cell? t) (list (mk-cons-head t) (mk-cons-tail t)))
|
||||||
|
(:else (list (first t) (rest t))))))
|
||||||
|
|
||||||
|
(define mk-cfg {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? false :var-name var-name :ctor-args mk-list-pair-args})
|
||||||
|
|
||||||
|
(define mk-cfg-occurs {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? true :var-name var-name :ctor-args mk-list-pair-args})
|
||||||
|
|
||||||
|
(define empty-s (empty-subst))
|
||||||
|
|
||||||
|
(define mk-fresh-counter 0)
|
||||||
|
|
||||||
|
(define
|
||||||
|
make-var
|
||||||
|
(fn
|
||||||
|
()
|
||||||
|
(begin
|
||||||
|
(set! mk-fresh-counter (+ mk-fresh-counter 1))
|
||||||
|
(mk-var (str "_." mk-fresh-counter)))))
|
||||||
|
|
||||||
|
(define mk-var? is-var?)
|
||||||
|
|
||||||
|
(define mk-walk (fn (t s) (walk-with mk-cfg t s)))
|
||||||
|
|
||||||
|
(define
|
||||||
|
mk-walk*
|
||||||
|
(fn
|
||||||
|
(t s)
|
||||||
|
(let
|
||||||
|
((w (mk-walk t s)))
|
||||||
|
(cond
|
||||||
|
((mk-cons-cell? w)
|
||||||
|
(let
|
||||||
|
((h (mk-walk* (mk-cons-head w) s))
|
||||||
|
(tl (mk-walk* (mk-cons-tail w) s)))
|
||||||
|
(cond
|
||||||
|
((empty? tl) (list h))
|
||||||
|
((mk-cons-cell? tl) tl)
|
||||||
|
((list? tl) (cons h tl))
|
||||||
|
(:else (mk-cons h tl)))))
|
||||||
|
((mk-list-pair? w) (map (fn (a) (mk-walk* a s)) w))
|
||||||
|
(:else w)))))
|
||||||
|
|
||||||
|
(define mk-unify (fn (u v s) (unify-with mk-cfg u v s)))
|
||||||
|
(define mk-unify-check (fn (u v s) (unify-with mk-cfg-occurs u v s)))
|
||||||
@@ -50,68 +50,106 @@ Key semantic mappings:
|
|||||||
## Roadmap
|
## Roadmap
|
||||||
|
|
||||||
### Phase 1 — variables + unification
|
### Phase 1 — variables + unification
|
||||||
- [ ] `make-var` → fresh logic variable (unique mutable box)
|
- [x] `make-var` → fresh logic variable (unique mutable box)
|
||||||
- [ ] `var?` `v` → bool — is this a logic variable?
|
- [x] `var?` `v` → bool — is this a logic variable?
|
||||||
- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
|
- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
|
||||||
- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
|
- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
|
||||||
- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
|
- [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
|
||||||
Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
|
Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
|
||||||
No occurs check by default; `unify-check` with occurs check as opt-in.
|
No occurs check by default; `unify-check` with occurs check as opt-in.
|
||||||
- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list)
|
- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
|
||||||
- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
|
- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
|
||||||
|
|
||||||
### Phase 2 — streams + goals
|
### Phase 2 — streams + goals
|
||||||
- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`),
|
- [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave),
|
||||||
`mplus` (interleave two streams), `bind` (apply goal to stream)
|
`mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host
|
||||||
- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy
|
`bind` primitive that silently shadows user defines.
|
||||||
- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))`
|
- [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends
|
||||||
- [ ] `succeed` / `fail` — trivial goals
|
and swaps when its left operand is paused, giving fair interleaving.
|
||||||
- [ ] `fresh` — `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many
|
- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))`
|
||||||
- [ ] `conde` — interleaving disjunction of goal lists
|
- [x] `==-check` — opt-in occurs-checked equality goal
|
||||||
- [ ] `condu` — committed choice (soft-cut): only explores first successful clause
|
- [x] `succeed` / `fail` — trivial goals
|
||||||
- [ ] `onceo` — succeeds at most once
|
- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction
|
||||||
- [ ] Tests: basic goal composition, backtracking, interleaving
|
- [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde`
|
||||||
|
adds the implicit-conj-per-clause sugar later)
|
||||||
|
- [x] `fresh` — introduces logic variables inside a goal body. Implemented as a
|
||||||
|
defmacro: `(fresh (x y) g1 g2 ...)` ⇒ `(let ((x (make-var)) (y (make-var)))
|
||||||
|
(mk-conj g1 g2 ...))`. Also `call-fresh` for programmatic goal building.
|
||||||
|
- [x] `conde` — sugar over disj+conj, one row per clause; defmacro that
|
||||||
|
wraps each clause body in `mk-conj` and folds via `mk-disj`. Notes:
|
||||||
|
with eager streams ordering is left-clause-first DFS; true interleaving
|
||||||
|
requires paused thunks (Phase 4 recursive relations).
|
||||||
|
- [x] `condu` — committed choice. defmacro folding clauses into a runtime
|
||||||
|
`condu-try` walker; first clause whose head goal yields a non-empty
|
||||||
|
stream commits its first answer, rest-goals run on that single subst.
|
||||||
|
- [x] `onceo` — `(stream-take 1 (g s))`; trims a goal's stream to ≤1 answer.
|
||||||
|
- [x] Tests: basic goal composition, backtracking, interleaving (110 cumulative)
|
||||||
|
|
||||||
### Phase 3 — run + reification
|
### Phase 3 — run + reification
|
||||||
- [ ] `run*` `goal` → list of all answers (reified)
|
- [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as
|
||||||
- [ ] `run n` `goal` → list of first n answers
|
fresh var, conj goals, take all from stream, reify each.
|
||||||
- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names
|
- [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all)
|
||||||
- [ ] `reify-s` → builds reification substitution for naming unbound vars consistently
|
- [x] `reify` `term` `subst` → walk* + build reification subst + walk* again
|
||||||
- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar
|
- [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a
|
||||||
- [ ] Query variable conventions: `q` as canonical query variable
|
`_.N` symbol via `(make-symbol (str "_." n))`
|
||||||
- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
|
- [x] `fresh` with multiple variables — already shipped Phase 2B.
|
||||||
|
- [x] Query variable conventions: `q` as canonical query variable (matches TRS)
|
||||||
|
- [x] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
|
||||||
`(run* q (conde ((== q 1)) ((== q 2))))` → `(1 2)`,
|
`(run* q (conde ((== q 1)) ((== q 2))))` → `(1 2)`,
|
||||||
Peano arithmetic, `appendo` preview
|
`(run* q (fresh (x y) (== q (list x y))))` → `((_.0 _.1))`. Peano +
|
||||||
|
`appendo` deferred to Phase 4.
|
||||||
|
|
||||||
### Phase 4 — standard relations
|
### Phase 4 — standard relations
|
||||||
- [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards
|
- [x] `appendo` `l` `s` `ls` — list append, runs forwards AND backwards.
|
||||||
- [ ] `membero` `x` `l` — x is a member of l
|
Canary green: `(run* q (appendo (1 2) (3 4) q))` → `((1 2 3 4))`;
|
||||||
- [ ] `listo` `l` — l is a proper list
|
`(run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s))))` →
|
||||||
- [ ] `nullo` `l` — l is empty
|
all four splits.
|
||||||
- [ ] `pairo` `p` — p is a pair (cons cell)
|
- [x] `membero` `x` `l` — enumerates: `(run* q (membero q (a b c)))` → `(a b c)`
|
||||||
- [ ] `caro` `p` `a` — car of pair
|
- [x] `listo` `l` — l is a proper list; enumerates list shapes with laziness
|
||||||
- [ ] `cdro` `p` `d` — cdr of pair
|
- [x] `nullo` `l` — l is empty
|
||||||
- [ ] `conso` `a` `d` `p` — cons
|
- [x] `pairo` `p` — p is a (non-empty) cons-cell / list
|
||||||
- [ ] `firsto` / `resto` — aliases for caro/cdro
|
- [x] `caro` / `cdro` / `conso` / `firsto` / `resto`
|
||||||
- [ ] `reverseo` `l` `r` — reverse of list
|
- [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean,
|
||||||
- [ ] `flatteno` `l` `f` — flatten nested lists
|
`run*` diverges due to interleaved unbounded list search (canonical TRS issue).
|
||||||
- [ ] `permuteo` `l` `p` — permutation of list
|
- [x] `flatteno` `l` `f` — flatten nested lists. Three conde clauses:
|
||||||
- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer)
|
empty → empty; pair → recurse on car & cdr + appendo; otherwise atom →
|
||||||
- [ ] Tests: run each relation forwards and backwards; generate from partial inputs
|
`(== flat (list tree))`. Atom-ness is asserted via `nafc (nullo tree)
|
||||||
|
+ nafc (pairo tree)` — both succeed only when tree is a ground non-list.
|
||||||
|
Works on ground inputs.
|
||||||
|
- [x] `permuteo` `l` `p` — permutation of list. Built on `inserto` (insert at any
|
||||||
|
position) and recursive permutation of tail. All 6 perms of (1 2 3) generated
|
||||||
|
forward; backward `run 1 q (permuteo q (a b c))` finds the input.
|
||||||
|
- [x] `lengtho` `l` `n` — length as a relation, Peano-encoded:
|
||||||
|
`:z` / `(:s :z)` / `(:s (:s :z))` ... matches TRS. Forward is direct;
|
||||||
|
backward enumerates lists of a given length.
|
||||||
|
- [x] Tests: run each relation forwards and backwards (so far 25 in
|
||||||
|
`tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
|
||||||
|
|
||||||
### Phase 5 — `project` + `matche` + negation
|
### Phase 5 — `project` + `matche` + negation
|
||||||
- [ ] `project` `(x ...) body` — access reified values of logic vars inside a goal;
|
- [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
|
||||||
escapes to ground values for arithmetic or string ops
|
in the body's lexical scope, then runs `(mk-conj body...)` on the same
|
||||||
- [ ] `matche` — pattern matching over logic terms (extension from core.logic)
|
substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
|
||||||
`(matche l ((head . tail) goal) (() goal))`
|
- [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` /
|
||||||
- [ ] `conda` — soft-cut disjunction (like Prolog `->`)
|
symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes
|
||||||
- [ ] `condu` — committed choice (already in phase 2; refine semantics here)
|
`(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol
|
||||||
- [ ] `nafc` — negation as finite failure with constraint
|
names in a pattern produce the same fresh var, so they unify (== check).
|
||||||
|
Built without quasiquote (the expander does not recurse into lambda
|
||||||
|
bodies). Fixed-length list patterns only — head/tail destructuring uses
|
||||||
|
`(fresh (a d) (conso a d target) body)` directly.
|
||||||
|
- [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
|
||||||
|
flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
|
||||||
|
- [x] `condu` — committed choice (Phase 2)
|
||||||
|
- [x] `nafc` — negation as finite failure: `(nafc g)` yields the input subst
|
||||||
|
iff g has zero answers. Standard caveats apply (open-world unsoundness;
|
||||||
|
diverges if g is infinite). `Phase 5 piece C`.
|
||||||
- [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche`
|
- [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche`
|
||||||
|
|
||||||
### Phase 6 — arithmetic constraints CLP(FD)
|
### Phase 6 — arithmetic constraints CLP(FD)
|
||||||
- [ ] Finite domain variables: `fd-var` with domain `[lo..hi]`
|
- [ ] Finite domain variables: `fd-var` with domain `[lo..hi]`
|
||||||
- [ ] `in` `x` `domain` — constrain x to domain
|
- [x] `ino` `x` `domain` — alias for `(membero x domain)` with the
|
||||||
|
constraint-store-friendly argument order. Sufficient for the
|
||||||
|
enumerate-then-filter style of finite-domain solving.
|
||||||
|
- [x] `all-distincto` `l` — pairwise-distinct elements via `nafc + membero`.
|
||||||
- [ ] `fd-eq` `x` `y` — x = y (constraint propagation)
|
- [ ] `fd-eq` `x` `y` — x = y (constraint propagation)
|
||||||
- [ ] `fd-neq` `x` `y` — x ≠ y
|
- [ ] `fd-neq` `x` `y` — x ≠ y
|
||||||
- [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints
|
- [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints
|
||||||
@@ -135,4 +173,217 @@ _(none yet)_
|
|||||||
|
|
||||||
_Newest first._
|
_Newest first._
|
||||||
|
|
||||||
_(awaiting phase 1)_
|
- **2026-05-08** — **enumerate-i / enumerate-from-i — 500-test milestone**: index-each-element relations. (enumerate-i l result) -> result is l with each element paired with its 0-based index. (enumerate-from-i n l result) starts at n. 5 new tests, **501/501** cumulative.
|
||||||
|
- **2026-05-08** — **partitiono**: relational partition. (partitiono pred l yes no) splits l so yes contains elements where pred succeeds and no contains the rest. Composes with intarith for numeric predicates. 5 new tests, 496/496 cumulative.
|
||||||
|
- **2026-05-08** — **appendo3**: 3-list append via two appendos. (appendo3 a b c r) is (appendo a b mid) ∧ (appendo mid c r). Recovers any of the three lists given the other two and the result. 5 new tests, 491/491 cumulative.
|
||||||
|
- **2026-05-08** — **lengtho-i**: integer-indexed length (intarith). Empty list -> 0; recurse with pluso-i. Drop-in fast replacement for Peano lengtho when the count fits in a host integer. 5 new tests, 486/486 cumulative.
|
||||||
|
- **2026-05-08** — **sumo + producto (intarith)**: fold a list of ground integers to its sum or product. Empty list -> identity (0 / 1). Recurse via pluso-i / *o-i. 9 new tests, 481/481 cumulative.
|
||||||
|
- **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative.
|
||||||
|
- **2026-05-08** — **sortedo (intarith)**: list is non-decreasing under integer ordering. Three conde clauses: empty / singleton / pair-and-recurse. Uses lteo-i for the adjacent-pair check (ground integers). 7 new tests, 463/463 cumulative.
|
||||||
|
- **2026-05-08** — **subseto**: every element of l1 is a member of l2. Recurses on l1, checking each element via membero. Allows duplicates in l1 (each independently in l2). 7 new tests, 456/456 cumulative.
|
||||||
|
- **2026-05-08** — **cycle-free path search**: mitigation for the cyclic-graph divergence — thread a accumulator through the recursion, gate each step with nafc + membero on visited. Terminates on graphs with cycles; no Phase-7 tabling required for the simple case. 3 new tests, 449/449 cumulative.
|
||||||
|
- **2026-05-08** — **removeo-allo**: removes every occurrence of x (vs rembero, which removes only the first). Three conde clauses: empty -> empty; head matches -> skip and recurse; head differs (nafc) -> keep and recurse. 5 new tests, 446/446 cumulative.
|
||||||
|
- **2026-05-08** — **btree-walko (matche showcase)**: walks a binary tree (:leaf v) | (:node l r) and emits each leaf value via conde. Demonstrates matche dispatch on tagged-list patterns, recursion through both branches via conde, and run* enumerating all 5 leaves of a small tree. 4 new tests, 441/441 cumulative.
|
||||||
|
- **2026-05-08** — **swap-firsto**: swap the first two elements of a list. Built via four conso constraints. Self-inverse on length-2+ lists; runs forward and backward. 6 new tests, 437/437 cumulative.
|
||||||
|
- **2026-05-08** — **pairlisto**: relational zip — pairs is the zipped list of (l1[i] l2[i]). Runs forward, recovers l1 given l2 and pairs, recovers l2 given l1 and pairs. 5 new tests, 431/431 cumulative.
|
||||||
|
- **2026-05-08** — **iterate-no**: relational iterated application. Applies a 2-arg relation n times (Peano n) starting from x to produce result. Generalises succ-iteration / list-cons-iteration / etc. 4 new tests, 426/426 cumulative.
|
||||||
|
- **2026-05-08** — **rev-acco / rev-2o**: accumulator-style reversal — faster than appendo-driven reverseo for forward queries because no quadratic appendos. Trade-off: rev-acco is asymmetric (cannot run cleanly backward in run*). 6 new tests, 422/422 cumulative.
|
||||||
|
- **2026-05-08** — **even-i / odd-i (intarith)**: ground-only parity goals via project. Composes with membero for filtered enumeration: -> . 5 new tests, 416/416 cumulative.
|
||||||
|
- **2026-05-08** — **selecto**: classic miniKanren "choose an element + rest". Direct base (l = (x . rest)) plus skip-head recurse. Enumerates all (element, rest) splits in run*; runs forward, backward, mid-pipeline. 6 new tests, 411/411 cumulative.
|
||||||
|
- **2026-05-08** — **subo (contiguous sublist)**: Two appendos chained — l = front ++ s ++ back. Goal order matters: appendo on the ground l first, so the search is finitary; then constrain front. 7 new tests, 405/405 cumulative.
|
||||||
|
- **2026-05-08** — **prefixo + suffixo**: classic appendo-derived sublist relations. (prefixo p l) ≡ p ⊕ ? = l; (suffixo s l) ≡ ? ⊕ s = l. Both enumerate all prefixes/suffixes when given a fresh first arg. 9 new tests, 398/398 cumulative.
|
||||||
|
- **2026-05-08** — **palindromeo**: 2-line definition (reverseo + ==). Succeeds when a list reads the same forwards and backwards. 7 new tests, 389/389 cumulative.
|
||||||
|
- **2026-05-08** — **not-membero**: relational "x is not a member of l".
|
||||||
|
Uses `nafc + ==` per element (the same skeleton all-distincto uses).
|
||||||
|
Useful as a constraint-style filter: `(membero x dom) (not-membero x
|
||||||
|
excluded)`. 4 new tests, 382/382 cumulative.
|
||||||
|
- **2026-05-08** — **repeato + concato**: repeato builds a list of n copies
|
||||||
|
(Peano n); concato is fold-appendo over a list of lists. Both run forward
|
||||||
|
and backward — repeato can recover the count from a uniform list. 10 new
|
||||||
|
tests, 378/378 cumulative.
|
||||||
|
- **2026-05-08** — **tako + dropo (Peano-indexed prefix/suffix)**: takes / drops
|
||||||
|
the first n elements via a Peano-encoded count. Round-trip
|
||||||
|
`(tako n l) ⊕ (dropo n l) = l` holds. 9 new tests, 368/368 cumulative.
|
||||||
|
- **2026-05-08** — **eveno / oddo Peano predicates**: classic miniKanren parity
|
||||||
|
relations. eveno: 0 or successor-of-successor of even; oddo: 1 or
|
||||||
|
successor-of-successor of odd. Both run forward (test) and backward
|
||||||
|
(enumerate). 12 new tests, 359/359 cumulative.
|
||||||
|
- **2026-05-08** — **defrel — Prolog-style relation definition macro**:
|
||||||
|
`(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...)` expands to
|
||||||
|
`(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...)))`.
|
||||||
|
Mirrors Prolog's clause syntax and inherits Zzz-via-conde so recursive
|
||||||
|
relations terminate. 3 new tests, 347/347 cumulative.
|
||||||
|
- **2026-05-08** — **lasto / init-o**: classic head/tail-style list relations.
|
||||||
|
lasto extracts the final element; init-o extracts everything-but-the-last.
|
||||||
|
Together with appendo, the round-trip `init ⊕ (last) = l` holds. 8 new
|
||||||
|
tests, 344/344 cumulative.
|
||||||
|
- **2026-05-08** — **Datalog-style relational database queries**: tests/rdb.sx
|
||||||
|
shows miniKanren as a query engine over fact tables. Defines two tables
|
||||||
|
(employees + project assignments), wraps each with a relation that does
|
||||||
|
membero over the table, then expresses queries: dept filter, salary >
|
||||||
|
threshold (intarith), join engineers ↔ runtime project, find anyone on
|
||||||
|
multiple distinct projects (nafc + ==). 5 new tests, 336/336 cumulative.
|
||||||
|
- **2026-05-08** — **Cyclic graph behaviour test (motivates Phase 7 tabling)**:
|
||||||
|
Demonstrates that naive patho on a 2-cycle generates ever-longer paths.
|
||||||
|
`run 5` truncates to a finite prefix; `run*` would diverge. This is
|
||||||
|
exactly the test case Phase 7 (tabled / SLG resolution) is designed
|
||||||
|
to fix. 3 new tests, 331/331 cumulative.
|
||||||
|
- **2026-05-08** — **numbero / stringo / symbolo (type predicates)**: ground-only
|
||||||
|
type tests via project. Compose with `membero` for type-filtered enumeration:
|
||||||
|
`(fresh (x) (membero x (1 "a" 2 "b" 3)) (numbero x) (== q x))` → `(1 2 3)`.
|
||||||
|
Note: SX keywords are strings, so `(stringo :k)` succeeds. 12 new tests,
|
||||||
|
328/328 cumulative.
|
||||||
|
- **2026-05-08** — **Graph reachability via patho**: classic miniKanren
|
||||||
|
graph search. `edgeo` looks up edges in a fact list via `membero`; `patho`
|
||||||
|
recursively builds paths via direct-edge OR (one edge + recurse + cons).
|
||||||
|
Enumerates all paths between two nodes, including alternates through
|
||||||
|
shortcuts. 6 new tests, 316/316 cumulative.
|
||||||
|
- **2026-05-08** — **everyo / someo (predicate-style relations)**:
|
||||||
|
`(everyo rel l)` — every element of l satisfies rel; `(someo rel l)` —
|
||||||
|
some element does. Both compose with intarith for numeric tests:
|
||||||
|
`(everyo (fn (x) (lto-i x 10)) (list 1 5 9))` succeeds. 10 new tests,
|
||||||
|
310/310 cumulative.
|
||||||
|
- **2026-05-08** — **mapo (relational map) — 300 test milestone**: `(mapo
|
||||||
|
rel l1 l2)` succeeds when l2 is l1 with each element rel-related. Works
|
||||||
|
forward and backward; composes with intarith — `(mapo (fn (a b) (*o-i
|
||||||
|
a a b)) (1 2 3 4) q)` → `((1 4 9 16))`. 7 new tests, **300/300** cumulative.
|
||||||
|
- **2026-05-08** — **samelengtho**: classic miniKanren relation that
|
||||||
|
succeeds when two lists have equal length. Symmetric — works to enumerate
|
||||||
|
both lists fresh: `(run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q
|
||||||
|
(list l1 l2))))` produces empty/empty, then 1-elem pairs, then 2-elem.
|
||||||
|
5 new tests, 293/293 cumulative.
|
||||||
|
- **2026-05-08** — **Pythagorean triples (intarith showcase)**: search for
|
||||||
|
(a, b, c) ∈ [1..10]³, a ≤ b, a² + b² = c² via `ino + lteo-i + *o-i +
|
||||||
|
pluso-i + ==`. Finds exactly `(3 4 5)` and `(6 8 10)`. Demonstrates the
|
||||||
|
enumerate-then-filter pattern with intarith escape into host arithmetic.
|
||||||
|
1 new test, 288/288 cumulative.
|
||||||
|
- **2026-05-08** — **intarith.sx — fast ground-only integer arithmetic**:
|
||||||
|
pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic
|
||||||
|
via `project`. They are not relational like Peano `pluso` (require args
|
||||||
|
to walk to numbers), but run at native host speed — a viable escape
|
||||||
|
hatch when puzzle size makes Peano impractical. Composes with relational
|
||||||
|
goals: `(membero x dom) (lto-i x 3)` filters dom by `< 3`. 18 new tests,
|
||||||
|
287/287 cumulative.
|
||||||
|
- **2026-05-08** — **2x2 Latin square**: small classic constraint demo using
|
||||||
|
`ino` + 4 `all-distincto` constraints. Enumerates exactly 2 squares
|
||||||
|
(`((1 2)(2 1))` and `((2 1)(1 2))`); a clue (top-left = 1) narrows to one.
|
||||||
|
3 new tests, 269/269 cumulative. Note: 3x3 (12 squares) is the natural
|
||||||
|
showcase but too slow under naive enumerate-then-filter — needs Phase 6
|
||||||
|
arc-consistency.
|
||||||
|
- **2026-05-08** — **rembero / assoco / nth-o**: more standard list relations.
|
||||||
|
rembero removes the first occurrence (uses `nafc (== a x)` to gate the
|
||||||
|
skip clause, so it's well-defined on ground lists). assoco is alist
|
||||||
|
lookup — works forward (key → value) and backward (value → key). nth-o
|
||||||
|
uses Peano indices into a list. 13 new tests, 266/266 cumulative.
|
||||||
|
- **2026-05-08** — **flatteno**: nested-list flattener via conde + appendo.
|
||||||
|
Atom-ness is detected via `nafc (nullo ...) + nafc (pairo ...)` so the
|
||||||
|
third clause only fires when the input is a ground non-list. Works for
|
||||||
|
`()` / atoms / flat lists / arbitrarily-nested lists. 7 new tests,
|
||||||
|
253/253 cumulative. Phase 4 list relations all complete.
|
||||||
|
- **2026-05-08** — **Laziness tests**: explicitly verifies the
|
||||||
|
Zzz-on-conde-clauses + mk-mplus-swap-on-paused machinery: an
|
||||||
|
infinitely-recursive relation truncated via `run 4 q (listo-aux q)`
|
||||||
|
produces exactly `(() (_.0) (_.0 _.1) (_.0 _.1 _.2))`; mixing two
|
||||||
|
infinite generators via `mk-disj` keeps both alive (no starvation);
|
||||||
|
`run*` terminates on a bounded query. 3 new tests, 246/246 cumulative.
|
||||||
|
- **2026-05-08** — **N-queens (classic miniKanren benchmark green)**:
|
||||||
|
`lib/minikanren/queens.sx`. Encoding cols(i) = column of queen in row i;
|
||||||
|
`ino-each` + `all-distincto` cover row/column constraints; `safe-diag`
|
||||||
|
uses `project` to escape into host arithmetic for the `|c_i - c_j| ≠
|
||||||
|
|i - j|` diagonal check; `all-cells-safe` walks pairs at construction
|
||||||
|
time. `(run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols
|
||||||
|
(list a b c d) 4)))` returns the two valid 4-queens placements
|
||||||
|
`(2 4 1 3)` and `(3 1 4 2)`. 6 new tests, 243/243 cumulative.
|
||||||
|
- **2026-05-08** — **Phase 6 piece A — minimal FD (ino + all-distincto)**:
|
||||||
|
`lib/minikanren/fd.sx`. `ino` is `membero` with the FD-style argument
|
||||||
|
order; `all-distincto` is `nafc + membero` walking the list. Together
|
||||||
|
they cover the enumerate-then-filter style of finite-domain solving —
|
||||||
|
`(fresh (a b c) (ino a D) (ino b D) (ino c D) (all-distincto (list a b c)))`
|
||||||
|
enumerates all distinct triples from D. Full FD with arc-consistency,
|
||||||
|
fd-plus etc. is still pending. 9 new tests, 237/237 cumulative.
|
||||||
|
- **2026-05-08** — **Classic puzzles + matche keyword fix**: matche now emits
|
||||||
|
keywords bare in the pattern->expr conversion so they self-evaluate to their
|
||||||
|
string name and unify with the same-keyword target value (instead of becoming
|
||||||
|
a quoted-keyword type). New `tests/classics.sx`: pet permutation puzzle,
|
||||||
|
parent/grandparent inference over a fact list, symbolic differentiation
|
||||||
|
driven by matche dispatch on `:x` / `(:+ a b)` / `(:* a b)` patterns.
|
||||||
|
6 new tests, 228/228 cumulative.
|
||||||
|
- **2026-05-08** — **Phase 5 piece D — matche, Phase 5 done**: pattern matching
|
||||||
|
macro (`lib/minikanren/matche.sx`) — symbols become fresh vars, atoms become
|
||||||
|
literals, lists recurse positionally, repeated names unify. 14 new tests
|
||||||
|
(literals, vars, wildcards, list patterns, multi-clause dispatch, nested
|
||||||
|
patterns, repeated-var-implies-eq). Built via `cons`/`list` rather than
|
||||||
|
quasiquote because SX's quasiquote does not recurse into lambda bodies — a
|
||||||
|
worth-knowing gotcha. 222/222 cumulative.
|
||||||
|
- **2026-05-08** — **Phase 4 piece C — permuteo + inserto**: standard recursive
|
||||||
|
insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3
|
||||||
|
as a set check. 208/208 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 5 piece C — nafc**: `lib/minikanren/nafc.sx`. Three-line
|
||||||
|
primitive: stream-take 1; if empty, `(unit s)`, else `mzero`. 7 tests including
|
||||||
|
double-negation and use as a guard. 201/201 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 5 piece B — project**: `lib/minikanren/project.sx` —
|
||||||
|
defmacro that walks each named var, rebinds them, and runs the body's mk-conj.
|
||||||
|
Demonstrated escape into host arithmetic / string ops (`(* n n)`, `(str s "!")`).
|
||||||
|
Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
|
||||||
|
- **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
|
||||||
|
minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
|
||||||
|
forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)
|
||||||
|
(== q (list a b))))` → all 4 pairs summing to 3. *o uses repeated pluso —
|
||||||
|
works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 5 piece A — conda**: soft-cut. Mirrors `condu` minus
|
||||||
|
the `onceo` on the head: all head answers are conjuncted through the rest of
|
||||||
|
the chosen clause. 7 new tests including the conda-vs-condu divergence test.
|
||||||
|
169/169 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 4 piece B — reverseo + lengtho**: reverseo runs forward
|
||||||
|
cleanly and `run 1`-cleanly backward; lengtho uses Peano-encoded lengths so it
|
||||||
|
works as a true relation in both directions (tests use the encoding directly).
|
||||||
|
10 new tests, 162/162 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 4 piece A — appendo canary green**: cons-cell support
|
||||||
|
in `unify.sx` + `(:s head tail)` lazy stream refactor in `stream.sx` + hygienic
|
||||||
|
`Zzz` (gensym'd subst-name) wrapping each `conde` clause + `lib/minikanren/
|
||||||
|
relations.sx` with `nullo` / `pairo` / `caro` / `cdro` / `conso` / `firsto` /
|
||||||
|
`resto` / `listo` / `appendo` / `membero`. 25 new tests in `tests/relations.sx`,
|
||||||
|
152/152 cumulative.
|
||||||
|
- **Three deep fixes shipped together**, all required to make `appendo`
|
||||||
|
terminate in both directions:
|
||||||
|
1. SX has no improper pairs, so a stream cell of mature subst + thunk
|
||||||
|
tail can't use `cons` — moved to a `(:s head tail)` tagged shape.
|
||||||
|
2. `(Zzz g)` wrapped its inner fn in a parameter named `s`, capturing
|
||||||
|
the user goal's own `s` binding (the `(appendo l s ls)` convention).
|
||||||
|
Replaced with `(gensym "zzz-s-")` for hygiene.
|
||||||
|
3. SX cons cells `(:cons h t)` for relational decomposition (so
|
||||||
|
`(conso a d l)` can split a list by head/tail without proper
|
||||||
|
improper pairs); `mk-walk*` re-flattens cons cells back to native
|
||||||
|
lists for clean reification output.
|
||||||
|
- **2026-05-07** — **Phase 3 done** (run + reification): `lib/minikanren/run.sx` (~28 lines).
|
||||||
|
`reify`/`reify-s`/`reify-name` for canonical `_.N` rendering of unbound vars in
|
||||||
|
left-to-right occurrence order; `run*` / `run` / `run-n` defmacros. 18 new tests
|
||||||
|
in `tests/run.sx`, including the **first classic miniKanren tests green**:
|
||||||
|
`(run* q (== q 1))` → `(1)`; `(run* q (fresh (x y) (== q (list x y))))` →
|
||||||
|
`((_.0 _.1))`. 128/128 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 2 piece D + done** (`condu` / `onceo`): `lib/minikanren/condu.sx`.
|
||||||
|
Both are commitment forms: `onceo` is `(stream-take 1 ...)`; `condu` walks clauses
|
||||||
|
and commits the first one whose head produces an answer. 10 tests in `tests/condu.sx`,
|
||||||
|
110/110 cumulative. Phase 2 complete — ready for Phase 3 (run + reification).
|
||||||
|
- **2026-05-07** — **Phase 2 piece C** (`conde`): `lib/minikanren/conde.sx` — single
|
||||||
|
defmacro folding clauses through `mk-disj` with internal `mk-conj`. 9 tests in
|
||||||
|
`tests/conde.sx`, 100/100 cumulative. Confirmed eager DFS ordering for ==-only
|
||||||
|
streams; true interleaving is a Phase 4 concern (paused thunks under recursion).
|
||||||
|
- **2026-05-07** — **Phase 2 piece B** (`fresh`): `lib/minikanren/fresh.sx` (~10 lines).
|
||||||
|
defmacro form for nice user-facing syntax + `call-fresh` for programmatic use.
|
||||||
|
9 new tests in `tests/fresh.sx`, 91/91 cumulative.
|
||||||
|
- **2026-05-07** — **Phase 2 piece A** (streams + ==/conj/disj): `lib/minikanren/stream.sx`
|
||||||
|
(mzero/unit/mk-mplus/mk-bind/stream-take, ~25 lines of code) + `lib/minikanren/goals.sx`
|
||||||
|
(succeed/fail/==/==-check/conj2/disj2/mk-conj/mk-disj, ~30 lines). Found and noted
|
||||||
|
a host-primitive name clash: `bind` is built in and silently shadows user defines —
|
||||||
|
must use `mk-bind`/`mk-mplus` etc. throughout. 34 tests in `tests/goals.sx`,
|
||||||
|
82/82 cumulative all green. fresh/conde/condu/onceo still pending.
|
||||||
|
- **2026-05-07** — **Phase 1 done**: `lib/minikanren/unify.sx` (53 lines, ~22 lines of actual code) +
|
||||||
|
`lib/minikanren/tests/unify.sx` (48 tests, all green). Kit consumption: `walk-with`,
|
||||||
|
`unify-with`, `occurs-with`, `extend`, `empty-subst`, `mk-var`, `is-var?`, `var-name`
|
||||||
|
all supplied by `lib/guest/match.sx`. Local additions: a miniKanren-flavoured cfg
|
||||||
|
(treats native SX lists as cons-pairs via `:ctor-head = :pair`, occurs-check off),
|
||||||
|
`make-var` fresh-counter, deep `mk-walk*` (kit's `walk*` only recurses into `:ctor`
|
||||||
|
form, not native lists), and `mk-unify` / `mk-unify-check` thin wrappers. The kit
|
||||||
|
earns its keep ~3× over by line count — confirms lib-guest match kit is reusable
|
||||||
|
for logic-language hosts as designed.
|
||||||
|
|||||||
Reference in New Issue
Block a user