mk: defrel — Prolog-style relation-definition macro
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...) expands to (define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...))). Mirrors Prolog's `name(Args) :- goals.` shape. Inherits the Zzz-on-each- clause laziness from conde, so user relations defined via defrel terminate on partial answers without needing manual delay. Tests redefine membero / listo / pluso through defrel and verify equivalence. 3 new tests, 347/347 cumulative.
This commit is contained in:
25
lib/minikanren/defrel.sx
Normal file
25
lib/minikanren/defrel.sx
Normal file
@@ -0,0 +1,25 @@
|
|||||||
|
;; lib/minikanren/defrel.sx — Prolog-style defrel macro.
|
||||||
|
;;
|
||||||
|
;; (defrel (NAME ARG1 ARG2 ...)
|
||||||
|
;; (CLAUSE1 ...)
|
||||||
|
;; (CLAUSE2 ...)
|
||||||
|
;; ...)
|
||||||
|
;;
|
||||||
|
;; expands to
|
||||||
|
;;
|
||||||
|
;; (define NAME (fn (ARG1 ARG2 ...) (conde (CLAUSE1 ...) (CLAUSE2 ...))))
|
||||||
|
;;
|
||||||
|
;; This puts each clause's goals immediately after the head, mirroring
|
||||||
|
;; Prolog's `name(Args) :- goals.` shape. Clauses are conde-conjoined
|
||||||
|
;; goals — `Zzz`-wrapping is automatic via `conde`, so recursive
|
||||||
|
;; relations terminate on partial answers.
|
||||||
|
|
||||||
|
(defmacro
|
||||||
|
defrel
|
||||||
|
(head &rest clauses)
|
||||||
|
(let
|
||||||
|
((name (first head)) (args (rest head)))
|
||||||
|
(list
|
||||||
|
(quote define)
|
||||||
|
name
|
||||||
|
(list (quote fn) args (cons (quote conde) clauses)))))
|
||||||
40
lib/minikanren/tests/defrel.sx
Normal file
40
lib/minikanren/tests/defrel.sx
Normal file
@@ -0,0 +1,40 @@
|
|||||||
|
;; lib/minikanren/tests/defrel.sx — Prolog-style relation definition macro.
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-membero x l)
|
||||||
|
((fresh (d) (conso x d l)))
|
||||||
|
((fresh (a d) (conso a d l) (my-membero x d))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-defines-membero"
|
||||||
|
(run* q (my-membero q (list 1 2 3)))
|
||||||
|
(list 1 2 3))
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-listo l)
|
||||||
|
((nullo l))
|
||||||
|
((fresh (a d) (conso a d l) (my-listo d))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-listo-bounded"
|
||||||
|
(run 3 q (my-listo q))
|
||||||
|
(list
|
||||||
|
(list)
|
||||||
|
(list (make-symbol "_.0"))
|
||||||
|
(list (make-symbol "_.0") (make-symbol "_.1"))))
|
||||||
|
|
||||||
|
;; Multi-arg relation with arithmetic.
|
||||||
|
|
||||||
|
(defrel
|
||||||
|
(my-pluso a b c)
|
||||||
|
((== a :z) (== b c))
|
||||||
|
((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (my-pluso a-1 b c-1))))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"defrel-pluso-2-3"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(my-pluso (list :s (list :s :z)) (list :s (list :s (list :s :z))) q))
|
||||||
|
(list (list :s (list :s (list :s (list :s (list :s :z)))))))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
@@ -173,6 +173,11 @@ _(none yet)_
|
|||||||
|
|
||||||
_Newest first._
|
_Newest first._
|
||||||
|
|
||||||
|
- **2026-05-08** — **defrel — Prolog-style relation definition macro**:
|
||||||
|
`(defrel (NAME ARGS...) (CLAUSE1 ...) (CLAUSE2 ...) ...)` expands to
|
||||||
|
`(define NAME (fn (ARGS...) (conde (CLAUSE1 ...) (CLAUSE2 ...) ...)))`.
|
||||||
|
Mirrors Prolog's clause syntax and inherits Zzz-via-conde so recursive
|
||||||
|
relations terminate. 3 new tests, 347/347 cumulative.
|
||||||
- **2026-05-08** — **lasto / init-o**: classic head/tail-style list relations.
|
- **2026-05-08** — **lasto / init-o**: classic head/tail-style list relations.
|
||||||
lasto extracts the final element; init-o extracts everything-but-the-last.
|
lasto extracts the final element; init-o extracts everything-but-the-last.
|
||||||
Together with appendo, the round-trip `init ⊕ (last) = l` holds. 8 new
|
Together with appendo, the round-trip `init ⊕ (last) = l` holds. 8 new
|
||||||
|
|||||||
Reference in New Issue
Block a user