-
Notifications
You must be signed in to change notification settings - Fork 29
/
Copy pathmicroKanren-test-programs.scm
129 lines (116 loc) · 2.79 KB
/
microKanren-test-programs.scm
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
(define-syntax test-check
(syntax-rules ()
((_ title tested-expression expected-result)
(begin
(printf "Testing ~s\n" title)
(let* ((expected expected-result)
(produced tested-expression))
(or (equal? expected produced)
(errorf 'test-check
"Failed: ~a~%Expected: ~a~%Computed: ~a~%"
'tested-expression expected produced)))))))
(define a-and-b
(conj
(call/fresh (lambda (a) (== a 7)))
(call/fresh
(lambda (b)
(disj
(== b 5)
(== b 6))))))
(define fives
(lambda (x)
(disj
(== x 5)
(lambda (a/c)
(lambda ()
((fives x) a/c))))))
(define appendo
(lambda (l s out)
(disj
(conj (== '() l) (== s out))
(call/fresh
(lambda (a)
(call/fresh
(lambda (d)
(conj
(== `(,a . ,d) l)
(call/fresh
(lambda (res)
(conj
(== `(,a . ,res) out)
(lambda (s/c)
(lambda ()
((appendo d s res) s/c))))))))))))))
(define appendo2
(lambda (l s out)
(disj
(conj (== '() l) (== s out))
(call/fresh
(lambda (a)
(call/fresh
(lambda (d)
(conj
(== `(,a . ,d) l)
(call/fresh
(lambda (res)
(conj
(lambda (s/c)
(lambda ()
((appendo2 d s res) s/c)))
(== `(,a . ,res) out))))))))))))
(define call-appendo
(call/fresh
(lambda (q)
(call/fresh
(lambda (l)
(call/fresh
(lambda (s)
(call/fresh
(lambda (out)
(conj
(appendo l s out)
(== `(,l ,s ,out) q)))))))))))
(define call-appendo2
(call/fresh
(lambda (q)
(call/fresh
(lambda (l)
(call/fresh
(lambda (s)
(call/fresh
(lambda (out)
(conj
(appendo2 l s out)
(== `(,l ,s ,out) q)))))))))))
(define call-appendo3
(call/fresh
(lambda (q)
(call/fresh
(lambda (l)
(call/fresh
(lambda (s)
(call/fresh
(lambda (out)
(conj
(== `(,l ,s ,out) q)
(appendo l s out)))))))))))
(define ground-appendo (appendo '(a) '(b) '(a b)))
(define ground-appendo2 (appendo2 '(a) '(b) '(a b)))
(define relo
(lambda (x)
(call/fresh
(lambda (x1)
(call/fresh
(lambda (x2)
(conj
(== x `(,x1 . ,x2))
(disj
(== x1 x2)
(lambda (s/c)
(lambda () ((relo x) s/c)))))))))))
(define many-non-ans
(call/fresh
(lambda (x)
(disj
(relo `(5 . 6))
(== x 3)))))