Improve type of negate

Now for functions with simple filters, it'll negate the
filters so that, e.g., (negate string?) can be used with
occurrence typing.

Please merge to v6.0
(cherry picked from commit 0f8ee73814)
This commit is contained in:
Asumu Takikawa 2013-11-21 21:12:40 -05:00 committed by Ryan Culpepper
parent 698b632cad
commit 4092df1cca
2 changed files with 28 additions and 2 deletions

View File

@ -873,8 +873,17 @@
;; Section 4.17.3 (racket/function) ;; Section 4.17.3 (racket/function)
[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 (b) (-> ((list) [b b] . ->... . Univ) [negate (-polydots (a b c d)
((list) [b b] . ->... . -Boolean)))] (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))))
(-> ((list) [d d] . ->... . Univ)
((list) [d d] . ->... . -Boolean))))]
;; probably the most useful cases ;; probably the most useful cases
;; doesn't cover cases where we pass multiple of the function's arguments to curry, ;; doesn't cover cases where we pass multiple of the function's arguments to curry,
;; also doesn't express that the returned function is itself curried ;; also doesn't express that the returned function is itself curried

View File

@ -161,6 +161,7 @@
racket/file racket/file
racket/fixnum racket/fixnum
racket/flonum racket/flonum
racket/function
racket/list racket/list
racket/math racket/math
racket/path racket/path
@ -1828,6 +1829,22 @@
(define (f s) (if (set? s) s (set))) (define (f s) (if (set? s) s (set)))
(void)) (void))
-Void] -Void]
;; negate
[tc-e
(let ()
(: x (U Symbol Void))
(define x 'foo)
(if ((negate void?) x) (symbol->string x) "foo"))
-String]
[tc-e
(let ()
(: pos? (Real -> Boolean : #:+ (Positive-Real @ 0) #:- (Nonpositive-Real @ 0)))
(define pos? (lambda: ([x : Real]) (positive? x)))
(: x Real)
(define x 3)
(if ((negate pos?) x) x -5))
#:ret (ret -NonPosReal (-FS -top -bot))]
) )
(test-suite (test-suite
"tc-literal tests" "tc-literal tests"