From 52070e07fc00cde97c8ca87e840eda15d8907df7 Mon Sep 17 00:00:00 2001 From: giles Date: Thu, 7 May 2026 20:03:42 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=203=20=E2=80=94=20run*=20/=20run=20?= =?UTF-8?q?/=20reify,=2018=20new=20tests?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit run.sx: reify-name builds canonical "_.N" symbols; reify-s walks a term left-to-right and assigns each unbound var its index in the discovery order; reify combines the two with two walk* passes. run-n is the runtime defmacro: binds the query var, takes ≤ n stream answers, reifies each. run* and run are sugar around it. First classic miniKanren tests green: (run* q (== q 1)) → (1) (run* q (conde ((== q 1)) ((== q 2)))) → (1 2) (run* q (fresh (x y) (== q (list x y)))) → ((_.0 _.1)) 128/128 cumulative. --- lib/minikanren/run.sx | 56 ++++++++++++++++++ lib/minikanren/tests/run.sx | 114 ++++++++++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 25 +++++--- 3 files changed, 187 insertions(+), 8 deletions(-) create mode 100644 lib/minikanren/run.sx create mode 100644 lib/minikanren/tests/run.sx diff --git a/lib/minikanren/run.sx b/lib/minikanren/run.sx new file mode 100644 index 00000000..811eebc5 --- /dev/null +++ b/lib/minikanren/run.sx @@ -0,0 +1,56 @@ +;; lib/minikanren/run.sx — Phase 3: drive a goal + reify the query var. +;; +;; reify-name N — make the canonical "_.N" reified symbol. +;; reify-s term rs — walk term in rs, add a mapping from each fresh +;; unbound var to its _.N name (left-to-right order). +;; reify q s — walk* q in s, build reify-s, walk* again to +;; substitute reified names in. +;; run-n n q-name g... — defmacro: bind q-name to a fresh var, conj goals, +;; take ≤ n answers from the stream, reify each +;; through q-name. n = -1 takes all (used by run*). +;; run* — defmacro: (run* q g...) ≡ (run-n -1 q g...) +;; run — defmacro: (run n q g...) ≡ (run-n n q g...) +;; The two-segment form is the standard TRS API. + +(define reify-name (fn (n) (make-symbol (str "_." n)))) + +(define + reify-s + (fn + (term rs) + (let + ((w (mk-walk term rs))) + (cond + ((is-var? w) (extend (var-name w) (reify-name (len rs)) rs)) + ((mk-list-pair? w) (reduce (fn (acc a) (reify-s a acc)) rs w)) + (:else rs))))) + +(define + reify + (fn + (term s) + (let + ((w (mk-walk* term s))) + (let ((rs (reify-s w (empty-subst)))) (mk-walk* w rs))))) + +(defmacro + run-n + (n q-name &rest goals) + (quasiquote + (let + (((unquote q-name) (make-var))) + (map + (fn (s) (reify (unquote q-name) s)) + (stream-take + (unquote n) + ((mk-conj (splice-unquote goals)) empty-s)))))) + +(defmacro + run* + (q-name &rest goals) + (quasiquote (run-n -1 (unquote q-name) (splice-unquote goals)))) + +(defmacro + run + (n q-name &rest goals) + (quasiquote (run-n (unquote n) (unquote q-name) (splice-unquote goals)))) diff --git a/lib/minikanren/tests/run.sx b/lib/minikanren/tests/run.sx new file mode 100644 index 00000000..c25a49e4 --- /dev/null +++ b/lib/minikanren/tests/run.sx @@ -0,0 +1,114 @@ +;; lib/minikanren/tests/run.sx — Phase 3 tests for run* / run / reify. + +;; --- canonical TRS one-liners --- + +(mk-test "run*-eq-one" (run* q (== q 1)) (list 1)) +(mk-test "run*-eq-string" (run* q (== q "hello")) (list "hello")) +(mk-test "run*-eq-symbol" (run* q (== q (quote sym))) (list (quote sym))) +(mk-test "run*-fail-empty" (run* q (== 1 2)) (list)) + +;; --- run with a count --- + +(mk-test + "run-3-of-many" + (run + 3 + q + (conde + ((== q 1)) + ((== q 2)) + ((== q 3)) + ((== q 4)) + ((== q 5)))) + (list 1 2 3)) + +(mk-test "run-zero-empty" (run 0 q (== q 1)) (list)) + +(mk-test + "run-1-takes-one" + (run 1 q (conde ((== q "a")) ((== q "b")))) + (list "a")) + +;; --- reification: unbound vars get _.N left-to-right --- + +(mk-test + "reify-single-unbound" + (run* q (fresh (x) (== q x))) + (list (make-symbol "_.0"))) + +(mk-test + "reify-pair-unbound" + (run* q (fresh (x y) (== q (list x y)))) + (list (list (make-symbol "_.0") (make-symbol "_.1")))) + +(mk-test + "reify-mixed-bound-unbound" + (run* q (fresh (x y) (== q (list 1 x 2 y)))) + (list + (list 1 (make-symbol "_.0") 2 (make-symbol "_.1")))) + +(mk-test + "reify-shared-unbound-same-name" + (run* q (fresh (x) (== q (list x x)))) + (list (list (make-symbol "_.0") (make-symbol "_.0")))) + +(mk-test + "reify-distinct-unbound-distinct-names" + (run* q (fresh (x y) (== q (list x y x y)))) + (list + (list + (make-symbol "_.0") + (make-symbol "_.1") + (make-symbol "_.0") + (make-symbol "_.1")))) + +;; --- conde + run* --- + +(mk-test + "run*-conde-three" + (run* + q + (conde ((== q 1)) ((== q 2)) ((== q 3)))) + (list 1 2 3)) + +(mk-test + "run*-conde-fresh-mix" + (run* + q + (conde ((fresh (x) (== q (list 1 x)))) ((== q "ground")))) + (list (list 1 (make-symbol "_.0")) "ground")) + +;; --- run* + conjunction --- + +(mk-test + "run*-conj-binds-q" + (run* q (fresh (x) (== x 5) (== q (list x x)))) + (list (list 5 5))) + +;; --- run* + condu --- + +(mk-test + "run*-condu-first-wins" + (run* q (condu ((== q 1)) ((== q 2)))) + (list 1)) + +(mk-test + "run*-onceo-trim" + (run* q (onceo (conde ((== q "a")) ((== q "b"))))) + (list "a")) + +;; --- multi-goal run --- + +(mk-test + "run*-three-goals" + (run* + q + (fresh + (x y z) + (== x 1) + (== y 2) + (== z 3) + (== q (list x y z)))) + (list (list 1 2 3))) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 344bcb77..f833e2bf 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -86,15 +86,18 @@ Key semantic mappings: - [x] Tests: basic goal composition, backtracking, interleaving (110 cumulative) ### Phase 3 — run + reification -- [ ] `run*` `goal` → list of all answers (reified) -- [ ] `run n` `goal` → list of first n answers -- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names -- [ ] `reify-s` → builds reification substitution for naming unbound vars consistently -- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar -- [ ] Query variable conventions: `q` as canonical query variable -- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`, +- [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as + fresh var, conj goals, take all from stream, reify each. +- [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all) +- [x] `reify` `term` `subst` → walk* + build reification subst + walk* again +- [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a + `_.N` symbol via `(make-symbol (str "_." n))` +- [x] `fresh` with multiple variables — already shipped Phase 2B. +- [x] Query variable conventions: `q` as canonical query variable (matches TRS) +- [x] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`, `(run* q (conde ((== q 1)) ((== q 2))))` → `(1 2)`, - Peano arithmetic, `appendo` preview + `(run* q (fresh (x y) (== q (list x y))))` → `((_.0 _.1))`. Peano + + `appendo` deferred to Phase 4. ### Phase 4 — standard relations - [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards @@ -148,6 +151,12 @@ _(none yet)_ _Newest first._ +- **2026-05-07** — **Phase 3 done** (run + reification): `lib/minikanren/run.sx` (~28 lines). + `reify`/`reify-s`/`reify-name` for canonical `_.N` rendering of unbound vars in + left-to-right occurrence order; `run*` / `run` / `run-n` defmacros. 18 new tests + in `tests/run.sx`, including the **first classic miniKanren tests green**: + `(run* q (== q 1))` → `(1)`; `(run* q (fresh (x y) (== q (list x y))))` → + `((_.0 _.1))`. 128/128 cumulative. - **2026-05-07** — **Phase 2 piece D + done** (`condu` / `onceo`): `lib/minikanren/condu.sx`. Both are commitment forms: `onceo` is `(stream-take 1 ...)`; `condu` walks clauses and commits the first one whose head produces an answer. 10 tests in `tests/condu.sx`,