From 3b2d3eb96f8b4003f038c519691e61f08273458e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Mon, 25 Sep 2017 15:44:38 +0200 Subject: [PATCH] Cleanup --- macrotypes/type-constraints.rkt | 150 ++++++++++++++------------------ turnstile/examples/infer.rkt | 2 +- turnstile/examples/mlish.rkt | 14 --- 3 files changed, 64 insertions(+), 102 deletions(-) diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt index 6e2088f..d7f5af4 100644 --- a/macrotypes/type-constraints.rkt +++ b/macrotypes/type-constraints.rkt @@ -24,78 +24,54 @@ ;; (Listof Id) (Listof (List Id Type)) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Id Type)) ;; Adds a new set of constaints to a substituion, using the type ;; unification algorithm for local type inference. -(define (add-constraints Xs substs new-cs [orig-cs new-cs] - #:variance [csvariance invariant]) +(define (add-constraints Xs substs new-cs [orig-cs new-cs]) (define Xs* (stx->list Xs)) (define (X? X) (member X Xs* free-identifier=?)) - (add-constraints/var? X? substs new-cs orig-cs - #:variance csvariance)) + (add-constraints/var? Xs* X? substs new-cs orig-cs)) -;; Variance Type Type -> Boolean -(define (typecheck?/variance variance a-expected b-actual) - (cond - [(variance-covariant? variance) (typecheck? b-actual a-expected)] - [(variance-contravariant? variance) (typecheck? b-actual a-expected)] - ;; invariant and irrelevant - ;; TODO: use a parameter to indicate whether we're making a co/contravariant typecheck?, or whether it's an invariant typecheck? (to avoid an exponential cost by branching at each step) - [else (and (typecheck? a-expected b-actual) - (typecheck? b-actual a-expected))])) - -;; (Listof Id) -> (free-id-table/c identifier? variance? #:immutable #t) -(define (default-variances Ys) - (make-immutable-free-id-table - (for/list ([X (in-list Ys)]) - (cons X covariant)))); invariant ;;;;;;;;;;;;; TODO: should be invariant, putting covariant for now for quick tests. - - - - - - - - - -(define (add-constraints/var? var? substs new-cs [orig-cs new-cs] - #:variance [csvariance invariant] - ;#:variances [variances* #f] - ) - (define (r #:substs [substs substs] #:new-cs [new-cs new-cs]) - (add-constraints/var? var? substs new-cs orig-cs #:variance csvariance)) +(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs]) + (define Xs (stx->list Xs*)) (define Ys (stx-map stx-car substs)) (define-syntax-class var [pattern x:id #:when (var? #'x)]) - #;(begin - (displayln "~~~~") - (if (stx-null? new-cs) - (displayln '()) - (begin (display 'a) (displayln (type->str (stx-car (stx-car new-cs)))) - (display 'b) (displayln (type->str (stx-car (stx-cdr (stx-car new-cs)))))))) (syntax-parse new-cs [() substs] - [([a-expected:var b-actual] . rst) + [([a:var b] . rst) (cond - [(member #'a-expected Ys free-identifier=?) + [(member #'a Ys free-identifier=?) ;; There are two cases. ;; Either #'a already maps to #'b or an equivalent type, ;; or #'a already maps to a type that conflicts with #'b. ;; In either case, whatever #'a maps to must be equivalent ;; to #'b, so add that to the constraints. - (r #:new-cs (cons (list (lookup #'a-expected substs) #'b-actual) - #'rst))] - [(and (identifier? #'b-actual) (var? #'b-actual) (free-identifier=? #'a-expected #'b-actual)) + (add-constraints/var? + Xs + var? + substs + (cons (list (lookup #'a substs) #'b) + #'rst) + orig-cs)] + [(and (identifier? #'b) (var? #'b) (free-identifier=? #'a #'b)) ;; #'a and #'b are equal, drop this constraint - (r #:new-cs #'rst)] + (add-constraints/var? Xs var? substs #'rst orig-cs)] [else - (define entry (occurs-check (list #'a-expected #'b-actual) orig-cs)) - (r ;; Add the mapping #'a -> #'b to the substitution, - #:substs (begin #;(displayln (list (type->str (car entry)) '-> (type->str (cadr entry)) 'with-substs substs)) - (add-substitution-entry entry substs #:new-cs new-cs #:orig-cs orig-cs)) + (define entry (occurs-check (list #'a #'b) orig-cs)) + (add-constraints/var? + Xs + var? + ;; Add the mapping #'a -> #'b to the substitution, + (add-substitution-entry entry substs) ;; and substitute that in each of the constraints. - #:new-cs (cs-substitute-entry entry #'rst))])] - [([a-expected b-actual:var] . rst) - (r #:new-cs #'([b-actual a-expected] . rst))] - [([a-expected b-actual] . rst) + (cs-substitute-entry entry #'rst) + orig-cs)])] + [([a b:var] . rst) + (add-constraints/var? Xs + var? + substs + #'([b a] . rst) + orig-cs)] + [([a b] . rst) ;; If #'a and #'b are base types, check that they're equal. ;; Identifers not within Xs count as base types. ;; If #'a and #'b are constructed types, check that the @@ -103,44 +79,54 @@ ;; recur. ;; Otherwise, raise an error. (cond - [(identifier? #'a-expected) + [(identifier? #'a) ;; #'a is an identifier, but not a var, so it is considered ;; a base type. We also know #'b is not a var, so #'b has ;; to be the same "identifier base type" as #'a. - (unless (and (identifier? #'b-actual) (free-identifier=? #'a-expected #'b-actual)) - #;(displayln 1) - (type-error #:src (get-orig #'b-actual) + (unless (and (identifier? #'b) (free-identifier=? #'a #'b)) + (type-error #:src (get-orig #'b) #:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a" (string-join (map type->str (stx-map stx-car orig-cs)) ", ") (string-join (map type->str (stx-map stx-cadr orig-cs)) ", ")) - #'a-expected #'b-actual)) - (r #:new-cs #'rst)] + #'a #'b)) + (add-constraints/var? Xs + var? + substs + #'rst + orig-cs)] [else - (syntax-parse #'[a-expected b-actual] + (syntax-parse #'[a b] [_ - #:when (typecheck?/variance csvariance #'a-expected #'b-actual);; variances ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (r #:new-cs #'rst)] + #:when (typecheck? #'a #'b) + (add-constraints/var? Xs + var? + substs + #'rst + orig-cs)] [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TODO: flip variance as needed depending on the variances for tycons1 / tycons2. #:when (typecheck? #'tycons1 #'tycons2) #:when (stx-length=? #'[τ1 ...] #'[τ2 ...]) - (r #:new-cs #'((τ1 τ2) ... . rst))] + (add-constraints/var? Xs + var? + substs + #'((τ1 τ2) ... . rst) + orig-cs)] [else - #;(displayln 2) - (type-error #:src (get-orig #'b-actual) + (type-error #:src (get-orig #'b) #:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a" (string-join (map type->str (stx-map stx-car orig-cs)) ", ") (string-join (map type->str (stx-map stx-cadr orig-cs)) ", ")) - #'a-expected #'b-actual)])])])) - - - - - - - - + #'a #'b)])])])) +;; Variance Type Type -> Boolean +(define (typecheck?/variance variance a b) + (cond + [(variance-covariant? variance) (typecheck? b a)] + [(variance-contravariant? variance) (typecheck? b a)] + ;; invariant and irrelevant + ;; TODO: use a parameter to indicate whether we're making a co/contravariant typecheck?, or whether it's an invariant typecheck? (to avoid an exponential cost by branching at each step) + [else (and (typecheck? a b) + (typecheck? b a))])) ;; (-> Any Boolean : (∩ X Id)) ;; (FreeIdTable (∩ X Id) Variance) @@ -196,21 +182,12 @@ [(_ . rest) (do-error)])) - - - - - - - - - (define (datum=? x y) (equal? (syntax->datum x) (syntax->datum y))) ;; add-substitution-entry : (List Id Type) (Listof (List Id Type)) -> (Listof (List Id Type)) ;; Adds the mapping a -> b to the substitution and substitutes for it in the other entries -(define (add-substitution-entry entry substs #:new-cs new-cs #:orig-cs orig-cs) +(define (add-substitution-entry entry substs) (match-define (list a b) entry) (cons entry (for/list ([subst (in-list substs)]) @@ -230,7 +207,6 @@ (match-define (list a b) entry) (cond [(stx-contains-id? b a) (type-error #:src (get-orig b) - ;; TODO: should escape the possible ~a within the type->str result ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #:msg (format (string-append "couldn't unify ~~a and ~~a because one contains the other\n" " expected: ~a\n" diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt index 4941be2..8335540 100644 --- a/turnstile/examples/infer.rkt +++ b/turnstile/examples/infer.rkt @@ -104,7 +104,7 @@ ;; some/inst/generalize : (Stx-Listof Id) Type-Stx Constraints -> Type-Stx (define (some/inst/generalize Xs* ty* cs1) (define Xs (stx->list Xs*)) - (define cs2 (add-constraints/var? identifier? '() cs1)) + (define cs2 (add-constraints/var? Xs identifier? '() cs1)) (define Vs (set-minus/Xs (stx-map stx-car cs2) Xs)) (define constrainable-vars (find-constrainable-vars Xs cs2 Vs)) diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index 27523e5..f3566ba 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -884,9 +884,6 @@ [⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))] ;; solve for type variables Xs #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax) - #:do {} #;{(newline) - (displayln "Solved argument types") - (map displayln (syntax->datum #'[[e_arg- ...] Xs* cs]))} ;; instantiate polymorphic function type #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) @@ -895,17 +892,6 @@ (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) ;; compute argument types #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...)) - #:do {}#;{(newline) - (displayln "Computed argument types") - (for ([a (in-syntax #'(τ_arg ...))] - [in (in-syntax #'(τ_in ...))] - [e (in-syntax #'(e_arg ...))]) - (display 'a=) (displayln (type->str a)) - (display 'i=) (displayln (type->str in)) - (display 'e=) (displayln (syntax->datum e)) - (display 'ck) (displayln (check? a in)) - (newline)) - (displayln "----")} ;; typecheck args [τ_arg τ⊑ τ_in #:for e_arg] ... #:with τ_out* (if (stx-null? #'(unsolved-X ...))