X-Git-Url: http://git.lukelau.me/?a=blobdiff_plain;f=typecheck.scm;h=7eb4fa96606d786b5e58d17f2d2601f4f52c85a3;hb=91145e54f41ee88f1e279a80430b3f5ed4e7a8c6;hp=0e4e265f2d2a47f81b8a13ea4ade24914c3b33a1;hpb=ba17902b367783f058108f2eb9dff163d34b735f;p=scheme.git

diff --git a/typecheck.scm b/typecheck.scm
index 0e4e265..7eb4fa9 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,18 +1,37 @@
-(define (app? x)
-  (and (list? x) (>= (length x) 2) (not (eq? (car x) 'lambda))))
+(load "ast.scm")
 
-(define (lambda? x)
-  (and (list? x) (eq? (car x) 'lambda)))
+(define (abs? t)
+  (and (list? t) (eq? (car t) 'abs)))
+
+(define (tvar? t)
+  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
+
+(define (concrete? t)
+  (case t
+    ('int #t)
+    ('bool #t)
+    ('void #t)
+    (else #f)))
 
-(define lambda-arg caadr)
-(define lambda-body caddr)
+(define (pretty-type t)
+  (cond ((abs? t)
+	 (string-append
+	  (if (abs? (cadr t))
+	      (string-append "(" (pretty-type (cadr t)) ")")
+	      (pretty-type (cadr t)))
+	  " -> "
+	  (pretty-type (caddr t))))
+	(else (symbol->string t))))
 
 					; ('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,43 +42,105 @@
     (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))))
-   ((app? prog)
+  (case (ast-type prog)
+    ('lambda 
+					; (lambda (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
+	(if (> (length (lambda-args prog)) 1)
+	    (list 'lambda (list (car (lambda-args prog)))
+		  (normalize (list 'lambda (cdr (lambda-args prog)) (caddr prog))))
+	    (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
+    ('app
      (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)
-   (else prog)))
+	 `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
+	 `(,(list (normalize (car prog)) (normalize (cadr prog)))
+	   ,(normalize (caddr prog))))) ; (f a b)
+    ('let
+	(append (list 'let
+		      (map (lambda (x) `(,(car x) ,(normalize (cadr x))))
+			   (let-bindings prog)))
+		(map normalize (let-body prog))))
+    (else (ast-traverse normalize prog))))
 
+(define (builtin-type x)
+  (case x
+    ('+ '(abs int (abs int int)))
+    ('- '(abs int (abs int int)))
+    ('* '(abs int (abs int int)))
+    ('! '(abs bool bool))
+    ('= '(abs int (abs int bool)))
+    ('bool->int '(abs bool int))
+    ('print '(abs string void))
+    (else #f)))
 
+; 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)))
-
-	   ((lambda? x)
-	    (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
+	  (case (ast-type x)
+	   ('int-literal (list '() 'int))
+	   ('bool-literal (list '() 'bool))
+	   ('string-literal (list '() 'string))
+	   ('builtin (list '() (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 (unify (cadr then-type-res)
+					   (cadr else-type-res)))
+		   (cs (consolidate
+			(car then-type-res)
+			(consolidate (car else-type-res)
+				     then-eq-else-cs)))
+		   (return-type (substitute cs (cadr then-type-res))))
+	      (when (not (eqv? (cadr cond-type-res) 'bool))
+		(error #f "if condition isn't bool"))
+	      (list cs return-type)))
+	   
+	   ('var  (list '() (env-lookup env x)))
+	   ('let
+	    (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
+	    (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")
+		   (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)))
+	      ;; (display "lambda:\n\t")
+	      ;; (display prog)
+	      ;; (display "\n\t")
+	      ;; (display cs)
+	      ;; (display "\n\t")
+	      ;; (display resolved-arg-type)
+	      ;; (newline)
 	      (list (car body-type-res)
 		    (list 'abs
-			  (env-lookup subd-env (lambda-arg x))
+			  resolved-arg-type
 			  (cadr body-type-res)))))
 	   
-	   ((app? x) ; (f a)
+	   ('app ; (f a)
 	    (let* ((arg-type-res (check env (cadr x)))
 		   (arg-type (cadr arg-type-res))
 		   (func-type-res (check env (car x)))
@@ -70,7 +151,9 @@
 				  (list 'abs
 					arg-type
 					(fresh-tvar))))
-		   (cs (append func-c (car arg-type-res) (car func-type-res)))
+		   (cs (consolidate
+			(consolidate func-c (car arg-type-res))
+			(car func-type-res)))
 		   
 		   (resolved-func-type (substitute cs func-type))
 		   (resolved-return-type (caddr resolved-func-type)))
@@ -86,7 +169,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")
@@ -97,19 +180,6 @@
       res))
   (cadr (check '() (normalize prog))))
 
-
-(define (abs? t)
-  (and (list? t) (eq? (car t) 'abs)))
-
-(define (tvar? t)
-  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
-
-(define (concrete? t)
-  (case t
-    ('int #t)
-    ('bool #t)
-    (else #f)))
-
 					; returns a list of pairs of constraints
 (define (unify a b)
   (cond ((eq? a b) '())
@@ -119,22 +189,32 @@
 		      (unify (caddr a) (caddr b))))
 	(else (error #f "could not unify"))))
 
-
 					; TODO: what's the most appropriate substitution?
 					; should all constraints just be limited to a pair?
 (define (substitute cs t)
-  (define (blah c)
-    (if (null? (cdr c))
-	(car c)
+					; gets the first concrete type
+					; otherwise returns the last type variable
+
+  (define (get-concrete c)
+    (let ((last (null? (cdr c))))
       (if (not (tvar? (car c)))
+	  (if (abs? (car c))
+	      (substitute cs (car c))
+	      (car c))
+	  (if last
 	      (car c)
-	    (blah (cdr c)))))
+	      (get-concrete (cdr c))))))
+  (cond
+   ((abs? t) (list 'abs
+		   (substitute cs (cadr t))
+		   (substitute cs (caddr t))))
+   (else
     (fold-left
      (lambda (t c)
        (if (member t c)
-	 (blah c)
+	   (get-concrete c)
 	   t))
-   t cs))
+     t cs))))
 
 (define (substitute-env cs env)
   (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))