4 (and (list? t) (eq? (car t) 'abs)))
7 (and (not (list? t)) (not (concrete? t)) (symbol? t)))
16 (define (pretty-type t)
20 (string-append "(" (pretty-type (cadr t)) ")")
21 (pretty-type (cadr t)))
23 (pretty-type (caddr t))))
24 (else (symbol->string t))))
26 (define (pretty-constraints cs)
28 (fold-left string-append
40 (define (env-lookup env n)
41 (if (null? env) (error #f "empty env") ; it's a type equality
42 (if (eq? (caar env) n)
44 (env-lookup (cdr env) n))))
46 (define (env-insert env n t)
47 (cons (cons n t) env))
54 (set! cur-tvar (+ cur-tvar 1))
56 (string-append "t" (number->string (- cur-tvar 1))))))
63 (define (normalize prog) ; (+ a b) -> ((+ a) b)
66 ; (lambda (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
67 (if (> (length (lambda-args prog)) 1)
68 (list 'lambda (list (car (lambda-args prog)))
69 (normalize (list 'lambda (cdr (lambda-args prog)) (caddr prog))))
70 (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
72 (if (null? (cddr prog))
73 `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
74 (normalize `(,(list (normalize (car prog)) (normalize (cadr prog)))
75 ,@(cddr prog))))) ; (f a b)
78 (map (lambda (x) `(,(car x) ,(normalize (cadr x))))
80 (map normalize (let-body prog))))
81 (else (ast-traverse normalize prog))))
83 (define (builtin-type x)
85 ('+ '(abs int (abs int int)))
86 ('- '(abs int (abs int int)))
87 ('* '(abs int (abs int int)))
89 ('= '(abs int (abs int bool)))
90 ('bool->int '(abs bool int))
91 ('print '(abs string void))
103 ('int-literal (list '() 'int))
104 ('bool-literal (list '() 'bool))
105 ('string-literal (list '() 'string))
106 ('builtin (list '() (builtin-type x)))
109 (let* ((cond-type-res (check env (cadr x)))
110 (then-type-res (check env (caddr x)))
111 (else-type-res (check env (cadddr x)))
112 (then-eq-else-cs (~ (cadr then-type-res)
113 (cadr else-type-res)))
114 (cs (constraint-merge
116 (constraint-merge (car else-type-res)
118 (return-type (substitute cs (cadr then-type-res))))
119 (when (not (eqv? (cadr cond-type-res) 'bool))
120 (error #f "if condition isn't bool"))
121 (list cs return-type)))
123 ('var (list '() (env-lookup env x)))
125 ; takes in the current environment and a scc
126 ; returns new environment with scc's types added in
127 (let* ([components (reverse (sccs (graph (let-bindings x))))]
131 ; create a new env with tvars for each component
133 ; scc-env = ((x . t0) (y . t1))
137 (env-insert acc c (fresh-tvar)))
139 ; typecheck each component
143 (let ([body (cadr (assoc c (let-bindings x)))])
144 (check scc-env body)))
146 ; collect all the constraints in the scc
152 ; unify with tvars from scc-env
154 (~ (env-lookup scc-env c) (cadr res))
157 '() type-results comps)]
158 ; substitute *only* the bindings in this scc
161 (if (memv (car x) comps)
162 (cons (car x) (substitute cs (cdr x)))
169 [new-env (fold-left process-component env components)])
170 (check new-env (last (let-body x)))))
173 (let* [(new-env (env-insert env (lambda-arg x) (fresh-tvar)))
175 (body-type-res (check new-env (lambda-body x)))
176 (cs (car body-type-res))
177 (subd-env (substitute-env (car body-type-res) new-env))
178 (arg-type (env-lookup subd-env (lambda-arg x)))
179 (resolved-arg-type (substitute cs arg-type))]
180 ;; (display "lambda:\n\t")
185 ;; (display (format "subd-env: ~a\n" subd-env))
186 ;; (display resolved-arg-type)
188 (list (car body-type-res)
191 (cadr body-type-res)))))
194 (if (eqv? (car x) (cadr x))
195 ; recursive function (f f)
196 (let* [(func-type (env-lookup env (car x)))
197 (return-type (fresh-tvar))
198 (other-func-type `(abs ,func-type ,return-type))
199 (cs (~ func-type other-func-type))
200 (resolved-return-type (substitute cs return-type))]
201 (list cs resolved-return-type))
204 (let* ((arg-type-res (check env (cadr x)))
205 (arg-type (cadr arg-type-res))
206 (func-type-res (check env (car x)))
207 (func-type (cadr func-type-res))
211 (substitute (car arg-type-res) func-type)
212 `(abs ,arg-type ,(fresh-tvar))))
213 (cs (constraint-merge
214 (constraint-merge func-c (car arg-type-res))
215 (car func-type-res)))
217 (resolved-func-type (substitute cs func-type))
218 (resolved-return-type (caddr resolved-func-type)))
219 ;; (display "app:\n")
222 ;; (display func-type)
224 ;; (display resolved-func-type)
226 ;; (display arg-type-res)
228 (if (abs? resolved-func-type)
229 (let ((return-type (substitute cs (caddr resolved-func-type))))
230 (list cs return-type))
231 (error #f "not a function"))))))))
232 (display "result of ")
235 (display (pretty-type (cadr res)))
237 (display (pretty-constraints (car res)))
241 ; we typecheck the lambda calculus only (only single arg lambdas)
242 (define (typecheck prog)
243 (cadr (check '() (normalize prog))))
245 ; returns a list of constraints
247 (let ([res (unify? a b)])
251 (format "couldn't unify ~a ~~ ~a" a b)))))
254 (cond [(eq? a b) '()]
255 [(tvar? a) (list (cons a b))]
256 [(tvar? b) (list (cons b a))]
257 [(and (abs? a) (abs? b))
258 (let* [(arg-cs (unify? (cadr a) (cadr b)))
259 (body-cs (unify? (substitute arg-cs (caddr a))
260 (substitute arg-cs (caddr b))))]
261 (constraint-merge body-cs arg-cs))]
264 (define (substitute cs t)
270 [(abs? t) `(abs ,(substitute cs (cadr t))
271 ,(substitute cs (caddr t)))]
274 ; applies substitutions to all variables in environment
275 (define (substitute-env cs env)
276 (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
278 ; composes constraints a onto b and merges, i.e. applies a to b
279 ; a should be the "more important" constraints
280 (define (constraint-merge a b)
281 (define (f cs constraint)
282 (cons (car constraint)
283 (substitute cs (cdr constraint))))
285 (define (most-concrete a b)
289 [(and (abs? a) (abs? b))
290 `(abs ,(most-concrete (cadr a) (cadr b))
291 ,(most-concrete (caddr a) (caddr b)))]
294 [else (error #f "impossible! most-concrete")]))
298 (if (assoc (car x) a)
299 (cons (cons (car x) (most-concrete (cdr (assoc (car x) a))
303 (fold-left gen '() b))
305 ;; (define (union p q)
310 ;; (let ([x (car q)])
311 ;; (if (assoc (car x) p)
312 ;; (if (eqv? (most-concrete (cddr (assoc (car x) p))
315 ;; (cons x (union (filter (p) (not (eqv?
319 (append (filter (lambda (x) (not (assoc (car x) p)))
322 (display "clashes: ")
325 (append (clashes) (union a (map (lambda (z) (f a z)) b))))
328 ;; ; a1 -> a2 ~ a3 -> a4;
329 ;; ; a1 -> a2 !~ bool -> bool
330 ;; ; basically can the tvars be renamed
331 (define (types-equal? x y)
332 (let ([cs (unify? x y)])
335 ([test (lambda (acc c)
337 (tvar? (car c)) ; the only substitutions allowed are tvar -> tvar
339 (fold-left test #t cs)))))
341 ; input: a list of binds ((x . y) (y . 3))
342 ; returns: pair of verts, edges ((x y) . (x . y))
344 (define (go bs orig-bs)
345 (define (find-refs prog)
349 ; only count a reference if its a binding
350 ['var (if (assoc x orig-bs) (list x) '())]
355 (let* [(bind (car bs))
358 (refs (find-refs (cdr bind)))
359 (edges (map (lambda (x) (cons vert x))
362 (rest (if (null? (cdr bs))
364 (go (cdr bs) orig-bs)))
365 (total-verts (cons vert (car rest)))
366 (total-edges (append edges (cdr rest)))]
367 (cons total-verts total-edges))))
370 (define (successors graph v)
374 (if (eqv? v (caar E))
375 (cons (cdar E) (go v (cdr E)))
379 ; takes in a graph (pair of vertices, edges)
380 ; returns a list of strongly connected components
382 ; ((x y w) . ((x . y) (x . w) (w . x))
392 ; this uses tarjan's algorithm, to get reverse
393 ; topological sorting for free
396 (let* ([indices (make-hash-table)]
397 [lowlinks (make-hash-table)]
398 [on-stack (make-hash-table)]
404 (get-hash-table indices v #f))
406 (get-hash-table lowlinks v #f))
412 (put-hash-table! indices v current)
413 (put-hash-table! lowlinks v current)
414 (set! current (+ current 1))
416 (put-hash-table! on-stack v #t)
420 (if (not (hashtable-contains? indices w))
421 ; successor w has not been visited, recurse
424 (put-hash-table! lowlinks
426 (min (lowlink v) (lowlink w))))
427 ; successor w has been visited
428 (when (get-hash-table on-stack w #f)
429 (put-hash-table! lowlinks v (min (lowlink v) (index w))))))
430 (successors graph v))
432 (when (= (index v) (lowlink v))
435 (let ([w (pop! stack)])
436 (put-hash-table! on-stack w #f)
439 (cons w (new-scc)))))])
440 (set! result (cons scc result))))))])
443 (when (not (hashtable-contains? indices v)) ; v.index == -1