From 889d96ca78ab9259c93657b97dee3df7ff6c4aff Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 28 Mar 2015 00:43:38 -0700 Subject: [PATCH] Strengthen infinity checks in comparison operations. This adds checks for infinity when comparing against reals and accounts for NaNs. --- .../base-env/base-env-numeric.rkt | 52 +++++++------------ .../typed-racket/types/numeric-tower.rkt | 5 ++ .../unit-tests/typecheck-tests.rkt | 11 ++++ 3 files changed, 36 insertions(+), 32 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 08997f55..aa683f59 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -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) diff --git a/typed-racket-lib/typed-racket/types/numeric-tower.rkt b/typed-racket-lib/typed-racket/types/numeric-tower.rkt index e666cda0..853b0ff1 100644 --- a/typed-racket-lib/typed-racket/types/numeric-tower.rkt +++ b/typed-racket-lib/typed-racket/types/numeric-tower.rkt @@ -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))) diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index 638f6c00..bdeedad0 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -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