Tidy up

diff --git a/typecheck.scm b/typecheck.scm
index df85cc1607209a6f61968092c4636b7027023142..57a7815897e2bc9dd9c466c972d35431807aba4d 100644 (file)
--- 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)
@@ -291,8 +288,12 @@
            ,(most-concrete (caddr a) (caddr b)))]
      [(abs? a) b]
      [(abs? b) a]
-     [else (error #f "impossible! most-concrete")]))
+     [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)
@@ -302,26 +303,10 @@
          acc))
     (fold-left gen '() b))
 
-  ;; (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? 
-       
-  
   (define (union p q)
     (append (filter (lambda (x) (not (assoc (car x) p)))
                    q)
            p))
-  (display "clashes: ")
-  (display (clashes))
-  (newline)
   (append (clashes) (union a (map (lambda (z) (f a z)) b))))