-; we typecheck the lambda calculus only (only single arg lambdas)
-(define (typecheck prog)
- (define (check env x)
- (display "check: ")
- (display x)
- (display "\n\t")
- (display env)
- (newline)
- (let
- ((res
- (cond
- ((integer? x) (list '() 'int))
- ((boolean? x) (list '() 'bool))
- ((eq? x 'inc) (list '() '(abs int int)))
- ((eq? x '+) (list '() '(abs int (abs int int))))
- ((symbol? x) (list '() (env-lookup env x)))
-
- ((let? x)
- (let ((new-env (fold-left
- (lambda (acc bind)
- (let ((t (check
- (env-insert acc (car bind) (fresh-tvar))
- (cadr bind))))
- (env-insert acc (car bind) (cadr t))))
- env (let-bindings x))))
- (check new-env (last (let-body x)))))
-
-
- ((lambda? x)
- (let* ((new-env (env-insert env (lambda-arg x) (fresh-tvar)))
- (body-type-res (check new-env (lambda-body x)))
- (subd-env (substitute-env (car body-type-res) new-env)))
- (display "lambda: ")
- (display body-type-res)
- (display "\n")
- (display subd-env)
- (display "\n")
- (list (car body-type-res)
- (list 'abs
- (env-lookup subd-env (lambda-arg x))
- (cadr body-type-res)))))
-
- ((app? x) ; (f a)
- (let* ((arg-type-res (check env (cadr x)))
- (arg-type (cadr arg-type-res))
- (func-type-res (check env (car x)))
- (func-type (cadr func-type-res))
+(define (check-let env x)
+
+ ; acc is a pair of (env . annotated bindings)
+ (define (process-component acc comps)
+ (let*
+ ; create a new env with tvars for each component
+ ; e.g. scc of (x y)
+ ; scc-env = ((x . t0) (y . t1))
+ ([scc-env
+ (fold-left
+ (lambda (acc c)
+ (env-insert acc c (fresh-tvar)))
+ (car acc) comps)]
+ ; typecheck each component
+ [type-results
+ (map
+ (lambda (c)
+ (let ([body (cadr (assoc c (let-bindings x)))])
+ (check scc-env body)))
+ comps)]
+ ; collect all the constraints in the scc
+ [cs
+ (fold-left
+ (lambda (acc res c)
+ (constraint-merge
+ (constraint-merge
+ ; unify with tvars from scc-env
+ ; result ~ tvar
+ (~ (env-lookup scc-env c) (cadr res))
+ (car res))
+ acc))
+ '() type-results comps)]
+ ; substitute *only* the bindings in this scc
+ [new-env
+ (map (lambda (x)
+ (if (memv (car x) comps)
+ (cons (car x) (substitute cs (cdr x)))
+ x))
+ scc-env)]
+
+ [annotated-bindings (append (cdr acc) ; the previous annotated bindings
+ (map list
+ comps
+ (map caddr type-results)))])
+ (cons new-env annotated-bindings)))
+ ; takes in the current environment and a scc
+ ; returns new environment with scc's types added in
+ (let* ([components (reverse (sccs (graph (let-bindings x))))]
+ [results (fold-left process-component (cons env '()) components)]
+ [new-env (car results)]
+ [annotated-bindings (cdr results)]
+
+ [body-results (map (lambda (body) (check new-env body)) (let-body x))]
+ [let-type (cadr (last body-results))]
+ [cs (fold-left (lambda (acc cs) (constraint-merge acc cs)) '() (map car body-results))]
+
+ [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
+ (list cs let-type annotated)))
+
+(define (check-app env x)
+ (if (eqv? (car x) (cadr x))
+ ; recursive function (f f)
+ ; TODO: what about ((f a) f)????
+ (let* ([func-type (env-lookup env (car x))]
+ [return-type (fresh-tvar)]
+ [other-func-type `(abs ,func-type ,return-type)]
+ [cs (~ func-type other-func-type)]
+ [resolved-return-type (substitute cs return-type)]
+
+ [annotated `(((,(car x) : ,func-type)
+ (,(cadr x) : ,func-type)) : ,resolved-return-type)])
+ (list cs resolved-return-type annotated)))
+
+ ; regular function
+ (let* ([arg-type-res (check env (cadr x))]
+ [arg-type (cadr arg-type-res)]
+ [func-type-res (check env (car x))]
+ [func-type (cadr func-type-res)]