-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtc.rkt
199 lines (185 loc) · 6.37 KB
/
tc.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
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
#lang typed/racket/shallow
(provide check-main)
(require "val.rkt"
"eval.rkt"
"expr.rkt"
"readback.rkt")
(define-type Gamma (Immutable-HashTable String Val))
(: *debug-mode* (Boxof Boolean))
(define *debug-mode* (box #f))
(: up-g (-> Gamma Patt Val Val Gamma))
(define (up-g gamma p t v)
(when (unbox *debug-mode*)
(displayln (format "up-g with:\n\t~a\n\t~a\n\t~a:\n\t~a"
gamma p t v)))
(match* (p t)
[((pwild) _)
gamma]
[((pvar x) t)
(hash-set gamma x t)]
[((ppair p1 p2) (vsigma t g))
(let ([gamma* (up-g gamma p1 t (vfst v))])
(up-g gamma* p2 (inst g (vfst v)) (vsnd v)))]))
(: check-type (-> Integer Telescope Gamma Expr Void))
(define (check-type k rho gamma e)
(when (unbox *debug-mode*)
(displayln (format "check-type with:\n\t~a\n\t~a\n\t~a\n\t~a" k rho gamma e)))
(match e
[(epi p a b)
(begin (check-type k rho gamma a)
(define gamma* (up-g gamma p (evaluate a rho) (gen-v k)))
(check-type (add1 k) (tupvar rho p (gen-v k)) gamma* b))]
[(esigma p a b)
(begin (check-type k rho gamma a)
(define gamma* (up-g gamma p (evaluate a rho) (gen-v k)))
(check-type (add1 k) (tupvar rho p (gen-v k)) gamma* b))]
[(eset) (void)]
[(eunit) (void)]
[(evoid) (void)]
[_ (check k rho gamma e (vset))]))
(: check (-> Integer Telescope Gamma Expr Val Void))
(define (check k rho gamma e* t*)
(when (unbox *debug-mode*)
(displayln (format "check with:\n\t~a\n\t~a\n\t~a\n\t~a\n\t~a"
k rho gamma e* t*)))
(match* (e* t*)
[((elam p e) (vpi t g))
(define gen (gen-v k))
(define gamma* (up-g gamma p t gen))
(check (add1 k) (tupvar rho p gen) gamma* e (inst g gen))]
[((etuple e1 e2) (vsigma t g))
(check k rho gamma e1 t)
(check k rho gamma e2 (inst g (evaluate e1 rho)))]
[((econ c e) (vsum (sclos cas rho*)))
(define a : (Option Expr)
(hash-ref cas c (lambda () #f)))
(when a
(check k rho gamma e (evaluate a rho*)))]
[((efun ces) (vpi (vsum (sclos cas rho*)) g))
(define ces* (hash-keys ces))
(define cas* (hash-keys cas))
(if (equal? ces* cas*)
(for* ([x (hash->list ces)]
[y (hash->list cas)])
(match* (x y)
[((cons c e) (cons _ a))
(check k rho gamma e
(vpi (evaluate a rho*)
(cmp g c)))]))
(error (format "branches do not match:\n\n\t~a\n\n\t~a"
cas ces)))]
[((eunit) (vset))
(void)]
[((eone) (vunit))
(void)]
[((epi p a b) (vset))
(check k rho gamma a (vset))
(define gen (gen-v k))
(define gamma* (up-g gamma p (evaluate a rho) gen))
(check (add1 k) (tupvar rho p gen) gamma* b (vset))]
[((esigma p a b) (vset))
(check k rho gamma (epi p a b) (vset))]
[((esum cas) (vset))
(for ([a (hash-values cas)])
(check k rho gamma a (vset)))]
[((edecl d e) t)
(define gamma* (check-decl k rho gamma d))
(check k (tupdec rho d) gamma* e t)]
[(_ _)
(define t** (check-infer k rho gamma e*))
(when (equal-nf? k t* t**)
(void))]))
(: check-infer (-> Integer Telescope Gamma Expr Val))
(define (check-infer k rho gamma e*)
(when (unbox *debug-mode*)
(displayln (format "check-infer with:~a\n\t~a\n\t~a\n\t~a"
k rho gamma e*)))
(match e*
[(eset) (vset)]
[(eunit) (vset)]
[(eone) (vunit)]
[(evoid) (vset)]
[(evar x)
(let ([res : (Option Val) (hash-ref gamma x #f)])
(if res
res
(error (format "check-infer error with gamma:\n\n\t~a\n\nand expr:\n\n\t~a"
gamma e*))))]
[(eapp rator rand)
(define t* (check-infer k rho gamma rator))
(letrec ([x (ext-pi t*)]
[t (car x)]
[g (cdr x)])
(begin (check k rho gamma rand t)
(inst g (evaluate rand rho))))]
[(etuple lhs rhs)
(define lft (check-infer k rho gamma lhs))
(define rht (check-infer k rho gamma rhs))
(vsigma lft (cval rht))]
[(efst e)
(define t (check-infer k rho gamma e))
(letrec ([x (ext-sigma t)]
[a (car x)])
a)]
[(esnd e)
(define t (check-infer k rho gamma e))
(letrec ([x (ext-sigma t)]
[g (cdr x)])
(inst g (vfst (evaluate e rho))))]
[_ (error
(format
(string-append
"unable to infer an expression which is not one of the following:"
"\n\ta projection (car/cdr <expr>)\n\ta tuple (cons <expr> <expr>)"
"\n\tan application (<expr> <expr>)"
"\n\ta variable, 0, unit, or set"
"\n\nthe expression given was of type:\n\t~a")
e*))]))
(: ext-pi (-> Val (Pairof Val Clos)))
(define (ext-pi t)
(match t
[(vpi t* g)
(cons t* g)]
[_ (error (format "error in ext-pi with:\n\n\t~a"
t))]))
(: ext-sigma (-> Val (Pairof Val Clos)))
(define (ext-sigma t)
(match t
[(vsigma t* g)
(cons t* g)]
[_ (error (format "error in ext-sigma with:\n\n\t~a"
t))]))
(: check-decl (-> Integer Telescope Gamma Decl Gamma))
(define (check-decl k rho gamma d)
(when (unbox *debug-mode*)
(displayln (format "check-decl with:\n\t~a\n\t~a\n\t~a\n\t~a"
k rho gamma d)))
(match d
[(ddec p a e)
(begin (check-type k rho gamma a)
(define t (evaluate a rho))
(check k rho gamma e t)
(up-g gamma p t (evaluate e rho)))]
[(drec p a e)
(begin (check-type k rho gamma a)
(define t (evaluate a rho))
(define gen (gen-v k))
(define gamma* (up-g gamma p t gen))
(pretty-display gamma*)
(check (add1 k) (tupvar rho p gen) gamma* e t)
(define v (evaluate e (tupdec rho d)))
(up-g gamma p t v))]))
(: equal-nf? (-> Integer Val Val Boolean))
(define (equal-nf? k m n)
(when (unbox *debug-mode*)
(displayln (format "equal-nf? with ~a ~a ~a"
k m n)))
(begin (define e (read-back-val k m))
(define g (read-back-val k n))
(equal? e g)))
(: check-main (-> Boolean Expr Val Void))
(define (check-main debug e t)
(set-box! *debug-mode* debug)
(when (unbox *debug-mode*)
(displayln (format "check-main with:\n\t~a\n\t~a" e t)))
(check 0 (tnil) (hash) e t))