Add consolidation, tie up with typechecker

Also normalize program before typechecking

diff --git a/compiler.scm b/compiler.scm
new file mode 100644 (file)
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 (file)
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 a396a246ee67cf1c65d975d1021a0f91693f36b5..0e4e265f2d2a47f81b8a13ea4ade24914c3b33a1 100644 (file)
--- 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)))))))