Start work on ADTs

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index 57a7815897e2bc9dd9c466c972d35431807aba4d..4cc93495fb9dd6bc90b03b9b06271e316c65a8bb 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)
@@ -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)))
 
@@ -226,18 +227,30 @@
                     (let ((return-type (substitute cs (caddr resolved-func-type))))
                       (list cs return-type))
                     (error #f "not a function")))))))
-    ;; (display "result of ")
-    ;; (display x)
-    ;; (display ":\n\t")
-    ;; (display (pretty-type (cadr res)))
-    ;; (display "\n\t[")
-    ;; (display (pretty-constraints (car res)))
-    ;; (display "]\n")
+    (display "result of ")
+    (display x)
+    (display ":\n\t")
+    (display (pretty-type (cadr res)))
+    (display "\n\t[")
+    (display (pretty-constraints (car res)))
+    (display "]\n")
     res))
 
                                        ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
-  (cadr (check '() (normalize prog))))
+  (define (constructor-type t ctr)
+    (fold-left (lambda (acc x) `(abs ,x ,acc)) t (cdr ctr)))
+  (define (constructors data-def)
+    (let ([type-name (cadr data-def)]
+         [ctrs (cddr data-def)])
+    (fold-left (lambda (acc ctr)
+                (cons (cons (car ctr) (constructor-type type-name ctr))
+                      acc))
+              '()
+              ctrs)))
+  (let ([init-env (flat-map constructors (program-datas prog))])
+    (display init-env)
+    (cadr (check init-env (normalize (program-body prog))))))
 
                                        ; returns a list of constraints
 (define (~ a b)
@@ -311,7 +324,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)])