Add pretty printing for types

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index eaff75efbe6fdf313e0522216c5e07d2486c75ac..21b874c2fdc043b41297575d84bdd12132d559a5 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -1,4 +1,27 @@
 (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
@@ -43,6 +66,14 @@
            (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)
@@ -57,10 +88,8 @@
          (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)))
-
           ((let? x)
            (let ((new-env (fold-left
                            (lambda (acc bind)
@@ -131,19 +160,6 @@
       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) '())