-
Notifications
You must be signed in to change notification settings - Fork 1
/
a11.rkt
83 lines (81 loc) · 2.04 KB
/
a11.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
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
#lang racket
(require C311/mk)
(provide (all-defined-out))
(define apply-Go
(lambda (G e t)
(fresh (a G^)
(== `(,a . ,G^) G)
(fresh (aa da)
(== `(,aa . ,da) a)
(conde
((== aa e) (== da t))
((=/= aa e) (apply-Go G^ e t)))))))
(define !-
(lambda (G e t)
(conde
((numbero e) (== 'Nat t))
((== t 'Bool)
(conde
((== #t e))
((== #f e))))
((fresh (e1 e2 t1 t2)
(== `(cons ,e1 ,e2) e)
(== t `(pairof ,t1 ,t2))
(!- G e1 t1)
(!- G e2 t2)))
((fresh (pe at dt)
(== `(car ,pe) e)
(== t at)
(!- G pe `(pairof ,at ,dt))))
((fresh (pe at dt)
(== `(cdr ,pe) e)
(== t dt)
(!- G pe `(pairof ,at ,dt))))
((fresh (ne1 ne2)
(== `(+ ,ne1 ,ne2) e)
(== 'Nat t)
(!- G ne1 'Nat)
(!- G ne2 'Nat)))
((fresh (ne1 ne2)
(== `(* ,ne1 ,ne2) e)
(== 'Nat t)
(!- G ne1 'Nat)
(!- G ne2 'Nat)))
((fresh (ne)
(== `(sub1 ,ne) e)
(== 'Nat t)
(!- G ne 'Nat)))
((fresh (ne)
(== `(zero? ,ne) e)
(== 'Bool t)
(!- G ne 'Nat)))
((fresh (be)
(== `(not ,be) e)
(== 'Bool t)
(!- G be 'Bool)))
((fresh (teste anse elsee)
(== `(if ,teste ,anse ,elsee) e)
(!- G teste 'Bool)
(!- G anse t)
(!- G elsee t)))
((symbolo e) (apply-Go G e t))
((fresh (x b)
(== `(lambda (,x) ,b) e)
(symbolo x)
(fresh (tx tb)
(== `(,tx -> ,tb) t)
(!- `((,x . ,tx) . ,G) b tb))))
((fresh (var val b lt bt)
(== `(let ((,var ,val)) ,b) e)
(!- G val lt)
(== lt t)
(!- `((,var . ,lt). ,G) b bt)))
((fresh (fe a)
(== `(fix ,fe) e)
(== t a)
(!- G fe `(,a -> ,a))))
((fresh (e1 arg)
(== `(,e1 ,arg) e)
(fresh (targ)
(!- G e1 `(,targ -> ,t))
(!- G arg targ)))))))