/
exercise-7.27.rkt
416 lines (363 loc) · 19.1 KB
/
exercise-7.27.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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
#lang eopl
;; Exercise 7.27 [★★] Rewrite the inferencer so that it works in two phases. In the first phase it should generate a
;; set of equations, and in the second phase, it should repeatedly call unify to solve them.
;; Grammar.
(define the-lexical-spec
'([whitespace (whitespace) skip]
[comment ("%" (arbno (not #\newline))) skip]
[identifier (letter (arbno (or letter digit "_" "-" "?"))) symbol]
[number (digit (arbno digit)) number]
[number ("-" digit (arbno digit)) number]))
(define the-grammar
'([program (expression) a-program]
[expression (number) const-exp]
[expression ("-" "(" expression "," expression ")") diff-exp]
[expression ("zero?" "(" expression ")") zero?-exp]
[expression ("if" expression "then" expression "else" expression) if-exp]
[expression (identifier) var-exp]
[expression ("let" identifier "=" expression "in" expression) let-exp]
[expression ("proc" "(" identifier ":" optional-type ")" expression) proc-exp]
[expression ("(" expression expression ")") call-exp]
[expression ("letrec" optional-type identifier "(" identifier ":" optional-type ")" "=" expression "in" expression)
letrec-exp]
[optional-type ("?") no-type]
[optional-type (type) a-type]
[type ("int") int-type]
[type ("bool") bool-type]
[type ("(" type "->" type ")") proc-type]
[type ("%tvar-type" number) tvar-type]))
(sllgen:make-define-datatypes the-lexical-spec the-grammar)
(define scan&parse (sllgen:make-string-parser the-lexical-spec the-grammar))
(define proc-type?
(lambda (ty)
(cases type ty
[proc-type (t1 t2) #t]
[else #f])))
(define tvar-type?
(lambda (ty)
(cases type ty
[tvar-type (serial-number) #t]
[else #f])))
(define proc-type->arg-type
(lambda (ty)
(cases type ty
[proc-type (arg-type result-type) arg-type]
[else (eopl:error 'proc-type->arg-type "Not a proc type: ~s" ty)])))
(define proc-type->result-type
(lambda (ty)
(cases type ty
[proc-type (arg-type result-type) result-type]
[else (eopl:error 'proc-type->result-types "Not a proc type: ~s" ty)])))
(define type-to-external-form
(lambda (ty)
(cases type ty
[int-type () 'int]
[bool-type () 'bool]
[proc-type (arg-type result-type) (list (type-to-external-form arg-type) '-> (type-to-external-form result-type))]
[tvar-type (serial-number) (string->symbol (string-append "tvar" (number->string serial-number)))])))
;; Data structures - expressed values.
(define-datatype proc proc?
[procedure [bvar symbol?]
[body expression?]
[env environment?]])
(define-datatype expval expval?
[num-val [value number?]]
[bool-val [boolean boolean?]]
[proc-val [proc proc?]])
(define expval-extractor-error
(lambda (variant value)
(eopl:error 'expval-extractors "Looking for a ~s, found ~s" variant value)))
(define expval->num
(lambda (v)
(cases expval v
[num-val (num) num]
[else (expval-extractor-error 'num v)])))
(define expval->bool
(lambda (v)
(cases expval v
[bool-val (bool) bool]
[else (expval-extractor-error 'bool v)])))
(define expval->proc
(lambda (v)
(cases expval v
[proc-val (proc) proc]
[else (expval-extractor-error 'proc v)])))
;; Data structures - environment.
(define-datatype environment environment?
[empty-env]
[extend-env [bvar symbol?]
[bval expval?]
[saved-env environment?]]
[extend-env-rec [p-name symbol?]
[b-var symbol?]
[p-body expression?]
[saved-env environment?]])
(define apply-env
(lambda (env search-sym)
(cases environment env
[empty-env () (eopl:error 'apply-env "No binding for ~s" search-sym)]
[extend-env (bvar bval saved-env) (if (eqv? search-sym bvar)
bval
(apply-env saved-env search-sym))]
[extend-env-rec (p-name b-var p-body saved-env) (if (eqv? search-sym p-name)
(proc-val (procedure b-var p-body env))
(apply-env saved-env search-sym))])))
;; Data structures - type environment.
(define-datatype type-environment type-environment?
[empty-tenv-record]
[extended-tenv-record [sym symbol?]
[type type?]
[tenv type-environment?]])
(define empty-tenv empty-tenv-record)
(define extend-tenv extended-tenv-record)
(define apply-tenv
(lambda (tenv sym)
(cases type-environment tenv
[empty-tenv-record () (eopl:error 'apply-tenv "Unbound variable ~s" sym)]
[extended-tenv-record (sym1 val1 old-env) (if (eqv? sym sym1)
val1
(apply-tenv old-env sym))])))
;; Data structures - substitution.
(define pair-of
(lambda (pred1 pred2)
(lambda (val)
(and (pair? val) (pred1 (car val)) (pred2 (cdr val))))))
(define substitution?
(list-of (pair-of tvar-type? type?)))
(define empty-subst
(lambda ()
'()))
(define apply-one-subst
(lambda (ty0 tvar ty1)
(cases type ty0
[int-type () (int-type)]
[bool-type () (bool-type)]
[proc-type (arg-type result-type) (proc-type (apply-one-subst arg-type tvar ty1)
(apply-one-subst result-type tvar ty1))]
[tvar-type (sn) (if (equal? ty0 tvar) ty1 ty0)])))
(define extend-subst
(lambda (subst tvar ty)
(cons (cons tvar ty)
(map (lambda (p)
(let ([oldlhs (car p)]
[oldrhs (cdr p)])
(cons oldlhs (apply-one-subst oldrhs tvar ty))))
subst))))
(define apply-subst-to-type
(lambda (ty subst)
(cases type ty
[int-type () (int-type)]
[bool-type () (bool-type)]
[proc-type (t1 t2) (proc-type (apply-subst-to-type t1 subst) (apply-subst-to-type t2 subst))]
[tvar-type (sn) (let ([tmp (assoc ty subst)])
(if tmp
(cdr tmp)
ty))])))
;; Data structures - answer.
(define-datatype answer answer?
[an-answer [type type?]
[subst substitution?]])
;; Unifier.
(define no-occurrence?
(lambda (tvar ty)
(cases type ty
[int-type () #t]
[bool-type () #t]
[proc-type (arg-type result-type) (and (no-occurrence? tvar arg-type)
(no-occurrence? tvar result-type))]
[tvar-type (serial-number) (not (equal? tvar ty))])))
(define report-no-occurrence-violation
(lambda (ty1 ty2 exp)
(eopl:error 'check-no-occurence!
"Can't unify: type variable ~s occurs in type ~s in expression ~s~%"
(type-to-external-form ty1)
(type-to-external-form ty2)
exp)))
(define report-unification-failure
(lambda (ty1 ty2 exp)
(eopl:error 'unification-failure
"Type mismatch: ~s doesn't match ~s in ~s~%"
(type-to-external-form ty1)
(type-to-external-form ty2)
exp)))
(define unifier
(lambda (ty1 ty2 subst exp)
(let ([ty1 (apply-subst-to-type ty1 subst)]
[ty2 (apply-subst-to-type ty2 subst)])
(cond [(equal? ty1 ty2) subst]
[(tvar-type? ty1) (if (no-occurrence? ty1 ty2)
(extend-subst subst ty1 ty2)
(report-no-occurrence-violation ty1 ty2 exp))]
[(tvar-type? ty2) (if (no-occurrence? ty2 ty1)
(extend-subst subst ty2 ty1)
(report-no-occurrence-violation ty2 ty1 exp))]
[(and (proc-type? ty1) (proc-type? ty2)) (let ([subst (unifier (proc-type->arg-type ty1)
(proc-type->arg-type ty2)
subst
exp)])
(let ([subst (unifier (proc-type->result-type ty1)
(proc-type->result-type ty2)
subst
exp)])
subst))]
[else (report-unification-failure ty1 ty2 exp)]))))
;; Inferrer.
(define sn 'uninitialized)
(define fresh-tvar-type
(let ([sn 0])
(lambda ()
(set! sn (+ sn 1))
(tvar-type sn))))
(define otype->type
(lambda (otype)
(cases optional-type otype
[no-type () (fresh-tvar-type)]
[a-type (ty) ty])))
(define type-of
(lambda (exp tenv subst)
(let ([type-and-equations (let loop ([equations '()]
[exp exp]
[tenv tenv]
[cont (lambda (ty equations)
(cons ty equations))])
(cases expression exp
[const-exp (num) (cont (int-type) equations)]
[zero?-exp (exp1) (loop equations
exp1
tenv
(lambda (ty equations)
(cont (bool-type)
(cons (list ty (int-type) exp1) equations))))]
[diff-exp (exp1 exp2) (loop equations
exp1
tenv
(lambda (ty1 equations)
(loop equations
exp2
tenv
(lambda (ty2 equations)
(cont (int-type)
(append (list (list ty1 (int-type) exp1)
(list ty2 (int-type) exp2))
equations))))))]
[if-exp (exp1 exp2 exp3) (loop equations
exp1
tenv
(lambda (ty1 equations)
(loop equations
exp2
tenv
(lambda (ty2 equations)
(loop equations
exp3
tenv
(lambda (ty3 equations)
(cont ty2
(append (list (list ty1
(bool-type)
exp1)
(list ty2
ty3
exp3))
equations))))))))]
[var-exp (var) (cont (apply-tenv tenv var) equations)]
[let-exp (var exp1 body) (loop equations
exp1
tenv
(lambda (ty equations)
(loop equations
body
(extend-tenv var ty tenv)
cont)))]
[proc-exp (var otype body) (let ([arg-type (otype->type otype)])
(loop equations
body
(extend-tenv var arg-type tenv)
(lambda (ty equations)
(cont (proc-type arg-type ty)
equations))))]
[call-exp (rator rand) (loop equations
rator
tenv
(lambda (rator-type equations)
(loop equations
rand
tenv
(lambda (rand-type equations)
(let* ([result-type (fresh-tvar-type)])
(cont result-type
(cons (list rator-type
(proc-type rand-type
result-type)
rator)
equations)))))))]
[letrec-exp (proc-result-otype proc-name bvar proc-arg-otype proc-body letrec-body)
(let* ([proc-result-type (otype->type proc-result-otype)]
[proc-arg-type (otype->type proc-arg-otype)]
[letrec-env (extend-tenv proc-name
(proc-type proc-arg-type proc-result-type)
tenv)])
(loop equations
proc-body
(extend-tenv bvar proc-arg-type letrec-env)
(lambda (proc-body-type equations)
(loop (cons (list proc-result-type proc-body-type proc-body)
equations)
letrec-body
letrec-env
cont))))]))])
(let loop ([subst subst]
[equations (cdr type-and-equations)])
(if (null? equations)
(an-answer (car type-and-equations) subst)
(let* ([equation (car equations)])
(loop (unifier (car equation)
(cadr equation)
subst
(caddr equation))
(cdr equations))))))))
(define type-of-program
(lambda (pgm)
(cases program pgm
[a-program (exp1) (cases answer (type-of exp1 (empty-tenv) (empty-subst))
[an-answer (ty subst) (apply-subst-to-type ty subst)])])))
;; Interpreter.
(define apply-procedure
(lambda (proc1 arg)
(cases proc proc1
[procedure (var body saved-env) (value-of body (extend-env var arg saved-env))])))
(define value-of
(lambda (exp env)
(cases expression exp
[const-exp (num) (num-val num)]
[var-exp (var) (apply-env env var)]
[diff-exp (exp1 exp2) (let ([val1 (expval->num (value-of exp1 env))]
[val2 (expval->num (value-of exp2 env))])
(num-val (- val1 val2)))]
[zero?-exp (exp1) (let ([val1 (expval->num (value-of exp1 env))])
(if (zero? val1)
(bool-val #t)
(bool-val #f)))]
[if-exp (exp0 exp1 exp2) (if (expval->bool (value-of exp0 env))
(value-of exp1 env)
(value-of exp2 env))]
[let-exp (var exp1 body) (let ([val (value-of exp1 env)])
(value-of body (extend-env var val env)))]
[proc-exp (bvar ty body) (proc-val (procedure bvar body env))]
[call-exp (rator rand) (let ([proc (expval->proc (value-of rator env))]
[arg (value-of rand env)])
(apply-procedure proc arg))]
[letrec-exp (ty1 p-name b-var ty2 p-body letrec-body) (value-of letrec-body
(extend-env-rec p-name b-var p-body env))])))
(define value-of-program
(lambda (pgm)
(cases program pgm
[a-program (body) (value-of body (empty-env))])))
;; Interface.
(define check
(lambda (string)
(type-to-external-form (type-of-program (scan&parse string)))))
(define run
(lambda (string)
(value-of-program (scan&parse string))))
(provide check num-val run)