Fix up typechecking of case

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index e3986062e358d763e99746f2ebdd26828337336f..1b2f21479eb539915b5e46bd0d646b78330d6d27 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -244,7 +244,40 @@
                      annotated)))
 
          
-         ('app (check-app env x)))))
+         ('app (check-app env x))
+         ['case
+             (let* ([expr-type-res (check env (case-expr x))]
+                    [expr-type (cadr expr-type-res)]
+                    [case-match-type-res (map (lambda (x) (check env x))
+                                              (map car (case-cases x)))]
+                    [case-match-types (map cadr case-match-type-res)]
+                    
+                    [case-expr-type-res (map (lambda (x) (check env x))
+                                             (map cadr (case-cases x)))]
+                    [case-expr-types (map cadr case-expr-type-res)]
+
+                    [case-match-equality-cs (fold-left constraint-merge '()
+                                                       (map (lambda (t) (~ t expr-type)) case-match-types))]
+
+                    [case-expr-equality-cs (fold-left constraint-merge '()
+                                                      (map (lambda (t) (~ t (car case-expr-types)))
+                                                           (cdr case-expr-types)))]
+
+                    [resolved-type (substitute case-expr-equality-cs (car case-expr-types))]
+
+                    [annotated `((case (,(case-expr x) : ,expr-type)
+                                   ,(map (lambda (c e et)
+                                           `(,c (,e : ,et)))
+                                         (map car (case-cases x))
+                                         (map cadr (case-cases x))
+                                         case-expr-types)) : ,resolved-type)]
+                    
+                    [cs (fold-left constraint-merge '()
+                                   (append case-match-equality-cs
+                                           case-expr-equality-cs
+                                           (car expr-type-res)))])
+               (list cs resolved-type annotated))])))
+               
     ;; (display "result of ")
     ;; (display x)
     ;; (display ":\n\t")
@@ -255,11 +288,12 @@
     res))
 
 (define (init-adts-env prog)
-  (flat-map data-tors-env (program-data-layouts prog)))
+  (flat-map data-tors-type-env (program-data-layouts prog)))
 
                                        ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
-  (cadr (check (init-adts-env prog) (normalize (program-body prog)))))
+  (let ([expanded (expand-pattern-matches prog)])
+    (cadr (check (init-adts-env expanded) (normalize (program-body expanded))))))
 
 
                                        ; before passing annotated types onto codegen
@@ -309,8 +343,11 @@
 
 (define ann-expr car)
 (define ann-type caddr)
+
+                                       ; prerequisites: expand-pattern-matches
 (define (annotate-types prog)
-  (denormalize (program-body prog)
+  (denormalize
+   (program-body prog)
    (caddr (check (init-adts-env prog) (normalize (program-body prog))))))