Check for complete pattern matches

diff --git a/ast.scm b/ast.scm
index d2328cc6449d014eacb085fdc0b734f620c1ceb2..eabad585fec27b4f6c83f3c747ca0c7925a80de2 100644 (file)
--- a/ast.scm
+++ b/ast.scm
@@ -64,28 +64,20 @@
 
 (define (ast-find p x)
   (define (inner y) (ast-find p y))
-  (define (any p x) (fold-left
-                    (lambda (acc y) (if acc #t (p y)))
-                    #f
-                    x))
-  (define (either . fs)
-    (if (null? fs) #f
-       (if (car fs) (car fs)
-           (apply either (cdr fs)))))
   
   (case (ast-type x)
-    ['let (either (p x)
+    ['let (or (p x)
              (any inner (let-bindings x))
              (any inner (let-body x)))]
-    ['app (either (p x)
+    ['app (or (p x)
              (any inner x))]
-    ['lambda (either (p x)
+    ['lambda (or (p x)
                 (inner (lambda-body x)))]
-    ['if (either (p x) (any inner (cdr x)))]
-    ['case (either (p x)
+    ['if (or (p x) (any inner (cdr x)))]
+    ['case (or (p x)
               (any inner (map cadr (case-cases x)))
               (inner (case-switch x)))]
-    ['stack (either (p x) (inner (caddr x)))]
+    ['stack (or (p x) (inner (caddr x)))]
     [else (p x)]))
 
 (define let-bindings cadr)
@@ -94,12 +86,37 @@
 (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 (constructor? data-layouts x)
+  (and (eqv? (ast-type x) 'var)
+       (assoc x (flat-map cdr data-layouts))))
+
+(define (all-cases data-layouts type)
+  (let ([sums (assoc type data-layouts)])
+    (if sums
+       (flat-map (lambda (sum)
+                   (let* ([sum-name (car sum)]
+                          [products (cdr sum)]
+                          [product-cases (map (lambda (y) (all-cases data-layouts y)) products)])
+                     (if (null? product-cases)
+                         (list sum-name) ; singletons aren't enclosed in a list [(foo x) 42] vs [foo 42]
+                         (apply combinations (cons (list sum-name) product-cases)))))
+                 (cdr sums))
+       '(:binding))))
+
+                                       ; does a cover b
+(define (case-covers? data-layouts a b)
+  (let ([a-binding? (and (eqv? (ast-type a) 'var) (not (constructor? data-layouts a)))])
+    (if (eqv? ':binding b)
+       a-binding?
+       (if a-binding?
+           #t
+           (if (eqv? (ast-type b) 'var)
+               (eqv? b a)
+               (all (map (lambda (p q)
+                           (case-covers? data-layouts p q))
+                         (cdr a) (cdr b))))))))
+
+(define (verify-cases data-layouts annotated-program)
 
   ;; (define (check-pattern switch-type pat)
 
@@ -121,13 +138,16 @@
   ;;      (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 ([expr (ann-expr annotated-program)])
+    (case (ast-type expr)
+      ['case
+         (let* ([switch-type (ann-type (case-switch expr))]
+                [cases (map car (case-cases expr))]
+                [case-covered?
+                 (lambda (x) (any (lambda (y) (case-covers? data-layouts y x)) cases))])
+           (unless (all (map case-covered? (all-cases data-layouts switch-type)))
+             (error #f "not all cases covered")))]
+      [else (ast-traverse (lambda (x) (verify-cases data-layouts x)) expr)])))
 
 
                                        ; (let ([(foo a b) (foo 123 345)]) a)

diff --git a/utils.scm b/utils.scm
index e063b85d08625500f5bbeb6e124214d98a464688..ea8900f51cf989caa59fc9ed6d4168d354621545 100644 (file)
--- a/utils.scm
+++ b/utils.scm
@@ -25,3 +25,20 @@
     ((_ s) (let ([x (car s)])
             (set! s (cdr s))
             x))))
+
+(define (any p x)
+  (fold-left
+   (lambda (acc y) (if acc #t (p y)))
+   #f
+   x))
+
+(define (all xs) (fold-left (lambda (acc x) (and acc x)) #t xs))
+
+                                       ; (combinations '(1 2) '(3)) => '((1 3) (2 3))
+(define (combinations . lists)
+  (case (length lists)
+    [0 '()]
+    [1 (map (lambda (x) (list x)) (car lists))]
+    [else (flat-map (lambda (x)
+                     (map (lambda (y) (cons x y))
+                          (apply combinations (cdr lists)))) (car lists))]))