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

Include both float zeroes in Non-Negative and Non-Positive types.

Browse Source 
Closes PR12706.

original commit: 8cbd26899f59773b7f574a79afca663e53ca02c9
This commit is contained in:
Vincent St-Amour 2012-04-16 17:36:23 -04:00
parent db9690f75f
commit 8b65ec4e4b
3 changed files with 41 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
collects/tests/typed-racket/fail/pr12706.rkt Normal file
View File

@ -0,0 +1,10 @@
#;
(exn-pred 2)
#lang typed/racket
(: foo (Nonnegative-Float -> Nonnegative-Float))
(define (foo x)
(cond [(> x 0.0) 1.0]
[else (ann x String)]))
(foo 0.0)

52
collects/typed-racket/base-env/base-env-numeric.rkt
View File

@ -473,58 +473,58 @@
(define fl<-type
(lambda ()
(from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter (Un -NonPosFlonum -FlonumPosZero) 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter (Un -NonNegFlonum -FlonumNegZero) 0)))
(-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter -NonPosFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter -NonNegFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
(-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0)))
(-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
(-> -Flonum -NonNegFlonum B : (-FS -top (-filter (Un -NonNegFlonum -FlonumNegZero) 0)))
(-> -Flonum -NonNegFlonum B : (-FS -top (-filter -NonNegFlonum 0)))
(-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1)))
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter (Un -NonPosFlonum -FlonumPosZero) 1)))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NonPosFlonum 1)))
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top))
(comp -Flonum))))
(define fl>-type
(lambda ()
(from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter (Un -NonNegFlonum -FlonumNegZero) 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter (Un -NonPosFlonum -FlonumPosZero) 0)))
(-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter -NonNegFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter -NonPosFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
(-> -NonNegFlonum -Flonum B : (-FS -top (-filter (Un -NonNegFlonum -FlonumNegZero) 1)))
(-> -NonNegFlonum -Flonum B : (-FS -top (-filter -NonNegFlonum 1)))
(-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top))
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
(-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0)))
(-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
(-> -Flonum -NonPosFlonum B : (-FS -top (-filter (Un -NonPosFlonum -FlonumPosZero) 0)))
(-> -Flonum -NonPosFlonum B : (-FS -top (-filter -NonPosFlonum 0)))
(comp -Flonum))))
(define fl<=-type
(lambda ()
(from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 1) (-filter -NegFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) (-filter -PosFlonum 0)))
(-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) (-filter -NegFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) (-filter -PosFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
(-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0)))
(-> -NonNegFlonum -Flonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 1) -top))
(-> -NonNegFlonum -Flonum B : (-FS (-filter -NonNegFlonum 1) -top))
(-> -Flonum -NonNegFlonum B : (-FS -top (-filter -PosFlonum 0)))
(-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1)))
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1)))
(-> -Flonum -NonPosFlonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) -top))
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
(comp -Flonum))))
(define fl>=-type
(lambda ()
(from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 1) (-filter -PosFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 0) (-filter -NegFlonum 0)))
(-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) (-filter -PosFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) (-filter -NegFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
(-> -NonNegFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -NonNegFlonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 0) -top))
(-> -Flonum -NonNegFlonum B : (-FS (-filter -NonNegFlonum 0) -top))
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
(-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0)))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -NonPosFlonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) -top))
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
(comp -Flonum))))
(define flmin-type
(lambda ()
@ -556,7 +556,7 @@
(unop -Flonum))))
(define flexp-type
(lambda ()
(from-cases ((Un -NonNegFlonum -FlonumNegZero) . -> . -PosFlonum)
(from-cases (-NonNegFlonum . -> . -PosFlonum)
(-NegFlonum . -> . -NonNegFlonum)
(-Flonum . -> . -Flonum)))) ; nan is the only non nonnegative case (returns nan)
(define flsqrt-type
@ -1192,24 +1192,22 @@
;; we could add cases to encode that
(commutative-case -PosFlonum -Flonum)
(varop -NonNegFlonum)
;; the following case is not guaranteed to return a NonNegFlonum
;; here's an example: (max 0.0 -0.0) -> -0.0
(commutative-case (Un -NonNegFlonum -FlonumNegZero) -Flonum)
(commutative-case -NonNegFlonum -Flonum)
(map varop (list -NegFlonum -NonPosFlonum -Flonum
-SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero))
(commutative-case -PosSingleFlonum -SingleFlonum)
(varop -NonNegSingleFlonum)
(commutative-case (Un -NonNegSingleFlonum -SingleFlonumNegZero) -SingleFlonum)
(commutative-case -NonNegSingleFlonum -SingleFlonum)
(map varop (list -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
-InexactRealPosZero -InexactRealNegZero -InexactRealZero))
(commutative-case -PosInexactReal -InexactReal)
(varop -NonNegInexactReal)
(commutative-case (Un -NonNegInexactReal -InexactRealNegZero) -InexactReal)
(commutative-case -NonNegInexactReal -InexactReal)
(map varop (list -NegInexactReal -NonPosInexactReal -InexactReal
-RealZero))
(commutative-case -PosReal -Real)
(varop -NonNegReal)
(commutative-case (Un -NonNegReal -RealZero) -InexactReal)
(commutative-case -NonNegReal -InexactReal)
(map varop (list -NegReal -NonPosReal -Real)))]
[min
(from-cases (map varop (list -Zero -One))
@ -1225,24 +1223,24 @@
-PosFlonum -NonNegFlonum))
(commutative-case -NegFlonum -Flonum)
(varop -NonPosFlonum)
(commutative-case (Un -NonPosFlonum -FlonumPosZero) -Flonum)
(commutative-case -NonPosFlonum -Flonum)
(map varop (list -Flonum
-SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero
-PosSingleFlonum -NonNegSingleFlonum))
(commutative-case -NegSingleFlonum -SingleFlonum)
(varop -NonPosSingleFlonum)
(commutative-case (Un -NonPosSingleFlonum -SingleFlonumPosZero) -SingleFlonum)
(commutative-case -NonPosSingleFlonum -SingleFlonum)
(map varop (list -SingleFlonum
-InexactRealPosZero -InexactRealNegZero -InexactRealZero
-PosInexactReal -NonNegInexactReal))
(commutative-case -NegInexactReal -InexactReal)
(varop -NonPosInexactReal)
(commutative-case (Un -NonPosInexactReal -InexactRealPosZero) -InexactReal)
(commutative-case -NonPosInexactReal -InexactReal)
(map varop (list -InexactReal
-RealZero -PosReal -NonNegReal))
(commutative-case -NegReal -Real)
(varop -NonPosReal)
(commutative-case (Un -NonPosReal -RealZero) -Real)
(commutative-case -NonPosReal -Real)
(varop -Real))]
[add1 (from-cases

12
collects/typed-racket/types/numeric-tower.rkt
View File

@ -149,13 +149,13 @@
#'(and/c flonum? positive?)
(lambda (x) (and (flonum? x) (positive? x)))
#'-PosFlonum))
(define -NonNegFlonum (*Un -PosFlonum -FlonumPosZero))
(define -NonNegFlonum (*Un -PosFlonum -FlonumZero))
(define -NegFlonum
(make-Base 'Negative-Float
#'(and/c flonum? negative?)
(lambda (x) (and (flonum? x) (negative? x)))
#'-NegFlonum))
(define -NonPosFlonum (*Un -NegFlonum -FlonumNegZero))
(define -NonPosFlonum (*Un -NegFlonum -FlonumZero))
(define -Flonum (*Un -NegFlonum -FlonumNegZero -FlonumPosZero -PosFlonum -FlonumNan)) ; 64-bit floats
;; inexact reals can be flonums (64-bit floats) or 32-bit floats
(define -SingleFlonumPosZero ; disjoint from Flonum 0s
@ -187,16 +187,16 @@
(lambda (x) #f)
#'-PosSingleFlonum))
(define -PosInexactReal (*Un -PosSingleFlonum -PosFlonum))
(define -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumPosZero))
(define -NonNegInexactReal (*Un -PosInexactReal -InexactRealPosZero))
(define -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumZero))
(define -NonNegInexactReal (*Un -PosInexactReal -InexactRealZero))
(define -NegSingleFlonum
(make-Base 'Negative-Single-Flonum
#'(and/c single-flonum? negative?)
(lambda (x) #f)
#'-NegSingleFlonum))
(define -NegInexactReal (*Un -NegSingleFlonum -NegFlonum))
(define -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumNegZero))
(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealNegZero))
(define -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumZero))
(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealZero))
(define -SingleFlonum (*Un -NegSingleFlonum -SingleFlonumNegZero -SingleFlonumPosZero -PosSingleFlonum -SingleFlonumNan))
(define -InexactReal (*Un -SingleFlonum -Flonum))