diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 9b1e21082a..fe0d22f21f 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -14,7 +14,7 @@ scheme/match mzlib/etc mzlib/trace racket/contract - unstable/sequence unstable/list unstable/debug + unstable/sequence unstable/list unstable/debug unstable/hash scheme/list) (import dmap^ constraints^ promote-demote^) @@ -478,7 +478,7 @@ ;; Y : (listof symbol?) - index variables that must have entries ;; R : Type? - result type into which we will be substituting (d/c (subst-gen C Y R) - (cset? (listof symbol?) Type? . -> . (or/c #f list?)) + (cset? (listof symbol?) Type? . -> . (or/c #f substitution/c)) (define var-hash (free-vars* R)) (define idx-hash (free-idxs* R)) ;; v : Symbol - variable for which to check variance @@ -499,11 +499,20 @@ ;; was found. If we're at this point and had no other constraints, then adding the ;; equivalent of the constraint (dcon null (c Bot X Top)) is okay. (define (extend-idxs S) + (define fi-R (fi R)) + ;; If the index variable v is not used in the type, then + ;; we allow it to be replaced with the empty list of types; + ;; otherwise we error, as we do not yet know what an appropriate + ;; lower bound is. + (define (demote/check-free v) + (if (memq v fi-R) + (int-err "attempted to demote dotted variable") + (i-subst null))) ;; absent-entries is #f if there's an error in the substitution, otherwise ;; it's a list of variables that don't appear in the substitution (define absent-entries (for/fold ([no-entry null]) ([v (in-list Y)]) - (let ([entry (assq v S)]) + (let ([entry (hash-ref S v #f)]) ;; Make sure we got a subst entry for an index var ;; (i.e. a list of types for the fixed portion ;; and a type for the starred portion) @@ -513,40 +522,42 @@ [(or (i-subst? entry) (i-subst/starred? entry) (i-subst/dotted? entry)) no-entry] [else #f])))) (and absent-entries - (append - (for/list ([missing (in-list absent-entries)]) + (hash-union + (for/hash ([missing (in-list absent-entries)]) (let ([var (hash-ref idx-hash missing Constant)]) - (evcase var - [Constant (int-err "attempted to demote dotted variable")] - [Covariant (int-err "attempted to demote dotted variable")] - [Contravariant (i-subst/starred missing null Univ)] - [Invariant (int-err "attempted to demote dotted variable")]))) + (values missing + (evcase var + [Constant (demote/check-free missing)] + [Covariant (demote/check-free missing)] + [Contravariant (i-subst/starred null Univ)] + [Invariant (demote/check-free missing)])))) S))) (match (car (cset-maps C)) [(cons cmap (dmap dm)) - (let ([subst (append - (for/list ([(k dc) (in-hash dm)]) + (let ([subst (hash-union + (for/hash ([(k dc) (in-hash dm)]) (match dc [(dcon fixed #f) - (i-subst k + (values k + (i-subst (for/list ([f fixed]) - (constraint->type f idx-hash #:variable k)))] + (constraint->type f idx-hash #:variable k))))] [(dcon fixed rest) - (i-subst/starred k - (for/list ([f fixed]) - (constraint->type f idx-hash #:variable k)) - (constraint->type rest idx-hash))] + (values k + (i-subst/starred (for/list ([f fixed]) + (constraint->type f idx-hash #:variable k)) + (constraint->type rest idx-hash)))] [(dcon-exact fixed rest) - (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)]) - (t-subst k (constraint->type v var-hash))))]) + (values k + (i-subst/starred + (for/list ([f fixed]) + (constraint->type f idx-hash #:variable k)) + (constraint->type rest idx-hash)))])) + (for/hash ([(k v) (in-hash cmap)]) + (values k (t-subst (constraint->type v var-hash)))))]) ;; verify that we got all the important variables (and (for/and ([v (fv R)]) - (let ([entry (assq v subst)]) + (let ([entry (hash-ref subst v #f)]) ;; Make sure we got a subst entry for a type var ;; (i.e. just a type to substitute) (and entry (t-subst? entry)))) diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index 8b5e91c767..e4bc51ece4 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -360,6 +360,7 @@ (values tail-ty tail-bound)] [t (values t #f)])]) (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (define (finish substitution) (do-ret (subst-all substitution (car rngs*)))) (cond [(null? doms*) (match f-ty [(tc-result1: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) @@ -378,7 +379,7 @@ (car doms*)) (car rests*) (car rngs*))) - => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] + => finish] ;; actual work, when we have a * function and ... final arg [(and (car rests*) tail-bound @@ -390,8 +391,7 @@ (car doms*)) (car rests*) (car rngs*))) - => (lambda (substitution) - (do-ret (subst-all substitution (car rngs*))))] + => finish] ;; ... function, ... arg, same bound on ... [(and (car drests*) tail-bound @@ -402,8 +402,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) - (do-ret (subst-all substitution (car rngs*))))] + => finish] ;; ... function, ... arg, different bound on ... [(and (car drests*) tail-bound @@ -417,7 +416,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) (do-ret (subst-all substitution (car rngs*))))] + => finish] ;; ... function, (List A B C etc) arg [(and (car drests*) (not tail-bound) @@ -427,8 +426,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) - (do-ret (subst-all substitution (car rngs*))))] + => finish] ;; if nothing matches, around the loop again [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [(tc-result1: (PolyDots: vars (Function: '()))) diff --git a/collects/typed-scheme/typecheck/tc-structs.rkt b/collects/typed-scheme/typecheck/tc-structs.rkt index 5ffb450b06..45c3a44682 100644 --- a/collects/typed-scheme/typecheck/tc-structs.rkt +++ b/collects/typed-scheme/typecheck/tc-structs.rkt @@ -11,6 +11,7 @@ syntax/struct mzlib/trace unstable/debug + racket/function scheme/match (for-syntax scheme/base)) @@ -197,9 +198,9 @@ ;; then register them (mk/register-sty nm flds parent-name parent-field-types types ;; 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]) (t-subst t Univ)) t)) + #:wrapper (λ (t) (make-Poly tvars t)) + #:type-wrapper (λ (t) (make-App t new-tvars #f)) + #:pred-wrapper (λ (t) (subst-all (make-simple-substitution tvars (map (const Univ) tvars)) t)) #:poly? tvars)) diff --git a/collects/typed-scheme/types/substitute.rkt b/collects/typed-scheme/types/substitute.rkt index 191833aefd..873b923647 100644 --- a/collects/typed-scheme/types/substitute.rkt +++ b/collects/typed-scheme/types/substitute.rkt @@ -9,15 +9,23 @@ 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)) + (struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted) + substitution/c make-simple-substitution) (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?])) +(d/c (make-simple-substitution vs ts) + (([vs (listof symbol?)] [ts (listof Type/c)]) () #:pre-cond (= (length vs) (length ts)) . ->d . [_ substitution/c]) + (for/hash ([v (in-list vs)] [t (in-list ts)]) + (values v (t-subst t)))) + +(d-s/c subst-rhs ()) +(d-s/c (t-subst subst-rhs) ([type Type/c])) +(d-s/c (i-subst subst-rhs) ([types (listof Type/c)])) +(d-s/c (i-subst/starred subst-rhs) ([types (listof Type/c)] [starred Type/c])) +(d-s/c (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?])) + +(define substitution/c (hash/c symbol? subst-rhs? #:immutable #t)) ;; substitute : Type Name Type -> Type (d/c (substitute image name target #:Un [Un (get-union-maker)]) @@ -130,16 +138,16 @@ ;; 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) + (substitution/c Type? . -> . Type?) + (for/fold ([t t]) ([(v r) s]) + (match r + [(t-subst img) (substitute img v t)] - [(i-subst v imgs) + [(i-subst imgs) (substitute-dots imgs #f v t)] - [(i-subst/starred v imgs rest) + [(i-subst/starred imgs rest) (substitute-dots imgs rest v t)] - [(i-subst/dotted v imgs dty dbound) + [(i-subst/dotted 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 86c1a983e8..fde4c80805 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -305,7 +305,7 @@ (=> unmatch) (unless (= (length ns) (length ms)) (unmatch)) - (subtype* A0 b1 (subst-all (map t-subst ms (map make-F ns)) b2))] + (subtype* A0 b1 (subst-all (make-simple-substitution 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 8e4df07c71..af9780bf3f 100644 --- a/collects/typed-scheme/types/utils.rkt +++ b/collects/typed-scheme/types/utils.rkt @@ -40,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 t-subst ns types) body)] + (subst-all (make-simple-substitution 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 t-subst fixed fixed-tys) body)]) + [body* (subst-all (make-simple-substitution fixed fixed-tys) body)]) (substitute-dots rest-tys #f dotted body*))] [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)])) @@ -56,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 t-subst fixed types) body)]) + (let ([body* (subst-all (make-simple-substitution fixed types) body)]) (substitute-dotted image var dotted body*))] [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))