From b936564e4a05bd4a23ec202a1c4919097ace7ca8 Mon Sep 17 00:00:00 2001
From: Luke Lau <luke_lau@icloud.com>
Date: Sat, 20 Jul 2019 17:48:01 +0100
Subject: [PATCH] Resolve types in lambda arguments, recursively substitute

Also add test
---
 tests.scm     | 10 ++++++++
 typecheck.scm | 65 +++++++++++++++++++++++++++++++--------------------
 2 files changed, 50 insertions(+), 25 deletions(-)
 create mode 100644 tests.scm

diff --git a/tests.scm b/tests.scm
new file mode 100644
index 0000000..39ca240
--- /dev/null
+++ b/tests.scm
@@ -0,0 +1,10 @@
+(load "typecheck.scm")
+
+(define (test actual expected)
+  (when (not (equal? actual expected))
+    (error #f
+	   (format "test failed:\nexpected: ~a\nactual:   ~a"
+		   expected actual))))
+
+(test (typecheck '(lambda (x) (+ ((lambda (y) (x y 3)) 5) 2)))
+      '(abs (abs int (abs int int)) int))
diff --git a/typecheck.scm b/typecheck.scm
index 98d1cf4..eaff75e 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -47,11 +47,11 @@
 ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
   (define (check env x)
-    (display "check: ")
-    (display x)
-    (display "\n\t")
-    (display env)
-    (newline)
+    ;; (display "check: ")
+    ;; (display x)
+    ;; (display "\n\t")
+    ;; (display env)
+    ;; (newline)
     (let
 	((res
 	  (cond
@@ -75,15 +75,20 @@
 	   ((lambda? x)
 	    (let* ((new-env (env-insert env (lambda-arg x) (fresh-tvar)))
 		   (body-type-res (check new-env (lambda-body x)))
-		   (subd-env (substitute-env (car body-type-res) new-env)))
-	      (display "lambda: ")
-	      (display body-type-res)
-	      (display "\n")
-	      (display subd-env)
-	      (display "\n")
+		   (cs (car body-type-res))
+		   (subd-env (substitute-env (car body-type-res) new-env))
+		   (arg-type (env-lookup subd-env (lambda-arg x)))
+		   (resolved-arg-type (substitute cs arg-type)))
+	      ;; (display "lambda:\n\t")
+	      ;; (display prog)
+	      ;; (display "\n\t")
+	      ;; (display cs)
+	      ;; (display "\n\t")
+	      ;; (display resolved-arg-type)
+	      ;; (newline)
 	      (list (car body-type-res)
 		    (list 'abs
-			  (env-lookup subd-env (lambda-arg x))
+			  resolved-arg-type
 			  (cadr body-type-res)))))
 	   
 	   ((app? x) ; (f a)
@@ -97,7 +102,9 @@
 				  (list 'abs
 					arg-type
 					(fresh-tvar))))
-		   (cs (append func-c (car arg-type-res) (car func-type-res)))
+		   (cs (consolidate
+			(consolidate func-c (car arg-type-res))
+			(car func-type-res)))
 		   
 		   (resolved-func-type (substitute cs func-type))
 		   (resolved-return-type (caddr resolved-func-type)))
@@ -114,13 +121,13 @@
 		  (let ((return-type (substitute cs (caddr resolved-func-type))))
 		    (list cs return-type))
 		  (error #f "not a function")))))))
-      (display "result of ")
-      (display x)
-      (display ":\n\t")
-      (display (cadr res))
-      (display "[")
-      (display (car res))
-      (display "]\n")
+      ;; (display "result of ")
+      ;; (display x)
+      ;; (display ":\n\t")
+      ;; (display (cadr res))
+      ;; (display "[")
+      ;; (display (car res))
+      ;; (display "]\n")
       res))
   (cadr (check '() (normalize prog))))
 
@@ -146,24 +153,32 @@
 		      (unify (caddr a) (caddr b))))
 	(else (error #f "could not unify"))))
 
-
 					; TODO: what's the most appropriate substitution?
 					; should all constraints just be limited to a pair?
 (define (substitute cs t)
 					; gets the first concrete type
 					; otherwise returns the last type variable
+
   (define (get-concrete c)
-    (if (null? (cdr c))
-	(car c)
+    (let ((last (null? (cdr c))))
       (if (not (tvar? (car c)))
+	  (if (abs? (car c))
+	      (substitute cs (car c))
+	      (car c))
+	  (if last
 	      (car c)
-	    (get-concrete (cdr c)))))
+	      (get-concrete (cdr c))))))
+  (cond
+   ((abs? t) (list 'abs
+		   (substitute cs (cadr t))
+		   (substitute cs (caddr t))))
+   (else
     (fold-left
      (lambda (t c)
        (if (member t c)
 	   (get-concrete c)
 	   t))
-   t cs))
+     t cs))))
 
 (define (substitute-env cs env)
   (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
-- 
2.30.2