suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make TypeFilter and NotTypeFilter have a Path as a subcomponent.

Browse Source 
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.
This commit is contained in:
Eric Dobson 2014-05-31 12:03:19 -07:00
parent aab724de35
commit 3831cb135e
14 changed files with 145 additions and 169 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
View File

@ -513,8 +513,9 @@
[ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #f))))] [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->* [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)
(make-pred-ty (list (make-pred-ty (list a) c d) (-lst a)) c (-lst d) 1) ;; predicate on second argument
(-arg-path 1))
(->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #t)))))] (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #t)))))]
[reverse (-poly (a) (-> (-lst a) (-lst a)))] [reverse (-poly (a) (-> (-lst a) (-lst a)))]
@ -942,14 +943,14 @@
[identity (-poly (a) (->acc (list a) a null))] [identity (-poly (a) (->acc (list a) a null))]
[const (-poly (a) (-> a (->* '() Univ a)))] [const (-poly (a) (-> a (->* '() Univ a)))]
[negate (-polydots (a b c d) [negate (-polydots (a b c d)
(cl->* (-> (-> c Univ : (-FS (-filter a 0 null) (-not-filter b 0 null))) (cl->* (-> (-> c Univ : (-FS (-filter a 0) (-not-filter b 0)))
(-> c -Boolean : (-FS (-not-filter b 0 null) (-filter a 0 null)))) (-> c -Boolean : (-FS (-not-filter b 0) (-filter a 0))))
(-> (-> c Univ : (-FS (-filter a 0 null) (-filter b 0 null))) (-> (-> c Univ : (-FS (-filter a 0) (-filter b 0)))
(-> c -Boolean : (-FS (-filter b 0 null) (-filter a 0 null)))) (-> c -Boolean : (-FS (-filter b 0) (-filter a 0))))
(-> (-> c Univ : (-FS (-not-filter a 0 null) (-filter b 0 null))) (-> (-> c Univ : (-FS (-not-filter a 0) (-filter b 0)))
(-> c -Boolean : (-FS (-filter b 0 null) (-not-filter a 0 null)))) (-> c -Boolean : (-FS (-filter b 0) (-not-filter a 0))))
(-> (-> c Univ : (-FS (-not-filter a 0 null) (-not-filter b 0 null))) (-> (-> c Univ : (-FS (-not-filter a 0) (-not-filter b 0)))
(-> c -Boolean : (-FS (-not-filter b 0 null) (-not-filter a 0 null)))) (-> c -Boolean : (-FS (-not-filter b 0) (-not-filter a 0))))
(-> ((list) [d d] . ->... . Univ) (-> ((list) [d d] . ->... . Univ)
((list) [d d] . ->... . -Boolean))))] ((list) [d d] . ->... . -Boolean))))]
;; probably the most useful cases ;; probably the most useful cases

25
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt vendored
View File

@ -64,13 +64,15 @@
`(-lst ,(sub elem-ty))] `(-lst ,(sub elem-ty))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f '()))) [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f '())))
`(simple-> (list ,@(map sub dom)) ,(sub t))] `(simple-> (list ,@(map sub dom)) ,(sub t))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth n) [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (TypeFilter: ft pth)
(NotTypeFilter: ft pth n)) (NotTypeFilter: ft pth))
(Empty:)))) (Empty:))))
#f #f '()))) #f #f '())))
`(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub n) ,(sub pth))] `(make-pred-ty (list ,@(map sub dom)) ,(sub t) ,(sub ft) ,(sub pth))]
[(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False) pth (list 0 0)) [(Function: (list (arr: dom (Values: (list (Result: t (FilterSet: (NotTypeFilter: (== -False)
(TypeFilter: (== -False) pth (list 0 0))) (Path: pth (list 0 0)))
(TypeFilter: (== -False)
(Path: pth (list 0 0))))
(Path: pth (list 0 0))))) (Path: pth (list 0 0)))))
#f #f '()))) #f #f '())))
`(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))] `(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))]
@ -122,15 +124,10 @@
(if cache-box name class-type)])] (if cache-box name class-type)])]
[(arr: dom rng rest drest kws) [(arr: dom rng rest drest kws)
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))] `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
[(TypeFilter: t p i) [(TypeFilter: t p)
`(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i) `(make-TypeFilter ,(sub t) ,(sub p))]
`(quote-syntax ,i) [(NotTypeFilter: t p)
`(list ,(car i) ,(cadr i))))] `(make-NotTypeFilter ,(sub t) ,(sub p))]
[(NotTypeFilter: t p i)
`(make-NotTypeFilter ,(sub t) ,(sub p)
,(if (identifier? i)
`(quote-syntax ,i)
`(list ,(car i) ,(cadr i))))]
[(Path: p i) [(Path: p i)
`(make-Path ,(sub p) ,(if (identifier? i) `(make-Path ,(sub p) ,(if (identifier? i)
`(quote-syntax ,i) `(quote-syntax ,i)

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -188,8 +188,8 @@
[(e e) (empty-cset X Y)] [(e e) (empty-cset X Y)]
[(e (Top:)) (empty-cset X Y)] [(e (Top:)) (empty-cset X Y)]
;; FIXME - is there something to be said about the logical ones? ;; 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)] [((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv V X Y s t)]
[((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cgen/inv V X Y s t)] [((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv V X Y s t)]
[(_ _) #f])) [(_ _) #f]))
;; s and t must be *latent* filter sets ;; s and t must be *latent* filter sets

22
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -3,7 +3,7 @@
;; This module provides functions for parsing types written by the user ;; This module provides functions for parsing types written by the user
(require "../utils/utils.rkt" (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 (rename-in (types abbrev union utils filter-ops resolve
classes subtype) classes subtype)
[make-arr* make-arr]) [make-arr* make-arr])
@ -212,16 +212,15 @@
(define-splicing-syntax-class idx-obj (define-splicing-syntax-class idx-obj
#:description "index object" #:description "index object"
#:attributes (arg depth pair) #:attributes (arg depth path)
(pattern (~seq idx:nat) (pattern (~seq idx:nat)
#:attr arg (syntax-e #'idx) #:attr arg (syntax-e #'idx)
#:attr depth 0 #: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) (pattern (~seq depth-idx:nat idx:nat)
#:attr arg (syntax-e #'idx) #:attr arg (syntax-e #'idx)
#:attr depth (syntax-e #'depth-idx) #:attr depth (syntax-e #'depth-idx)
#:attr pair (list (syntax-e #'depth-idx) #:attr path (-arg-path (attribute arg) (attribute depth))))
(syntax-e #'idx))))
(define-syntax-class @ (define-syntax-class @
#:description "@" #:description "@"
@ -246,19 +245,21 @@
(pattern :Top^ #:attr prop -top) (pattern :Top^ #:attr prop -top)
(pattern :Bot^ #:attr prop -bot) (pattern :Bot^ #:attr prop -bot)
(pattern (t:expr :@ pe:path-elem ... i:id) (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) (pattern (t:expr :@ ~! pe:path-elem ... i:idx-obj)
#:fail-unless (< (attribute i.arg) (length doms)) #:fail-unless (< (attribute i.arg) (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a" (format "Filter proposition's object index ~a is larger than argument length ~a"
(attribute i.arg) (length doms)) (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) (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) (pattern (:! t:expr :@ ~! pe:path-elem ... i:idx-obj)
#:fail-unless (< (attribute i.arg) (length doms)) #:fail-unless (< (attribute i.arg) (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a" (format "Filter proposition's object index ~a is larger than argument length ~a"
(attribute i.arg) (length doms)) (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) (pattern (:! t:expr)
#:attr prop (-not-filter (parse-type #'t) 0)) #:attr prop (-not-filter (parse-type #'t) 0))
(pattern (and (~var p (prop doms)) ...) (pattern (and (~var p (prop doms)) ...)
@ -411,7 +412,8 @@
[(~or (:->^ dom rng :colon^ latent:simple-latent-filter) [(~or (:->^ dom rng :colon^ latent:simple-latent-filter)
(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 ;; 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 [(~or (:->^ dom ... rng
:colon^ ~! (~var latent (full-latent (syntax->list #'(dom ...))))) :colon^ ~! (~var latent (full-latent (syntax->list #'(dom ...)))))
(dom ... :->^ rng (dom ... :->^ rng

19
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/filter-rep.rkt
View File

@ -5,7 +5,8 @@
racket/lazy-require) racket/lazy-require)
;; TODO use something other than 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?) (provide Filter/c FilterSet/c name-ref/c hash-name filter-equal?)
@ -31,15 +32,15 @@
(def-filter Bot () [#:fold-rhs #:base]) (def-filter Bot () [#:fold-rhs #:base])
(def-filter Top () [#: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]) (def-filter TypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] [#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))] [#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#: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]) (def-filter NotTypeFilter ([t (and/c Type/c (not/c Univ?) (not/c Bottom?))] [p Path?])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] [#:intern (list (Rep-seq t) (Rep-seq p))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))] [#:frees (λ (f) (combine-frees (map f (list t p))))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*NotTypeFilter (type-rec-id t) (object-rec-id p))])
;; implication ;; implication
(def-filter ImpFilter ([a Filter/c] [c Filter/c])) (def-filter ImpFilter ([a Filter/c] [c Filter/c]))

12
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
View File

@ -54,13 +54,9 @@
(alt equal? equal?-able))) (alt equal? equal?-able)))
(match* ((single-value v1) (single-value v2)) (match* ((single-value v1) (single-value v2))
[((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val))))
(ret -Boolean (ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))]
(-FS (-filter-at (-val val) o)
(-not-filter-at (-val val) o)))]
[((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o))
(ret -Boolean (ret -Boolean (-FS (-filter (-val val) o) (-not-filter (-val val) o)))]
(-FS (-filter-at (-val val) o)
(-not-filter-at (-val val) o)))]
[((tc-result1: t _ o) [((tc-result1: t _ o)
(or (and (? (lambda _ (id=? #'member comparator))) (or (and (? (lambda _ (id=? #'member comparator)))
(tc-result1: (List: (list (and ts (Value: _)) ...)))) (tc-result1: (List: (list (and ts (Value: _)) ...))))
@ -70,8 +66,8 @@
(tc-result1: (List: (list (and ts (Value: (? eq?-able))) ...)))))) (tc-result1: (List: (list (and ts (Value: (? eq?-able))) ...))))))
(let ([ty (apply Un ts)]) (let ([ty (apply Un ts)])
(ret (Un (-val #f) t) (ret (Un (-val #f) t)
(-FS (-filter-at ty o) (-FS (-filter ty o)
(-not-filter-at ty o))))] (-not-filter ty o))))]
[(_ _) (ret -Boolean)])) [(_ _) (ret -Boolean)]))

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
View File

@ -69,7 +69,7 @@
(for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)]) (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
(match f (match f
[(Bot:) (set-box! flag #f) (env-map (lambda (k v) (Un)) Γ)] [(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 (update-type/lexical
(lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)]) (lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)])
(when (type-equal? new-t -Bottom) (when (type-equal? new-t -Bottom)

3
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
View File

@ -89,8 +89,7 @@
(if (OrFilter? new-or) (if (OrFilter? new-or)
(loop (cons new-or derived-formulas) derived-atoms (cdr worklist)) (loop (cons new-or derived-formulas) derived-atoms (cdr worklist))
(loop derived-formulas derived-atoms (cons new-or (cdr worklist)))))] (loop derived-formulas derived-atoms (cons new-or (cdr worklist)))))]
[(TypeFilter: _ _ _) (loop derived-formulas (cons p derived-atoms) (cdr worklist))] [(or (? TypeFilter?) (? NotTypeFilter?)) (loop derived-formulas (cons p derived-atoms) (cdr worklist))]
[(NotTypeFilter: _ _ _) (loop derived-formulas (cons p derived-atoms) (cdr worklist))]
[(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))] [(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
[(Top:) (loop derived-formulas derived-atoms (cdr worklist))] [(Top:) (loop derived-formulas derived-atoms (cdr worklist))]

49
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
View File

@ -125,21 +125,19 @@
(define/cond-contract (subst-filter f k o polarity) (define/cond-contract (subst-filter f k o polarity)
(-> Filter/c name-ref/c Object? boolean? Filter/c) (-> Filter/c name-ref/c Object? boolean? Filter/c)
(define (ap f) (subst-filter f k o polarity)) (define (ap f) (subst-filter f k o polarity))
(define (tf-matcher t p i k o polarity maker) (define (tf-matcher t p i maker)
(match o (cond
[(or (Empty:) (NoObject:)) [(name-ref=? i k)
(cond [(name-ref=? i k) (match o
(if polarity -top -bot)] [(Empty:)
[(index-free-in? k t) (if polarity -top -bot)] (if polarity -top -bot)]
[else f])] [_
[(Path: p* i*) (maker
(cond [(name-ref=? i k) (subst-type t k o polarity)
(maker (-acc-path p o))])]
(subst-type t k o polarity) [(index-free-in? k t) (if polarity -top -bot)]
i* [else f]))
(append p p*))]
[(index-free-in? k t) (if polarity -top -bot)]
[else f])]))
(match f (match f
[(ImpFilter: ant consq) [(ImpFilter: ant consq)
(-imp (subst-filter ant k o (not polarity)) (ap consq))] (-imp (subst-filter ant k o (not polarity)) (ap consq))]
@ -147,10 +145,10 @@
[(OrFilter: fs) (apply -or (map ap fs))] [(OrFilter: fs) (apply -or (map ap fs))]
[(Bot:) -bot] [(Bot:) -bot]
[(Top:) -top] [(Top:) -top]
[(TypeFilter: t p i) [(TypeFilter: t (Path: p i))
(tf-matcher t p i k o polarity -filter)] (tf-matcher t p i -filter)]
[(NotTypeFilter: t p i) [(NotTypeFilter: t (Path: p i))
(tf-matcher t p i k o polarity -not-filter)])) (tf-matcher t p i -not-filter)]))
;; Determine if the object k occurs free in the given type ;; Determine if the object k occurs free in the given type
(define (index-free-in? k type) (define (index-free-in? k type)
@ -163,21 +161,8 @@
(if (name-ref=? i k) (if (name-ref=? i k)
(return #t) (return #t)
o)])) 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) (define (for-type t)
(type-case (#:Type for-type (type-case (#:Type for-type
#:Filter for-filter
#:Object for-object) #:Object for-object)
t t
[#:arr dom rng rest drest kws [#:arr dom rng rest drest kws

19
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
View File

@ -241,23 +241,14 @@
(define/cond-contract make-pred-ty (define/cond-contract make-pred-ty
(c:case-> (c:-> Type/c Type/c) (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 Type/c)
(c:-> (c:listof Type/c) Type/c Type/c (c:-> (c:listof Type/c) Type/c Type/c Object? 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))
(case-lambda (case-lambda
[(in out t n p) [(in out t p)
(make-Function (->* in out : (-FS (-filter t p) (-not-filter t p)))]
(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) [(in out t)
(make-pred-ty in out t 0 null)] (make-pred-ty in out t (make-Path null (list 0 0)))]
[(t) [(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 -true-filter (-FS -top -bot))
(define/decl -false-filter (-FS -bot -top)) (define/decl -false-filter (-FS -bot -top))

53
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt
View File

@ -118,44 +118,55 @@
(define/decl -bot-filter (make-FilterSet -bot -bot)) (define/decl -bot-filter (make-FilterSet -bot -bot))
(define/decl -no-obj (make-NoObject)) (define/decl -no-obj (make-NoObject))
(define/decl -empty-obj (make-Empty)) (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 + -) (define/cond-contract (-FS + -)
(c:-> Filter/c Filter/c FilterSet?) (c:-> Filter/c Filter/c FilterSet?)
(make-FilterSet + -)) (make-FilterSet + -))
;; Abbreviation for filters ;; Abbreviation for filters
;; `i` can be an integer for backwards compatibility ;; `i` can be an integer or name-ref/c for backwards compatibility
(define/cond-contract (-filter t i [p null]) ;; FIXME: Make all callers pass in an object and remove backwards compatibility
(c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c) (define/cond-contract (-filter t i)
(define i* (if (integer? i) (list 0 i) 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 (cond
[(and (identifier? i) (is-var-mutated? i)) -top] [(and (identifier? i) (is-var-mutated? i)) -top]
[(Empty? o) -top]
[(equal? Univ t) -top] [(equal? Univ t) -top]
[(equal? -Bottom t) -bot] [(equal? -Bottom t) -bot]
[else (make-TypeFilter t p i*)])) [else (make-TypeFilter t o)]))
;; Abbreviation for not filters ;; Abbreviation for not filters
;; `i` can be an integer for backwards compatibility ;; `i` can be an integer or name-ref/c for backwards compatibility
(define/cond-contract (-not-filter t i [p null]) ;; FIXME: Make all callers pass in an object and remove backwards compatibility
(c:->* (Type/c (c:or/c integer? name-ref/c)) ((c:listof PathElem?)) Filter/c) (define/cond-contract (-not-filter t i)
(define i* (if (integer? i) (list 0 i) 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 (cond
[(and (identifier? i) (is-var-mutated? i)) -top] [(and (identifier? i) (is-var-mutated? i)) -top]
[(Empty? o) -top]
[(equal? -Bottom t) -top] [(equal? -Bottom t) -top]
[(equal? Univ t) -bot] [(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 ;; A Type that corresponds to the any contract for the
;; return type of functions ;; return type of functions
(define (-AnyValues f) (make-AnyValues f)) (define (-AnyValues f) (make-AnyValues f))
@ -221,8 +232,8 @@
(define (->acc dom rng path) (define (->acc dom rng path)
(make-Function (list (make-arr* dom rng (make-Function (list (make-arr* dom rng
#:filters (-FS (-not-filter (-val #f) (list 0 0) path) #:filters (-FS (-not-filter (-val #f) (make-Path path (list 0 0)))
(-filter (-val #f) (list 0 0) path)) (-filter (-val #f) (make-Path path (list 0 0))))
#:object (make-Path path (list 0 0)))))) #:object (make-Path path (list 0 0))))))
(define (cl->* . args) (define (cl->* . args)

73
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
View File

@ -19,10 +19,10 @@
;; Returns true if the AND of the two filters is equivalent to Bot ;; Returns true if the AND of the two filters is equivalent to Bot
(define (contradictory? f1 f2) (define (contradictory? f1 f2)
(match* (f1 f2) (match* (f1 f2)
[((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2)) [((TypeFilter: t1 p) (NotTypeFilter: t2 p))
(and (name-ref=? i1 i2) (subtype t1 t2))] (subtype t1 t2)]
[((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1)) [((NotTypeFilter: t2 p) (TypeFilter: t1 p))
(and (name-ref=? i1 i2) (subtype t1 t2))] (subtype t1 t2)]
[((Bot:) _) #t] [((Bot:) _) #t]
[(_ (Bot:)) #t] [(_ (Bot:)) #t]
[(_ _) #f])) [(_ _) #f]))
@ -31,10 +31,10 @@
;; Returns true if the OR of the two filters is equivalent to Top ;; Returns true if the OR of the two filters is equivalent to Top
(define (complementary? f1 f2) (define (complementary? f1 f2)
(match* (f1 f2) (match* (f1 f2)
[((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2)) [((TypeFilter: t1 p) (NotTypeFilter: t2 p))
(and (name-ref=? i1 i2) (subtype t2 t1))] (subtype t2 t1)]
[((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1)) [((NotTypeFilter: t2 p) (TypeFilter: t1 p))
(and (name-ref=? i1 i2) (subtype t2 t1))] (subtype t2 t1)]
[((Top:) (Top:)) #t] [((Top:) (Top:)) #t]
[(_ _) #f])) [(_ _) #f]))
@ -54,18 +54,12 @@
(memf (lambda (f) (filter-equal? f f2)) fs)] (memf (lambda (f) (filter-equal? f f2)) fs)]
[(f1 (AndFilter: fs)) [(f1 (AndFilter: fs))
(memf (lambda (f) (filter-equal? f f1)) fs)] (memf (lambda (f) (filter-equal? f f1)) fs)]
[((TypeFilter: t1 p1 i1) [((TypeFilter: t1 p) (TypeFilter: t2 p))
(TypeFilter: t2 p1 i2)) (subtype t2 t1)]
(and (name-ref=? i1 i2) [((NotTypeFilter: t2 p) (NotTypeFilter: t1 p))
(subtype t2 t1))] (subtype t2 t1)]
[((NotTypeFilter: t2 p1 i2) [((NotTypeFilter: t1 p) (TypeFilter: t2 p))
(NotTypeFilter: t1 p1 i1)) (not (overlap t1 t2))]
(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)))]
[(_ _) #f])) [(_ _) #f]))
(define (hash-name-ref i) (define (hash-name-ref i)
@ -86,33 +80,32 @@
(for/list ([v (in-dict-values tf-map)]) v) (for/list ([v (in-dict-values tf-map)]) v)
(for/list ([v (in-dict-values ntf-map)]) v)) (for/list ([v (in-dict-values ntf-map)]) v))
(match (car props) (match (car props)
[(and p (TypeFilter: t1 f1 x) (? (lambda _ or?))) [(and f (TypeFilter: t1 p) (? (lambda _ or?)))
(hash-update! tf-map (hash-update! tf-map
(list f1 (hash-name-ref x)) p
(match-lambda [(TypeFilter: t2 _ _) (-filter (Un t1 t2) x f1)] (match-lambda [(TypeFilter: t2 _) (-filter (Un t1 t2) p)]
[p (int-err "got something that isn't a typefilter ~a" p)]) [p (int-err "got something that isn't a typefilter ~a" p)])
p) f)
(loop (cdr props) others)] (loop (cdr props) others)]
[(and p (TypeFilter: t1 f1 x) (? (lambda _ (not or?)))) [(and f (TypeFilter: t1 p) (? (lambda _ (not or?))))
(match (hash-ref tf-map (list f1 (hash-name-ref x)) #f) (match (hash-ref tf-map p #f)
[(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _ _) [(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 ;; we're in an And, and we got two types for the same path that do not overlap
(list -bot)] (list -bot)]
[(TypeFilter: t2 _ _) [(TypeFilter: t2 _)
(hash-set! tf-map (list f1 (hash-name-ref x)) (hash-set! tf-map p
(-filter (restrict t1 t2) x f1)) (-filter (restrict t1 t2) p))
(loop (cdr props) others)] (loop (cdr props) others)]
[#f [#f
(hash-set! tf-map (list f1 (hash-name-ref x)) (hash-set! tf-map p
(-filter t1 x f1)) (-filter t1 p))
(loop (cdr props) others)])] (loop (cdr props) others)])]
[(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?)))) [(and f (NotTypeFilter: t1 p) (? (lambda _ (not or?))))
(hash-update! ntf-map (hash-update! ntf-map p
(list f1 (hash-name-ref x)) (match-lambda [(NotTypeFilter: t2 _)
(match-lambda [(NotTypeFilter: t2 _ _) (-not-filter (Un t1 t2) p)]
(-not-filter (Un t1 t2) x f1)]
[p (int-err "got something that isn't a nottypefilter ~a" p)]) [p (int-err "got something that isn't a nottypefilter ~a" p)])
p) f)
(loop (cdr props) others)] (loop (cdr props) others)]
[p (loop (cdr props) (cons p others))])))) [p (loop (cdr props) (cons p others))]))))
@ -122,8 +115,8 @@
(match p (match p
[(Bot:) -top] [(Bot:) -top]
[(Top:) -bot] [(Top:) -bot]
[(TypeFilter: t p o) (-not-filter t o p)] [(TypeFilter: t p) (-not-filter t p)]
[(NotTypeFilter: t p o) (-filter t o p)] [(NotTypeFilter: t p) (-filter t p)]
[(AndFilter: fs) (apply -or (map invert-filter fs))] [(AndFilter: fs) (apply -or (map invert-filter fs))]
[(OrFilter: fs) (apply -and (map invert-filter fs))] [(OrFilter: fs) (apply -and (map invert-filter fs))]
[(ImpFilter: f1 f2) (-and f1 (invert-filter f2))])) [(ImpFilter: f1 f2) (-and f1 (invert-filter f2))]))

10
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
View File

@ -115,9 +115,9 @@
(match filt (match filt
[(FilterSet: thn els) `(,(filter->sexp thn) \| ,(filter->sexp els))] [(FilterSet: thn els) `(,(filter->sexp thn) \| ,(filter->sexp els))]
[(NoFilter:) '-] [(NoFilter:) '-]
[(NotTypeFilter: type path nm) [(NotTypeFilter: type (Path: path nm))
`(! ,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp 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))] `(,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))]
[(Bot:) 'Bot] [(Bot:) 'Bot]
[(Top:) 'Top] [(Top:) 'Top]
@ -240,8 +240,8 @@
[(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) [(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:))))
(list (type->sexp t))] (list (type->sexp t))]
[(Values: (list (Result: t [(Values: (list (Result: t
(FilterSet: (TypeFilter: ft pth (list 0 0)) (FilterSet: (TypeFilter: ft (Path: pth (list 0 0)))
(NotTypeFilter: ft pth (list 0 0))) (NotTypeFilter: ft (Path: pth (list 0 0))))
(Empty:)))) (Empty:))))
;; Only print a simple filter for single argument functions, ;; Only print a simple filter for single argument functions,
;; since parse-type only accepts simple latent filters on single ;; 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 ;; special case (even when complex printing is off) because it's
;; useful to users who use functions like `filter`. ;; useful to users who use functions like `filter`.
[(Values: (list (Result: t [(Values: (list (Result: t
(FilterSet: (TypeFilter: ft '() (list 0 0)) (Top:)) (FilterSet: (TypeFilter: ft (Path: '() (list 0 0))) (Top:))
(Empty:)))) (Empty:))))
#:when (= 1 (length dom)) #:when (= 1 (length dom))
`(,(type->sexp t) : #:+ ,(type->sexp ft))] `(,(type->sexp t) : #:+ ,(type->sexp ft))]

2
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/init-env-tests.rkt
View File

@ -26,7 +26,7 @@
'(simple-> (list -String) -Symbol)) '(simple-> (list -String) -Symbol))
(check-equal? (check-equal?
(convert (make-pred-ty -String)) (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? (check-equal?
(convert (->acc (list (-lst -String)) -String (list -car))) (convert (->acc (list (-lst -String)) -String (list -car)))
'(->acc (list (-lst -String)) -String `(,-car))) '(->acc (list (-lst -String)) -String `(,-car)))