Add bindings to pattern matching in case statement typechecking

diff --git a/ast.scm b/ast.scm
index 86d522560a8012546e6a754499b1216052d8ce70..109ce91a49ff95f7857550c0119f958b90caeefd 100644 (file)
--- a/ast.scm
+++ b/ast.scm
@@ -36,7 +36,7 @@
     ('app (map f x))
     ('lambda `(lambda ,(lambda-args x) ,(f (lambda-body x))))
     ('if `(if ,@(map f (cdr x))))
-    ('case `(case ,(f (case-expr x))
+    ('case `(case ,(f (case-switch x))
              ,@(map (lambda (x)
                       (list (car x) (f (cadr x))))
                     (case-cases x))))
@@ -56,7 +56,7 @@
     ['if (append (f x)
                 (flat-map inner (cdr x)))]
     ['case (append (f x)
-                  (inner (case-expr x))
+                  (inner (case-switch x))
                   (flat-map inner (map cadr (case-cases x))))]
     ['stack (append (f x)
                    (inner (caddr x)))]
@@ -88,9 +88,45 @@
 (define let-bindings cadr)
 (define let-body cddr)
 
-(define case-expr cadr)
+(define case-switch cadr)
 (define case-cases cddr)
 
+;; (define (verify-cases data-layouts annotated-program)
+
+;;   (define allowed-match-ast-types    
+;;     '((Int . (int-literal var))
+;;       (Bool . (bool-literal var))
+;;       (String . (string-literal var))))
+
+;;   (define (check-pattern switch-type pat)
+
+;;     (define (impossible-match)
+;;       (error "Can't pattern match ~a with ~a" switch-type (ann-expr pat)))
+
+;;     (if (assoc switch-type data-layouts)
+;;     (begin
+;;       (let ([sums (cdr (assoc switch-type data-layouts))])
+;;         (unless (eqv? (ast-type (ann-expr pat)) 'var) (impossible-match))
+;;         (unless (assoc (car (ann-expr pat)) sums) (impossible-match))
+;;         (unless 
+;;       )
+;;        (begin
+;;      (unless (assoc switch-type allowed-match-ast-types)
+;;        (error #f "Can't pattern match on ~a" switch-type))
+        
+;;      (let ([allowed (cdr (assoc switch-type allowed-match-ast-types))])
+;;        (unless (assoc (ast-type (ann-expr pat)) allowed) (impossible-match)))))))
+
+  
+;;   (let ([expr (ann-expr annotated-program)])
+;;     (case (ast-type expr)
+;;       ['case
+;;       (let* ([switch-type (ann-type (case-switch expr))]
+;;              [allowed (cdr (assoc switch-type allowed-match-ast-types))])
+;;         (for-each 
+;;           []))]))))
+
+
                                        ; (let ([(foo a b) (foo 123 345)]) a)
                                        ;   |
                                        ;   v
@@ -98,7 +134,7 @@
                                         ;       [b (foo~1 (foo 123 345)]) a)
 (define (expand-pattern-matches program)
   (define (go x)
-    (define (pattern-match binding)
+    (define (let-pattern-match binding)
       (let ([binding-name (car binding)]
            [body (cadr binding)])
        (if (eqv? (ast-type binding-name) 'var)
@@ -132,11 +168,12 @@
                               binding)))
              
              (flat-map (lambda (y i)
-                         (pattern-match (list y `(,(destructor i) ,body))))
+                         (let-pattern-match (list y `(,(destructor i) ,body))))
                        products
                        (range 0 (length products)))))))
+
     (case (ast-type x)
-      ['let `(let ,(flat-map pattern-match (let-bindings x))
+      ['let `(let ,(flat-map let-pattern-match (let-bindings x))
               ,@(map go (let-body x)))]
       [else (ast-traverse go x)]))
   (program-map-exprs go program))

diff --git a/typecheck.scm b/typecheck.scm
index 1b2f21479eb539915b5e46bd0d646b78330d6d27..ebfd816ad62a9538839c808187d55cbeaad593db 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -90,7 +90,7 @@
     ('print '(abs String Void))
     (else (error #f "Couldn't find type for builtin" x))))
 
-(define (check-let env x)
+(define (check-let dls env x)
 
   ; acc is a pair of (env . annotated bindings)
   (define (process-component acc comps)
@@ -108,7 +108,7 @@
          (map
           (lambda (c)
             (let ([body (cadr (assoc c (let-bindings x)))])
-              (check scc-env body)))
+              (check dls scc-env body)))
           comps)]
                                        ; collect all the constraints in the scc
         [cs
@@ -142,14 +142,14 @@
         [new-env (car results)]
         [annotated-bindings (cdr results)]
 
-        [body-results (map (lambda (body) (check new-env body)) (let-body x))]
+        [body-results (map (lambda (body) (check dls new-env body)) (let-body x))]
         [let-type (cadr (last body-results))]
         [cs (fold-left (lambda (acc cs) (constraint-merge acc cs)) '() (map car body-results))]
 
         [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
     (list cs let-type annotated)))
 
-(define (check-app env x)
+(define (check-app dls env x)
   (if (eqv? (car x) (cadr x))
                                        ; recursive function (f f)
                                        ; TODO: what about ((f a) f)????
@@ -164,9 +164,9 @@
        (list cs resolved-return-type annotated)))
 
                                        ; regular function
-  (let* ([arg-type-res (check env (cadr x))]
+  (let* ([arg-type-res (check dls env (cadr x))]
         [arg-type (cadr arg-type-res)]
-        [func-type-res (check env (car x))]
+        [func-type-res (check dls env (car x))]
         [func-type (cadr func-type-res)]
         
                                        ; f ~ a -> t0
@@ -188,8 +188,47 @@
          (list cs return-type annotated))
        (error #f "not a function"))))
 
+(define (check-case dls env x)
+
+  (define (check-match switch-type x)
+    (let ([pattern (car x)]
+         [expr (cadr x)])
+      (if (eqv? (ast-type pattern) 'app)
+                                       ; a pattern match with bindings
+         (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)])
+             (check dls new-env expr)))
+                                       ; a pattern match without bindings
+         (check dls env expr))))
+  
+  (let* ([switch-type-res (check dls env (case-switch x))]
+        [switch-type (cadr switch-type-res)]
+        
+        [case-expr-type-res (map (lambda (x) (check-match switch-type x)) (case-cases x))]
+        [case-expr-types (map cadr case-expr-type-res)]
+
+        [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) : ,switch-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 '()
+                       (cons (car switch-type-res) case-expr-equality-cs))])
+    (list cs resolved-type annotated)))
+
 ; returns a list (constraints type annotated)
-(define (check env x)
+(define (check dls env x)
   (define (make-result cs type)
     (list cs type `(,x : ,type)))
   ;; (display "check: ")
@@ -206,9 +245,9 @@
          ('builtin (make-result '() (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)))
+          (let* ((cond-type-res (check dls env (cadr x)))
+                 (then-type-res (check dls env (caddr x)))
+                 (else-type-res (check dls env (cadddr x)))
                  (then-eq-else-cs (~ (cadr then-type-res)
                                      (cadr else-type-res)))
                  (cs (constraint-merge
@@ -223,13 +262,13 @@
             (list cs return-type annotated)))
          
          ('var (make-result '() (env-lookup env x)))
-         ('let (check-let env x))
+         ('let (check-let dls env x))
 
          
          ('lambda
              (let* ([new-env (env-insert env (lambda-arg x) (fresh-tvar))]
 
-                    [body-type-res (check new-env (lambda-body x))]
+                    [body-type-res (check dls new-env (lambda-body x))]
                     [cs (car body-type-res)]
                     [subd-env (substitute-env (car body-type-res) new-env)]
                     [arg-type (env-lookup subd-env (lambda-arg x))]
@@ -244,39 +283,9 @@
                      annotated)))
 
          
-         ('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)]
+         ('app (check-app dls env x))
+         ['case (check-case dls env x)])))
              
-                    [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)
@@ -293,7 +302,9 @@
                                        ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
   (let ([expanded (expand-pattern-matches prog)])
-    (cadr (check (init-adts-env expanded) (normalize (program-body expanded))))))
+    (cadr (check (program-data-layouts prog)
+                (init-adts-env expanded)
+                (normalize (program-body expanded))))))
 
 
                                        ; before passing annotated types onto codegen