X-Git-Url: http://git.lukelau.me/?a=blobdiff_plain;f=typecheck.scm;h=57a7815897e2bc9dd9c466c972d35431807aba4d;hb=74729258ddf19dfeb175cf98d5a3891cd8160faf;hp=6a99869c0697302f361a9e28ac216013f5d018d6;hpb=9d93b066cfd6505849dff12146159bedeadf96b9;p=scheme.git

diff --git a/typecheck.scm b/typecheck.scm
index 6a99869..57a7815 100644
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -92,11 +92,11 @@
     (else #f)))
 
 (define (check env x)
-  (display "check: ")
-  (display x)
-  (display "\n\t")
-  (display env)
-  (newline)
+  ;; (display "check: ")
+  ;; (display x)
+  ;; (display "\n\t")
+  ;; (display env)
+  ;; (newline)
   (let
       ((res
 	(case (ast-type x)
@@ -162,9 +162,6 @@
 					 (cons (car x) (substitute cs (cdr x)))
 					 x))
 				   scc-env)])
-			  		(display "cs:")
-		(display cs)
-		(newline)
 			  new-env))]
 		     [new-env (fold-left process-component env components)])
 		(check new-env (last (let-body x)))))
@@ -198,7 +195,7 @@
 		      (other-func-type `(abs ,func-type ,return-type))
 		      (cs (~ func-type other-func-type))
 		      (resolved-return-type (substitute cs return-type))]
-		 (list cs resolved-return-type))
+		 (list cs resolved-return-type)))
 
 					; regular function
 	       (let* ((arg-type-res (check env (cadr x)))
@@ -228,14 +225,14 @@
 		 (if (abs? resolved-func-type)
 		     (let ((return-type (substitute cs (caddr resolved-func-type))))
 		       (list cs return-type))
-		     (error #f "not a function"))))))))
-    (display "result of ")
-    (display x)
-    (display ":\n\t")
-    (display (pretty-type (cadr res)))
-    (display "\n\t[")
-    (display (pretty-constraints (car res)))
-    (display "]\n")
+		     (error #f "not a function")))))))
+    ;; (display "result of ")
+    ;; (display x)
+    ;; (display ":\n\t")
+    ;; (display (pretty-type (cadr res)))
+    ;; (display "\n\t[")
+    ;; (display (pretty-constraints (car res)))
+    ;; (display "]\n")
     res))
 
 					; we typecheck the lambda calculus only (only single arg lambdas)
@@ -278,9 +275,9 @@
 					; composes constraints a onto b and merges, i.e. applies a to b
 					; a should be the "more important" constraints
 (define (constraint-merge a b)
-  (define (f constraint)
+  (define (f cs constraint)
     (cons (car constraint)
-	  (substitute a (cdr constraint))))
+	  (substitute cs (cdr constraint))))
   
   (define (most-concrete a b)
     (cond
@@ -291,26 +288,26 @@
 	    ,(most-concrete (caddr a) (caddr b)))]
      [(abs? a) b]
      [(abs? b) a]
-     [else (error #f "impossible! most-concrete")]))
-
-  (define (union p q)
-    (cond
-     [(null? p) q]
-     [(null? q) p]
-     [else
-      (let ([x (car q)])
-	(if (assoc (car x) p)
-	    (if (eqv? (most-concrete (cddr (assoc (car x) p))
-				     (cdr x))
-		      (cdr x))
-		(cons x (union (filter (p) (not (eqv? 
-	
+     [else a]))
+
+					; for any two constraints that clash, e.g. t1 ~ abs t2 t3
+					; and t1 ~ abs int t3
+					; prepend the most concrete version of the type to the
+					; list of constraints
+  (define (clashes)
+    (define (gen acc x)
+      (if (assoc (car x) a)
+	  (cons (cons (car x) (most-concrete (cdr (assoc (car x) a))
+					     (cdr x)))
+		acc)
+	  acc))
+    (fold-left gen '() b))
 
   (define (union p q)
     (append (filter (lambda (x) (not (assoc (car x) p)))
 		    q)
 	    p))
-  (union a (map f b)))
+  (append (clashes) (union a (map (lambda (z) (f a z)) b))))
 
 
 ;; 					; a1 -> a2 ~ a3 -> a4;