X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=55c2fd8201f2467ff3e136189412b6dc351780fd;hp=eaff75efbe6fdf313e0522216c5e07d2486c75ac;hb=8aacba5976424791fb51d5d36118269d32c4096a;hpb=b936564e4a05bd4a23ec202a1c4919097ace7ca8

diff --git a/typecheck.scm b/typecheck.scm
index eaff75e..55c2fd8 100644
--- 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
@@ -34,15 +57,26 @@
 	(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
-		  (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)))
 
+(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 +91,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 +163,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) '())