From b8c9e1f63f71f6fcb1d8302c229533a5662e955c Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Wed, 13 Mar 2013 22:56:13 -0700 Subject: [PATCH] Cleanup of subtyping, additional comments, and improved short circuting. original commit: 71d6189132cecffc75b4d2fdb41c985a1a763380 --- .../tests/typed-racket/succeed/pr12644.rkt | 4 ++-- collects/typed-racket/base-env/base-env.rkt | 2 +- collects/typed-racket/types/substitute.rkt | 12 +++++++----- collects/typed-racket/types/subtype.rkt | 18 +++++++++++------- 4 files changed, 21 insertions(+), 15 deletions(-) diff --git a/collects/tests/typed-racket/succeed/pr12644.rkt b/collects/tests/typed-racket/succeed/pr12644.rkt index 9c4fad47..6c58ddbb 100644 --- a/collects/tests/typed-racket/succeed/pr12644.rkt +++ b/collects/tests/typed-racket/succeed/pr12644.rkt @@ -9,14 +9,14 @@ (: v (Listof (U inf Byte))) (define v - (list + (list (with-handlers ((void values)) 2) (with-handlers ((void add1)) 3) (with-handlers ((void f)) 4) (with-handlers ((void g)) 5))) -(list +(list (with-handlers ((void values)) 6) (with-handlers ((void add1)) 7) (with-handlers ((void f)) 8) diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt index 1c893aa2..d6b67441 100644 --- a/collects/typed-racket/base-env/base-env.rkt +++ b/collects/typed-racket/base-env/base-env.rkt @@ -1392,7 +1392,7 @@ -[values (-polydots (a b) (cl->* +[values (-polydots (a b) (cl->* (-> (-values null)) (->acc (list a) a null) ((list a) (b b) . ->... . (make-ValuesDots (list (-result a)) b 'b))))] diff --git a/collects/typed-racket/types/substitute.rkt b/collects/typed-racket/types/substitute.rkt index 1ecb1df5..10b9370c 100644 --- a/collects/typed-racket/types/substitute.rkt +++ b/collects/typed-racket/types/substitute.rkt @@ -34,7 +34,7 @@ (for/hash ([v (in-list vs)] [t (in-list ts)]) (values v (t-subst t)))) - +;; TODO: Figure out if free var checking/short circuiting is actually a performance improvement. ;; substitute-many : Hash[Name,Type] Type -> Type (define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))]) @@ -132,16 +132,18 @@ (map sb kws)))]) target)) -;; implements curly brace substitution from the formalism -;; substitute-dotted : Type Name Name Type -> Type +;; implements curly brace substitution from the formalism, with the addition +;; that a substitution can include fixed args in addition to a different dotted arg +;; substitute-dotted : Listof[Type] Type Name Name Type -> Type (define (substitute-dotted pre-image image image-bound name target) (define (sb t) (substitute-dotted pre-image image image-bound name t)) + ;; We do a quick check on the free variables to see if we can short circuit the substitution (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 - (let ((extra-types (if (eq? name dbound) pre-image null))) + (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)))] @@ -156,7 +158,7 @@ image target)] [#:arr dom rng rest drest kws - (let ((extra-types (if (and drest (eq? name (cdr drest))) pre-image null))) + (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)) diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index a70995ef..774daabb 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/collects/typed-racket/types/subtype.rkt @@ -244,6 +244,7 @@ (parameterize ([current-seen A0]) (match* (s t) [(_ (Univ:)) A0] + [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0] ;; error is top and bot [(_ (Error:)) A0] [((Error:) _) A0] @@ -359,27 +360,31 @@ (=> unmatch) (unless (= (length ns) (length ms)) (unmatch)) + ;; substitute ns for ms in b2 to make it look like b1 (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)) (cond - ((< (length ns) (length ms)) + [(< (length ns) (length ms)) (define-values (short-ms rest-ms) (split-at ms (length ns))) + ;; substitute ms for ns in b1 to make it look like b2 (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 + (subtype* A0 (subst-all subst b1) b2)] + [else (define-values (short-ns rest-ns) (split-at ns (length ms))) + ;; substitute ns for ms in b2 to make it look like b1 (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))))] + (subtype* A0 b1 (subst-all subst b2))])] [((PolyDots: (list ns ... n-dotted) b1) (Poly: (list ms ...) b2)) (=> unmatch) (unless (<= (length ns) (length ms)) (unmatch)) + ;; substitute ms for ns in b1 to make it look like b2 (define subst (hash-set (make-simple-substitution ns (map make-F (take ms (length ns)))) n-dotted (i-subst (map make-F (drop ms (length ns)))))) @@ -389,10 +394,10 @@ ;; use unification to see if we can use the polytype here [((Poly: vs b) s) (=> unmatch) - (if (infer vs null (list b) (list s) (make-Univ)) A0 (unmatch))] + (if (infer vs null (list b) (list s) Univ) A0 (unmatch))] [((PolyDots: (list vs ... vdotted) b) s) (=> unmatch) - (if (infer vs (list vdotted) (list b) (list s) (make-Univ) ) + (if (infer vs (list vdotted) (list b) (list s) Univ) A0 (unmatch))] [(s (or (Poly: vs b) (PolyDots: vs b))) @@ -509,7 +514,6 @@ [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound)) (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)] - [((or (ValuesDots: _ _ _) (Values: _) (AnyValues:)) (AnyValues:)) A0] ;; trivial case for Result [((Result: t f o) (Result: t* f o)) (subtype* A0 t t*)]