X-Git-Url: https://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=b2b001f1d27220211e5f67e651d641c9895f5b5c;hp=cfb30cc4dc40b690c126d08a5a10fa10688faa62;hb=HEAD;hpb=89ef32141732e6d0bbfc7484b465844b62d8d139

diff --git a/typecheck.scm b/typecheck.scm
index cfb30cc..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
@@ -131,7 +132,7 @@
 	       scc-env)]
 
 	 [annotated-bindings (append (cdr acc) ; the previous annotated bindings
-				     (map cons
+				     (map list
 					  comps
 					  (map caddr type-results)))])
       (cons new-env annotated-bindings)))
@@ -142,16 +143,111 @@
 	 [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)))])
+	 [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
     (list cs let-type annotated)))
 
+(define (check-app dls env x)
+  (if (eqv? (car x) (cadr x))
+					; recursive function (f f)
+					; TODO: what about ((f a) f)????
+      (let* ([func-type (env-lookup env (car x))]
+	     [return-type (fresh-tvar)]
+	     [other-func-type `(abs ,func-type ,return-type)]
+	     [cs (~ func-type other-func-type)]
+	     [resolved-return-type (substitute cs return-type)]
+
+	     [annotated `(((,(car x) : ,func-type)
+			   (,(cadr x) : ,func-type)) : ,resolved-return-type)])
+	(list cs resolved-return-type annotated)))
+
+					; regular function
+  (let* ([arg-type-res (check dls env (cadr x))]
+	 [arg-type (cadr arg-type-res)]
+	 [func-type-res (check dls env (car x))]
+	 [func-type (cadr func-type-res)]
+	 
+					; f ~ a -> t0
+	 [func-c (~
+		  (substitute (car arg-type-res) func-type)
+		  `(abs ,arg-type ,(fresh-tvar)))]
+	 [cs (constraint-merge
+	      (constraint-merge func-c (car arg-type-res))
+	      (car func-type-res))]
+	 
+	 [resolved-func-type (substitute cs func-type)]
+	 [resolved-return-type (caddr resolved-func-type)]
+
+	 [annotated `((,(caddr func-type-res)
+		       ,(caddr arg-type-res)) : ,resolved-return-type)])
+
+    (if (abs? resolved-func-type)
+	(let ((return-type (substitute cs (caddr resolved-func-type))))
+	  (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: ")
@@ -163,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
@@ -185,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))]
@@ -199,51 +294,17 @@
 
 		     [lambda-type `(abs ,resolved-arg-type ,(cadr body-type-res))]
 
-		     ; TODO: do we need to annotate the lambda argument?
-		     [annotated `(lambda (,(lambda-arg x)) ,(caddr body-type-res))])
+		     [annotated `((lambda (,(lambda-arg x)) ,(caddr body-type-res)) : ,lambda-type)])
 		
 		(list (car body-type-res) ; constraints
 		      lambda-type  ; type
 		      annotated)))
 
 	  
-	  ('app ; (f a)
-	   (if (eqv? (car x) (cadr x))
-					; recursive function (f f)
-	       (let* ([func-type (env-lookup env (car x))]
-		      [return-type (fresh-tvar)]
-		      [other-func-type `(abs ,func-type ,return-type)]
-		      [cs (~ func-type other-func-type)]
-		      [resolved-return-type (substitute cs return-type)]
-
-		      [annotated `(((,(car x) : ,func-type)
-				    (,(cadr x) : ,func-type)) : ,resolved-return-type)])
-		 (list cs resolved-return-type annotated)))
-
-					; regular function
-	   (let* ([arg-type-res (check env (cadr x))]
-		  [arg-type (cadr arg-type-res)]
-		  [func-type-res (check env (car x))]
-		  [func-type (cadr func-type-res)]
-		  
-					; f ~ a -> t0
-		  [func-c (~
-			   (substitute (car arg-type-res) func-type)
-			   `(abs ,arg-type ,(fresh-tvar)))]
-		  [cs (constraint-merge
-		       (constraint-merge func-c (car arg-type-res))
-		       (car func-type-res))]
-		  
-		  [resolved-func-type (substitute cs func-type)]
-		  [resolved-return-type (caddr resolved-func-type)]
+	  ('app (check-app dls env x))
+	  ['case (check-case dls env x)])))
 	      
-		  [annotated `((,(caddr func-type-res)
-				,(caddr arg-type-res)) : ,resolved-return-type)])
 		
-	     (if (abs? resolved-func-type)
-		 (let ((return-type (substitute cs (caddr resolved-func-type))))
-		   (list cs return-type annotated))
-		 (error #f "not a function")))))))
     ;; (display "result of ")
     ;; (display x)
     ;; (display ":\n\t")
@@ -254,14 +315,76 @@
     res))
 
 (define (init-adts-env prog)
-  (flat-map data-tors-env (map data-layout (program-datas prog))))
+  (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
+					; we need to restore the pre-normalization structure
+					; (this is important for function arity etc)
+(define (denormalize orig normed)
+
+  (define (collapse-lambdas n x)
+    (case n
+      [0 x]
+      [else
+       (let* ([inner-lambda (lambda-body (ann-expr x))]
+	      [arg (lambda-arg (ann-expr x))]
+	      [inner-collapsed (ann-expr (collapse-lambdas (- n 1) inner-lambda))])
+	 `((lambda ,(cons arg (lambda-args inner-collapsed))
+	     ,(lambda-body inner-collapsed)) : ,(ann-type x)))]))
+
+  (define (collapse-apps n x)
+    (case n
+      [-1 (error #f "nullary functions not handled yet")]
+      [0 x]
+      [else
+       (let* ([inner-app (car (ann-expr x))]
+	      [inner-collapsed (collapse-apps (- n 1) inner-app)])
+	 `(,(append (ann-expr inner-collapsed) (cdr (ann-expr x))) : ,(ann-type x)))]))
+
+  (case (ast-type orig)
+    ['lambda
+	(let ([collapsed (collapse-lambdas (- (length (lambda-args orig)) 1) normed)])
+	  `((lambda ,(lambda-args (ann-expr collapsed))
+	      ,(denormalize (lambda-body orig)
+			    (lambda-body (ann-expr collapsed)))) : ,(ann-type collapsed)))]
+    ['app
+     (let ([collapsed (collapse-apps (- (length orig) 2) normed)])
+       `(,(map (lambda (o n) (denormalize o n)) orig (ann-expr collapsed))
+	 : ,(ann-type collapsed)))]
+    ['let
+	`((let ,(map (lambda (o n) (list (car o) (denormalize (cadr o) (cadr n))))
+		     (let-bindings orig)
+		     (let-bindings (ann-expr normed)))
+	    ,@(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))]
+    ['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)
-  (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