diff --git a/collects/tests/typed-scheme/unit-tests/subst-tests.rkt b/collects/tests/typed-scheme/unit-tests/subst-tests.rkt index 6bb8593c..42332056 100644 --- a/collects/tests/typed-scheme/unit-tests/subst-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/subst-tests.rkt @@ -2,7 +2,7 @@ (require "test-utils.ss" (for-syntax scheme/base) (rep type-rep) - (types utils abbrev) + (types utils abbrev substitute) rackunit) (define-syntax-rule (s img var tgt result) diff --git a/collects/typed-scheme/infer/constraints.rkt b/collects/typed-scheme/infer/constraints.rkt index fb504a5c..444ddca9 100644 --- a/collects/typed-scheme/infer/constraints.rkt +++ b/collects/typed-scheme/infer/constraints.rkt @@ -62,13 +62,6 @@ (fail! S T)) (make-c S (or var X) T))])) -(define (subst-all/c sub -c) - (match -c - [(struct c (S X T)) - (make-c (subst-all sub S) - (F-n (subst-all sub (make-F X))) - (subst-all sub T))])) - (define (cset-meet x y) (match* (x y) [((struct cset (maps1)) (struct cset (maps2))) diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 434a53ca..9b1e2108 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -5,7 +5,8 @@ (combine-in (utils tc-utils) (rep free-variance type-rep filter-rep rep-utils) - (types utils convenience union subtype remove-intersect resolve) + (types utils convenience union subtype remove-intersect resolve + substitute) (env type-name-env index-env tvar-env)) make-env -> ->* one-of/c) "constraint-structs.rkt" @@ -509,7 +510,7 @@ (cond [(not no-entry) no-entry] [(not entry) (cons v no-entry)] - [(= (length entry) 3) no-entry] + [(or (i-subst? entry) (i-subst/starred? entry) (i-subst/dotted? entry)) no-entry] [else #f])))) (and absent-entries (append @@ -518,7 +519,7 @@ (evcase var [Constant (int-err "attempted to demote dotted variable")] [Covariant (int-err "attempted to demote dotted variable")] - [Contravariant (list missing null Univ)] + [Contravariant (i-subst/starred missing null Univ)] [Invariant (int-err "attempted to demote dotted variable")]))) S))) (match (car (cset-maps C)) @@ -526,24 +527,29 @@ (let ([subst (append (for/list ([(k dc) (in-hash dm)]) (match dc + [(dcon fixed #f) + (i-subst k + (for/list ([f fixed]) + (constraint->type f idx-hash #:variable k)))] [(dcon fixed rest) - (list k - (for/list ([f fixed]) - (constraint->type f idx-hash #:variable k)) - (and rest (constraint->type rest idx-hash)))] + (i-subst/starred k + (for/list ([f fixed]) + (constraint->type f idx-hash #:variable k)) + (constraint->type rest idx-hash))] [(dcon-exact fixed rest) - (list k - (for/list ([f fixed]) - (constraint->type f idx-hash #:variable k)) - (constraint->type rest idx-hash))])) + (i-subst/starred + k + (for/list ([f fixed]) + (constraint->type f idx-hash #:variable k)) + (constraint->type rest idx-hash))])) (for/list ([(k v) (in-hash cmap)]) - (list k (constraint->type v var-hash))))]) + (t-subst k (constraint->type v var-hash))))]) ;; verify that we got all the important variables (and (for/and ([v (fv R)]) (let ([entry (assq v subst)]) ;; Make sure we got a subst entry for a type var ;; (i.e. just a type to substitute) - (and entry (= (length entry) 2)))) + (and entry (t-subst? entry)))) (extend-idxs subst)))])) ;; V : a set of variables not to mention in the constraints diff --git a/collects/typed-scheme/infer/restrict.rkt b/collects/typed-scheme/infer/restrict.rkt index b0825050..9664ee4b 100644 --- a/collects/typed-scheme/infer/restrict.rkt +++ b/collects/typed-scheme/infer/restrict.rkt @@ -2,7 +2,7 @@ (require "../utils/utils.rkt") (require (rep type-rep) - (types utils union subtype remove-intersect resolve) + (types utils union subtype remove-intersect resolve substitute) "signatures.rkt" scheme/match mzlib/trace) diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index 180fa36c..8b5e91c7 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -13,7 +13,7 @@ ;; end fixme (for-syntax syntax/parse scheme/base (utils tc-utils)) (private type-annotation) - (types utils abbrev union subtype resolve convenience type-table) + (types utils abbrev union subtype resolve convenience type-table substitute) (utils tc-utils) (only-in srfi/1 alist-delete) (except-in (env type-env-structs tvar-env index-env) extend) @@ -417,16 +417,7 @@ (cons (make-ListDots tail-ty tail-bound) arg-tys) (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*)) (car rngs*))))) - => (lambda (substitution) - (define drest-bound (cdr (car drests*))) - (let ([dots-subst (assq drest-bound substitution)]) - (unless dots-subst - (int-err "expected dotted substitution for ~a" drest-bound)) - (do-ret (substitute-dotted (cadr dots-subst) - tail-bound - drest-bound - (subst-all (alist-delete drest-bound substitution eq?) - (car rngs*))))))] + => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] ;; ... function, (List A B C etc) arg [(and (car drests*) (not tail-bound) @@ -436,8 +427,7 @@ (untuple tail-ty) (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*) (car (car drests*)) (car rngs*) (fv (car rngs*)))) - => (lambda (substitution) - (define drest-bound (cdr (car drests*))) + => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] ;; if nothing matches, around the loop again [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] diff --git a/collects/typed-scheme/typecheck/tc-structs.rkt b/collects/typed-scheme/typecheck/tc-structs.rkt index 828f36ff..5ffb450b 100644 --- a/collects/typed-scheme/typecheck/tc-structs.rkt +++ b/collects/typed-scheme/typecheck/tc-structs.rkt @@ -3,7 +3,7 @@ (require "../utils/utils.rkt" (except-in (rep type-rep free-variance) Dotted) (private parse-type) - (types convenience utils union resolve abbrev) + (types convenience utils union resolve abbrev substitute) (env global-env type-env-structs type-name-env tvar-env) (utils tc-utils) "def-binding.rkt" @@ -199,7 +199,7 @@ ;; wrap everything in the approriate forall #:wrapper (lambda (t) (make-Poly tvars t)) #:type-wrapper (lambda (t) (make-App t new-tvars #f)) - #:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t)) + #:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (t-subst t Univ)) t)) #:poly? tvars)) diff --git a/collects/typed-scheme/types/substitute.rkt b/collects/typed-scheme/types/substitute.rkt new file mode 100644 index 00000000..191833ae --- /dev/null +++ b/collects/typed-scheme/types/substitute.rkt @@ -0,0 +1,145 @@ +#lang racket/base + +(require "../utils/utils.rkt" + (rep type-rep filter-rep object-rep rep-utils) + (utils tc-utils) + (only-in (rep free-variance) combine-frees) + (env index-env tvar-env) + scheme/match + scheme/contract) + +(provide subst-all substitute substitute-dots substitute-dotted subst + (struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)) + +(define (subst v t e) (substitute t v e)) + +(d-s/c substitution ([name symbol?])) +(d-s/c (t-subst substitution) ([type Type/c])) +(d-s/c (i-subst substitution) ([types (listof Type/c)])) +(d-s/c (i-subst/starred substitution) ([types (listof Type/c)] [starred Type/c])) +(d-s/c (i-subst/dotted substitution) ([types (listof Type/c)] [dty Type/c] [dbound symbol?])) + +;; substitute : Type Name Type -> Type +(d/c (substitute image name target #:Un [Un (get-union-maker)]) + ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?) + (define (sb t) (substitute image name t)) + (if (hash-ref (free-vars* target) name #f) + (type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb)) + target + [#:Union tys (Un (map sb tys))] + [#:F name* (if (eq? name* name) image target)] + [#:arr dom rng rest drest kws + (begin + (when (and (pair? drest) + (eq? name (cdr drest)) + (not (bound-tvar? name))) + (int-err "substitute used on ... variable ~a in type ~a" name target)) + (make-arr (map sb dom) + (sb rng) + (and rest (sb rest)) + (and drest (cons (sb (car drest)) (cdr drest))) + (map sb kws)))] + [#:ValuesDots types dty dbound + (begin + (when (and (eq? name dbound) (not (bound-tvar? name))) + (int-err "substitute used on ... variable ~a in type ~a" name target)) + (make-ValuesDots (map sb types) (sb dty) dbound))] + [#:ListDots dty dbound + (begin + (when (and (eq? name dbound) (not (bound-tvar? name))) + (int-err "substitute used on ... variable ~a in type ~a" name target)) + (make-ListDots (sb dty) dbound))]) + target)) + +;; implements angle bracket substitution from the formalism +;; substitute-dots : Listof[Type] Option[type] Name Type -> Type +(d/c (substitute-dots images rimage name target) + ((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?) + (define (sb t) (substitute-dots images rimage name t)) + (if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f)) + (type-case (#:Type sb #:Filter (sub-f sb)) target + [#:ListDots dty dbound + (if (eq? name dbound) + ;; We need to recur first, just to expand out any dotted usages of this. + (let ([expanded (sb dty)]) + (for/fold ([t (make-Value null)]) + ([img images]) + (make-Pair (substitute img name expanded) t))) + (make-ListDots (sb dty) dbound))] + [#:ValuesDots types dty dbound + (if (eq? name dbound) + (make-Values + (append + (map sb types) + ;; We need to recur first, just to expand out any dotted usages of this. + (let ([expanded (sb dty)]) + (for/list ([img images]) + (make-Result + (substitute img name expanded) + (make-FilterSet (make-Top) (make-Top)) + (make-Empty)))))) + (make-ValuesDots (map sb types) (sb dty) dbound))] + [#:arr dom rng rest drest kws + (if (and (pair? drest) + (eq? name (cdr drest))) + (make-arr (append + (map sb dom) + ;; We need to recur first, just to expand out any dotted usages of this. + (let ([expanded (sb (car drest))]) + (map (lambda (img) (substitute img name expanded)) images))) + (sb rng) + rimage + #f + (map sb kws)) + (make-arr (map sb dom) + (sb rng) + (and rest (sb rest)) + (and drest (cons (sb (car drest)) (cdr drest))) + (map sb kws)))]) + target)) + +;; implements curly brace substitution from the formalism +;; substitute-dotted : Type Name Name Type -> Type +(define (substitute-dotted image image-bound name target) + (define (sb t) (substitute-dotted image image-bound name t)) + (if (hash-ref (free-idxs* target) name #f) + (type-case (#:Type sb #:Filter (sub-f sb)) + target + [#:ValuesDots types dty dbound + (make-ValuesDots (map sb types) + (sb dty) + (if (eq? name dbound) image-bound dbound))] + [#:ListDots dty dbound + (make-ListDots (sb dty) + (if (eq? name dbound) image-bound dbound))] + [#:F name* + (if (eq? name* name) + image + target)] + [#:arr dom rng rest drest kws + (make-arr (map sb dom) + (sb rng) + (and rest (sb rest)) + (and drest + (cons (substitute image (cdr drest) (sb (car drest))) + (if (eq? name (cdr drest)) image-bound (cdr drest)))) + (map sb kws))]) + target)) + +;; substitute many variables +;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]] +;; subst-all : substitution Type -> Type +(d/c (subst-all s t) + ((listof substitution?) Type/c . -> . Type/c) + (for/fold ([t t]) ([e s]) + (match e + [(t-subst v img) + (substitute img v t)] + [(i-subst v imgs) + (substitute-dots imgs #f v t)] + [(i-subst/starred v imgs rest) + (substitute-dots imgs rest v t)] + [(i-subst/dotted v imgs dty dbound) + (int-err "i-subst/dotted nyi") + #; + (substitute-dotted imgs rest v t)]))) \ No newline at end of file diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index 7b5d91de..86c1a983 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -2,7 +2,7 @@ (require "../utils/utils.rkt" (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) - (types utils comparison resolve abbrev) + (types utils comparison resolve abbrev substitute) (env type-name-env) (only-in (infer infer-dummy) unify) scheme/match unstable/match @@ -305,8 +305,7 @@ (=> unmatch) (unless (= (length ns) (length ms)) (unmatch)) - ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) - (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] + (subtype* A0 b1 (subst-all (map t-subst ms (map make-F ns)) b2))] [((Refinement: par _ _) t) (subtype* A0 par t)] ;; use unification to see if we can use the polytype here diff --git a/collects/typed-scheme/types/utils.rkt b/collects/typed-scheme/types/utils.rkt index 177754a0..8e4df07c 100644 --- a/collects/typed-scheme/types/utils.rkt +++ b/collects/typed-scheme/types/utils.rkt @@ -4,6 +4,7 @@ (require (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) + "substitute.rkt" (only-in (rep free-variance) combine-frees) (env index-env tvar-env) scheme/match @@ -13,12 +14,6 @@ (for-syntax scheme/base syntax/parse)) (provide fv fv/list fi - substitute - substitute-dots - substitute-dotted - subst-all - subst - ;ret instantiate-poly instantiate-poly-dotted tc-result? @@ -33,125 +28,6 @@ current-poly-struct) -;; substitute : Type Name Type -> Type -(d/c (substitute image name target #:Un [Un (get-union-maker)]) - ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?) - (define (sb t) (substitute image name t)) - (if (hash-ref (free-vars* target) name #f) - (type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb)) - target - [#:Union tys (Un (map sb tys))] - [#:F name* (if (eq? name* name) image target)] - [#:arr dom rng rest drest kws - (begin - (when (and (pair? drest) - (eq? name (cdr drest)) - (not (bound-tvar? name))) - (int-err "substitute used on ... variable ~a in type ~a" name target)) - (make-arr (map sb dom) - (sb rng) - (and rest (sb rest)) - (and drest (cons (sb (car drest)) (cdr drest))) - (map sb kws)))] - [#:ValuesDots types dty dbound - (begin - (when (and (eq? name dbound) (not (bound-tvar? name))) - (int-err "substitute used on ... variable ~a in type ~a" name target)) - (make-ValuesDots (map sb types) (sb dty) dbound))] - [#:ListDots dty dbound - (begin - (when (and (eq? name dbound) (not (bound-tvar? name))) - (int-err "substitute used on ... variable ~a in type ~a" name target)) - (make-ListDots (sb dty) dbound))]) - target)) - -;; implements angle bracket substitution from the formalism -;; substitute-dots : Listof[Type] Option[type] Name Type -> Type -(d/c (substitute-dots images rimage name target) - ((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?) - (define (sb t) (substitute-dots images rimage name t)) - (if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f)) - (type-case (#:Type sb #:Filter (sub-f sb)) target - [#:ListDots dty dbound - (if (eq? name dbound) - ;; We need to recur first, just to expand out any dotted usages of this. - (let ([expanded (sb dty)]) - (for/fold ([t (make-Value null)]) - ([img images]) - (make-Pair (substitute img name expanded) t))) - (make-ListDots (sb dty) dbound))] - [#:ValuesDots types dty dbound - (if (eq? name dbound) - (make-Values - (append - (map sb types) - ;; We need to recur first, just to expand out any dotted usages of this. - (let ([expanded (sb dty)]) - (for/list ([img images]) - (make-Result - (substitute img name expanded) - (make-FilterSet (make-Top) (make-Top)) - (make-Empty)))))) - (make-ValuesDots (map sb types) (sb dty) dbound))] - [#:arr dom rng rest drest kws - (if (and (pair? drest) - (eq? name (cdr drest))) - (make-arr (append - (map sb dom) - ;; We need to recur first, just to expand out any dotted usages of this. - (let ([expanded (sb (car drest))]) - (map (lambda (img) (substitute img name expanded)) images))) - (sb rng) - rimage - #f - (map sb kws)) - (make-arr (map sb dom) - (sb rng) - (and rest (sb rest)) - (and drest (cons (sb (car drest)) (cdr drest))) - (map sb kws)))]) - target)) - -;; implements curly brace substitution from the formalism -;; substitute-dotted : Type Name Name Type -> Type -(define (substitute-dotted image image-bound name target) - (define (sb t) (substitute-dotted image image-bound name t)) - (if (hash-ref (free-idxs* target) name #f) - (type-case (#:Type sb #:Filter (sub-f sb)) - target - [#:ValuesDots types dty dbound - (make-ValuesDots (map sb types) - (sb dty) - (if (eq? name dbound) image-bound dbound))] - [#:ListDots dty dbound - (make-ListDots (sb dty) - (if (eq? name dbound) image-bound dbound))] - [#:F name* - (if (eq? name* name) - image - target)] - [#:arr dom rng rest drest kws - (make-arr (map sb dom) - (sb rng) - (and rest (sb rest)) - (and drest - (cons (substitute image (cdr drest) (sb (car drest))) - (if (eq? name (cdr drest)) image-bound (cdr drest)))) - (map sb kws))]) - target)) - -;; substitute many variables -;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]] -;; subst-all : substitution Type -> Type -(define (subst-all s t) - (for/fold ([t t]) ([e s]) - (match e - [(list v (list imgs ...) starred) - (substitute-dots imgs starred v t)] - [(list v img) - (substitute img v t)]))) - - ;; unfold : Type -> Type ;; must be applied to a Mu (define (unfold t) @@ -164,13 +40,13 @@ [(Poly: ns body) (unless (= (length types) (length ns)) (int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types))) - (subst-all (map list ns types) body)] + (subst-all (map t-subst ns types) body)] [(PolyDots: (list fixed ... dotted) body) (unless (>= (length types) (length fixed)) (int-err "instantiate-poly: wrong number of types: expected at least ~a, got ~a" (length fixed) (length types))) (let* ([fixed-tys (take types (length fixed))] [rest-tys (drop types (length fixed))] - [body* (subst-all (map list fixed fixed-tys) body)]) + [body* (subst-all (map t-subst fixed fixed-tys) body)]) (substitute-dots rest-tys #f dotted body*))] [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)])) @@ -180,7 +56,7 @@ (unless (= (length fixed) (length types)) (int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a, types were ~a" (length fixed) (length types) types)) - (let ([body* (subst-all (map list fixed types) body)]) + (let ([body* (subst-all (map t-subst fixed types) body)]) (substitute-dotted image var dotted body*))] [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)])) @@ -277,8 +153,6 @@ [(list (tc-result1: t f o) ...) (ret t f o)])) -(define (subst v t e) (substitute t v e)) - ;; type comparison