From be225976d32c0d7e7e1b9cda95462ad12dec8161 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Wed, 1 Apr 2015 23:02:14 -0700 Subject: [PATCH] Make subtype work with restricted filters. Closes PR 15025. --- .../typed-racket/typecheck/tc-subst.rkt | 5 +++++ typed-racket-lib/typed-racket/types/subtype.rkt | 13 +++++++------ typed-racket-test/unit-tests/subtype-tests.rkt | 5 +++++ 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 5baec779..fbcc1d39 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -14,6 +14,7 @@ (provide add-scope) (provide/cond-contract + [restrict-values (-> SomeValues/c (listof Type/c) SomeValues/c)] [values->tc-results (->* (SomeValues/c (listof Object?)) ((listof Type/c)) full-tc-results/c)] [replace-names (-> (listof (list/c identifier? Object?)) tc-results/c tc-results/c)]) @@ -32,6 +33,10 @@ [t (in-list ts)]) (subst-tc-results res (list 0 arg) o #t t))) +;; Restrict the objects in v refering to the current functions arguments to be of the types ts. +(define (restrict-values v ts) + (for/fold ([v v]) ([t (in-list ts)] [arg (in-naturals)]) + (subst-type v (list 0 arg) (-arg-path arg) #t t))) ;; replace-names: (listof (list/c identifier? Object?) tc-results? -> tc-results? ;; For each name replaces all uses of it in res with the corresponding object. diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index ae951f21..cbf9dffd 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -10,7 +10,8 @@ (lazy-require ("union.rkt" (Un)) - ("../infer/infer.rkt" (infer))) + ("../infer/infer.rkt" (infer)) + ("../typecheck/tc-subst.rkt" (restrict-values))) (define subtype-cache (make-hash)) @@ -103,19 +104,19 @@ (arr: t1 t2 #f #f '())) (subtype-seq A0 (subtypes* t1 s1) - (subtype* s2 t2))] + (subtype* (restrict-values s2 t1) t2))] [((arr: s1 s2 #f #f s-kws) (arr: t1 t2 #f #f t-kws)) (subtype-seq A0 (subtypes* t1 s1) (kw-subtypes* s-kws t-kws) - (subtype* s2 t2))] + (subtype* (restrict-values s2 t1) t2))] [((arr: s-dom s-rng s-rest #f s-kws) (arr: t-dom t-rng #f #f t-kws)) (subtype-seq A0 (subtypes*/varargs t-dom s-dom s-rest) (kw-subtypes* s-kws t-kws) - (subtype* s-rng t-rng))] + (subtype* (restrict-values s-rng t-dom) t-rng))] [((arr: s-dom s-rng #f #f s-kws) (arr: t-dom t-rng t-rest #f t-kws)) #f] @@ -125,7 +126,7 @@ (subtypes*/varargs t-dom s-dom s-rest) (subtype* t-rest s-rest) (kw-subtypes* s-kws t-kws) - (subtype* s-rng t-rng))] + (subtype* (restrict-values s-rng t-dom) t-rng))] ;; handle ... varargs when the bounds are the same [((arr: s-dom s-rng #f (cons s-drest dbound) s-kws) (arr: t-dom t-rng #f (cons t-drest dbound) t-kws)) @@ -133,7 +134,7 @@ (subtype* t-drest s-drest) (subtypes* t-dom s-dom) (kw-subtypes* s-kws t-kws) - (subtype* s-rng t-rng))] + (subtype* (restrict-values s-rng t-dom) t-rng))] [(_ _) #f])) ;; check subtyping of filters, so that predicates subtype correctly diff --git a/typed-racket-test/unit-tests/subtype-tests.rkt b/typed-racket-test/unit-tests/subtype-tests.rkt index 3f62de35..1e49d7f1 100644 --- a/typed-racket-test/unit-tests/subtype-tests.rkt +++ b/typed-racket-test/unit-tests/subtype-tests.rkt @@ -370,4 +370,9 @@ (-prefab '(foo #(0)) -String)] [FAIL (-prefab '(foo #()) -String) (-prefab '(foo #(0)) (-opt -String))] + + ;; Filter subtyping + ((make-pred-ty (list -Real) -Boolean (Un (-val 0.0) (-val 0))) + (make-pred-ty (list -Int) -Boolean (-val 0))) + ))