X-Git-Url: https://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=b2b001f1d27220211e5f67e651d641c9895f5b5c;hp=35e818866df9603a3ecaa4cc721b548035d26abc;hb=HEAD;hpb=86531822ef58c5b29751976f5b41d1c631bdd459

diff --git a/typecheck.scm b/typecheck.scm
index 35e8188..b2b001f 100644
--- 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)))
@@ -90,7 +91,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 +109,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 +143,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 +165,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 +189,65 @@
 	  (list cs return-type annotated))
 	(error #f "not a function"))))
 
+(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)
+	['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)]
+		   [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)]
+					; a pattern match without bindings
+	[else (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 ,(caddr switch-type-res)
+			,@(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: ")
@@ -201,14 +259,13 @@
       ((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)))
 
 	  ('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 +280,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,7 +301,10 @@
 		      annotated)))
 
 	  
-	  ('app (check-app env x)))))
+	  ('app (check-app dls env x))
+	  ['case (check-case dls env x)])))
+	      
+		
     ;; (display "result of ")
     ;; (display x)
     ;; (display ":\n\t")
@@ -258,8 +318,12 @@
   (flat-map data-tors-type-env (program-data-layouts prog)))
 
 					; we typecheck the lambda calculus only (only single arg lambdas)
-(define (typecheck prog)
-  (cadr (check (init-adts-env prog) (normalize (program-body 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))))))
 
 
 					; before passing annotated types onto codegen
@@ -300,18 +364,27 @@
 	`((let ,(map (lambda (o n) (list (car o) (denormalize (cadr o) (cadr n))))
 		     (let-bindings orig)
 		     (let-bindings (ann-expr normed)))
-	    ,@(map (lambda (o n) (denormalize o n))
+	    ,@(map denormalize
 		   (let-body orig)
 		   (let-body (ann-expr normed)))) : ,(ann-type normed))]
     ['if `((if ,@(map denormalize (cdr orig) (cdr (ann-expr normed))))
-	   : (ann-type normed))]
+	   : ,(ann-type normed))]
+    ['case `((case ,(denormalize (case-switch orig) (case-switch (ann-expr normed)))
+	       ,@(map (lambda (o n) (cons (car o) (denormalize (cadr o) (cadr n))))
+		      (case-cases orig) (case-cases (ann-expr normed))))
+	     : ,(ann-type normed))]
     [else normed]))
 
 (define ann-expr car)
 (define ann-type caddr)
+
+					; prerequisites: expand-pattern-matches
 (define (annotate-types prog)
-  (denormalize (program-body prog)
-  (caddr (check (init-adts-env prog) (normalize (program-body prog))))))
+  (denormalize
+   (program-body prog)
+   (caddr (check (program-data-layouts prog)
+		 (init-adts-env prog)
+		 (normalize (program-body prog))))))
 
   
 					; returns a list of constraints