Add recursive let-bindings

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index eaff75efbe6fdf313e0522216c5e07d2486c75ac..55c2fd8201f2467ff3e136189412b6dc351780fd 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,4 +1,27 @@
 (load "ast.scm")
 (load "ast.scm")

+
+(define (abs? t)
+  (and (list? t) (eq? (car t) 'abs)))
+
+(define (tvar? t)
+  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
+
+(define (concrete? t)
+  (case t
+    ('int #t)
+    ('bool #t)
+    (else #f)))
+
+(define (pretty-type t)
+  (cond ((abs? t)
+        (string-append
+         (if (abs? (cadr t))
+             (string-append "(" (pretty-type (cadr t)) ")")
+             (pretty-type (cadr t)))
+         " -> "
+         (pretty-type (caddr t))))
+       (else (symbol->string t))))
+

                                        ; ('a, ('b, 'a))
 (define (env-lookup env n)
   (if (null? env) (error #f "empty env")                       ; it's a type equality
                                        ; ('a, ('b, 'a))
 (define (env-lookup env n)
   (if (null? env) (error #f "empty env")                       ; it's a type equality


@@ -34,15 +57,26 @@
        (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
    ((app? prog)
     (if (null? (cddr prog))
        (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
    ((app? prog)
     (if (null? (cddr prog))

-       (cons (normalize (car prog)) (normalize (cdr prog))) ; (f a)
-       (list (list (normalize (car prog)) (normalize (cadr prog))) (normalize (caddr prog))))) ; (f a b)
+       `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
+       `(,(list (normalize (car prog)) (normalize (cadr prog)))
+         ,(normalize (caddr prog))))) ; (f a b)
+       ;; (list (list (normalize (car prog))
+       ;;          (normalize (cadr prog))) (normalize (caddr prog))))) ; (f a b)

    ((let? prog)
     (append (list 'let
    ((let? prog)
     (append (list 'let

-                 (map (lambda (x) (cons (car x) (normalize (cdr x))))
+                 (map (lambda (x) `(,(car x) ,(normalize (cadr x))))

                       (let-bindings prog)))
            (map normalize (let-body prog))))
    (else prog)))
 
                       (let-bindings prog)))
            (map normalize (let-body prog))))
    (else prog)))
 

+(define (builtin-type x)
+  (case x
+    ('+ '(abs int (abs int int)))
+    ('- '(abs int (abs int int)))
+    ('* '(abs int (abs int int)))
+    ('! '(abs bool bool))
+    ('bool->int '(abs bool int))
+    (else #f)))

 
 ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)
 
 ; we typecheck the lambda calculus only (only single arg lambdas)
 (define (typecheck prog)


@@ -57,10 +91,8 @@
          (cond
           ((integer? x) (list '() 'int))
           ((boolean? x) (list '() 'bool))
          (cond
           ((integer? x) (list '() 'int))
           ((boolean? x) (list '() 'bool))

-          ((eq? x 'inc) (list '() '(abs int int)))
-          ((eq? x '+)   (list '() '(abs int (abs int int))))
+          ((builtin-type x) (list '() (builtin-type x)))

           ((symbol? x)  (list '() (env-lookup env x)))
           ((symbol? x)  (list '() (env-lookup env x)))

-

           ((let? x)
            (let ((new-env (fold-left
                            (lambda (acc bind)
           ((let? x)
            (let ((new-env (fold-left
                            (lambda (acc bind)


@@ -131,19 +163,6 @@
       res))
   (cadr (check '() (normalize prog))))
 
       res))
   (cadr (check '() (normalize prog))))
 

-
-(define (abs? t)
-  (and (list? t) (eq? (car t) 'abs)))
-
-(define (tvar? t)
-  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
-
-(define (concrete? t)
-  (case t
-    ('int #t)
-    ('bool #t)
-    (else #f)))
-

                                        ; returns a list of pairs of constraints
 (define (unify a b)
   (cond ((eq? a b) '())
                                        ; returns a list of pairs of constraints
 (define (unify a b)
   (cond ((eq? a b) '())