From: Luke Lau <luke_lau@icloud.com>
Date: Mon, 29 Jul 2019 12:27:38 +0000 (+0100)
Subject: Refactor unify
X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=commitdiff_plain;h=d486b87b4fb6311cd627887fe3da67a8f8d4cbb4

Refactor unify
---

diff --git a/typecheck.scm b/typecheck.scm
index 313db0e..a767ed0 100644
--- 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)