From 2ee4c7a0869aee6f794c30f2317012c57e20a1fd Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 31 May 2014 12:03:19 -0700 Subject: [PATCH] Make TypeFilter and NotTypeFilter have a Path as a subcomponent. This changes Filters to have a Path as a subcomponent instead of having the list of Path-Elems and name-ref/c separately. This is part of the rework to have better object support. original commit: 3831cb135ea65d259edb291836b9a2c46a32411b --- .../typed-racket/base-env/base-env.rkt | 21 +++--- .../typed-racket/env/init-envs.rkt | 25 +++---- .../typed-racket/infer/infer-unit.rkt | 4 +- .../typed-racket/private/parse-type.rkt | 22 +++--- .../typed-racket/rep/filter-rep.rkt | 19 ++--- .../typecheck/tc-app/tc-app-eq.rkt | 12 +-- .../typed-racket/typecheck/tc-envops.rkt | 2 +- .../typecheck/tc-metafunctions.rkt | 3 +- .../typed-racket/typecheck/tc-subst.rkt | 49 +++++-------- .../typed-racket/types/abbrev.rkt | 19 ++--- .../typed-racket/types/base-abbrev.rkt | 53 ++++++++------ .../typed-racket/types/filter-ops.rkt | 73 +++++++++---------- .../typed-racket/types/printer.rkt | 10 +-- .../unit-tests/init-env-tests.rkt | 2 +- 14 files changed, 145 insertions(+), 169 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt index e1e81377..673c4bdb 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt @@ -513,8 +513,9 @@ [ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #f))))] [andmap (-polydots (a c d b) (cl->* - ;; 1 means predicate on second argument - (make-pred-ty (list (make-pred-ty (list a) c d) (-lst a)) c (-lst d) 1) + (make-pred-ty (list (make-pred-ty (list a) c d) (-lst a)) c (-lst d) + ;; predicate on second argument + (-arg-path 1)) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #t)))))] [reverse (-poly (a) (-> (-lst a) (-lst a)))] @@ -942,14 +943,14 @@ [identity (-poly (a) (->acc (list a) a null))] [const (-poly (a) (-> a (->* '() Univ a)))] [negate (-polydots (a b c d) - (cl->* (-> (-> c Univ : (-FS (-filter a 0 null) (-not-filter b 0 null))) - (-> c -Boolean : (-FS (-not-filter b 0 null) (-filter a 0 null)))) - (-> (-> c Univ : (-FS (-filter a 0 null) (-filter b 0 null))) - (-> c -Boolean : (-FS (-filter b 0 null) (-filter a 0 null)))) - (-> (-> c Univ : (-FS (-not-filter a 0 null) (-filter b 0 null))) - (-> c -Boolean : (-FS (-filter b 0 null) (-not-filter a 0 null)))) - (-> (-> c Univ : (-FS (-not-filter a 0 null) (-not-filter b 0 null))) - (-> c -Boolean : (-FS (-not-filter b 0 null) (-not-filter a 0 null)))) + (cl->* (-> (-> c Univ : (-FS (-filter a 0) (-not-filter b 0))) + (-> c -Boolean : (-FS (-not-filter b 0) (-filter a 0)))) + (-> (-> c Univ : (-FS (-filter a 0) (-filter b 0))) + (-> c -Boolean : (-FS (-filter b 0) (-filter a 0)))) + (-> (-> c Univ : (-FS (-not-filter a 0) (-filter b 0))) + (-> c -Boolean : (-FS (-filter b 0) (-not-filter a 0)))) + (-> (-> c Univ : (-FS (-not-filter a 0) (-not-filter b 0))) + (-> c -Boolean : (-FS (-not-filter b 0) (-not-filter a 0)))) (-> ((list) [d d] . ->... . Univ) ((list) [d d] . ->... . -Boolean))))] ;; probably the most useful cases diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt index 5e85f73f..1b86f18d 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -64,13 +64,15 @@ `(-lst ,(sub elem-ty))] [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f '()))) `(simple-> (list ,@(map sub dom)) ,(sub t))] - [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth n) - (NotTypeFilter: ft pth n)) + [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth) + (NotTypeFilter: ft pth)) (Empty:)))) #f #f '()))) - `(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub n) ,(sub pth))] - [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False) pth (list 0 0)) - (TypeFilter: (== -False) pth (list 0 0))) + `(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub pth))] + [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False) + (Path: pth (list 0 0))) + (TypeFilter: (== -False) + (Path: pth (list 0 0)))) (Path: pth (list 0 0))))) #f #f '()))) `(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))] @@ -122,15 +124,10 @@ (if cache-box name class-type)])] [(arr: dom rng rest drest kws) `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))] - [(TypeFilter: t p i) - `(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i) - `(quote-syntax ,i) - `(list ,(car i) ,(cadr i))))] - [(NotTypeFilter: t p i) - `(make-NotTypeFilter ,(sub t) ,(sub p) - ,(if (identifier? i) - `(quote-syntax ,i) - `(list ,(car i) ,(cadr i))))] + [(TypeFilter: t p) + `(make-TypeFilter ,(sub t) ,(sub p))] + [(NotTypeFilter: t p) + `(make-NotTypeFilter ,(sub t) ,(sub p))] [(Path: p i) `(make-Path ,(sub p) ,(if (identifier? i) `(quote-syntax ,i) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index 6be11f09..e28f69c7 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -188,8 +188,8 @@ [(e e) (empty-cset X Y)] [(e (Top:)) (empty-cset X Y)] ;; FIXME - is there something to be said about the logical ones? - [((TypeFilter: s p i) (TypeFilter: t p i)) (cgen/inv V X Y s t)] - [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cgen/inv V X Y s t)] + [((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv V X Y s t)] + [((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv V X Y s t)] [(_ _) #f])) ;; s and t must be *latent* filter sets diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index e9383e11..193970a2 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -3,7 +3,7 @@ ;; This module provides functions for parsing types written by the user (require "../utils/utils.rkt" - (except-in (rep type-rep object-rep filter-rep) make-arr) + (except-in (rep type-rep object-rep) make-arr) (rename-in (types abbrev union utils filter-ops resolve classes subtype) [make-arr* make-arr]) @@ -212,16 +212,15 @@ (define-splicing-syntax-class idx-obj #:description "index object" - #:attributes (arg depth pair) + #:attributes (arg depth path) (pattern (~seq idx:nat) #:attr arg (syntax-e #'idx) #:attr depth 0 - #:attr pair (list 0 (syntax-e #'idx))) + #:attr path (-arg-path (attribute arg) (attribute depth))) (pattern (~seq depth-idx:nat idx:nat) #:attr arg (syntax-e #'idx) #:attr depth (syntax-e #'depth-idx) - #:attr pair (list (syntax-e #'depth-idx) - (syntax-e #'idx)))) + #:attr path (-arg-path (attribute arg) (attribute depth)))) (define-syntax-class @ #:description "@" @@ -246,19 +245,21 @@ (pattern :Top^ #:attr prop -top) (pattern :Bot^ #:attr prop -bot) (pattern (t:expr :@ pe:path-elem ... i:id) - #:attr prop (-filter (parse-type #'t) #'i (attribute pe.pe))) + #:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (-id-path #'i)))) + ;; Here is wrong check (pattern (t:expr :@ ~! pe:path-elem ... i:idx-obj) #:fail-unless (< (attribute i.arg) (length doms)) (format "Filter proposition's object index ~a is larger than argument length ~a" (attribute i.arg) (length doms)) - #:attr prop (-filter (parse-type #'t) (attribute i.pair) (attribute pe.pe))) + #:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute i.path)))) (pattern (:! t:expr :@ pe:path-elem ... i:id) - #:attr prop (-not-filter (parse-type #'t) #'i (attribute pe.pe))) + #:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (-id-path #'i)))) + ;; Here is wrong check (pattern (:! t:expr :@ ~! pe:path-elem ... i:idx-obj) #:fail-unless (< (attribute i.arg) (length doms)) (format "Filter proposition's object index ~a is larger than argument length ~a" (attribute i.arg) (length doms)) - #:attr prop (-not-filter (parse-type #'t) (attribute i.pair) (attribute pe.pe))) + #:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute i.path)))) (pattern (:! t:expr) #:attr prop (-not-filter (parse-type #'t) 0)) (pattern (and (~var p (prop doms)) ...) @@ -411,7 +412,8 @@ [(~or (:->^ dom rng :colon^ latent:simple-latent-filter) (dom :->^ rng :colon^ latent:simple-latent-filter)) ;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty - (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) 0 (attribute latent.path))] + (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) + (-acc-path (attribute latent.path) (-arg-path 0)))] [(~or (:->^ dom ... rng :colon^ ~! (~var latent (full-latent (syntax->list #'(dom ...))))) (dom ... :->^ rng diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt index 368aaf25..f5edf2ae 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt @@ -5,7 +5,8 @@ racket/lazy-require) ;; TODO use something other than lazy-require. -(lazy-require ["type-rep.rkt" (Type/c Univ? Bottom?)]) +(lazy-require ["type-rep.rkt" (Type/c Univ? Bottom?)] + ["object-rep.rkt" (Path?)]) (provide Filter/c FilterSet/c name-ref/c hash-name filter-equal?) @@ -31,15 +32,15 @@ (def-filter Bot () [#:fold-rhs #:base]) (def-filter Top () [#:fold-rhs #:base]) -(def-filter TypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p (listof PathElem?)] [v name-ref/c]) - [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] - [#:frees (λ (f) (combine-frees (map f (cons t p))))] - [#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) +(def-filter TypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?]) + [#:intern (list (Rep-seq t) (Rep-seq p))] + [#:frees (λ (f) (combine-frees (map f (list t p))))] + [#:fold-rhs (*TypeFilter (type-rec-id t) (object-rec-id p))]) -(def-filter NotTypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p (listof PathElem?)] [v name-ref/c]) - [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] - [#:frees (λ (f) (combine-frees (map f (cons t p))))] - [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) +(def-filter NotTypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?]) + [#:intern (list (Rep-seq t) (Rep-seq p))] + [#:frees (λ (f) (combine-frees (map f (list t p))))] + [#:fold-rhs (*NotTypeFilter (type-rec-id t) (object-rec-id p))]) ;; implication (def-filter ImpFilter ([a Filter/c] [c Filter/c])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt index 5e02e339..af8e626c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt @@ -54,13 +54,9 @@ (alt equal? equal?-able))) (match* ((single-value v1) (single-value v2)) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) - (ret -Boolean - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] + (ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))] [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) - (ret -Boolean - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] + (ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))] [((tc-result1: t _ o) (or (and (? (lambda _ (id=? #'member comparator))) (tc-result1: (List: (list (and ts (Value: _)) ...)))) @@ -70,8 +66,8 @@ (tc-result1: (List: (list (and ts (Value: (? eq?-able))) ...)))))) (let ([ty (apply Un ts)]) (ret (Un (-val #f) t) - (-FS (-filter-at ty o) - (-not-filter-at ty o))))] + (-FS (-filter ty o) + (-not-filter ty o))))] [(_ _) (ret -Boolean)])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index afb1f099..08fa5c82 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -69,7 +69,7 @@ (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)]) (match f [(Bot:) (set-box! flag #f) (env-map (lambda (k v) (Un)) Γ)] - [(or (TypeFilter: ft lo x) (NotTypeFilter: ft lo x)) + [(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x))) (update-type/lexical (lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)]) (when (type-equal? new-t -Bottom) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt index b825c8fa..e4cd3c89 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt @@ -89,8 +89,7 @@ (if (OrFilter? new-or) (loop (cons new-or derived-formulas) derived-atoms (cdr worklist)) (loop derived-formulas derived-atoms (cons new-or (cdr worklist)))))] - [(TypeFilter: _ _ _) (loop derived-formulas (cons p derived-atoms) (cdr worklist))] - [(NotTypeFilter: _ _ _) (loop derived-formulas (cons p derived-atoms) (cdr worklist))] + [(or (? TypeFilter?) (? NotTypeFilter?)) (loop derived-formulas (cons p derived-atoms) (cdr worklist))] [(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))] [(Top:) (loop derived-formulas derived-atoms (cdr worklist))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 69736752..8eb94373 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -125,21 +125,19 @@ (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 (tf-matcher t p i k o polarity maker) - (match o - [(or (Empty:) (NoObject:)) - (cond [(name-ref=? i k) - (if polarity -top -bot)] - [(index-free-in? k t) (if polarity -top -bot)] - [else f])] - [(Path: p* i*) - (cond [(name-ref=? i k) - (maker - (subst-type t k o polarity) - i* - (append p p*))] - [(index-free-in? k t) (if polarity -top -bot)] - [else f])])) + (define (tf-matcher t p i maker) + (cond + [(name-ref=? i k) + (match o + [(Empty:) + (if polarity -top -bot)] + [_ + (maker + (subst-type t k o polarity) + (-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))] @@ -147,10 +145,10 @@ [(OrFilter: fs) (apply -or (map ap fs))] [(Bot:) -bot] [(Top:) -top] - [(TypeFilter: t p i) - (tf-matcher t p i k o polarity -filter)] - [(NotTypeFilter: t p i) - (tf-matcher t p i k o polarity -not-filter)])) + [(TypeFilter: t (Path: p i)) + (tf-matcher t p i -filter)] + [(NotTypeFilter: t (Path: p i)) + (tf-matcher t p i -not-filter)])) ;; Determine if the object k occurs free in the given type (define (index-free-in? k type) @@ -163,21 +161,8 @@ (if (name-ref=? i k) (return #t) o)])) - (define (for-filter o) - (filter-case (#:Type for-type - #:Filter for-filter) - o - [#:NotTypeFilter t p i - (if (name-ref=? i k) - (return #t) - o)] - [#:TypeFilter t p i - (if (name-ref=? i k) - (return #t) - o)])) (define (for-type t) (type-case (#:Type for-type - #:Filter for-filter #:Object for-object) t [#:arr dom rng rest drest kws diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt index 5762ea75..70e85e7c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -241,23 +241,14 @@ (define/cond-contract make-pred-ty (c:case-> (c:-> Type/c Type/c) (c:-> (c:listof Type/c) Type/c Type/c Type/c) - (c:-> (c:listof Type/c) Type/c Type/c - (c:or/c integer? name-ref/c) Type/c) - (c:-> (c:listof Type/c) Type/c Type/c - (c:or/c integer? name-ref/c) (c:listof PathElem?) Type/c)) + (c:-> (c:listof Type/c) Type/c Type/c Object? Type/c)) (case-lambda - [(in out t n p) - (make-Function - (list - (make-arr* - in out - #:filters (-FS (-filter t n p) (-not-filter t n p)))))] - [(in out t n) - (make-pred-ty in out t n null)] + [(in out t p) + (->* in out : (-FS (-filter t p) (-not-filter t p)))] [(in out t) - (make-pred-ty in out t 0 null)] + (make-pred-ty in out t (make-Path null (list 0 0)))] [(t) - (make-pred-ty (list Univ) -Boolean t 0 null)])) + (make-pred-ty (list Univ) -Boolean t (make-Path null (list 0 0)))])) (define/decl -true-filter (-FS -top -bot)) (define/decl -false-filter (-FS -bot -top)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt index 339ea368..bbd625d3 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt @@ -118,44 +118,55 @@ (define/decl -bot-filter (make-FilterSet -bot -bot)) (define/decl -no-obj (make-NoObject)) (define/decl -empty-obj (make-Empty)) +(define (-id-path id) + (make-Path null id)) +(define (-arg-path arg [depth 0]) + (make-Path null (list depth arg))) +(define (-acc-path path-elems o) + (match o + [(Empty:) -empty-obj] + [(Path: p o) (make-Path (append path-elems p) o)])) (define/cond-contract (-FS + -) (c:-> Filter/c Filter/c FilterSet?) (make-FilterSet + -)) ;; Abbreviation for filters -;; `i` can be an integer for backwards compatibility -(define/cond-contract (-filter t i [p null]) - (c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c) - (define i* (if (integer? i) (list 0 i) i)) +;; `i` can be an integer or name-ref/c for backwards compatibility +;; FIXME: Make all callers pass in an object and remove backwards compatibility +(define/cond-contract (-filter t i) + (c:-> Type/c (c:or/c integer? name-ref/c Object?) Filter/c) + (define o + (cond + [(Object? i) i] + [(integer? i) (make-Path null (list 0 i))] + [else (make-Path null i)])) (cond [(and (identifier? i) (is-var-mutated? i)) -top] + [(Empty? o) -top] [(equal? Univ t) -top] [(equal? -Bottom t) -bot] - [else (make-TypeFilter t p i*)])) + [else (make-TypeFilter t o)])) ;; Abbreviation for not filters -;; `i` can be an integer for backwards compatibility -(define/cond-contract (-not-filter t i [p null]) - (c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c) - (define i* (if (integer? i) (list 0 i) i)) +;; `i` can be an integer or name-ref/c for backwards compatibility +;; FIXME: Make all callers pass in an object and remove backwards compatibility +(define/cond-contract (-not-filter t i) + (c:-> Type/c (c:or/c integer? name-ref/c Object?) Filter/c) + (define o + (cond + [(Object? i) i] + [(integer? i) (make-Path null (list 0 i))] + [else (make-Path null i)])) (cond [(and (identifier? i) (is-var-mutated? i)) -top] + [(Empty? o) -top] [(equal? -Bottom t) -top] [(equal? Univ t) -bot] - [else (make-NotTypeFilter t p i*)])) + [else (make-NotTypeFilter t o)])) -(define (-filter-at t o) - (match o - [(Path: p i) (-filter t i p)] - [_ -top])) -(define (-not-filter-at t o) - (match o - [(Path: p i) (-not-filter t i p)] - [_ -top])) - ;; A Type that corresponds to the any contract for the ;; return type of functions (define (-AnyValues f) (make-AnyValues f)) @@ -221,8 +232,8 @@ (define (->acc dom rng path) (make-Function (list (make-arr* dom rng - #:filters (-FS (-not-filter (-val #f) (list 0 0) path) - (-filter (-val #f) (list 0 0) path)) + #:filters (-FS (-not-filter (-val #f) (make-Path path (list 0 0))) + (-filter (-val #f) (make-Path path (list 0 0)))) #:object (make-Path path (list 0 0)))))) (define (cl->* . args) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt index 9be9845e..4ec5b150 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt @@ -19,10 +19,10 @@ ;; Returns true if the AND of the two filters is equivalent to Bot (define (contradictory? f1 f2) (match* (f1 f2) - [((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2)) - (and (name-ref=? i1 i2) (subtype t1 t2))] - [((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1)) - (and (name-ref=? i1 i2) (subtype t1 t2))] + [((TypeFilter: t1 p) (NotTypeFilter: t2 p)) + (subtype t1 t2)] + [((NotTypeFilter: t2 p) (TypeFilter: t1 p)) + (subtype t1 t2)] [((Bot:) _) #t] [(_ (Bot:)) #t] [(_ _) #f])) @@ -31,10 +31,10 @@ ;; Returns true if the OR of the two filters is equivalent to Top (define (complementary? f1 f2) (match* (f1 f2) - [((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2)) - (and (name-ref=? i1 i2) (subtype t2 t1))] - [((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1)) - (and (name-ref=? i1 i2) (subtype t2 t1))] + [((TypeFilter: t1 p) (NotTypeFilter: t2 p)) + (subtype t2 t1)] + [((NotTypeFilter: t2 p) (TypeFilter: t1 p)) + (subtype t2 t1)] [((Top:) (Top:)) #t] [(_ _) #f])) @@ -54,18 +54,12 @@ (memf (lambda (f) (filter-equal? f f2)) fs)] [(f1 (AndFilter: fs)) (memf (lambda (f) (filter-equal? f f1)) fs)] - [((TypeFilter: t1 p1 i1) - (TypeFilter: t2 p1 i2)) - (and (name-ref=? i1 i2) - (subtype t2 t1))] - [((NotTypeFilter: t2 p1 i2) - (NotTypeFilter: t1 p1 i1)) - (and (name-ref=? i1 i2) - (subtype t2 t1))] - [((NotTypeFilter: t1 p1 i1) - (TypeFilter: t2 p1 i2)) - (and (name-ref=? i1 i2) - (not (overlap t1 t2)))] + [((TypeFilter: t1 p) (TypeFilter: t2 p)) + (subtype t2 t1)] + [((NotTypeFilter: t2 p) (NotTypeFilter: t1 p)) + (subtype t2 t1)] + [((NotTypeFilter: t1 p) (TypeFilter: t2 p)) + (not (overlap t1 t2))] [(_ _) #f])) (define (hash-name-ref i) @@ -86,33 +80,32 @@ (for/list ([v (in-dict-values tf-map)]) v) (for/list ([v (in-dict-values ntf-map)]) v)) (match (car props) - [(and p (TypeFilter: t1 f1 x) (? (lambda _ or?))) + [(and f (TypeFilter: t1 p) (? (lambda _ or?))) (hash-update! tf-map - (list f1 (hash-name-ref x)) - (match-lambda [(TypeFilter: t2 _ _) (-filter (Un t1 t2) x f1)] + p + (match-lambda [(TypeFilter: t2 _) (-filter (Un t1 t2) p)] [p (int-err "got something that isn't a typefilter ~a" p)]) - p) + f) (loop (cdr props) others)] - [(and p (TypeFilter: t1 f1 x) (? (lambda _ (not or?)))) - (match (hash-ref tf-map (list f1 (hash-name-ref x)) #f) - [(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _ _) + [(and f (TypeFilter: t1 p) (? (lambda _ (not or?)))) + (match (hash-ref tf-map p #f) + [(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _) ;; we're in an And, and we got two types for the same path that do not overlap (list -bot)] - [(TypeFilter: t2 _ _) - (hash-set! tf-map (list f1 (hash-name-ref x)) - (-filter (restrict t1 t2) x f1)) + [(TypeFilter: t2 _) + (hash-set! tf-map p + (-filter (restrict t1 t2) p)) (loop (cdr props) others)] [#f - (hash-set! tf-map (list f1 (hash-name-ref x)) - (-filter t1 x f1)) + (hash-set! tf-map p + (-filter t1 p)) (loop (cdr props) others)])] - [(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?)))) - (hash-update! ntf-map - (list f1 (hash-name-ref x)) - (match-lambda [(NotTypeFilter: t2 _ _) - (-not-filter (Un t1 t2) x f1)] + [(and f (NotTypeFilter: t1 p) (? (lambda _ (not or?)))) + (hash-update! ntf-map p + (match-lambda [(NotTypeFilter: t2 _) + (-not-filter (Un t1 t2) p)] [p (int-err "got something that isn't a nottypefilter ~a" p)]) - p) + f) (loop (cdr props) others)] [p (loop (cdr props) (cons p others))])))) @@ -122,8 +115,8 @@ (match p [(Bot:) -top] [(Top:) -bot] - [(TypeFilter: t p o) (-not-filter t o p)] - [(NotTypeFilter: t p o) (-filter t o p)] + [(TypeFilter: t p) (-not-filter t p)] + [(NotTypeFilter: t p) (-filter t p)] [(AndFilter: fs) (apply -or (map invert-filter fs))] [(OrFilter: fs) (apply -and (map invert-filter fs))] [(ImpFilter: f1 f2) (-and f1 (invert-filter f2))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt index e441700e..7f193e33 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt @@ -115,9 +115,9 @@ (match filt [(FilterSet: thn els) `(,(filter->sexp thn) \| ,(filter->sexp els))] [(NoFilter:) '-] - [(NotTypeFilter: type path nm) + [(NotTypeFilter: type (Path: path nm)) `(! ,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))] - [(TypeFilter: type path nm) + [(TypeFilter: type (Path: path nm)) `(,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))] [(Bot:) 'Bot] [(Top:) 'Top] @@ -240,8 +240,8 @@ [(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) (list (type->sexp t))] [(Values: (list (Result: t - (FilterSet: (TypeFilter: ft pth (list 0 0)) - (NotTypeFilter: ft pth (list 0 0))) + (FilterSet: (TypeFilter: ft (Path: pth (list 0 0))) + (NotTypeFilter: ft (Path: pth (list 0 0)))) (Empty:)))) ;; Only print a simple filter for single argument functions, ;; since parse-type only accepts simple latent filters on single @@ -255,7 +255,7 @@ ;; special case (even when complex printing is off) because it's ;; useful to users who use functions like `filter`. [(Values: (list (Result: t - (FilterSet: (TypeFilter: ft '() (list 0 0)) (Top:)) + (FilterSet: (TypeFilter: ft (Path: '() (list 0 0))) (Top:)) (Empty:)))) #:when (= 1 (length dom)) `(,(type->sexp t) : #:+ ,(type->sexp ft))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/init-env-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/init-env-tests.rkt index 3d96f246..c44f4258 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/init-env-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/init-env-tests.rkt @@ -26,7 +26,7 @@ '(simple-> (list -String) -Symbol)) (check-equal? (convert (make-pred-ty -String)) - '(make-pred-ty (list Univ) -Boolean -String `(0 0) `())) + '(make-pred-ty (list Univ) -Boolean -String (make-Path `() (list 0 0)))) (check-equal? (convert (->acc (list (-lst -String)) -String (list -car))) '(->acc (list (-lst -String)) -String `(,-car)))