From fff1029008b7399f597e0227fff2bf05b8a27b3c Mon Sep 17 00:00:00 2001
From: Luke Lau <luke_lau@icloud.com>
Date: Fri, 16 Aug 2019 16:06:44 +0100
Subject: [PATCH] Check for complete pattern matches

---
 ast.scm   | 74 +++++++++++++++++++++++++++++++++++--------------------
 utils.scm | 17 +++++++++++++
 2 files changed, 64 insertions(+), 27 deletions(-)

diff --git a/ast.scm b/ast.scm
index d2328cc..eabad58 100644
--- 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 e063b85..ea8900f 100644
--- 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))]))
-- 
2.30.2