X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=821035230affddf4d813074316f5aecaeaa2efc5;hp=57a7815897e2bc9dd9c466c972d35431807aba4d;hb=844dcd052c6f551d9936693c2b4c49cf920c7051;hpb=74729258ddf19dfeb175cf98d5a3891cd8160faf

diff --git a/typecheck.scm b/typecheck.scm
index 57a7815..8210352 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -4,14 +4,13 @@
   (and (list? t) (eq? (car t) 'abs)))
 
 (define (tvar? t)
-  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
+  (and (not (list? t))
+       (not (concrete? t))
+       (symbol? t)))
 
 (define (concrete? t)
-  (case t
-    ('int #t)
-    ('bool #t)
-    ('void #t)
-    (else #f)))
+  (and (symbol? t)
+       (char-upper-case? (string-ref (symbol->string t) 0))))
 
 (define (pretty-type t)
   (cond ((abs? t)
@@ -38,7 +37,7 @@
 
 					; ('a, ('b, 'a))
 (define (env-lookup env n)
-  (if (null? env) (error #f "empty env")			; it's a type equality
+  (if (null? env) (error #f "empty env" env n)			; it's a type equality
       (if (eq? (caar env) n)
 	  (cdar env)
 	  (env-lookup (cdr env) n))))
@@ -82,46 +81,16 @@
 
 (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)))
-
-(define (check env x)
-  ;; (display "check: ")
-  ;; (display x)
-  ;; (display "\n\t")
-  ;; (display env)
-  ;; (newline)
-  (let
-      ((res
-	(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 (~ (cadr then-type-res)
-				      (cadr else-type-res)))
-		  (cs (constraint-merge
-		       (car then-type-res)
-		       (constraint-merge (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
+    ('+ '(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 (error #f "Couldn't find type for builtin" x))))
+
+(define (check-let env x)
   					; 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))))]
@@ -166,6 +135,38 @@
 	 [new-env (fold-left process-component env components)])
     (check new-env (last (let-body x)))))
 
+(define (check env x)
+  ;; (display "check: ")
+  ;; (display x)
+  ;; (display "\n\t")
+  ;; (display env)
+  ;; (newline)
+  (let
+      ((res
+	(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 (~ (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))))
+	     (list cs return-type)))
+	  
+	  ('var (list '() (env-lookup env x)))
+	  ('let (check-let env x))
+
+	  
 	  ('lambda
 	      (let* [(new-env (env-insert env (lambda-arg x) (fresh-tvar)))
 
@@ -237,7 +238,12 @@
 
 					; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
-  (cadr (check '() (normalize prog))))
+
+  (let ([init-env (flat-map data-tors (program-datas prog))])
+    (display init-env)
+    (newline)
+    (cadr (check init-env (normalize (program-body prog))))))
+
   
 					; returns a list of constraints
 (define (~ a b)
@@ -311,7 +317,7 @@
 
 
 ;; 					; a1 -> a2 ~ a3 -> a4;
-;; 					; a1 -> a2 !~ bool -> bool
+;; 					; a1 -> a2 !~ Bool -> Bool
 ;; 					; basically can the tvars be renamed
 (define (types-equal? x y)
   (let ([cs (unify? x y)])