From ba17902b367783f058108f2eb9dff163d34b735f Mon Sep 17 00:00:00 2001
From: Luke Lau <luke_lau@icloud.com>
Date: Wed, 17 Jul 2019 21:53:26 +0100
Subject: [PATCH] Add consolidation, tie up with typechecker

Also normalize program before typechecking
---
 compiler.scm  |  59 +++++++++++++++++
 rts.c         |  11 ++++
 typecheck.scm | 179 ++++++++++++++++++++++++++++++++------------------
 3 files changed, 185 insertions(+), 64 deletions(-)
 create mode 100644 compiler.scm
 create mode 100644 rts.c

diff --git a/compiler.scm b/compiler.scm
new file mode 100644
index 0000000..351e11b
--- /dev/null
+++ b/compiler.scm
@@ -0,0 +1,59 @@
+(load "typecheck.scm")
+
+(define (emit . s)
+  (begin
+    (apply printf s)
+    (display "\n")))
+
+(define (compile-add xs)
+  (define (go ys)
+    (if (null? ys)
+      (emit "movq %rbx, %rax")
+      (begin
+	(emit "addq $~a, %rbx" (car ys))
+	(go (cdr ys)))))
+  (begin
+    (emit "movq $0, %rbx")
+    (go xs)))
+
+(define (compile-expr e)
+  (if (and (list? e) (eq? (car e) '+))
+      (compile-add (cdr e))
+      (emit "movq $~a, %rax" e)))
+
+(define (compile-program program)
+  (emit ".text")
+  (emit ".p2align 4,,15")
+  (emit ".globl _scheme_entry")
+  (emit "_scheme_entry:")
+
+  ; handle incoming call from C
+  (emit "push %rbp")
+  (emit "push %rbx")
+  (for-each (lambda (i)
+	      (emit (string-append
+		     "push %r"
+		     (number->string i))))
+	    '(12 13 14 15))
+
+  ; our code goes here
+  (compile-expr program)
+
+  ; restore preserved registers
+  (for-each (lambda (i)
+	      (emit (string-append
+		     "pop %r"
+		     (number->string i))))
+	    '(15 14 13 12))
+  (emit "pop %rbx")
+  (emit "pop %rbp")
+
+  (emit "ret"))
+
+(define (compile-to-binary program)
+  (when (not (eq? (typecheck program) 'int)) (error #f "not an int"))
+  (let ([tmp-path "/tmp/a.s"])
+    (when (file-exists? tmp-path) (delete-file tmp-path))
+    (with-output-to-file tmp-path
+      (lambda () (compile-program program)))
+    (system "clang -fomit-frame-pointer /tmp/a.s rts.c")))
diff --git a/rts.c b/rts.c
new file mode 100644
index 0000000..0678901
--- /dev/null
+++ b/rts.c
@@ -0,0 +1,11 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+__attribute__((__cdecl__))
+extern int scheme_entry();
+
+int main(int argc, const char**argv) {
+  int val = scheme_entry();
+  printf("%d\n", val);
+  return 0;
+}
diff --git a/typecheck.scm b/typecheck.scm
index a396a24..0e4e265 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,11 +1,10 @@
-(define (is-app? x)
-  (and (list? x) (not (eq? (car x) 'lambda))))
+(define (app? x)
+  (and (list? x) (>= (length x) 2) (not (eq? (car x) 'lambda))))
 
-
-(define (is-lambda? x)
+(define (lambda? x)
   (and (list? x) (eq? (car x) 'lambda)))
 
-(define lambda-arg cadr)
+(define lambda-arg caadr)
 (define lambda-body caddr)
 
 ; ('a, ('b, 'a))
@@ -24,66 +23,79 @@
     (string->symbol
      (string-append "t" (number->string (- cur-tvar 1))))))
 
-(define (typecheck env x)
-  (display "typechecking:\n\t")
-  (display x)
-  (display "\t")
-  (display env)
-  (display "\n")
+					
+(define (normalize prog) ; (+ a b) -> ((+ a) b)
+  (cond
+   ((lambda? prog) '(lambda (lambda-arg prog) (normalize (lambda-body 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)
+   (else prog)))
+  
+
+(define (typecheck prog)
+  (define (check env x)
     (let
 	((res
 	  (cond
 	   ((integer? x) (list '() 'int))
 	   ((boolean? x) (list '() 'bool))
 	   ((eq? x 'inc) (list '() '(abs int int)))
+	   ((eq? x '+)   (list '() '(abs int (abs int int))))
 	   ((symbol? x) (list '() (env-lookup env x)))
 
-	 ((is-lambda? x)
+	   ((lambda? x)
 	    (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
-		 (body-type-res (typecheck new-env (lambda-body x)))
-		 (subd-env (substitute (car body-type-res) new-env)))
-	    (display "lambda: ")
-	    (display body-type-res)
-	    (display "\n")
+		   (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")
 	      (list (car body-type-res)
 		    (list 'abs
 			  (env-lookup subd-env (lambda-arg x))
 			  (cadr body-type-res)))))
 	   
-	 ((is-app? x) ; (f a)
-	  (let* ((arg-type-res (typecheck env (cadr x)))
-					; typecheck f with the knowledge that f : a -> x
-		 (func-type-res (typecheck env (car x)))
+	   ((app? x) ; (f a)
+	    (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))
-		 (c (unify func-type
+		   
+					; f ~ a -> t0
+		   (func-c (unify func-type
 				  (list 'abs
-				 (cadr arg-type-res)
+					arg-type
 					(fresh-tvar))))
-		 (new-env (substitute c env))
-		 (resolved-func-type (env-lookup new-env (car x))))
-	    (display "is-app:\n")
-	    (display c)
-	    (display "\n")
-	    (display new-env)
-	    (display "\n")
-	    (display resolved-func-type)
-	    (display "\n")
-	    (display arg-type-res)
-	    (display "\n")
+		   (cs (append func-c (car arg-type-res) (car func-type-res)))
+		   
+		   (resolved-func-type (substitute cs func-type))
+		   (resolved-return-type (caddr resolved-func-type)))
+	      ;; (display "app:\n")
+	      ;; (display cs)
+	      ;; (display "\n")
+	      ;; (display func-type)
+	      ;; (display "\n")
+	      ;; (display resolved-func-type)
+	      ;; (display "\n")
+	      ;; (display arg-type-res)
+	      ;; (display "\n")
 	      (if (abs? resolved-func-type)
-		(list (append c
-			      (unify (cadr arg-type-res)
-				     (cadr resolved-func-type)))
-		      (caddr resolved-func-type))
+		  (let ((return-type (substitute cs (caddr resolved-func-type))))
+		    (list cs return-type))
 		  (error #f "wah")))))))
-    (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))))
 
 
 (define (abs? t)
@@ -101,26 +113,65 @@
 					; returns a list of pairs of constraints
 (define (unify a b)
   (cond ((eq? a b) '())
-	((or (tvar? a) (tvar? b)) (list (cons a b)))
+	((or (tvar? a) (tvar? b)) (~ a b))
 	((and (abs? a) (abs? b))
-	 (append (unify (cadr a) (cadr b))
+	 (consolidate (unify (cadr a) (cadr b))
 		      (unify (caddr a) (caddr b))))
 	(else (error #f "could not unify"))))
 
-					; takes a list of constraints and a type environment, and makes it work
-(define (substitute c env)
-  (let ((go (lambda (x) (let ((tv (cdr x))
-			      (n (car x)))
-			  ;; (display tv)
-			  ;; (display "\n")
-			  ;; (display n)
-			  (cons n (fold-left
-				   (lambda (a y)
-				     ;; (display y)
-				     ;; (display ":")
-				     ;; (display a)
-				     (cond ((eq? a (car y)) (cdr y))
-					   ((eq? a (cdr y)) (car y))
-					   (else a)))
-				   tv c))))))
-  (map go env)))
+
+					; TODO: what's the most appropriate substitution?
+					; should all constraints just be limited to a pair?
+(define (substitute cs t)
+  (define (blah c)
+    (if (null? (cdr c))
+	(car c)
+	(if (not (tvar? (car c)))
+	    (car c)
+	    (blah (cdr c)))))
+  (fold-left
+   (lambda (t c)
+     (if (member t c)
+	 (blah c)
+	 t))
+   t cs))
+
+(define (substitute-env cs env)
+  (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
+
+(define (~ a b)
+  (list (list a b)))
+
+(define (consolidate x y)
+  (define (merge a b)
+    (cond ((null? a) b)
+	  ((null? b) a)
+	  (else (if (member (car b) a)
+		    (merge a (cdr b))
+		    (cons (car b) (merge a (cdr b)))))))
+  (define (overlap? a b)
+    (if (or (null? a) (null? b))
+	#f
+	(if (fold-left (lambda (acc v)
+			 (or acc (eq? v (car a))))
+		       #f b)
+	    #t
+	    (overlap? (cdr a) b))))
+
+  (cond ((null? y) x)
+	((null? x) y)
+	(else (let* ((a (car y))
+		     (merged (fold-left
+			      (lambda (acc b)
+				(if acc
+				    acc
+				    (if (overlap? a b)
+					(cons (merge a b) b)
+					#f)))
+			      #f x))
+		     (removed (if merged
+				  (filter (lambda (b) (not (eq? b (cdr merged)))) x)
+				  x)))
+		(if merged
+		    (consolidate removed (cons (car merged) (cdr y)))
+		    (consolidate (cons a x) (cdr y)))))))
-- 
2.30.2