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

Improve type of negate

Browse Source 
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

original commit: 0f8ee738142c8e253c638c836fc1c5c893751d32
This commit is contained in:
Asumu Takikawa 2013-11-21 21:12:40 -05:00
parent 1baea70249
commit f44c9539f0
2 changed files with 28 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -873,8 +873,17 @@
;; Section 4.17.3 (racket/function)
[identity (-poly (a) (->acc (list a) a null))]
[const (-poly (a) (-> a (->* '() Univ a)))]
[negate (-polydots (b) (-> ((list) [b b] . ->... . Univ)
((list) [b b] . ->... . -Boolean)))]
[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))))
(-> ((list) [d d] . ->... . Univ)
((list) [d d] . ->... . -Boolean))))]
;; probably the most useful cases
;; 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

17
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -161,6 +161,7 @@
racket/file
racket/fixnum
racket/flonum
racket/function
racket/list
racket/math
racket/path
@ -1828,6 +1829,22 @@
(define (f s) (if (set? s) s (set)))
(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
"tc-literal tests"