mk: phase 3 — run* / run / reify, 18 new tests
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
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.
This commit is contained in:
56
lib/minikanren/run.sx
Normal file
56
lib/minikanren/run.sx
Normal file
@@ -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))))
|
||||
114
lib/minikanren/tests/run.sx
Normal file
114
lib/minikanren/tests/run.sx
Normal file
@@ -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!)
|
||||
Reference in New Issue
Block a user