mk: phase 2C — conde, the canonical and-or sugar
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 50s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 50s
conde.sx is a single defmacro: (conde (g1a g1b ...) (g2a g2b ...) ...) folds to (mk-disj (mk-conj g1a g1b ...) (mk-conj g2a g2b ...) ...). 9 tests cover single/multi-clause, mixed success/failure, conjunction inside clauses, fresh+disj inside a clause, nesting, and all-fail / no-clauses. 100/100 cumulative.
This commit is contained in:
20
lib/minikanren/conde.sx
Normal file
20
lib/minikanren/conde.sx
Normal file
@@ -0,0 +1,20 @@
|
||||
;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
|
||||
;; miniKanren and-or form.
|
||||
;;
|
||||
;; (conde (g1a g1b ...) (g2a g2b ...) ...)
|
||||
;; ≡ (mk-disj (mk-conj g1a g1b ...)
|
||||
;; (mk-conj g2a g2b ...) ...)
|
||||
;;
|
||||
;; Each clause is a list of goals, conj'd internally; clauses are disj'd
|
||||
;; among one another (interleaved via mk-mplus, so left-recursive
|
||||
;; relations don't starve the right-hand clauses).
|
||||
|
||||
(defmacro
|
||||
conde
|
||||
(&rest clauses)
|
||||
(quasiquote
|
||||
(mk-disj
|
||||
(splice-unquote
|
||||
(map
|
||||
(fn (clause) (quasiquote (mk-conj (splice-unquote clause))))
|
||||
clauses)))))
|
||||
93
lib/minikanren/tests/conde.sx
Normal file
93
lib/minikanren/tests/conde.sx
Normal file
@@ -0,0 +1,93 @@
|
||||
;; lib/minikanren/tests/conde.sx — Phase 2 piece C tests for `conde`.
|
||||
;;
|
||||
;; Note on ordering: mk-mplus only interleaves when the left stream is a
|
||||
;; paused thunk. Eager streams from == compose via mature DFS order
|
||||
;; (left-clause results first, then right-clause). True interleaving is
|
||||
;; tested in Phase 4 via recursive relations.
|
||||
|
||||
;; --- single-clause conde ≡ conj of clause body ---
|
||||
|
||||
(mk-test
|
||||
"conde-one-clause"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 5 ((conde ((== q 7))) empty-s))))
|
||||
(map (fn (s) (mk-walk q s)) res)))
|
||||
(list 7))
|
||||
|
||||
(mk-test
|
||||
"conde-one-clause-multi-goals"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 5 ((conde ((fresh (x) (== x 5) (== q (list x x))))) empty-s))))
|
||||
(map (fn (s) (mk-walk* q s)) res)))
|
||||
(list (list 5 5)))
|
||||
|
||||
;; --- multi-clause: produces one row per clause (eager DFS order) ---
|
||||
|
||||
(mk-test
|
||||
"conde-three-clauses"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 10 ((conde ((== q 1)) ((== q 2)) ((== q 3))) empty-s))))
|
||||
(map (fn (s) (mk-walk q s)) res)))
|
||||
(list 1 2 3))
|
||||
|
||||
(mk-test
|
||||
"conde-mixed-success-failure"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 10 ((conde ((== q "a")) ((== 1 2)) ((== q "b"))) empty-s))))
|
||||
(map (fn (s) (mk-walk q s)) res)))
|
||||
(list "a" "b"))
|
||||
|
||||
;; --- conde with conjuncts inside clauses ---
|
||||
|
||||
(mk-test
|
||||
"conde-clause-conj"
|
||||
(let
|
||||
((q (mk-var "q")) (r (mk-var "r")))
|
||||
(let
|
||||
((res (stream-take 10 ((conde ((== q 1) (== r 10)) ((== q 2) (== r 20))) empty-s))))
|
||||
(map (fn (s) (list (mk-walk q s) (mk-walk r s))) res)))
|
||||
(list (list 1 10) (list 2 20)))
|
||||
|
||||
;; --- conde + fresh: multiple solutions per clause ---
|
||||
|
||||
(mk-test
|
||||
"conde-with-fresh-and-disj"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 10 ((conde ((fresh (x) (mk-disj (== x 1) (== x 2)) (== q x))) ((== q 100))) empty-s))))
|
||||
(map (fn (s) (mk-walk q s)) res)))
|
||||
(list 1 2 100))
|
||||
|
||||
;; --- nested conde ---
|
||||
|
||||
(mk-test
|
||||
"conde-nested"
|
||||
(let
|
||||
((q (mk-var "q")))
|
||||
(let
|
||||
((res (stream-take 10 ((conde ((conde ((== q 1)) ((== q 2)))) ((== q 3))) empty-s))))
|
||||
(map (fn (s) (mk-walk q s)) res)))
|
||||
(list 1 2 3))
|
||||
|
||||
;; --- conde all clauses fail → empty stream ---
|
||||
|
||||
(mk-test
|
||||
"conde-all-fail"
|
||||
((conde ((== 1 2)) ((== 3 4)))
|
||||
empty-s)
|
||||
(list))
|
||||
|
||||
;; --- empty conde: no clauses ⇒ fail ---
|
||||
|
||||
(mk-test "conde-no-clauses" ((conde) empty-s) (list))
|
||||
|
||||
(mk-tests-run!)
|
||||
Reference in New Issue
Block a user