suzanne.soy/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.
This commit is contained in:
Vincent St-Amour 2012-04-16 17:36:23 -04:00
parent 1bcf56f5e9
commit 8cbd26899f
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 (define fl<-type
(lambda () (lambda ()
(from-cases (from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter (Un -NonPosFlonum -FlonumPosZero) 1))) (-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter -NonPosFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter (Un -NonNegFlonum -FlonumNegZero) 0))) (-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter -NonNegFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
(-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) (-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0)))
(-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) (-> -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))) (-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1)))
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) (-> -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)) (-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top))
(comp -Flonum)))) (comp -Flonum))))
(define fl>-type (define fl>-type
(lambda () (lambda ()
(from-cases (from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter (Un -NonNegFlonum -FlonumNegZero) 1))) (-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) (-filter -NonNegFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter (Un -NonPosFlonum -FlonumPosZero) 0))) (-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) (-filter -NonPosFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) (-> -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)) (-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top))
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) (-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
(-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0))) (-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0)))
(-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) (-> -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)))) (comp -Flonum))))
(define fl<=-type (define fl<=-type
(lambda () (lambda ()
(from-cases (from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 1) (-filter -NegFlonum 1))) (-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) (-filter -NegFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 0) (-filter -PosFlonum 0))) (-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) (-filter -PosFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
(-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) (-> -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))) (-> -Flonum -NonNegFlonum B : (-FS -top (-filter -PosFlonum 0)))
(-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) (-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1)))
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) (-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) (-> -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)))) (comp -Flonum))))
(define fl>=-type (define fl>=-type
(lambda () (lambda ()
(from-cases (from-cases
(-> -FlonumZero -Flonum B : (-FS (-filter (Un -NonPosFlonum -FlonumPosZero) 1) (-filter -PosFlonum 1))) (-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) (-filter -PosFlonum 1)))
(-> -Flonum -FlonumZero B : (-FS (-filter (Un -NonNegFlonum -FlonumNegZero) 0) (-filter -NegFlonum 0))) (-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) (-filter -NegFlonum 0)))
(-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -PosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1)))
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) (-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
(-> -NonNegFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -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)) (-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
(-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0))) (-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0)))
(-> -NonPosFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) (-> -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)))) (comp -Flonum))))
(define flmin-type (define flmin-type
(lambda () (lambda ()
@ -556,7 +556,7 @@
(unop -Flonum)))) (unop -Flonum))))
(define flexp-type (define flexp-type
(lambda () (lambda ()
(from-cases ((Un -NonNegFlonum -FlonumNegZero) . -> . -PosFlonum) (from-cases (-NonNegFlonum . -> . -PosFlonum)
(-NegFlonum . -> . -NonNegFlonum) (-NegFlonum . -> . -NonNegFlonum)
(-Flonum . -> . -Flonum)))) ; nan is the only non nonnegative case (returns nan) (-Flonum . -> . -Flonum)))) ; nan is the only non nonnegative case (returns nan)
(define flsqrt-type (define flsqrt-type
@ -1192,24 +1192,22 @@
;; we could add cases to encode that ;; we could add cases to encode that
(commutative-case -PosFlonum -Flonum) (commutative-case -PosFlonum -Flonum)
(varop -NonNegFlonum) (varop -NonNegFlonum)
;; the following case is not guaranteed to return a NonNegFlonum (commutative-case -NonNegFlonum -Flonum)
;; here's an example: (max 0.0 -0.0) -> -0.0
(commutative-case (Un -NonNegFlonum -FlonumNegZero) -Flonum)
(map varop (list -NegFlonum -NonPosFlonum -Flonum (map varop (list -NegFlonum -NonPosFlonum -Flonum
-SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero)) -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero))
(commutative-case -PosSingleFlonum -SingleFlonum) (commutative-case -PosSingleFlonum -SingleFlonum)
(varop -NonNegSingleFlonum) (varop -NonNegSingleFlonum)
(commutative-case (Un -NonNegSingleFlonum -SingleFlonumNegZero) -SingleFlonum) (commutative-case -NonNegSingleFlonum -SingleFlonum)
(map varop (list -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum (map varop (list -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
-InexactRealPosZero -InexactRealNegZero -InexactRealZero)) -InexactRealPosZero -InexactRealNegZero -InexactRealZero))
(commutative-case -PosInexactReal -InexactReal) (commutative-case -PosInexactReal -InexactReal)
(varop -NonNegInexactReal) (varop -NonNegInexactReal)
(commutative-case (Un -NonNegInexactReal -InexactRealNegZero) -InexactReal) (commutative-case -NonNegInexactReal -InexactReal)
(map varop (list -NegInexactReal -NonPosInexactReal -InexactReal (map varop (list -NegInexactReal -NonPosInexactReal -InexactReal
-RealZero)) -RealZero))
(commutative-case -PosReal -Real) (commutative-case -PosReal -Real)
(varop -NonNegReal) (varop -NonNegReal)
(commutative-case (Un -NonNegReal -RealZero) -InexactReal) (commutative-case -NonNegReal -InexactReal)
(map varop (list -NegReal -NonPosReal -Real)))] (map varop (list -NegReal -NonPosReal -Real)))]
[min [min
(from-cases (map varop (list -Zero -One)) (from-cases (map varop (list -Zero -One))
@ -1225,24 +1223,24 @@
-PosFlonum -NonNegFlonum)) -PosFlonum -NonNegFlonum))
(commutative-case -NegFlonum -Flonum) (commutative-case -NegFlonum -Flonum)
(varop -NonPosFlonum) (varop -NonPosFlonum)
(commutative-case (Un -NonPosFlonum -FlonumPosZero) -Flonum) (commutative-case -NonPosFlonum -Flonum)
(map varop (list -Flonum (map varop (list -Flonum
-SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero
-PosSingleFlonum -NonNegSingleFlonum)) -PosSingleFlonum -NonNegSingleFlonum))
(commutative-case -NegSingleFlonum -SingleFlonum) (commutative-case -NegSingleFlonum -SingleFlonum)
(varop -NonPosSingleFlonum) (varop -NonPosSingleFlonum)
(commutative-case (Un -NonPosSingleFlonum -SingleFlonumPosZero) -SingleFlonum) (commutative-case -NonPosSingleFlonum -SingleFlonum)
(map varop (list -SingleFlonum (map varop (list -SingleFlonum
-InexactRealPosZero -InexactRealNegZero -InexactRealZero -InexactRealPosZero -InexactRealNegZero -InexactRealZero
-PosInexactReal -NonNegInexactReal)) -PosInexactReal -NonNegInexactReal))
(commutative-case -NegInexactReal -InexactReal) (commutative-case -NegInexactReal -InexactReal)
(varop -NonPosInexactReal) (varop -NonPosInexactReal)
(commutative-case (Un -NonPosInexactReal -InexactRealPosZero) -InexactReal) (commutative-case -NonPosInexactReal -InexactReal)
(map varop (list -InexactReal (map varop (list -InexactReal
-RealZero -PosReal -NonNegReal)) -RealZero -PosReal -NonNegReal))
(commutative-case -NegReal -Real) (commutative-case -NegReal -Real)
(varop -NonPosReal) (varop -NonPosReal)
(commutative-case (Un -NonPosReal -RealZero) -Real) (commutative-case -NonPosReal -Real)
(varop -Real))] (varop -Real))]
[add1 (from-cases [add1 (from-cases

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

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