From 240ed90b20d00d903e37f396fb8ea4ff950fca7f Mon Sep 17 00:00:00 2001 From: giles Date: Thu, 7 May 2026 21:51:52 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=205A=20=E2=80=94=20conda,=20soft-cu?= =?UTF-8?q?t=20without=20onceo?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit conda-try mirrors condu-try but on the chosen clause it (mk-bind (head-goal s) (rest-conj)) — all head answers flow through. condu by contrast applies rest-conj to (first peek), keeping only one head answer. 7 new tests covering: first-non-failing-wins, skip-failing-head, all-fail, no-clauses, the conda-vs-condu divergence (`(1 2)` vs `(1)`), rest-goals running on every head answer, and the soft-cut no-fallthrough property. 169/169 cumulative. --- lib/minikanren/conda.sx | 42 ++++++++++++++++++++ lib/minikanren/tests/conda.sx | 75 +++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 9 ++++- 3 files changed, 124 insertions(+), 2 deletions(-) create mode 100644 lib/minikanren/conda.sx create mode 100644 lib/minikanren/tests/conda.sx diff --git a/lib/minikanren/conda.sx b/lib/minikanren/conda.sx new file mode 100644 index 00000000..6806c10a --- /dev/null +++ b/lib/minikanren/conda.sx @@ -0,0 +1,42 @@ +;; lib/minikanren/conda.sx — Phase 5 piece A: `conda`, the soft-cut. +;; +;; (conda (g0 g ...) (h0 h ...) ...) +;; — first clause whose head g0 produces ANY answer wins; ALL of g0's +;; answers are then conj'd with the rest of that clause; later +;; clauses are NOT tried. +;; — differs from condu only in not wrapping g0 in onceo: condu +;; commits to the SINGLE first answer, conda lets the head's full +;; answer-set flow into the rest of the clause. +;; (Reasoned Schemer chapter 10; Byrd 5.3.) + +(define + conda-try + (fn + (clauses s) + (cond + ((empty? clauses) mzero) + (:else + (let + ((cl (first clauses))) + (let + ((head-goal (first cl)) (rest-goals (rest cl))) + (let + ((peek (stream-take 1 (head-goal s)))) + (if + (empty? peek) + (conda-try (rest clauses) s) + (mk-bind (head-goal s) (mk-conj-list rest-goals)))))))))) + +(defmacro + conda + (&rest clauses) + (quasiquote + (fn + (s) + (conda-try + (list + (splice-unquote + (map + (fn (cl) (quasiquote (list (splice-unquote cl)))) + clauses))) + s)))) diff --git a/lib/minikanren/tests/conda.sx b/lib/minikanren/tests/conda.sx new file mode 100644 index 00000000..0f6ed1e6 --- /dev/null +++ b/lib/minikanren/tests/conda.sx @@ -0,0 +1,75 @@ +;; lib/minikanren/tests/conda.sx — Phase 5 piece A tests for `conda`. + +;; --- conda commits to first non-failing head, keeps ALL its answers --- + +(mk-test + "conda-first-clause-keeps-all" + (run* + q + (conda + ((mk-disj (== q 1) (== q 2))) + ((== q 100)))) + (list 1 2)) + +(mk-test + "conda-skips-failing-head" + (run* + q + (conda + ((== 1 2)) + ((mk-disj (== q 10) (== q 20))))) + (list 10 20)) + +(mk-test + "conda-all-fail" + (run* + q + (conda ((== 1 2)) ((== 3 4)))) + (list)) + +(mk-test "conda-no-clauses" (run* q (conda)) (list)) + +;; --- conda DIFFERS from condu: conda keeps all head answers --- + +(mk-test + "conda-vs-condu-divergence" + (list + (run* + q + (conda + ((mk-disj (== q 1) (== q 2))) + ((== q 100)))) + (run* + q + (condu + ((mk-disj (== q 1) (== q 2))) + ((== q 100))))) + (list (list 1 2) (list 1))) + +;; --- conda head's rest-goals run on every head answer --- + +(mk-test + "conda-rest-goals-run-on-all-answers" + (run* + q + (fresh + (x r) + (conda + ((mk-disj (== x 1) (== x 2)) + (== r (list :tag x)))) + (== q r))) + (list (list :tag 1) (list :tag 2))) + +;; --- if rest-goals fail on a head answer, that head answer is filtered; +;; the clause does not fall through to next clauses (per soft-cut). --- + +(mk-test + "conda-rest-fails-no-fallthrough" + (run* + q + (conda + ((mk-disj (== q 1) (== q 2)) (== q 99)) + ((== q 200)))) + (list)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index f60651fc..aa332a34 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -124,8 +124,9 @@ Key semantic mappings: escapes to ground values for arithmetic or string ops - [ ] `matche` — pattern matching over logic terms (extension from core.logic) `(matche l ((head . tail) goal) (() goal))` -- [ ] `conda` — soft-cut disjunction (like Prolog `->`) -- [ ] `condu` — committed choice (already in phase 2; refine semantics here) +- [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) - [ ] `nafc` — negation as finite failure with constraint - [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche` @@ -155,6 +156,10 @@ _(none yet)_ _Newest first._ +- **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).