- (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))
+ (case (ast-type x)
+ ('int-literal (make-result '() 'Int))
+ ('bool-literal (make-result '() 'Bool))
+ ('string-literal (make-result '() 'String))
+ ('builtin (make-result '() (builtin-type x)))
+
+ ('if
+ (let* ((cond-type-res (check env (cadr x)))
+ (then-type-res (check env (caddr x)))
+ (else-type-res (check env (cadddr x)))
+ (then-eq-else-cs (~ (cadr then-type-res)
+ (cadr else-type-res)))
+ (cs (constraint-merge
+ (car then-type-res)
+ (constraint-merge (~ (cadr cond-type-res) 'Bool)
+ (constraint-merge (car else-type-res)
+ then-eq-else-cs))))
+ (return-type (substitute cs (cadr then-type-res)))
+ [annotated `((if ,(caddr cond-type-res)
+ ,(caddr then-type-res)
+ ,(caddr else-type-res)) : ,return-type)])
+ (list cs return-type annotated)))
+
+ ('var (make-result '() (env-lookup env x)))
+ ('let (check-let env x))
+
+
+ ('lambda
+ (let* ([new-env (env-insert env (lambda-arg x) (fresh-tvar))]
+
+ [body-type-res (check new-env (lambda-body x))]
+ [cs (car body-type-res)]
+ [subd-env (substitute-env (car body-type-res) new-env)]
+ [arg-type (env-lookup subd-env (lambda-arg x))]
+ [resolved-arg-type (substitute cs arg-type)]
+
+ [lambda-type `(abs ,resolved-arg-type ,(cadr body-type-res))]
+
+ ; TODO: do we need to annotate the lambda argument?
+ [annotated `(lambda (,(lambda-arg x)) ,(caddr body-type-res))])
+
+ (list (car body-type-res) ; constraints
+ lambda-type ; type
+ annotated)))
+
+
+ ('app ; (f a)
+ (if (eqv? (car x) (cadr x))
+ ; recursive function (f 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)]