From 02c4f0dd11034435cf74db68cc12ea86e9441c77 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Tue, 26 Feb 2013 23:25:19 -0800 Subject: [PATCH] Make PolyDots be subtypes even if they have different fixed arguments. original commit: 75f89107b1449deda042b62feaebb9b9bf3c92ec --- .../typed-racket/unit-tests/subtype-tests.rkt | 6 +++ collects/typed-racket/types/abbrev.rkt | 3 -- collects/typed-racket/types/base-abbrev.rkt | 5 +++ collects/typed-racket/types/substitute.rkt | 41 ++++++++++--------- collects/typed-racket/types/subtype.rkt | 20 +++++---- collects/typed-racket/types/utils.rkt | 2 +- 6 files changed, 46 insertions(+), 31 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt index 67091af6..c3f68ac1 100644 --- a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt @@ -206,6 +206,12 @@ [(-polydots (a) (->... null (a a) (make-ListDots a 'a))) (-poly (a b) (-> a b (-Tuple (list a b))))] + + [(-polydots (b a) (-> (->... (list b) (a a) (make-ValuesDots (list (-result b)) a 'a)) Univ)) + (-polydots (a) (-> (->... (list) (a a) (make-ValuesDots null a 'a)) Univ))] + + [(-polydots (a) (->... (list) (a a) (make-ListDots a 'a))) + (-polydots (b a) (->... (list b) (a a) (-pair b (make-ListDots a 'a))))] )) (define-go diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt index a0ac8083..c94f32fd 100644 --- a/collects/typed-racket/types/abbrev.rkt +++ b/collects/typed-racket/types/abbrev.rkt @@ -33,7 +33,6 @@ (define -App make-App) -(define -pair make-Pair) (define -mpair make-MPair) (define -Param make-Param) (define -box make-Box) @@ -51,8 +50,6 @@ -(define (-lst* #:tail [tail (-val null)] . args) - (for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl))) (define (-Tuple l) (foldr -pair (-val '()) l)) diff --git a/collects/typed-racket/types/base-abbrev.rkt b/collects/typed-racket/types/base-abbrev.rkt index b9b88446..f11b277e 100644 --- a/collects/typed-racket/types/base-abbrev.rkt +++ b/collects/typed-racket/types/base-abbrev.rkt @@ -32,6 +32,11 @@ ;; Void is needed for Params (define -Void (make-Base 'Void #'void? void? #'-Void #f)) +;; -lst* Type is needed by substitute for ListDots +(define -pair make-Pair) +(define (-lst* #:tail [tail (-val null)] . args) + (for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl))) + ;; Simple union type, does not check for overlaps diff --git a/collects/typed-racket/types/substitute.rkt b/collects/typed-racket/types/substitute.rkt index 47174599..1ecb1df5 100644 --- a/collects/typed-racket/types/substitute.rkt +++ b/collects/typed-racket/types/substitute.rkt @@ -5,6 +5,7 @@ (utils tc-utils) (rep free-variance) (env index-env tvar-env) + (only-in (types base-abbrev) -lst* -result) racket/match racket/set racket/contract @@ -133,31 +134,36 @@ ;; 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)) +(define (substitute-dotted pre-image image image-bound name target) + (define (sb t) (substitute-dotted pre-image image image-bound name t)) (if (or (set-member? (free-vars-names (free-idxs* target)) name) (set-member? (free-vars-names (free-vars* target)) name)) (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))] + (let ((extra-types (if (eq? name dbound) pre-image null))) + (make-ValuesDots (append (map sb types) (map -result extra-types)) + (sb dty) + (if (eq? name dbound) image-bound dbound)))] [#:ListDots dty dbound - (make-ListDots (sb dty) - (if (eq? name dbound) image-bound dbound))] + (apply -lst* + (if (eq? name dbound) pre-image null) + #:tail + (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))]) + (let ((extra-types (if (and drest (eq? name (cdr drest))) pre-image null))) + (make-arr (append (map sb dom) extra-types) + (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 @@ -174,7 +180,6 @@ [_ acc]))) (define t-substed-ty (substitute-many t-substs ty)) - (for/fold ([t t-substed-ty]) ([(v r) (in-hash s)]) (match r [(t-subst img) t] @@ -182,9 +187,5 @@ (substitute-dots imgs #f v t)] [(i-subst/starred imgs rest) (substitute-dots imgs rest v t)] - [(i-subst/dotted null dty dbound) - (substitute-dotted dty dbound v t)] [(i-subst/dotted imgs dty dbound) - (int-err "i-subst/dotted nyi") - #; - (substitute-dotted imgs rest v t)]))) + (substitute-dotted imgs dty dbound v t)]))) diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index 6b9f1a4f..a70995ef 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/collects/typed-racket/types/subtype.rkt @@ -362,13 +362,19 @@ (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))] [((PolyDots: (list ns ... n-dotted) b1) (PolyDots: (list ms ... m-dotted) b2)) - (=> unmatch) - (unless (= (length ns) (length ms)) - (unmatch)) - (define subst - (hash-set (make-simple-substitution ms (map make-F ns)) - m-dotted (i-subst/dotted null (make-F n-dotted) n-dotted))) - (subtype* A0 b1 (subst-all subst b2))] + (cond + ((< (length ns) (length ms)) + (define-values (short-ms rest-ms) (split-at ms (length ns))) + (define subst + (hash-set (make-simple-substitution ns (map make-F short-ms)) + n-dotted (i-subst/dotted (map make-F rest-ms) (make-F m-dotted) m-dotted))) + (subtype* A0 (subst-all subst b1) b2)) + (else + (define-values (short-ns rest-ns) (split-at ns (length ms))) + (define subst + (hash-set (make-simple-substitution ms (map make-F short-ns)) + m-dotted (i-subst/dotted (map make-F rest-ns) (make-F n-dotted) n-dotted))) + (subtype* A0 b1 (subst-all subst b2))))] [((PolyDots: (list ns ... n-dotted) b1) (Poly: (list ms ...) b2)) (=> unmatch) diff --git a/collects/typed-racket/types/utils.rkt b/collects/typed-racket/types/utils.rkt index 32c93241..70c0542f 100644 --- a/collects/typed-racket/types/utils.rkt +++ b/collects/typed-racket/types/utils.rkt @@ -51,7 +51,7 @@ " types: expected ~a, got ~a, types were ~a") (length fixed) (length types) types)) (let ([body* (subst-all (make-simple-substitution fixed types) body)]) - (substitute-dotted image var dotted body*))] + (substitute-dotted null image var dotted body*))] [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))