Refactor unify

diff --git a/typecheck.scm b/typecheck.scm
index 313db0e2a9d48fbdbc7fcaff2f89eab749f905b7..a767ed07fb1c2244819c0bcbbb2539ff9ecc12bf 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -98,7 +98,7 @@
             (let* ((cond-type-res (check env (cadr x)))
                    (then-type-res (check env (caddr x)))
                    (else-type-res (check env (cadddr x)))
-                   (then-eq-else-cs (unify (cadr then-type-res)
+                   (then-eq-else-cs (~ (cadr then-type-res)
                                        (cadr else-type-res)))
                    (cs (consolidate
                         (car then-type-res)
@@ -141,7 +141,7 @@
                                  (consolidate (car res)
                                        ; unify with tvars from scc-env
                                        ; result ~ tvar
-                                              (unify (cadr res) (env-lookup scc-env c)))))
+                                              (~ (cadr res) (env-lookup scc-env c)))))
                               '() type-results comps)]
                                        ; substitute *only* the bindings in this scc
                             [new-env
@@ -180,7 +180,7 @@
                 (let* [(func-type (env-lookup env (car x)))
                        (return-type (fresh-tvar))
                        (other-func-type `(abs ,func-type ,return-type))
-                       (cs (unify func-type other-func-type))]
+                       (cs (~ func-type other-func-type))]
                   (list cs return-type))
 
                                        ; regular function
@@ -190,7 +190,8 @@
                        (func-type (cadr func-type-res))
                        
                                        ; f ~ a -> t0
-                       (func-c (unify func-type
+                       (func-c (~
+                                func-type
                                 (list 'abs
                                       arg-type
                                       (fresh-tvar))))
@@ -224,7 +225,7 @@
   (cadr (check '() (normalize prog))))
 
                                        ; returns a list of pairs of constraints
-(define (unify a b)
+(define (~ a b)
   (let ([res (unify? a b)])
     (if res
        res
@@ -232,14 +233,14 @@
               (format "couldn't unify ~a ~~ ~a" a b)))))
 
 (define (unify? a b)
-  (cond ((eq? a b) '())
-       ((or (tvar? a) (tvar? b)) (~ a b))
-       ((and (abs? a) (abs? b))
-        (let* [(arg-cs (unify (cadr a) (cadr b)))
-               (body-cs (unify (substitute arg-cs (caddr a))
+  (cond [(eq? a b) '()]
+       [(or (tvar? a) (tvar? b)) (list (list a b))]
+       [(and (abs? a) (abs? b))
+        (let* [(arg-cs (unify? (cadr a) (cadr b)))
+               (body-cs (unify? (substitute arg-cs (caddr a))
                                (substitute arg-cs (caddr b))))]
-          (consolidate arg-cs body-cs)))
-       (else #f)))
+          (consolidate arg-cs body-cs))]
+       [else #f]))
 
                                        ; TODO: what's the most appropriate substitution?
                                        ; should all constraints just be limited to a pair?
@@ -277,9 +278,6 @@
 (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)