diff --git a/lib/minikanren/fresh.sx b/lib/minikanren/fresh.sx new file mode 100644 index 00000000..e10abb5c --- /dev/null +++ b/lib/minikanren/fresh.sx @@ -0,0 +1,23 @@ +;; lib/minikanren/fresh.sx — Phase 2 piece B: `fresh` for introducing +;; logic variables inside a goal body. +;; +;; (fresh (x y z) goal1 goal2 ...) +;; ≡ (let ((x (make-var)) (y (make-var)) (z (make-var))) +;; (mk-conj goal1 goal2 ...)) +;; +;; A macro rather than a function so user-named vars are real lexical +;; bindings — which is also what miniKanren convention expects. +;; The empty-vars form (fresh () goal ...) is just a goal grouping. + +(defmacro + fresh + (vars &rest goals) + (quasiquote + (let + (unquote (map (fn (v) (list v (list (quote make-var)))) vars)) + (mk-conj (splice-unquote goals))))) + +;; call-fresh — functional alternative for code that builds goals +;; programmatically: +;; ((call-fresh (fn (x) (== x 7))) empty-s) → ({:_.N 7}) +(define call-fresh (fn (f) (fn (s) ((f (make-var)) s)))) diff --git a/lib/minikanren/tests/fresh.sx b/lib/minikanren/tests/fresh.sx new file mode 100644 index 00000000..e4df2bda --- /dev/null +++ b/lib/minikanren/tests/fresh.sx @@ -0,0 +1,101 @@ +;; lib/minikanren/tests/fresh.sx — Phase 2 piece B tests for `fresh`. + +;; --- empty fresh: pure goal grouping --- + +(mk-test + "fresh-empty-vars-equiv-conj" + ((fresh () (== 1 1)) empty-s) + (list empty-s)) + +(mk-test + "fresh-empty-vars-no-goals-is-succeed" + ((fresh ()) empty-s) + (list empty-s)) + +;; --- single var --- + +(mk-test + "fresh-one-var-bound" + (let + ((s (first ((fresh (x) (== x 7)) empty-s)))) + (let ((vs (vals s))) (first vs))) + 7) + +;; --- multiple vars + multiple goals --- + +(mk-test + "fresh-two-vars-three-goals" + (let + ((q (mk-var "q")) + (g + (fresh + (x y) + (== x 10) + (== y 20) + (== q (list x y))))) + (mk-walk* q (first (g empty-s)))) + (list 10 20)) + +(mk-test + "fresh-three-vars" + (let + ((q (mk-var "q")) + (g + (fresh + (a b c) + (== a 1) + (== b 2) + (== c 3) + (== q (list a b c))))) + (mk-walk* q (first (g empty-s)))) + (list 1 2 3)) + +;; --- fresh interacts with disj --- + +(mk-test + "fresh-with-disj" + (let + ((q (mk-var "q"))) + (let + ((g (fresh (x) (mk-disj (== x 1) (== x 2)) (== q x)))) + (let + ((res (stream-take 5 (g empty-s)))) + (map (fn (s) (mk-walk q s)) res)))) + (list 1 2)) + +;; --- nested fresh --- + +(mk-test + "fresh-nested" + (let + ((q (mk-var "q")) + (g + (fresh + (x) + (fresh + (y) + (== x 1) + (== y 2) + (== q (list x y)))))) + (mk-walk* q (first (g empty-s)))) + (list 1 2)) + +;; --- call-fresh (functional alternative) --- + +(mk-test + "call-fresh-binds-and-walks" + (let + ((s (first ((call-fresh (fn (x) (== x 99))) empty-s)))) + (first (vals s))) + 99) + +(mk-test + "call-fresh-distinct-from-outer-vars" + (let + ((q (mk-var "q"))) + (let + ((g (call-fresh (fn (x) (mk-conj (== x 5) (== q (list x x))))))) + (mk-walk* q (first (g empty-s))))) + (list 5 5)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 0e2243c6..9236d449 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -72,7 +72,9 @@ Key semantic mappings: - [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 +- [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 - [ ] `condu` — committed choice (soft-cut) - [ ] `onceo` — succeeds at most once @@ -141,6 +143,9 @@ _(none yet)_ _Newest first._ +- **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. - **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