Formulate destructors properly

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index 57a7815897e2bc9dd9c466c972d35431807aba4d..821035230affddf4d813074316f5aecaeaa2efc5 100644 (file)
--- 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)])