diff --git a/lib/minikanren/tests/laziness.sx b/lib/minikanren/tests/laziness.sx new file mode 100644 index 00000000..d3440ac4 --- /dev/null +++ b/lib/minikanren/tests/laziness.sx @@ -0,0 +1,77 @@ +;; lib/minikanren/tests/laziness.sx — verify Zzz wrapping (in conde) +;; lets infinitely-recursive relations produce finite prefixes via run-n. + +;; --- a relation that has no base case but conde-protects via Zzz --- + +(define + listo-aux + (fn + (l) + (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo-aux d)))))) + +(mk-test + "infinite-relation-truncates-via-run-n" + (run 4 q (listo-aux q)) + (list + (list) + (list (make-symbol "_.0")) + (list (make-symbol "_.0") (make-symbol "_.1")) + (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2")))) + +;; --- two infinite generators interleaved via mk-disj must both produce +;; answers (no starvation) — the fairness test --- + +(define + ones-gen + (fn + (l) + (conde + ((== l (list))) + ((fresh (d) (conso 1 d l) (ones-gen d)))))) + +(define + twos-gen + (fn + (l) + (conde + ((== l (list))) + ((fresh (d) (conso 2 d l) (twos-gen d)))))) + +(mk-test + "interleaving-keeps-both-streams-alive" + (let + ((res (run 4 q (mk-disj (ones-gen q) (twos-gen q))))) + (and + (= (len res) 4) + (and + (some + (fn + (x) + (and + (list? x) + (and (not (empty? x)) (= (first x) 1)))) + res) + (some + (fn + (x) + (and + (list? x) + (and (not (empty? x)) (= (first x) 2)))) + res)))) + true) + +;; --- run* terminates on a relation whose conde has finite base case +;; reached from any starting point --- + +(mk-test + "run-star-terminates-on-bounded-relation" + (run* + q + (fresh + (l) + (== l (list 1 2 3)) + (listo l) + (== q :ok))) + (list :ok)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 35b5193d..4151863d 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -169,6 +169,12 @@ _(none yet)_ _Newest first._ +- **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`