diff --git a/lib/minikanren/goals.sx b/lib/minikanren/goals.sx new file mode 100644 index 00000000..6f6cc227 --- /dev/null +++ b/lib/minikanren/goals.sx @@ -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))) diff --git a/lib/minikanren/stream.sx b/lib/minikanren/stream.sx new file mode 100644 index 00000000..11da7b2a --- /dev/null +++ b/lib/minikanren/stream.sx @@ -0,0 +1,58 @@ +;; lib/minikanren/stream.sx — Phase 2 piece A: lazy streams of substitutions. +;; +;; Three stream shapes per The Reasoned Schemer (chapter 9): +;; mzero — empty stream (the SX empty list) +;; mature — '(s . rest) (a proper SX list of substitutions) +;; immature — a thunk (an SX lambda taking zero args, returns a stream) +;; +;; Immature thunks are how miniKanren keeps search lazy and supports +;; interleaved disjunction without diverging on left-recursive relations. +;; SX has plain function closures, so a thunk is just (fn () body). +;; +;; Names are mk-prefixed: SX has a host primitive `bind` that would shadow +;; a user-level definition. + +(define mzero (list)) + +(define unit (fn (s) (list s))) + +(define stream-pause? (fn (s) (and (not (list? s)) (callable? s)))) + +;; mk-mplus — interleave two streams. If the first is mature/empty we use it +;; directly; if it is paused, we suspend and swap so the other stream gets +;; explored fairly (Reasoned Schemer "interleave"). +(define + mk-mplus + (fn + (s1 s2) + (cond + ((empty? s1) s2) + ((stream-pause? s1) (fn () (mk-mplus s2 (s1)))) + (:else (cons (first s1) (mk-mplus (rest s1) s2)))))) + +;; mk-bind — apply goal g to every substitution in stream s, mk-mplus-ing results. +(define + mk-bind + (fn + (s g) + (cond + ((empty? s) mzero) + ((stream-pause? s) (fn () (mk-bind (s) g))) + (:else (mk-mplus (g (first s)) (mk-bind (rest s) g)))))) + +;; stream-take — force up to n results out of a (possibly lazy) stream. +;; n = -1 to take all (used by run*). +(define + stream-take + (fn + (n s) + (cond + ((= n 0) (list)) + ((empty? s) (list)) + ((stream-pause? s) (stream-take n (s))) + (:else + (cons + (first s) + (stream-take + (if (= n -1) -1 (- n 1)) + (rest s))))))) diff --git a/lib/minikanren/tests/goals.sx b/lib/minikanren/tests/goals.sx new file mode 100644 index 00000000..f08a9c5c --- /dev/null +++ b/lib/minikanren/tests/goals.sx @@ -0,0 +1,216 @@ +;; lib/minikanren/tests/goals.sx — Phase 2 tests for stream.sx + goals.sx. +;; +;; Loaded after: lib/guest/match.sx, lib/minikanren/unify.sx, +;; lib/minikanren/stream.sx, lib/minikanren/goals.sx. +;; Reuses the mk-test* counters from tests/unify.sx — load that first to +;; accumulate, or call mk-tests-run! after this file alone for fresh totals. + +;; --- stream-take base cases --- + +(mk-test + "stream-take-zero-from-mature" + (stream-take 0 (list 1 2 3)) + (list)) + +(mk-test "stream-take-from-empty" (stream-take 5 mzero) (list)) + +(mk-test + "stream-take-mature-list" + (stream-take 5 (list 1 2 3)) + (list 1 2 3)) + +(mk-test + "stream-take-fewer-than-available" + (stream-take 2 (list 10 20 30)) + (list 10 20)) + +(mk-test + "stream-take-all-with-neg-1" + (stream-take -1 (list 1 2 3 4)) + (list 1 2 3 4)) + +;; --- stream-take forces immature thunks --- + +(mk-test + "stream-take-forces-thunk" + (stream-take 3 (fn () (list "a" "b" "c"))) + (list "a" "b" "c")) + +(mk-test + "stream-take-forces-nested-thunks" + (stream-take + 3 + (fn () (fn () (list 1 2 3)))) + (list 1 2 3)) + +;; --- mk-mplus interleaves --- + +(mk-test + "mplus-empty-left" + (mk-mplus mzero (list 1 2)) + (list 1 2)) +(mk-test + "mplus-empty-right" + (mk-mplus (list 1 2) mzero) + (list 1 2)) + +(mk-test + "mplus-mature-mature" + (mk-mplus (list 1 2) (list 3 4)) + (list 1 2 3 4)) + +(mk-test + "mplus-with-paused-left-swaps" + (stream-take 4 (mk-mplus (fn () (list "a" "b")) (list "c" "d"))) + (list "c" "d" "a" "b")) + +;; --- mk-bind --- + +(mk-test "bind-empty-stream" (mk-bind mzero (fn (s) (unit s))) (list)) + +(mk-test + "bind-singleton-identity" + (mk-bind (list 5) (fn (x) (list x))) + (list 5)) + +(mk-test + "bind-flat-multi" + (mk-bind + (list 1 2) + (fn (x) (list x (* x 10)))) + (list 1 10 2 20)) + +(mk-test + "bind-fail-prunes-some" + (mk-bind + (list 1 2 3) + (fn (x) (if (= x 2) (list) (list x)))) + (list 1 3)) + +;; --- core goals: succeed / fail --- + +(mk-test "succeed-yields-singleton" (succeed empty-s) (list empty-s)) + +(mk-test "fail-yields-mzero" (fail empty-s) (list)) + +;; --- == --- + +(mk-test + "eq-ground-success" + (mk-unified? (first ((== 1 1) empty-s))) + true) + +(mk-test "eq-ground-failure" ((== 1 2) empty-s) (list)) + +(mk-test + "eq-binds-var" + (let + ((x (mk-var "x"))) + (mk-walk x (first ((== x 7) empty-s)))) + 7) + +(mk-test + "eq-list-success" + (let + ((x (mk-var "x"))) + (mk-walk x (first ((== x (list 1 2)) empty-s)))) + (list 1 2)) + +(mk-test + "eq-list-mismatch-fails" + ((== (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 ((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"))) + ((conj2 (== x 1) (== x 2)) empty-s)) + (list)) + +(mk-test "conj-empty-is-succeed" ((mk-conj) empty-s) (list empty-s)) + +(mk-test + "conj-single-is-goal" + (let + ((x (mk-var "x"))) + (mk-walk x (first ((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 ((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" ((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 (distributivity check) --- + +(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 (occurs-checked equality goal) --- + +(mk-test + "eq-check-no-occurs-fails" + (let ((x (mk-var "x"))) ((==-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 ((==-check x 5) empty-s)))) + 5) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 1e5890a6..0e2243c6 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -61,14 +61,20 @@ Key semantic mappings: - [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs ### Phase 2 — streams + goals -- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`), - `mplus` (interleave two streams), `bind` (apply goal to stream) -- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy -- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))` -- [ ] `succeed` / `fail` — trivial goals -- [ ] `fresh` — `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many -- [ ] `conde` — interleaving disjunction of goal lists -- [ ] `condu` — committed choice (soft-cut): only explores first successful clause +- [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave), + `mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host + `bind` primitive that silently shadows user defines. +- [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends + and swaps when its left operand is paused, giving fair interleaving. +- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))` +- [x] `==-check` — opt-in occurs-checked equality goal +- [x] `succeed` / `fail` — trivial goals +- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction +- [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde` + adds the implicit-conj-per-clause sugar later) +- [ ] `fresh` — introduces logic variables inside a goal body +- [ ] `conde` — sugar over disj+conj, one row per clause +- [ ] `condu` — committed choice (soft-cut) - [ ] `onceo` — succeeds at most once - [ ] Tests: basic goal composition, backtracking, interleaving @@ -135,6 +141,12 @@ _(none yet)_ _Newest first._ +- **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`