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

Strengthen infinity checks in comparison operations.

Browse Source 
This adds checks for infinity when comparing against reals and accounts
for NaNs.
This commit is contained in:
Eric Dobson 2015-03-28 00:43:38 -07:00
parent 3889036b12
commit 889d96ca78
3 changed files with 36 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1012,14 +1012,12 @@
(-> -NegRat -Fixnum B : (-FS -top (-filter -NegFixnum 1)))
(-> -NonPosInt -Fixnum B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1))))
(-> -NonPosRat -Fixnum B : (-FS -top (-filter -NonPosFixnum 1)))
(-> -Rat (-val +inf.0) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.0) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.0) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.0) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.f) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.f) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.f) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.f) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Real -PosInfinity B : (-FS (-not-filter (Un -InexactRealNan -PosInfinity) 0)
(-filter (Un -InexactRealNan -PosInfinity) 0)))
(-> -NegInfinity -Real B : (-FS (-not-filter (Un -InexactRealNan -NegInfinity) 1)
(-filter (Un -InexactRealNan -NegInfinity) 1)))
(-> -PosInfinity -Real B : -false-filter)
(-> -Real -NegInfinity B : -false-filter)
;; If applying filters resulted in the interesection of the filter and the
;; original type, we'd only need the cases for Fixnums and those for Reals.
;; Cases for Integers and co would fall out naturally from the Real cases,
@ -1077,14 +1075,12 @@
(-> -Fixnum -NegRat B : (-FS -top (-filter -NegFixnum 0)))
(-> -Fixnum -NonPosInt B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1))))
(-> -Fixnum -NonPosRat B : (-FS -top (-filter -NonPosFixnum 0)))
(-> (-val +inf.0) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.0) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.0) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.0) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.f) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.f) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.f) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.f) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -PosInfinity -Real B : (-FS (-not-filter (Un -InexactRealNan -PosInfinity) 1)
(-filter (Un -InexactRealNan -PosInfinity) 1)))
(-> -Real -NegInfinity B : (-FS (-not-filter (Un -InexactRealNan -NegInfinity) 0)
(-filter (Un -InexactRealNan -NegInfinity) 0)))
(-> -Real -PosInfinity B : -false-filter)
(-> -NegInfinity -Real B : -false-filter)
(>-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(>-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(>-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)
@ -1138,14 +1134,10 @@
(-> -Fixnum -NegReal B : (-FS (-filter -NegFixnum 0) -top))
(-> -Fixnum -NonPosInt B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)) -top))
(-> -Fixnum -NonPosReal B : (-FS (-filter -NonPosFixnum 0) -top))
(-> -Rat (-val +inf.0) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.0) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.0) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.0) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.f) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.f) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.f) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.f) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Real -PosInfinity B : (-FS (-not-filter -InexactRealNan 0) (-filter -InexactRealNan 0)))
(-> -NegInfinity -Real B : (-FS (-not-filter -InexactRealNan 1) (-filter -InexactRealNan 1)))
(-> -PosInfinity -Real B : (-FS (-filter -PosInfinity 1) (-not-filter -PosInfinity 1)))
(-> -Real -NegInfinity B : (-FS (-filter -NegInfinity 0) (-not-filter -NegInfinity 0)))
(<=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(<=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(<=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)
@ -1199,14 +1191,10 @@
(-> -NegReal -Fixnum B : (-FS (-filter -NegFixnum 1) -top))
(-> -NonPosInt -Fixnum B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)) -top))
(-> -NonPosReal -Fixnum B : (-FS (-filter -NonPosFixnum 1) -top))
(-> (-val +inf.0) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.0) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.0) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.0) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> (-val +inf.f) -Rat B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -Rat (-val +inf.f) B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> (-val -inf.f) -Rat B : (-FS (-filter (Un) 0) -top)) ; can't happen
(-> -Rat (-val -inf.f) B : (-FS -top (-filter (Un) 0))) ; guaranteed
(-> -PosInfinity -Real B : (-FS (-not-filter -InexactRealNan 1) (-filter -InexactRealNan 1)))
(-> -Real -NegInfinity B : (-FS (-not-filter -InexactRealNan 0) (-filter -InexactRealNan 0)))
(-> -Real -PosInfinity B : (-FS (-filter -PosInfinity 0) (-not-filter -PosInfinity 0)))
(-> -NegInfinity -Real B : (-FS (-filter -NegInfinity 1) (-not-filter -NegInfinity 1)))
(>=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero)
(>=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero)
(>=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum)

5
typed-racket-lib/typed-racket/types/numeric-tower.rkt
View File

@ -18,6 +18,7 @@
-SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero -SingleFlonumNan -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum
-InexactRealPosZero -InexactRealNegZero -InexactRealZero -InexactRealNan -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal -InexactReal
-RealZero -PosReal -NonNegReal -NegReal -NonPosReal -Real
-PosInfinity -NegInfinity
-ExactImaginary -FloatImaginary -SingleFlonumImaginary -InexactImaginary -Imaginary
-ExactNumber -ExactComplex -FloatComplex -SingleFlonumComplex -InexactComplex -Number
(rename-out (-Int -Integer))
@ -57,6 +58,10 @@
(define/decl -Zero (make-Value 0)) ; exact
(define/decl -One (make-Value 1))
;; Infinities (These are part of Flonum/Single-Flonum, but useful abbreviatios.)
(define/decl -PosInfinity (*Un (-val +inf.0) (-val +inf.f)))
(define/decl -NegInfinity (*Un (-val -inf.0) (-val -inf.f)))
;; Integers
(define/decl -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned
#'(and/c byte? (lambda (x) (> x 1)))

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

@ -3571,6 +3571,17 @@
(t:-> -Byte -Boolean : (-FS (-filter -PosByte 0) (-filter -Zero 0)))]
[tc-e/t (lambda: ([x : Fixnum]) (negative? x))
(t:-> -Fixnum -Boolean : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0)))]
[tc-e (< (ann 0 Integer) +inf.0)
#:ret (ret -Boolean -true-filter)]
[tc-e (> -inf.0 (ann 0 Exact-Rational))
#:ret (ret -Boolean -false-filter)]
[tc-e/t (lambda: ([x : Flonum]) (and (<= +inf.f x) x))
(t:-> -Flonum (t:Un (-val #f) (-val +inf.0))
: (-FS (-filter (-val +inf.0) 0) (-not-filter (-val +inf.0) 0)))]
[tc-e/t (lambda: ([x : Flonum]) (or (>= +inf.f x) x))
(t:-> -Flonum (t:Un (-val #t) -FlonumNan)
: -true-filter)]
)
(test-suite