Add notes on ownership

[scheme.git] / typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
index 313db0e2a9d48fbdbc7fcaff2f89eab749f905b7..e96f6943767e1c5ab463398d11146d8f8ae450ce 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,8 +180,9 @@
                 (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))]
-                  (list cs return-type))
+                       (cs (~ func-type other-func-type))
+                       (resolved-return-type (substitute cs return-type))]
+                  (list cs resolved-return-type))
 
                                        ; regular function
                 (let* ((arg-type-res (check env (cadr x)))
@@ -190,7 +191,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 +226,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,21 +234,27 @@
               (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?
+                                       ; this is currently horrific and i don't know what im doing.
+                                       ; should probably use ast-find here or during consolidation
+                                       ; to detect substitutions more than one layer deep
+                                       ; e.g. (abs t1 int) ~ (abs bool int)
+                                       ; substituting these constraints with t1 should resolve t1 with bool
 (define (substitute cs t)
                                        ; gets the first concrete type
                                        ; otherwise returns the last type variable
 
+                                       ; removes t itself from cs, to prevent infinite recursion
   (define cs-without-t
     (map (lambda (c)
           (filter (lambda (x) (not (eqv? t x))) c))
@@ -277,9 +285,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)
@@ -326,18 +331,21 @@
              (lambda (acc c)
                (if (tvar? c) acc #f))]
             [test (lambda (acc c)
-                    (and acc (fold-left test-kind #t c)))])
+                    (and acc
+                         (fold-left test-kind #t c) ; check only tvar substitutions
+                         (<= (length c) 2)))])      ; check maximum 2 subs per equality group
          (fold-left test #t cs)))))
 
                                        ; input: a list of binds ((x . y) (y . 3))
                                        ; returns: pair of verts, edges ((x y) . (x . y))
 (define (graph bs)
+  (define (go bs orig-bs)
     (define (find-refs prog)
       (ast-collect
        (lambda (x)
         (case (ast-type x)
                                        ; only count a reference if its a binding
-        ['var (if (assoc x bs) (list x) '())]
+          ['var (if (assoc x orig-bs) (list x) '())]
           [else '()]))
        prog))
     (if (null? bs)
@@ -351,10 +359,11 @@
 
               (rest (if (null? (cdr bs))
                         (cons '() '())
-                      (graph (cdr bs))))
+                        (go (cdr bs) orig-bs)))
               (total-verts (cons vert (car rest)))
               (total-edges (append edges (cdr rest)))]
          (cons total-verts total-edges))))
+  (go bs bs))
 
 (define (successors graph v)
   (define (go v E)