X-Git-Url: https://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=a7384294ac0e5ad2e4d7225a53cca150b93ba2ea;hp=0e4e265f2d2a47f81b8a13ea4ade24914c3b33a1;hb=3ce93ef63f164f8dc63c89f1a97f46e200c71d02;hpb=b5fad4a5e1ad7d15dc440089edc9e137bc377be9

diff --git a/typecheck.scm b/typecheck.scm
index 0e4e265..a738429 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,18 +1,13 @@
-(define (app? x)
-  (and (list? x) (>= (length x) 2) (not (eq? (car x) 'lambda))))
-
-(define (lambda? x)
-  (and (list? x) (eq? (car x) 'lambda)))
-
-(define lambda-arg caadr)
-(define lambda-body caddr)
-
+(load "ast.scm")
 					; ('a, ('b, 'a))
-(define (env-lookup env x)
+(define (env-lookup env n)
   (if (null? env) (error #f "empty env")			; it's a type equality
-      (if (eq? (caar env) x)
+      (if (eq? (caar env) n)
 	  (cdar env)
-	  (env-lookup (cdr env) x))))
+	  (env-lookup (cdr env) n))))
+
+(define (env-insert env n t)
+  (cons (cons n t) env))
 
 (define abs-arg cadr)
 
@@ -23,19 +18,32 @@
     (string->symbol
      (string-append "t" (number->string (- cur-tvar 1))))))
 
+(define (last xs)
+  (if (null? (cdr xs))
+      (car xs)
+      (last (cdr xs))))
+
 					
 (define (normalize prog) ; (+ a b) -> ((+ a) b)
   (cond
-   ((lambda? prog) '(lambda (lambda-arg prog) (normalize (lambda-body prog))))
+   ((lambda? prog) (list 'lambda (lambda-arg prog) (normalize (lambda-body prog))))
    ((app? prog)
     (if (null? (cddr prog))
 	(cons (normalize (car prog)) (normalize (cdr prog))) ; (f a)
 	(normalize (cons (cons (car prog) (list (cadr prog))) (cddr prog))))) ; (f a b)
+   ((let? prog)
+    (append (list 'let
+		  (map (lambda (x) (cons (car x) (normalize (cdr x))))
+		       (let-bindings prog)))
+	    (map normalize (let-body prog))))
    (else prog)))
 
 
 (define (typecheck prog)
   (define (check env x)
+    ;; (display "check: ")
+    ;; (display x)
+    ;; (display "\n")
     (let
 	((res
 	  (cond
@@ -45,6 +53,17 @@
 	   ((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 (cons (cons (lambda-arg x) (fresh-tvar)) env))
 		   (body-type-res (check new-env (lambda-body x)))
@@ -86,7 +105,7 @@
 	      (if (abs? resolved-func-type)
 		  (let ((return-type (substitute cs (caddr resolved-func-type))))
 		    (list cs return-type))
-		  (error #f "wah")))))))
+		  (error #f "not a function")))))))
       ;; (display "result of ")
       ;; (display x)
       ;; (display ":\n\t")
@@ -123,16 +142,18 @@
 					; TODO: what's the most appropriate substitution?
 					; should all constraints just be limited to a pair?
 (define (substitute cs t)
-  (define (blah c)
+					; gets the first concrete type
+					; otherwise returns the last type variable
+  (define (get-concrete c)
     (if (null? (cdr c))
 	(car c)
 	(if (not (tvar? (car c)))
 	    (car c)
-	    (blah (cdr c)))))
+	    (get-concrete (cdr c)))))
   (fold-left
    (lambda (t c)
      (if (member t c)
-	 (blah c)
+	 (get-concrete c)
 	 t))
    t cs))