From c754a8ee059baaa2b8b7541ad329b6a0d5474543 Mon Sep 17 00:00:00 2001 From: giles Date: Thu, 7 May 2026 19:59:17 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=202C=20=E2=80=94=20conde,=20the=20c?= =?UTF-8?q?anonical=20and-or=20sugar?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- lib/minikanren/conde.sx | 20 ++++++++ lib/minikanren/tests/conde.sx | 93 +++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 9 +++- 3 files changed, 121 insertions(+), 1 deletion(-) create mode 100644 lib/minikanren/conde.sx create mode 100644 lib/minikanren/tests/conde.sx diff --git a/lib/minikanren/conde.sx b/lib/minikanren/conde.sx new file mode 100644 index 00000000..ffcb9a28 --- /dev/null +++ b/lib/minikanren/conde.sx @@ -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))))) diff --git a/lib/minikanren/tests/conde.sx b/lib/minikanren/tests/conde.sx new file mode 100644 index 00000000..ec761064 --- /dev/null +++ b/lib/minikanren/tests/conde.sx @@ -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!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 9236d449..4d4d0de7 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -75,7 +75,10 @@ Key semantic mappings: - [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. -- [ ] `conde` — sugar over disj+conj, one row per clause +- [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). - [ ] `condu` — committed choice (soft-cut) - [ ] `onceo` — succeeds at most once - [ ] Tests: basic goal composition, backtracking, interleaving @@ -143,6 +146,10 @@ _(none yet)_ _Newest first._ +- **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.