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

diff --git a/typecheck.scm b/typecheck.scm
index cfb30cc..e398606 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -131,7 +131,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)))
@@ -146,9 +146,47 @@
 	 [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 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 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)]
+
+	 [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"))))
 
 ; returns a list (constraints type annotated)
 (define (check env x)
@@ -199,51 +237,14 @@
 
 		     [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)]
-
-		  [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")))))))
+	  ('app (check-app env x)))))
     ;; (display "result of ")
     ;; (display x)
     ;; (display ":\n\t")
@@ -254,14 +255,63 @@
     res))
 
 (define (init-adts-env prog)
-  (flat-map data-tors-env (map data-layout (program-datas prog))))
+  (flat-map data-tors-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)))))
 
+
+					; 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 (lambda (o n) (denormalize o n))
+		   (let-body orig)
+		   (let-body (ann-expr normed)))) : ,(ann-type normed))]
+    ['if `((if ,@(map denormalize (cdr orig) (cdr (ann-expr normed))))
+	   : (ann-type normed))]
+    [else normed]))
+
+(define ann-expr car)
+(define ann-type caddr)
 (define (annotate-types prog)
-  (caddr (check (init-adts-env prog) (normalize (program-body prog)))))
+  (denormalize (program-body prog)
+  (caddr (check (init-adts-env prog) (normalize (program-body prog))))))
 
   
 					; returns a list of constraints