From: Luke Lau <luke_lau@icloud.com>
Date: Thu, 15 Aug 2019 11:14:35 +0000 (+0100)
Subject: Add bindings to pattern matching in case statement typechecking
X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=commitdiff_plain;h=d6b60d54bc90e5ebdc643d05d0b806ae7fd8aa7c

Add bindings to pattern matching in case statement typechecking
---

diff --git a/ast.scm b/ast.scm
index 86d5225..109ce91 100644
--- 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 1b2f214..ebfd816 100644
--- 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