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

Add a syntax for some asymmetric predicate filters

Browse Source 
Relevant for PR 14423

original commit: 6c97d968530421968bc34f0d641a9047c98b5225
This commit is contained in:
Asumu Takikawa 2014-04-24 11:47:27 -04:00
parent a98676792e
commit 9d7f92fbb7
4 changed files with 30 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -245,26 +245,30 @@
#:attributes (prop)
(pattern :Top^ #:attr prop -top)
(pattern :Bot^ #:attr prop -bot)
(pattern (t:expr :@ pe:path-elem ... i:idx-obj)
(pattern (t:expr :@ pe:path-elem ... i:id)
#:attr prop (-filter (parse-type #'t) #'i (attribute pe.pe)))
(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)))
(pattern (t:expr :@ pe:path-elem ... i:id)
#:attr prop (-filter (parse-type #'t) #'i (attribute pe.pe)))
(pattern (:! t:expr :@ pe:path-elem ... i:idx-obj)
(pattern (:! t:expr :@ pe:path-elem ... i:id)
#:attr prop (-not-filter (parse-type #'t) #'i (attribute pe.pe)))
(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)))
(pattern (:! t:expr :@ pe:path-elem ... i:id)
#:attr prop (-not-filter (parse-type #'t) #'i (attribute pe.pe)))
(pattern (:! t:expr)
#:attr prop (-not-filter (parse-type #'t) 0))
(pattern (and (~var p (prop doms)) ...)
#:attr prop (apply -and (attribute p.prop)))
(pattern (or (~var p (prop doms)) ...)
#:attr prop (apply -or (attribute p.prop)))
(pattern ((~literal implies) (~var p1 (prop doms)) (~var p2 (prop doms)))
#:attr prop (-imp (attribute p1.prop) (attribute p2.prop))))
#:attr prop (-imp (attribute p1.prop) (attribute p2.prop)))
(pattern t:expr
#:attr prop (-filter (parse-type #'t) 0)))
(define-syntax-class object
#:attributes (object)

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

@ -251,6 +251,13 @@
`(,(type->sexp t) : ,(type->sexp ft))
`(,(type->sexp t) : ,(type->sexp ft) @
,@(map pathelem->sexp pth)))]
;; Print asymmetric filters with only a positive filter as a
;; 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 '() id) (Top:))
(Empty:))))
`(,(type->sexp t) : #:+ ,(type->sexp ft))]
[(Values: (list (Result: t fs (Empty:))))
(if (print-complex-filters?)
`(,(type->sexp t) : ,(filter->sexp fs))

8
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt
View File

@ -143,6 +143,14 @@
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0 null) (-filter -Number 0 null)))]
[(-> Any Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
(t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0 null) (-filter -Number 0 null)))]
[(All (a b) (-> (-> a Any : #:+ b) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS (-filter b 0) -top)) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:+ (! b)) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS (-not-filter b 0) -top)) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:- b) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS -top (-filter b 0))) (-lst a) (-lst b)))]
[(All (a b) (-> (-> a Any : #:- (! b)) (Listof a) (Listof b)))
(-poly (a b) (t:-> (asym-pred a Univ (-FS -top (-not-filter b 0))) (-lst a) (-lst b)))]
[(Number -> Number -> Number)
(t:-> -Number (t:-> -Number -Number))]
[(-> Number (-> Number Number))

4
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/type-printer-tests.rkt
View File

@ -71,6 +71,10 @@
(check-prints-as? (-> -Input-Port (make-Values (list (-result -String -true-filter)
(-result -String -true-filter))))
"(-> Input-Port (values (String : (Top | Bot)) (String : (Top | Bot))))")
(check-prints-as? (make-pred-ty -String)
"(-> Any Boolean : String)")
(check-prints-as? (asym-pred Univ -Boolean (-FS (-filter -String 0) -top))
"(-> Any Boolean : #:+ String)")
(check-prints-as? (-> Univ (make-Values (list (-result -String -top-filter -empty-obj)
(-result -String -top-filter -empty-obj))))
"(-> Any (values String String))")