-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathanf-typechecker.rkt
158 lines (142 loc) · 6.57 KB
/
anf-typechecker.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
#lang typed/racket/base
(require "types.rkt" "ir-anf-ast.rkt" "primop.rkt" "ir-anf-printable-ast.rkt")
(require racket/list racket/match)
(provide type-check)
(: type-check (expression -> Void))
(define (type-check expr)
(define-type environment (HashTable unique type))
(: check (environment -> (expression -> type)))
(define (check env)
(: type-assert (unique type -> Void))
(define (type-assert sym expected)
(let ((actual (hash-ref env sym (lambda () (error 'type-check "Unbound identifier ~a in ~a" sym env)))))
(unless (equal? actual expected)
(error 'type-check "Identifier ~a has type ~a. Expected ~a." sym actual expected))))
(: expr-type-assert (expression type -> Void))
(define (expr-type-assert expr expected)
(let ((actual (recur expr)))
(unless (equal? actual expected)
(error 'type-check "Expression ~a has type ~a. Expected ~a." (anf->printable expr) actual expected))))
(: assert (Boolean String -> Void))
(define (assert bool str)
(unless bool
(error 'type-check "Invariant violated: ~a" str)))
(: recur (expression -> type))
(define (recur expr)
(match expr
((bind-primop var bind-type op args body)
(let ((val-type
(match op
((integer-constant-primop n) (assert (empty? args) "zero args int constant") int-type)
((string-constant-primop str) (assert (empty? args) "nyi1") string-type)
((unit-primop) (assert (empty? args) "nyi2") unit-type)
((nil-primop ty) (assert (empty? args) "nyi3") ty)
((runtime-primop ty name) (assert (empty? args) "nyi4") ty)
((math-primop sym)
(assert (= (length args) 2) "nyi5")
(type-assert (first args) int-type)
(type-assert (second args) int-type)
int-type)
((comparison-primop sym ty)
(assert (= (length args) 2) "nyi-comparison")
(type-assert (first args) ty)
(type-assert (second args) ty)
int-type)
((equality-primop eql ty)
(assert (= (length args) 2) "nyi6")
(type-assert (first args) ty)
(type-assert (second args) ty)
int-type)
((call-known-runtime-primop ty _)
(let ((arg-types (function-type-arg-types ty)))
(type-assert (first args) ty)
(for-each (lambda: ((arg : unique) (ty : type)) (type-assert arg ty)) (rest args) arg-types)
(function-type-return-type ty)))
((call-known-function-primop ty _)
(let ((arg-types (function-type-arg-types ty)))
(type-assert (first args) ty)
(for-each (lambda: ((arg : unique) (ty : type)) (type-assert arg ty)) (rest args) arg-types)
(function-type-return-type ty)))
((call-closure-primop ty)
(let ((arg-types (function-type-arg-types ty)))
(type-assert (first args) ty)
(for-each (lambda: ((arg : unique) (ty : type)) (type-assert arg ty)) (rest args) arg-types)
(function-type-return-type ty)))
((create-box-primop ty)
(assert (= (length args) 1) "nyi7")
(type-assert (first args) (box-type-elem-type ty))
ty)
((create-array-primop ty)
(assert (= (length args) 2) "nyi8")
(type-assert (first args) int-type)
(type-assert (second args) (array-type-elem-type ty))
ty)
((create-record-primop ty)
(let ((fields (map (inst cdr Symbol type) (record-type-fields ty))))
(assert (= (length args) (length fields)) "nyi9")
(for-each type-assert args fields)
ty))
((box-ref-primop ty)
(assert (= (length args) 1) "nyi10")
(type-assert (first args) ty)
(box-type-elem-type ty))
((array-ref-primop ty)
(assert (= (length args) 2) "nyi11")
(type-assert (first args) ty)
(type-assert (second args) int-type)
(array-type-elem-type ty))
((field-ref-primop ty name)
(assert (= (length args) 1) "nyi12")
(type-assert (first args) ty)
(record-type-field-type ty name))
((box-set!-primop ty)
(assert (= (length args) 2) "nyi13")
(type-assert (first args) ty)
(type-assert (second args) (box-type-elem-type ty))
unit-type)
((array-set!-primop ty)
(assert (= (length args) 3) "nyi14")
(type-assert (first args) ty)
(type-assert (second args) int-type)
(type-assert (third args) (array-type-elem-type ty))
unit-type)
((undefined-primop ty)
(assert (= (length args) 0) "undefined-primop does not have zero args")
ty)
((field-set!-primop ty name)
(assert (= (length args) 2) "nyi15")
(type-assert (first args) ty)
(type-assert (second args) (record-type-field-type ty name))
unit-type)
(else (error 'type-check "Not yet implemented ~a" op)))))
(assert (equal? bind-type val-type) (format "binding type ~a doesn't equals val-type ~a for expr ~a" bind-type val-type expr))
((check (hash-set env var bind-type)) body)))
((conditional c t f ty)
(type-assert c int-type)
(expr-type-assert t ty)
(expr-type-assert f ty)
ty)
((bind-rec funs body)
(let ((env (for/fold: : environment
((env : environment env))
((pair : (Pair unique function) funs))
(hash-set env (car pair) (function->function-type (cdr pair))))))
(for-each (check-function env) (map (inst cdr unique function) funs))
((check env) body)))
((return name)
(hash-ref env name
(lambda () (error 'type-check "Unbound identifier ~a in ~a" name env))))))
recur)
(: check-function (environment -> (function -> Void)))
(define ((check-function env) fun)
(match fun
((function name args return body)
(let ((env (for/fold: : environment
((env : environment env))
((arg : (Pair unique type) args))
(hash-set env (car arg) (cdr arg)))))
(let ((ty ((check env) body)))
(unless (equal? ty return)
(error 'type-check "Body of function has return type ~a which doesn't match expected ~a" ty return)))))))
((check (make-immutable-hash empty)) expr)
(void))