-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathtest-interp.ss
108 lines (97 loc) · 3.1 KB
/
test-interp.ss
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
(load "mk.scm")
(define eval-expo
(lambda (exp env val)
(conde
((fresh (rator rand x body env^ a)
(== `(,rator ,rand) exp)
(eval-expo rator env `(closure ,x ,body ,env^))
(eval-expo rand env a)
(eval-expo body `((,x . ,a) . ,env^) val)))
((fresh (x body)
(== `(lambda (,x) ,body) exp)
(symbolo x)
(== `(closure ,x ,body ,env) val)
(not-in-envo 'lambda env)))
((symbolo exp) (lookupo exp env val)))))
(define not-in-envo
(lambda (x env)
(conde
((== '() env))
((fresh (y v rest)
(== `((,y . ,v) . ,rest) env)
(=/= y x)
(not-in-envo x rest))))))
(define lookupo
(lambda (x env t)
(conde
((fresh (y v rest)
(== `((,y . ,v) . ,rest) env) (== y x)
(== v t)))
((fresh (y v rest)
(== `((,y . ,v) . ,rest) env) (=/= y x)
(lookupo x rest t))))))
(test-check "running backwards"
(run 5 (q) (eval-expo q '() '(closure y x ((x . (closure z z ()))))))
'(((lambda (x) (lambda (y) x)) (lambda (z) z))
((lambda (x) (x (lambda (y) x))) (lambda (z) z))
(((lambda (x) (lambda (y) x))
((lambda (_.0) _.0) (lambda (z) z)))
(sym _.0))
(((lambda (_.0) _.0)
((lambda (x) (lambda (y) x)) (lambda (z) z)))
(sym _.0))
((((lambda (_.0) _.0) (lambda (x) (lambda (y) x)))
(lambda (z) z))
(sym _.0))))
(define lookupo
(lambda (x env t)
(fresh (rest y v)
(== `((,y . ,v) . ,rest) env)
(conde
((== y x) (== v t))
((=/= y x) (lookupo x rest t))))))
(test-check "eval-exp-lc 1"
(run* (q) (eval-expo '(((lambda (x) (lambda (y) x)) (lambda (z) z)) (lambda (a) a)) '() q))
'((closure z z ())))
(test-check "eval-exp-lc 2"
(run* (q) (eval-expo '((lambda (x) (lambda (y) x)) (lambda (z) z)) '() q))
'((closure y x ((x . (closure z z ()))))))
(test-check "running backwards"
(run 5 (q) (eval-expo q '() '(closure y x ((x . (closure z z ()))))))
'(((lambda (x) (lambda (y) x)) (lambda (z) z))
((lambda (x) (x (lambda (y) x))) (lambda (z) z))
(((lambda (x) (lambda (y) x))
((lambda (_.0) _.0) (lambda (z) z)))
(sym _.0))
((((lambda (_.0) _.0) (lambda (x) (lambda (y) x)))
(lambda (z) z))
(sym _.0))
(((lambda (_.0) _.0)
((lambda (x) (lambda (y) x)) (lambda (z) z)))
(sym _.0))))
(test-check "fully-running-backwards"
(run 5 (q)
(fresh (e v)
(eval-expo e '() v)
(== `(,e ==> ,v) q)))
'((((lambda (_.0) _.1)
==> (closure _.0 _.1 ())) (sym _.0))
((((lambda (_.0) _.0) (lambda (_.1) _.2))
==>
(closure _.1 _.2 ()))
(sym _.0 _.1))
((((lambda (_.0) (lambda (_.1) _.2)) (lambda (_.3) _.4))
==>
(closure _.1 _.2 ((_.0 . (closure _.3 _.4 ())))))
(=/= ((_.0 lambda)))
(sym _.0 _.1 _.3))
((((lambda (_.0) (_.0 _.0)) (lambda (_.1) _.1))
==>
(closure _.1 _.1 ()))
(sym _.0 _.1))
((((lambda (_.0) (_.0 _.0))
(lambda (_.1) (lambda (_.2) _.3)))
==>
(closure _.2 _.3 ((_.1 . (closure _.1 (lambda (_.2) _.3) ())))))
(=/= ((_.1 lambda)))
(sym _.0 _.1 _.2))))