suzanne.soy/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
This commit is contained in:
Asumu Takikawa 2013-11-21 21:12:40 -05:00
parent d29256eeb2
commit 0f8ee73814
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"