Fix total pattern match verification

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index c6b90e701f467d1651d87c434441b4305ea98742..b2b001f1d27220211e5f67e651d641c9895f5b5c 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,4 +1,5 @@
 (load "ast.scm")
+(load "stdlib.scm")
 
 (define (abs? t)
   (and (list? t) (eq? (car t) 'abs)))
@@ -191,6 +192,20 @@
 (define (check-case dls env x)
 
   (define (check-match switch-type x)
+    
+    (define (get-bindings product-types pattern)
+      (define (go product-type product)
+       (case (ast-type product)
+         ['var (list (cons product product-type))]
+                                       ; an inner pattern match
+         ['app (let* ([inner-sum (car product)]
+                      [inner-sums (cdr (assoc product-type dls))]
+                      [inner-product-types (cdr (assoc inner-sum inner-sums))])
+                 (get-bindings inner-product-types product))]
+         [else '()]))
+      (flat-map go product-types (cdr pattern)))
+
+    
     (let ([pattern (car x)]
          [expr (cadr x)])
       (case (ast-type pattern)
@@ -199,8 +214,9 @@
          (let ([sum (assoc (car pattern) (cdr (assoc switch-type dls)))])
            (unless sum (error #f "can't pattern match ~a with ~a" switch-type pattern))
            (let* ([names (cdr pattern)]
-                  [types (cdr sum)]
-                  [new-env (fold-left env-insert env names types)])
+                  [product-types (cdr sum)]
+                  [new-env (append (get-bindings product-types pattern) env)])
+
              (check dls new-env expr)))]
                                        ; pattern match with binding and no constructor
        ['var (check dls (env-insert env pattern switch-type) expr)]
@@ -243,7 +259,6 @@
       ((res
        (case (ast-type x)
          ('int-literal (make-result '() 'Int))
-         ('bool-literal (make-result '() 'Bool))
          ('string-literal (make-result '() 'String))
          ('builtin (make-result '() (builtin-type x)))
 
@@ -303,8 +318,9 @@
   (flat-map data-tors-type-env (program-data-layouts prog)))
 
                                        ; we typecheck the lambda calculus only (only single arg lambdas)
-(define (typecheck prog)
-  (let ([expanded (expand-pattern-matches prog)])
+(define (typecheck prog-without-stdlib)
+  (let* ([prog (append stdlib prog-without-stdlib)]
+        [expanded (expand-pattern-matches prog)])
     (cadr (check (program-data-layouts prog)
                 (init-adts-env expanded)
                 (normalize (program-body expanded))))))