From 64e7552f99ab98b7db77797cecfc3f34331296df Mon Sep 17 00:00:00 2001
From: Luke Lau <luke_lau@icloud.com>
Date: Sat, 20 Jul 2019 17:02:28 +0100
Subject: [PATCH] Normalize lambdas to be single arguments only

---
 ast.scm       |  7 +++++--
 typecheck.scm | 44 ++++++++++++++++++++++++++------------------
 2 files changed, 31 insertions(+), 20 deletions(-)

diff --git a/ast.scm b/ast.scm
index 19dc7a0..05716e4 100644
--- a/ast.scm
+++ b/ast.scm
@@ -13,8 +13,11 @@
 (define (lambda? x)
   (and (list? x) (eq? (car x) 'lambda)))
 
-(define lambda-arg cadr)
-(define lambda-body cddr)
+; for use in normalized form
+(define lambda-arg caadr)
+; for use elsewhere
+(define lambda-args cadr)
+(define lambda-body caddr)
 
 (define (var? x)
   (and (not (list? x)) (symbol? x)))
diff --git a/typecheck.scm b/typecheck.scm
index a738429..98d1cf4 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -26,11 +26,16 @@
 					
 (define (normalize prog) ; (+ a b) -> ((+ a) b)
   (cond
-   ((lambda? prog) (list 'lambda (lambda-arg prog) (normalize (lambda-body prog))))
+   ; (lambda (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
+   ((lambda? prog)
+    (if (> (length (lambda-args prog)) 1)
+	(list 'lambda (list (car (lambda-args prog)))
+	      (normalize (list 'lambda (cdr (lambda-args prog)) (caddr prog))))
+	(list 'lambda (lambda-args prog) (normalize (caddr prog)))))
    ((app? prog)
     (if (null? (cddr prog))
 	(cons (normalize (car prog)) (normalize (cdr prog))) ; (f a)
-	(normalize (cons (cons (car prog) (list (cadr prog))) (cddr prog))))) ; (f a b)
+	(list (list (normalize (car prog)) (normalize (cadr prog))) (normalize (caddr prog))))) ; (f a b)
    ((let? prog)
     (append (list 'let
 		  (map (lambda (x) (cons (car x) (normalize (cdr x))))
@@ -39,11 +44,14 @@
    (else prog)))
 
 
+; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
   (define (check env x)
-    ;; (display "check: ")
-    ;; (display x)
-    ;; (display "\n")
+    (display "check: ")
+    (display x)
+    (display "\n\t")
+    (display env)
+    (newline)
     (let
 	((res
 	  (cond
@@ -65,14 +73,14 @@
 		  
 
 	   ((lambda? x)
-	    (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
+	    (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")
+	      (display "lambda: ")
+	      (display body-type-res)
+	      (display "\n")
+	      (display subd-env)
+	      (display "\n")
 	      (list (car body-type-res)
 		    (list 'abs
 			  (env-lookup subd-env (lambda-arg x))
@@ -106,13 +114,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))))
 
-- 
2.30.2