From b35e568b559038a7b848f81c70ec50753dc3f736 Mon Sep 17 00:00:00 2001 From: Luke Lau Date: Mon, 29 Jul 2019 00:40:30 +0100 Subject: [PATCH] Substitute only the variables in the scc This preserves the most generic possible type Also add a test for type equality (unifies, but only type variable substitutions) Fix graph when there's no bindings --- tests.scm | 6 ++-- typecheck.scm | 96 +++++++++++++++++++++++++++------------------------ 2 files changed, 54 insertions(+), 48 deletions(-) diff --git a/tests.scm b/tests.scm index 6b66bec..65b99d9 100644 --- a/tests.scm +++ b/tests.scm @@ -8,7 +8,7 @@ expected actual)))) (define (test . xs) (apply test-f (cons equal? xs))) -(define (test-types . xs) (apply test-f (cons types-unify? xs))) +(define (test-types . xs) (apply test-f (cons types-equal? xs))) (define (read-file file) (call-with-input-file file @@ -43,12 +43,12 @@ (test-types (typecheck '(let ([bar (lambda (y) y)] [foo (lambda (x) (foo (bar #t)))]) foo)) - '(abs bool t0)) + '(abs bool a)) (test-types (typecheck '(let ([bar (lambda (y) y)] [foo (lambda (x) (foo (bar #t)))]) bar)) - '(abs t0 t0)) + '(abs a a)) (test-prog '(+ 1 2) 3) (test-prog '((lambda (x) ((lambda (y) (+ x y)) 42)) 100) 142) diff --git a/typecheck.scm b/typecheck.scm index 25a0e45..313db0e 100644 --- a/typecheck.scm +++ b/typecheck.scm @@ -81,11 +81,11 @@ ; we typecheck the lambda calculus only (only single arg lambdas) (define (typecheck prog) (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) @@ -116,54 +116,44 @@ (let* ([components (reverse (sccs (graph (let-bindings x))))] [process-component (lambda (acc comps) - (display comps) - (newline) (let* + ; create a new env with tvars for each component + ; e.g. scc of (x y) + ; scc-env = ((x . t0) (y . t1)) ([scc-env (fold-left (lambda (acc c) (env-insert acc c (fresh-tvar))) acc comps)] + ; typecheck each component [type-results (map (lambda (c) - (begin (display scc-env) (newline) (let ([body (cadr (assoc c (let-bindings x)))]) - (display body)(newline)(check scc-env body)))) + (check scc-env body))) comps)] + ; collect all the constraints in the scc [cs (fold-left (lambda (acc res c) (consolidate acc - (unify (cadr res) (env-lookup scc-env c)))) - '() type-results comps)]) - (display "process-component env:\n") - (display (substitute-env cs scc-env)) - (newline) - (substitute-env cs scc-env)))] + (consolidate (car res) + ; unify with tvars from scc-env + ; result ~ tvar + (unify (cadr res) (env-lookup scc-env c))))) + '() type-results comps)] + ; substitute *only* the bindings in this scc + [new-env + (map (lambda (x) + (if (memv (car x) comps) + (cons (car x) (substitute cs (cdr x))) + x)) + scc-env)]) + new-env))] [new-env (fold-left process-component env components)]) (check new-env (last (let-body x))))) - ;; (let ((new-env (fold-left - ;; (lambda (acc bind) - ;; (let* [(bind-tvar (fresh-tvar)) - ;; (env-with-tvar (env-insert acc (car bind) bind-tvar)) - ;; (bind-res (check env-with-tvar (cadr bind))) - ;; (bind-type (cadr bind-res)) - ;; (cs (consolidate (car bind-res) - ;; (unify bind-type bind-tvar)))] - ;; (substitute-env cs env-with-tvar))) - ;; env (let-bindings x)))) - ;; (display "sccs of graph\n") - ;; (display (sccs (graph (let-bindings x)))) - ;; (newline) - ;; (display "env when checking body:\n\t") - ;; (display new-env) - ;; (newline) - ;; (check new-env (last (let-body x))))) - - ('lambda (let* [(new-env (env-insert env (lambda-arg x) (fresh-tvar))) @@ -223,18 +213,25 @@ (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 (car res)) - (display "]\n") + ;; (display "result of ") + ;; (display x) + ;; (display ":\n\t") + ;; (display (pretty-type (cadr res))) + ;; (display "\n\t[") + ;; (display (car res)) + ;; (display "]\n") res)) (cadr (check '() (normalize prog)))) ; returns a list of pairs of constraints (define (unify a b) + (let ([res (unify? a b)]) + (if res + res + (error #f + (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)) @@ -242,7 +239,7 @@ (body-cs (unify (substitute arg-cs (caddr a)) (substitute arg-cs (caddr b))))] (consolidate arg-cs body-cs))) - (else (error #f "could not unify")))) + (else #f))) ; TODO: what's the most appropriate substitution? ; should all constraints just be limited to a pair? @@ -322,7 +319,15 @@ ; a1 -> a2 !~ bool -> bool ; basically can the tvars be renamed (define (types-equal? x y) - (error #f "todo")) + (let ([cs (unify? x y)]) + (if (not cs) #f + (let* + ([test-kind + (lambda (acc c) + (if (tvar? c) acc #f))] + [test (lambda (acc c) + (and acc (fold-left test-kind #t c)))]) + (fold-left test #t cs))))) ; input: a list of binds ((x . y) (y . 3)) ; returns: pair of verts, edges ((x y) . (x . y)) @@ -335,6 +340,8 @@ ['var (if (assoc x bs) (list x) '())] [else '()])) prog)) + (if (null? bs) + '(() . ()) (let* [(bind (car bs)) (vert (car bind)) @@ -347,7 +354,7 @@ (graph (cdr bs)))) (total-verts (cons vert (car rest))) (total-edges (append edges (cdr rest)))] - (cons total-verts total-edges))) + (cons total-verts total-edges)))) (define (successors graph v) (define (go v E) @@ -420,7 +427,6 @@ (list w) (cons w (new-scc)))))]) (set! result (cons scc result))))))]) - (for-each (lambda (v) (when (not (hashtable-contains? indices v)) ; v.index == -1 -- 2.30.2