Tidy up
[scheme.git] / typecheck.scm
index 6a99869c0697302f361a9e28ac216013f5d018d6..57a7815897e2bc9dd9c466c972d35431807aba4d 100644 (file)
     (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)
                                         (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)))))
                      (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)))
                 (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)
                                        ; 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
            ,(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;