diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 456ca52d..7c29118c 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -7,6 +7,7 @@ racket/match racket/list (contract-req) (except-in (types abbrev utils filter-ops) -> ->* one-of/c) + (only-in (infer infer) restrict) (rep type-rep object-rep filter-rep rep-utils)) (provide add-scope) @@ -45,8 +46,8 @@ ;; filters if they conflict with the argument type. (define/cond-contract (subst-tc-results res k o polarity t) (-> full-tc-results/c name-ref/c Object? boolean? Type? full-tc-results/c) - (define (st t) (subst-type t k o polarity)) - (define (sf f) (subst-filter f k o polarity)) + (define (st ty) (subst-type ty k o polarity t)) + (define (sf f) (subst-filter f k o polarity t)) (define (sfs fs) (subst-filter-set fs k o polarity t)) (define (so ob) (subst-object ob k o polarity)) (match res @@ -59,8 +60,8 @@ ;; Substitution of objects into a filter set ;; This is essentially ψ+|ψ- [o/x] from the paper -(define/cond-contract (subst-filter-set fs k o polarity [t Univ]) - (->* ((or/c FilterSet? NoFilter?) name-ref/c Object? boolean?) (Type/c) FilterSet?) +(define/cond-contract (subst-filter-set fs k o polarity t) + (-> (or/c FilterSet? NoFilter?) name-ref/c Object? boolean? Type/c FilterSet?) (define extra-filter (-filter t k)) (define (add-extra-filter f) (define f* (-and f extra-filter)) @@ -70,22 +71,22 @@ [else f])) (match fs [(FilterSet: f+ f-) - (-FS (subst-filter (add-extra-filter f+) k o polarity) - (subst-filter (add-extra-filter f-) k o polarity))] + (-FS (subst-filter (add-extra-filter f+) k o polarity t) + (subst-filter (add-extra-filter f-) k o polarity t))] [_ -top-filter])) ;; Substitution of objects into a type ;; This is essentially t [o/x] from the paper -(define/cond-contract (subst-type t k o polarity) - (-> Type/c name-ref/c Object? boolean? Type/c) - (define (st t) (subst-type t k o polarity)) - (define/cond-contract (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity)) +(define/cond-contract (subst-type t k o polarity ty) + (-> Type/c name-ref/c Object? boolean? Type/c Type/c) + (define (st t) (subst-type t k o polarity ty)) + (define/cond-contract (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity ty)) (type-case (#:Type st #:Filter sf #:Object (lambda (f) (subst-object f k o polarity))) t [#:arr dom rng rest drest kws - (let* ([st* (λ (t) (subst-type t (add-scope k) (add-scope/object o) polarity))]) + (let* ([st* (λ (t) (subst-type t (add-scope k) (add-scope/object o) polarity ty))]) (make-arr (map st dom) (st* rng) (and rest (st rest)) @@ -124,9 +125,9 @@ ;; Substitution of objects into a filter in a filter set ;; This is ψ+ [o/x] and ψ- [o/x] -(define/cond-contract (subst-filter f k o polarity) - (-> Filter/c name-ref/c Object? boolean? Filter/c) - (define (ap f) (subst-filter f k o polarity)) +(define/cond-contract (subst-filter f k o polarity ty) + (-> Filter/c name-ref/c Object? boolean? Type/c Filter/c) + (define (ap f) (subst-filter f k o polarity ty)) (define (tf-matcher t p i maker) (cond [(name-ref=? i k) @@ -135,14 +136,14 @@ (if polarity -top -bot)] [_ (maker - (subst-type t k o polarity) + (restrict ty (subst-type t k o polarity ty)) (-acc-path p o))])] [(index-free-in? k t) (if polarity -top -bot)] [else f])) (match f [(ImpFilter: ant consq) - (-imp (subst-filter ant k o (not polarity)) (ap consq))] + (-imp (subst-filter ant k o (not polarity) ty) (ap consq))] [(AndFilter: fs) (apply -and (map ap fs))] [(OrFilter: fs) (apply -or (map ap fs))] [(Bot:) -bot] diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt index dd2f696a..7d692f11 100644 --- a/typed-racket-test/unit-tests/metafunction-tests.rkt +++ b/typed-racket-test/unit-tests/metafunction-tests.rkt @@ -4,7 +4,7 @@ rackunit racket/format (typecheck tc-metafunctions tc-subst) (rep filter-rep type-rep object-rep) - (types abbrev union filter-ops tc-result) + (types abbrev union filter-ops tc-result numeric-tower) (for-syntax racket/base syntax/parse)) (provide tests) @@ -146,6 +146,11 @@ (list (make-Path null #'x)) (list Univ)) (ret null null null (-> Univ -Boolean : (-FS (-filter -String #'x) -top)) 'b)) + ;; Filter is restricted by type of object + (check-equal? + (values->tc-results (make-Values (list (-result -Boolean (-FS (-filter -PosReal '(0 0)) (-filter -NonPosReal '(0 0)))))) + (list (make-Path null #'x)) (list -Integer)) + (ret -Boolean (-FS (-filter -PosInt #'x) (-filter -NonPosInt #'x)))) ) (test-suite "replace-names" diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index e42019ef..b1759640 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -774,9 +774,9 @@ (if (equal? sym x) 3 x)) #:ret (ret -PosByte -true-filter)] - [tc-e (let: ([x : (Listof Symbol)'(a b c)]) - (cond [(memq 'a x) => car] - [else 'foo])) + [tc-e/t (let: ([x : (Listof Symbol)'(a b c)]) + (cond [(memq 'a x) => car] + [else 'foo])) -Symbol] [tc-e (list 2 3 4) (-lst* -PosByte -PosByte -PosByte)] @@ -1988,7 +1988,7 @@ (for/and: : Any ([i (in-range 4)]) (my-pred))) #:ret (ret Univ -top-filter -empty-obj)] - [tc-e + [tc-e/t (let () (define: long : (List 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 Integer) (list 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1))