-
Notifications
You must be signed in to change notification settings - Fork 9
/
mk-syntax.rkt
44 lines (44 loc) · 1.36 KB
/
mk-syntax.rkt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
(define-syntax define-relation
(syntax-rules ()
((_ (name param ...) g ...)
(define (name param ...)
(relate (lambda () (fresh () g ...)) `(,name name ,param ...))))))
;; Low-level goals
(define succeed (== #t #t))
(define fail (== #f #t))
(define-syntax conj*
(syntax-rules ()
((_) succeed)
((_ g) g)
((_ gs ... g-final) (conj (conj* gs ...) g-final))))
(define-syntax disj*
(syntax-rules ()
((_) fail)
((_ g) g)
((_ g0 gs ...) (disj g0 (disj* gs ...)))))
;; High level goals
(define-syntax fresh
(syntax-rules ()
((_ (x ...) g0 gs ...)
(let ((x (var/fresh 'x)) ...) (conj* g0 gs ...)))))
(define-syntax conde
(syntax-rules ()
((_ (g gs ...) (h hs ...) ...)
(disj* (conj* g gs ...) (conj* h hs ...) ...))))
;; Queries
(define-syntax query
(syntax-rules ()
((_ (x ...) g0 gs ...)
(let ((goal (fresh (x ...) (== (list x ...) initial-var) g0 gs ...)))
(pause empty-state goal)))))
(define (stream-take n s)
(if (eqv? 0 n) '()
(let ((s (mature s)))
(if (pair? s)
(cons (car s) (stream-take (and n (- n 1)) (cdr s)))
'()))))
(define-syntax run
(syntax-rules ()
((_ n body ...) (map reify/initial-var (stream-take n (query body ...))))))
(define-syntax run*
(syntax-rules () ((_ body ...) (run #f body ...))))