X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=e96f6943767e1c5ab463398d11146d8f8ae450ce;hp=313db0e2a9d48fbdbc7fcaff2f89eab749f905b7;hb=f605bff88ce12e5f4384ab308c036350bfa86cb5;hpb=b35e568b559038a7b848f81c70ec50753dc3f736 diff --git a/typecheck.scm b/typecheck.scm index 313db0e..e96f694 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,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)