From 90741c2747353e0b194cba42859f930d13e8a6ce Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Tue, 24 Jul 2012 17:52:14 -0400 Subject: [PATCH] Include NaN in all floating-point types. Makes more closure properties hold, but weakens occurrence typing for some comparisons involving flonums. original commit: a6d5a98b61c033340c66b91dd53c18ea50db8c60 --- .../unit-tests/typecheck-tests.rkt | 2 +- .../base-env/base-env-numeric.rkt | 371 ++++++++---------- collects/typed-racket/types/numeric-tower.rkt | 56 +-- 3 files changed, 193 insertions(+), 236 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt index 1974ce03..272f2e4f 100644 --- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -208,7 +208,7 @@ (tc-e (lcm (ann 3 Integer) -1/2) -NonNegRat) (tc-e (expt 0.5 0.3) -PosFlonum) (tc-e (expt 0.5 2) -PosFlonum) - (tc-e (expt 0.5 0) -PosReal) + (tc-e (expt 0.5 0) -PosFlonum) (tc-e (flexpt 0.5 0.3) -NonNegFlonum) (tc-e (flexpt 0.00000000001 100000000000.0) -NonNegFlonum) (tc-e (flexpt -2.0 -0.5) -Flonum) ; NaN diff --git a/collects/typed-racket/base-env/base-env-numeric.rkt b/collects/typed-racket/base-env/base-env-numeric.rkt index f5dd16fb..2174f5a1 100644 --- a/collects/typed-racket/base-env/base-env-numeric.rkt +++ b/collects/typed-racket/base-env/base-env-numeric.rkt @@ -441,8 +441,7 @@ (lambda () (cl->* (-> -FlonumZero -FlonumZero) (-> (Un -PosFlonum -NegFlonum) -PosFlonum) - (-> (Un -NonNegFlonum -NonPosFlonum) -NonNegFlonum) - (-> -Flonum (Un -NonNegFlonum -FlonumNan))))) + (-> -Flonum -NonNegFlonum)))) (define fl+-type (lambda () (from-cases (map (lambda (t) (commutative-binop t -FlonumZero t)) @@ -465,7 +464,7 @@ (binop -FlonumZero) ;; we don't have Pos Pos -> Pos, possible underflow (binop -PosFlonum -NonNegFlonum) - (binop (Un -NonNegFlonum -FlonumNan)) + (binop -NonNegFlonum) (commutative-binop -NegFlonum -PosFlonum -NonPosFlonum) (binop -NegFlonum -NonNegFlonum) (binop -Flonum)))) @@ -475,9 +474,9 @@ (-FlonumPosZero -NegFlonum . -> . -FlonumNegZero) (-FlonumNegZero -PosFlonum . -> . -FlonumNegZero) (-FlonumNegZero -NegFlonum . -> . -FlonumPosZero) - (-PosFlonum -PosFlonum . -> . (Un -NonNegFlonum -FlonumNan)) ; possible underflow - (commutative-binop -PosFlonum -NegFlonum (Un -NonPosFlonum -FlonumNan)) - (-NegFlonum -NegFlonum . -> . (Un -NonNegFlonum -FlonumNan)) + (-PosFlonum -PosFlonum . -> . -NonNegFlonum) ; possible underflow + (commutative-binop -PosFlonum -NegFlonum -NonPosFlonum) + (-NegFlonum -NegFlonum . -> . -NonNegFlonum) (binop -Flonum)))) (define fl=-type (lambda () @@ -491,72 +490,69 @@ (define fl<-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) (-filter -NonPosFlonum 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) (-filter -NonNegFlonum 0))) + ;; false case, we know nothing, lhs may be NaN. same for all comparison that can involve floats + (-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) -top)) + (-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) -top)) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) - (-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) + (-> -Flonum -PosFlonum B : (-FS -top -top)) (-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) - (-> -Flonum -NonNegFlonum B : (-FS -top (-filter -NonNegFlonum 0))) - (-> -NegFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) + (-> -Flonum -NonNegFlonum B : (-FS -top -top)) + (-> -NegFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) - (-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NonPosFlonum 1))) + (-> -NonPosFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top)) (comp -Flonum)))) (define fl>-type (lambda () (from-cases - (-> -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))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) -top)) + (-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) -top)) + (-> -PosFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) - (-> -NonNegFlonum -Flonum B : (-FS -top (-filter -NonNegFlonum 1))) + (-> -NonNegFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top)) (-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) - (-> -Flonum -NegFlonum B : (-FS -top (-filter -NegFlonum 0))) + (-> -Flonum -NegFlonum B : (-FS -top -top)) (-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top)) - (-> -Flonum -NonPosFlonum B : (-FS -top (-filter -NonPosFlonum 0))) + (-> -Flonum -NonPosFlonum B : (-FS -top -top)) (comp -Flonum)))) (define fl<=-type (lambda () (from-cases - (-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) (-filter -NegFlonum 1))) - (-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) (-filter -PosFlonum 0))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) -top)) + (-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) -top)) (-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top)) - (-> -Flonum -PosFlonum B : (-FS -top (-filter -PosFlonum 0))) + (-> -Flonum -PosFlonum B : (-FS -top -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 -NonNegFlonum B : (-FS -top -top)) + (-> -NegFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top)) - (-> -NonPosFlonum -Flonum B : (-FS -top (-filter -NegFlonum 1))) + (-> -NonPosFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top)) (comp -Flonum)))) (define fl>=-type (lambda () (from-cases - (-> -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))) + (-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) -top)) + (-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) -top)) + (-> -PosFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top)) - (-> -NonNegFlonum -Flonum B : (-FS -top (-filter -PosFlonum 1))) + (-> -NonNegFlonum -Flonum B : (-FS -top -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 -NegFlonum B : (-FS -top -top)) + (-> -NonPosFlonum -Flonum B : (-FS -top -top)) (-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top)) (comp -Flonum)))) (define flmin-type (lambda () - (from-cases (commutative-case -NegFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case (Un -NegFlonum -FlonumNan) -Flonum) - (commutative-case -NonPosFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case (Un -NonPosFlonum -FlonumNan) -NonPosFlonum) + (from-cases (commutative-case -NegFlonum -Flonum) + (commutative-case -NonPosFlonum -Flonum) (map binop (list -PosFlonum -NonNegFlonum -Flonum))))) (define flmax-type (lambda () - (from-cases (commutative-case -PosFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case (Un -PosFlonum -FlonumNan) -Flonum) - (commutative-case -NonNegFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case (Un -NonNegFlonum -FlonumNan) -Flonum) + (from-cases (commutative-case -PosFlonum -Flonum) + (commutative-case -NonNegFlonum -Flonum) (map binop (list -NegFlonum -NonPosFlonum -Flonum))))) (define flround-type ; truncate too (lambda () @@ -588,7 +584,7 @@ (lambda () (from-cases (-FlonumZero -PosFlonum . -> . -FlonumZero) ; (flexpt -0.0 0.1) -> 0.0 ; not sign preserving ((Un -PosFlonum -NegFlonum) -FlonumZero . -> . -PosFlonum) ; always returns 1.0 - (-PosFlonum (Un -NonNegFlonum -NonPosFlonum) . -> . -NonNegFlonum) ; can underflow, and can't have NaN as exponent + (-NonNegFlonum -Flonum . -> . -NonNegFlonum) ; can underflow (-Flonum -Flonum . -> . -Flonum)))) (define fx->fl-type @@ -614,18 +610,18 @@ ;; There's a repetitive pattern in the types of each comparison operator. ;; As explained below, this is because filters don't do intersections. - (define (<-type-pattern base pos non-neg neg non-pos) - (list (-> base -RealZero B : (-FS (-filter neg 0) (-filter non-neg 0))) - (-> -RealZero base B : (-FS (-filter pos 1) (-filter non-pos 1))) + (define (<-type-pattern base pos non-neg neg non-pos [zero -RealZero]) + (list (-> base zero B : (-FS (-filter neg 0) (-filter non-neg 0))) + (-> zero base B : (-FS (-filter pos 1) (-filter non-pos 1))) (-> base -PosReal B : (-FS -top (-filter pos 0))) (-> base -NonNegReal B : (-FS -top (-filter non-neg 0))) (-> -NonNegReal base B : (-FS (-filter pos 1) -top)) (-> base -NonPosReal B : (-FS (-filter neg 0) -top)) (-> -NegReal base B : (-FS -top (-filter neg 1))) (-> -NonPosReal base B : (-FS -top (-filter non-pos 1))))) - (define (>-type-pattern base pos non-neg neg non-pos) - (list (-> base -RealZero B : (-FS (-filter pos 0) (-filter non-pos 0))) - (-> -RealZero base B : (-FS (-filter neg 1) (-filter non-neg 1))) + (define (>-type-pattern base pos non-neg neg non-pos [zero -RealZero]) + (list (-> base zero B : (-FS (-filter pos 0) (-filter non-pos 0))) + (-> zero base B : (-FS (-filter neg 1) (-filter non-neg 1))) (-> base -NonNegReal B : (-FS (-filter pos 0) -top)) (-> -PosReal base B : (-FS -top (-filter pos 1))) (-> -NonNegReal base B : (-FS -top (-filter non-neg 1))) @@ -633,18 +629,18 @@ (-> base -NegReal B : (-FS -top (-filter neg 0))) (-> base -NonPosReal B : (-FS -top (-filter non-pos 0))))) ;; this is > with flipped filters - (define (<=-type-pattern base pos non-neg neg non-pos) - (list (-> base -RealZero B : (-FS (-filter non-pos 0) (-filter pos 0))) - (-> -RealZero base B : (-FS (-filter non-neg 1) (-filter neg 1))) + (define (<=-type-pattern base pos non-neg neg non-pos [zero -RealZero]) + (list (-> base zero B : (-FS (-filter non-pos 0) (-filter pos 0))) + (-> zero base B : (-FS (-filter non-neg 1) (-filter neg 1))) (-> base -NonNegReal B : (-FS -top (-filter pos 0))) (-> -PosReal base B : (-FS (-filter pos 1) -top)) (-> -NonNegReal base B : (-FS (-filter non-neg 1) -top)) (-> -NonPosReal base B : (-FS -top (-filter neg 1))) (-> base -NegReal B : (-FS (-filter neg 0) -top)) (-> base -NonPosReal B : (-FS (-filter non-pos 0) -top)))) - (define (>=-type-pattern base pos non-neg neg non-pos) - (list (-> base -RealZero B : (-FS (-filter non-neg 0) (-filter neg 0))) - (-> -RealZero base B : (-FS (-filter non-pos 1) (-filter pos 1))) + (define (>=-type-pattern base pos non-neg neg non-pos [zero -RealZero]) + (list (-> base zero B : (-FS (-filter non-neg 0) (-filter neg 0))) + (-> zero base B : (-FS (-filter non-pos 1) (-filter pos 1))) (-> base -PosReal B : (-FS (-filter pos 0) -top)) (-> base -NonNegReal B : (-FS (-filter non-neg 0) -top)) (-> -NonNegReal base B : (-FS -top (-filter pos 1))) @@ -782,50 +778,50 @@ (-> -Nat -One B : (-FS (-filter -Zero 0) -top)) (-> -Byte -RealZero B : (-FS (-filter (Un) 0) -top)) (-> -Byte -One B : (-FS (-filter -Zero 0) -top)) - (-> -RealZero -Byte B : (-FS (-filter -PosByte 1) (-filter -Zero 1))) + (-> -Zero -Byte B : (-FS (-filter -PosByte 1) (-filter -Zero 1))) ; can't be -RealZero, which includes NaN (-> -Byte -PosByte B : (-FS -top (-filter -PosByte 0))) (-> -Byte -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -PosInt -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) - (-> -PosReal -Byte B : (-FS (-filter -PosByte 1) -top)) + (-> -PosReal -Byte B : (-FS (-filter -PosByte 1) -top)) ; -PosReal is ok here, no filter for #f (-> -Byte -PosInt B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) - (-> -Byte -PosReal B : (-FS -top (-filter -PosByte 0))) + (-> -Byte -PosRat B : (-FS -top (-filter -PosByte 0))) ; can't be -PosReal, which includes NaN (-> -Nat -Byte B : (-FS (-and (-filter -Byte 0) (-filter -PosByte 1)) -top)) (-> -NonNegReal -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -Byte -Nat B : (-FS -top (-filter -Byte 1))) (-> -Index -RealZero B : (-FS (-filter (Un) 0) -top)) (-> -Index -One B : (-FS (-filter -Zero 0) -top)) - (-> -RealZero -Index B : (-FS (-filter -PosIndex 1) (-filter -Zero 1))) + (-> -Zero -Index B : (-FS (-filter -PosIndex 1) (-filter -Zero 1))) ; can't be -RealZero, which includes NaN (-> -Index -PosIndex B : (-FS -top (-filter -PosIndex 0))) (-> -Index -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -PosInt -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) (-> -PosReal -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Index -PosInt B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1)))) - (-> -Index -PosReal B : (-FS -top (-filter -PosIndex 0))) + (-> -Index -PosRat B : (-FS -top (-filter -PosIndex 0))) ; can't be -PosReal, which includes NaN (-> -Nat -Index B : (-FS (-and (-filter -Index 0) (-filter -PosIndex 1)) -top)) (-> -NonNegReal -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Index -Nat B : (-FS -top (-filter -Index 1))) - (-> -Fixnum -RealZero B : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0))) - (-> -RealZero -Fixnum B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1))) + (-> -Fixnum -Zero B : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0))) ; can't be -RealZero + (-> -Zero -Fixnum B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1))) (-> -Fixnum -PosInt B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)))) - (-> -Fixnum -PosReal B : (-FS -top (-filter -PosFixnum 0))) + (-> -Fixnum -PosRat B : (-FS -top (-filter -PosFixnum 0))) (-> -Fixnum -Nat B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)))) - (-> -Fixnum -NonNegReal B : (-FS -top (-filter -NonNegFixnum 0))) + (-> -Fixnum -NonNegRat B : (-FS -top (-filter -NonNegFixnum 0))) (-> -Nat -Fixnum B : (-FS (-and (-filter -PosFixnum 1) (-filter -NonNegFixnum 0)) -top)) (-> -NonNegReal -Fixnum B : (-FS (-filter -PosFixnum 1) -top)) (-> -Fixnum -NonPosInt B : (-FS (-and (-filter -NegFixnum 0) (-filter -NonPosFixnum 1)) -top)) (-> -Fixnum -NonPosReal B : (-FS (-filter -NegFixnum 0) -top)) (-> -NegInt -Fixnum B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)))) - (-> -NegReal -Fixnum B : (-FS -top (-filter -NegFixnum 1))) + (-> -NegRat -Fixnum B : (-FS -top (-filter -NegFixnum 1))) (-> -NonPosInt -Fixnum B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)))) - (-> -NonPosReal -Fixnum B : (-FS -top (-filter -NonPosFixnum 1))) + (-> -NonPosRat -Fixnum B : (-FS -top (-filter -NonPosFixnum 1))) ;; 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, ;; since we'd keep track of the representation knowledge we'd already have, ;; and the Real cases are enough to give us sign information. ;; In the meantime, repetition is hard to avoid. - (<-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt) - (<-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat) + (<-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero) + (<-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero) (<-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum) (<-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) (<-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal) @@ -836,44 +832,44 @@ (-> -One -Nat B : (-FS (-filter -Zero 1) -top)) (-> -RealZero -Byte B : (-FS (-filter (Un) 1) -top)) (-> -One -Byte B : (-FS (-filter -Zero 1) -top)) - (-> -Byte -RealZero B : (-FS (-filter -PosByte 0) (-filter -Zero 0))) + (-> -Byte -Zero B : (-FS (-filter -PosByte 0) (-filter -Zero 0))) (-> -PosByte -Byte B : (-FS -top (-filter -PosByte 1))) (-> -Byte -Byte B : (-FS (-filter -PosByte 0) -top)) (-> -Byte -PosInt B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -Byte -PosReal B : (-FS (-filter -PosByte 0) -top)) (-> -PosInt -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) - (-> -PosReal -Byte B : (-FS -top (-filter -PosByte 1))) + (-> -PosRat -Byte B : (-FS -top (-filter -PosByte 1))) (-> -Byte -Nat B : (-FS (-and (-filter -PosByte 0) (-filter -Byte 1)) -top)) (-> -Byte -NonNegReal B : (-FS (-filter -PosByte 0) -top)) (-> -Nat -Byte B : (-FS -top (-filter -Byte 0))) (-> -RealZero -Index B : (-FS (-filter (Un) 1) -top)) (-> -One -Index B : (-FS (-filter -Zero 1) -top)) - (-> -Index -RealZero B : (-FS (-filter -PosIndex 0) (-filter -Zero 0))) + (-> -Index -Zero B : (-FS (-filter -PosIndex 0) (-filter -Zero 0))) (-> -PosIndex -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Index B : (-FS (-filter -PosIndex 0) -top)) (-> -Index -PosInt B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) (-> -Index -PosReal B : (-FS (-filter -PosIndex 0) -top)) (-> -PosInt -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1)))) - (-> -PosReal -Index B : (-FS -top (-filter -PosIndex 1))) + (-> -PosRat -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Nat B : (-FS (-and (-filter -PosIndex 0) (-filter -Index 1)) -top)) (-> -Index -NonNegReal B : (-FS (-filter -PosIndex 0) -top)) (-> -Nat -Index B : (-FS -top (-filter -Index 0))) - (-> -RealZero -Fixnum B : (-FS (-filter -NegFixnum 1) (-filter -NonNegFixnum 1))) + (-> -Zero -Fixnum B : (-FS (-filter -NegFixnum 1) (-filter -NonNegFixnum 1))) (-> -Fixnum -RealZero B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0))) (-> -PosInt -Fixnum B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)))) - (-> -PosReal -Fixnum B : (-FS -top (-filter -PosFixnum 1))) + (-> -PosRat -Fixnum B : (-FS -top (-filter -PosFixnum 1))) (-> -Nat -Fixnum B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)))) - (-> -NonNegReal -Fixnum B : (-FS -top (-filter -NonNegFixnum 1))) + (-> -NonNegRat -Fixnum B : (-FS -top (-filter -NonNegFixnum 1))) (-> -Fixnum -Nat B : (-FS (-and (-filter -PosFixnum 0) (-filter -NonNegFixnum 1)) -top)) (-> -Fixnum -NonNegReal B : (-FS (-filter -PosFixnum 0) -top)) (-> -NonPosInt -Fixnum B : (-FS (-and (-filter -NonPosFixnum 0) (-filter -NegFixnum 1)) -top)) (-> -NonPosReal -Fixnum B : (-FS (-filter -NegFixnum 1) -top)) (-> -Fixnum -NegInt B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)))) - (-> -Fixnum -NegReal B : (-FS -top (-filter -NegFixnum 0))) + (-> -Fixnum -NegRat B : (-FS -top (-filter -NegFixnum 0))) (-> -Fixnum -NonPosInt B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NonPosFixnum 1)))) - (-> -Fixnum -NonPosReal B : (-FS -top (-filter -NonPosFixnum 0))) - (>-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt) - (>-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat) + (-> -Fixnum -NonPosRat B : (-FS -top (-filter -NonPosFixnum 0))) + (>-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero) + (>-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero) (>-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum) (>-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) (>-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal) @@ -881,49 +877,49 @@ (->* (list R R) R B))] [<= (from-cases (-> -Pos -One B : (-FS (-filter -One 0) -top)) - (-> -Byte -RealZero B : (-FS (-filter -Zero 0) (-filter -PosByte 0))) - (-> -RealZero -Byte B : (-FS -top (-filter (Un) 1))) + (-> -Byte -Zero B : (-FS (-filter -Zero 0) (-filter -PosByte 0))) + (-> -Zero -Byte B : (-FS -top (-filter (Un) 1))) (-> -One -Byte B : (-FS (-filter -PosByte 1) (-filter -Zero 1))) (-> -PosByte -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -Byte -Byte B : (-FS -top (-filter -PosByte 0))) (-> -PosInt -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -PosReal -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -Byte -PosInt B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) - (-> -Byte -PosReal B : (-FS -top (-filter -PosByte 0))) + (-> -Byte -PosRat B : (-FS -top (-filter -PosByte 0))) (-> -Nat -Byte B : (-FS (-filter -Byte 0) -top)) (-> -Byte -Nat B : (-FS -top (-and (-filter -PosByte 0) (-filter -Byte 1)))) - (-> -Byte -NonNegReal B : (-FS -top (-filter -PosByte 0))) - (-> -Index -RealZero B : (-FS (-filter -Zero 0) (-filter -PosIndex 0))) - (-> -RealZero -Index B : (-FS -top (-filter (Un) 1))) + (-> -Byte -NonNegRat B : (-FS -top (-filter -PosByte 0))) + (-> -Index -Zero B : (-FS (-filter -Zero 0) (-filter -PosIndex 0))) + (-> -Zero -Index B : (-FS -top (-filter (Un) 1))) (-> -One -Index B : (-FS (-filter -PosIndex 1) (-filter -Zero 1))) (-> -PosIndex -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Index -Index B : (-FS -top (-filter -PosIndex 0))) (-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) (-> -PosReal -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Index -Pos B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1)))) - (-> -Index -PosReal B : (-FS -top (-filter -PosIndex 0))) + (-> -Index -PosRat B : (-FS -top (-filter -PosIndex 0))) (-> -Nat -Index B : (-FS (-filter -Index 0) -top)) (-> -Index -Nat B : (-FS -top (-and (-filter -PosIndex 0) (-filter -Index 1)))) - (-> -Index -NonNegReal B : (-FS -top (-filter -PosIndex 0))) - (-> -NonNegFixnum -RealZero B : (-FS (-filter -Zero 0) (-filter -PosFixnum 0))) - (-> -RealZero -NonNegFixnum B : (-FS (-filter -Zero 1) (-filter (Un) 1))) + (-> -Index -NonNegRat B : (-FS -top (-filter -PosIndex 0))) + (-> -NonNegFixnum -Zero B : (-FS (-filter -Zero 0) (-filter -PosFixnum 0))) + (-> -Zero -NonNegFixnum B : (-FS (-filter -Zero 1) (-filter (Un) 1))) (-> -One -NonNegFixnum B : (-FS -top (-filter -Zero 1))) - (-> -RealZero -Fixnum B : (-FS (-filter -NonNegFixnum 1) (-filter -NegFixnum 1))) - (-> -Fixnum -RealZero B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0))) + (-> -Zero -Fixnum B : (-FS (-filter -NonNegFixnum 1) (-filter -NegFixnum 1))) + (-> -Fixnum -Zero B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0))) (-> -PosInt -Fixnum B : (-FS (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)) -top)) (-> -PosReal -Fixnum B : (-FS (-filter -PosFixnum 1) -top)) (-> -Nat -Fixnum B : (-FS (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)) -top)) (-> -NonNegReal -Fixnum B : (-FS (-filter -NonNegFixnum 1) -top)) (-> -Fixnum -Nat B : (-FS -top (-and (-filter -PosFixnum 0) (-filter -NonNegFixnum 1)))) - (-> -Fixnum -NonNegReal B : (-FS -top (-filter -PosFixnum 0))) + (-> -Fixnum -NonNegRat B : (-FS -top (-filter -PosFixnum 0))) (-> -NonPosInt -Fixnum B : (-FS -top (-and (-filter -NonPosFixnum 0) (-filter -NegFixnum 1)))) - (-> -NonPosReal -Fixnum B : (-FS -top (-filter -NegFixnum 1))) + (-> -NonPosRat -Fixnum B : (-FS -top (-filter -NegFixnum 1))) (-> -Fixnum -NegInt B : (-FS (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)) -top)) (-> -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)) - (<=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt) - (<=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat) + (<=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero) + (<=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero) (<=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum) (<=-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) (<=-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal) @@ -931,49 +927,49 @@ (->* (list R R) R B))] [>= (from-cases (-> -One -Pos B : (-FS (-filter -One 1) -top)) - (-> -RealZero -Byte B : (-FS (-filter -Zero 1) (-filter -PosByte 1))) - (-> -Byte -RealZero B : (-FS -top (-filter (Un) 0))) + (-> -Zero -Byte B : (-FS (-filter -Zero 1) (-filter -PosByte 1))) + (-> -Byte -Zero B : (-FS -top (-filter (Un) 0))) (-> -Byte -One B : (-FS (-filter -PosByte 0) (-filter -Zero 0))) (-> -Byte -PosByte B : (-FS (-filter -PosByte 0) -top)) (-> -Byte -Byte B : (-FS -top (-filter -PosByte 1))) (-> -Byte -PosInt B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -Byte -PosReal B : (-FS (-filter -PosByte 0) -top)) (-> -PosInt -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) - (-> -PosReal -Byte B : (-FS -top (-filter -PosByte 0))) + (-> -PosRat -Byte B : (-FS -top (-filter -PosByte 0))) (-> -Byte -Nat B : (-FS (-filter -Byte 1) -top)) (-> -Nat -Byte B : (-FS -top (-and (-filter -Byte 0) (-filter -PosByte 1)))) - (-> -NonNegReal -Byte B : (-FS -top (-filter -PosByte 1))) - (-> -RealZero -Index B : (-FS (-filter -Zero 1) (-filter -PosIndex 1))) - (-> -Index -RealZero B : (-FS -top (-filter (Un) 0))) + (-> -NonNegRat -Byte B : (-FS -top (-filter -PosByte 1))) + (-> -Zero -Index B : (-FS (-filter -Zero 1) (-filter -PosIndex 1))) + (-> -Index -Zero B : (-FS -top (-filter (Un) 0))) (-> -Index -One B : (-FS (-filter -PosIndex 0) (-filter -Zero 0))) (-> -Index -PosIndex B : (-FS (-filter -PosIndex 0) -top)) (-> -Index -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) (-> -Index -PosReal B : (-FS (-filter -PosIndex 0) -top)) (-> -Pos -Index B : (-FS -top (-and (-filter -PosIndex 0) (-filter -PosIndex 1)))) - (-> -PosReal -Index B : (-FS -top (-filter -PosIndex 1))) + (-> -PosRat -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Nat B : (-FS (-filter -Index 1) -top)) (-> -Nat -Index B : (-FS -top (-and (-filter -Index 0) (-filter -PosIndex 1)))) - (-> -NonNegReal -Index B : (-FS -top (-filter -PosIndex 1))) - (-> -RealZero -NonNegFixnum B : (-FS (-filter -Zero 1) (-filter -PosFixnum 1))) - (-> -NonNegFixnum -RealZero B : (-FS (-filter -Zero 0) (-filter (Un) 0))) + (-> -NonNegRat -Index B : (-FS -top (-filter -PosIndex 1))) + (-> -Zero -NonNegFixnum B : (-FS (-filter -Zero 1) (-filter -PosFixnum 1))) + (-> -NonNegFixnum -Zero B : (-FS (-filter -Zero 0) (-filter (Un) 0))) (-> -NonNegFixnum -One B : (-FS -top (-filter -Zero 0))) - (-> -Fixnum -RealZero B : (-FS (-filter -NonNegFixnum 0) (-filter -NegFixnum 0))) - (-> -RealZero -Fixnum B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1))) + (-> -Fixnum -Zero B : (-FS (-filter -NonNegFixnum 0) (-filter -NegFixnum 0))) + (-> -Zero -Fixnum B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1))) (-> -Fixnum -PosInt B : (-FS (-and (-filter -PosFixnum 0) (-filter -PosFixnum 1)) -top)) (-> -Fixnum -PosReal B : (-FS (-filter -PosFixnum 0) -top)) (-> -Fixnum -Nat B : (-FS (-and (-filter -NonNegFixnum 0) (-filter -NonNegFixnum 1)) -top)) (-> -Fixnum -NonNegReal B : (-FS (-filter -NonNegFixnum 0) -top)) (-> -Nat -Fixnum B : (-FS -top (-and (-filter -NonNegFixnum 0) (-filter -PosFixnum 1)))) - (-> -NonNegReal -Fixnum B : (-FS -top (-filter -PosFixnum 1))) + (-> -NonNegRat -Fixnum B : (-FS -top (-filter -PosFixnum 1))) (-> -Fixnum -NonPosInt B : (-FS -top (-and (-filter -NegFixnum 0) (-filter -NonPosFixnum 1)))) - (-> -Fixnum -NonPosReal B : (-FS -top (-filter -NegFixnum 0))) + (-> -Fixnum -NonPosRat B : (-FS -top (-filter -NegFixnum 0))) (-> -NegInt -Fixnum B : (-FS (-and (-filter -NegFixnum 0) (-filter -NegFixnum 1)) -top)) (-> -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)) - (>=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt) - (>=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat) + (>=-type-pattern -Int -PosInt -Nat -NegInt -NonPosInt -Zero) + (>=-type-pattern -Rat -PosRat -NonNegRat -NegRat -NonPosRat -Zero) (>=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum) (>=-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) (>=-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal) @@ -1010,50 +1006,41 @@ (-> -NonPosRat -NonPosRat -NonPosRat -NonPosRat) (map varop (list -Rat -FlonumZero)) ; no pos * -> pos, possible underflow - ; no pos * -> non-neg, possible NaN: (* small small +inf.0) - (-> -PosFlonum -PosFlonum -NonNegFlonum) - (-> -NonNegFlonum -NonNegFlonum) - (varop-1+ (Un -NonNegFlonum -FlonumNan)) ; (* +inf.0 0.0) -> +nan.o + (varop-1+ -NonNegFlonum) (-> -NegFlonum -NegFlonum) (-> -NonPosFlonum -NonPosFlonum) ;; can't do NonPos NonPos -> NonNeg: (* -1.0 0.0) -> NonPos! (-> -NegFlonum -NegFlonum -NonNegFlonum) ; possible underflow, so no neg neg -> pos - (-> -NegFlonum -NegFlonum -NegFlonum (Un -NonPosFlonum -FlonumNan)) ; see above + (-> -NegFlonum -NegFlonum -NegFlonum -NonPosFlonum) ; see above ;; limited flonum contagion rules ;; (* 0) is exact 0 (i.e. not a float) - (commutative-case -NonNegFlonum -PosReal (Un -NonNegFlonum -FlonumNan)) ; real args don't include 0 + (commutative-case -NonNegFlonum -PosReal) ; real args don't include 0 (commutative-case -Flonum (Un -PosReal -NegReal) -Flonum) (map varop (list -Flonum -SingleFlonumZero)) - (-> -PosSingleFlonum -PosSingleFlonum -NonNegSingleFlonum) - (-> -NonNegSingleFlonum -NonNegSingleFlonum) - (varop-1+ (Un -NonNegSingleFlonum -FlonumNan)) + (varop-1+ -NonNegSingleFlonum) ;; we could add contagion rules for negatives, but we haven't for now (-> -NegSingleFlonum -NegSingleFlonum) (-> -NonPosSingleFlonum -NonPosSingleFlonum) (-> -NegSingleFlonum -NegSingleFlonum -NonNegSingleFlonum) ; possible underflow, so no neg neg -> pos - (-> -NegSingleFlonum -NegSingleFlonum -NegSingleFlonum (Un -NonPosSingleFlonum -SingleFlonumNan)) - (commutative-case -NonNegSingleFlonum (Un -PosRat -NonNegSingleFlonum) (Un -NonNegSingleFlonum -SingleFlonumNan)) + (-> -NegSingleFlonum -NegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) + (commutative-case -NonNegSingleFlonum (Un -PosRat -NonNegSingleFlonum)) (commutative-case -SingleFlonum (Un -PosRat -NegRat -SingleFlonum) -SingleFlonum) (map varop (list -SingleFlonum -InexactRealZero)) - (-> -PosInexactReal -PosInexactReal -NonNegInexactReal) - (-> -NonNegInexactReal -NonNegInexactReal) - (varop-1+ (Un -NonNegInexactReal -InexactRealNan)) + (varop-1+ -NonNegInexactReal) (-> -NegInexactReal -NegInexactReal) (-> -NonPosInexactReal -NonPosInexactReal) (-> -NegInexactReal -NegInexactReal -NonNegInexactReal) - (-> -NegInexactReal -NegInexactReal -NegInexactReal (Un -NonPosInexactReal -InexactRealNan)) - (commutative-case -NonNegInexactReal (Un -PosRat -NonNegInexactReal) (Un -NonNegInexactReal -SingleFlonumNan)) + (-> -NegInexactReal -NegInexactReal -NegInexactReal -NonPosInexactReal) + (commutative-case -NonNegInexactReal (Un -PosRat -NonNegInexactReal)) (commutative-case -InexactReal (Un -PosRat -NegRat -InexactReal) -InexactReal) (varop -InexactReal) ;; reals - (-> -PosReal -PosReal -NonNegReal) - (-> -NonNegReal -NonNegReal) - (varop-1+ (Un -NonNegReal -InexactRealNan)) ; (* +inf.0 0.0) -> +nan.0 + (varop-1+ -NonNegReal) ; (* +inf.0 0.0) -> +nan.0 (-> -NegReal -NegReal) (-> -NonPosReal -NonPosReal) (-> -NegReal -NegReal -NonNegReal) (commutative-binop -NegReal -PosReal -NonPosReal) - (-> -NegReal -NegReal -NegReal (Un -NonPosReal -InexactRealNan)) + (-> -NegReal -NegReal -NegReal -NonPosReal) (varop -Real) ;; complexes (commutative-case -FloatComplex (Un -InexactComplex -InexactReal -PosRat -NegRat) -FloatComplex) @@ -1179,46 +1166,39 @@ (-> -NonPosRat -NonPosRat -NonPosRat -NonPosRat) (varop-1+ -Rat) (-> -FlonumZero (Un -PosFlonum -NegFlonum)) ; one of the infinities - (varop-1+ -PosFlonum (Un -NonNegFlonum -FlonumNan)) ; possible underflow - ;; if we mix Pos and NonNeg (or just NonNeg), we go to Flonum: (/ +inf.0 0.0) -> NaN + ;; No (-> -NonNegFlonum -NonNegFlonum -NonNegFlonum), (/ 0.1 -0.0) => -inf.0 ;; No (-> -NonPosFlonum -NonPosFlonum), (/ 0.0) => +inf.0 - (-> -NegFlonum -NegFlonum (Un -NonNegFlonum -FlonumNan)) - (-> -NegFlonum -NegFlonum -NegFlonum (Un -NonPosFlonum -FlonumNan)) + (-> -NegFlonum -NegFlonum -NonNegFlonum) + (-> -NegFlonum -NegFlonum -NegFlonum -NonPosFlonum) ;; limited flonum contagion rules ;; (/ 0 ) is exact 0 (i.e. not a float) - (-> -PosFlonum -PosReal (Un -NonNegFlonum -FlonumNan)) - (-> -PosReal -PosFlonum (Un -NonNegFlonum -FlonumNan)) - (commutative-case -PosFlonum -PosReal (Un -NonNegFlonum -FlonumNan)) + (-> -PosFlonum -PosReal -NonNegFlonum) + (-> -PosReal -PosFlonum -NonNegFlonum) + (commutative-case -PosFlonum -PosReal -NonNegFlonum) (->* (list (Un -PosReal -NegReal -Flonum) -Flonum) -Flonum -Flonum) (->* (list -Flonum) -Real -Flonum) ; if any argument after the first is exact 0, not a problem (varop-1+ -Flonum) (-> -SingleFlonumZero (Un -PosSingleFlonum -NegSingleFlonum)) ; one of the infinities - (varop-1+ -PosSingleFlonum (Un -NonNegSingleFlonum -SingleFlonumNan)) ; possible underflow ;; we could add contagion rules for negatives, but we haven't for now - (-> -NegSingleFlonum -NegSingleFlonum (Un -NonNegSingleFlonum -SingleFlonumNan)) ; possible underflow, so no neg neg -> pos - (-> -NegSingleFlonum -NegSingleFlonum -NegSingleFlonum (Un -NonPosSingleFlonum -SingleFlonumNan)) - (-> -PosSingleFlonum (Un -PosRat -PosSingleFlonum) (Un -NonNegSingleFlonum -SingleFlonumNan)) - (-> (Un -PosRat -PosSingleFlonum) -PosSingleFlonum (Un -NonNegSingleFlonum -SingleFlonumNan)) - (commutative-case -PosSingleFlonum (Un -PosRat -PosSingleFlonum) (Un -NonNegSingleFlonum -SingleFlonumNan)) + (-> -NegSingleFlonum -NegSingleFlonum -NonNegSingleFlonum) ; possible underflow, so no neg neg -> pos + (-> -NegSingleFlonum -NegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum) + (commutative-case -PosSingleFlonum (Un -PosRat -PosSingleFlonum) -NonNegSingleFlonum) (commutative-case -SingleFlonum (Un -PosRat -NegRat -SingleFlonum) -SingleFlonum) (varop-1+ -SingleFlonum) (-> -InexactRealZero (Un -PosInexactReal -NegInexactReal)) - (varop-1+ -PosInexactReal (Un -NonNegInexactReal -InexactRealNan)) ; possible underflow - (-> -NegInexactReal -NegInexactReal (Un -NonNegInexactReal -InexactRealNan)) - (-> -NegInexactReal -NegInexactReal -NegInexactReal (Un -NonPosInexactReal -InexactRealNan)) - (-> -PosInexactReal (Un -PosRat -PosInexactReal) (Un -NonNegInexactReal -InexactRealNan)) - (-> (Un -PosRat -PosInexactReal) -PosInexactReal (Un -NonNegInexactReal -InexactRealNan)) - (commutative-case -PosInexactReal (Un -PosRat -PosInexactReal) (Un -NonNegInexactReal -InexactRealNan)) + (-> -NegInexactReal -NegInexactReal -NonNegInexactReal) + (-> -NegInexactReal -NegInexactReal -NegInexactReal -NonPosInexactReal) + (commutative-case -PosInexactReal (Un -PosRat -PosInexactReal) -NonNegInexactReal) (commutative-case -InexactReal (Un -PosRat -NegRat -InexactReal) -InexactReal) (varop-1+ -InexactReal) ;; reals (varop-1+ -PosReal) (-> -NegReal -NegReal) (-> -NonPosReal -NonPosReal) - (-> -NegReal -NegReal (Un -NonNegReal -InexactRealNan)) - (-> -NegReal -PosReal (Un -NonPosReal -InexactRealNan)) - (-> -PosReal -NegReal (Un -NonPosReal -InexactRealNan)) - (-> -NegReal -NegReal -NegReal (Un -NonPosReal -InexactRealNan)) + (-> -NegReal -NegReal -NonNegReal) + (-> -NegReal -PosReal -NonPosReal) + (-> -PosReal -NegReal -NonPosReal) + (-> -NegReal -NegReal -NegReal -NonPosReal) (varop-1+ -Real) ;; complexes (commutative-case -FloatComplex (Un -InexactComplex -InexactReal -PosRat -NegRat) -FloatComplex) @@ -1246,31 +1226,21 @@ -FlonumPosZero -FlonumNegZero -FlonumZero)) ;; inexactness is contagious: (max 3 2.3) => 3.0 ;; we could add cases to encode that - ;; because of NaN propagation, can't have arbitrary Flonum on rhs - (commutative-case -PosFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case -PosFlonum -Flonum (Un -PosFlonum -FlonumNan)) - (varop -NonNegFlonum) - (commutative-case -NonNegFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case -NonNegFlonum -Flonum (Un -NonNegFlonum -FlonumNan)) + (commutative-case -PosFlonum -Flonum) + (commutative-case -NonNegFlonum -Flonum) (map varop (list -NegFlonum -NonPosFlonum -Flonum -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero)) - (commutative-case -PosSingleFlonum (Un -NonNegSingleFlonum -NonPosSingleFlonum)) - (commutative-case -PosSingleFlonum -SingleFlonum (Un -PosSingleFlonum -SingleFlonumNan)) + (commutative-case -PosSingleFlonum -SingleFlonum) (varop -NonNegSingleFlonum) - (commutative-case -NonNegSingleFlonum (Un -NonNegSingleFlonum -NonPosSingleFlonum)) - (commutative-case -NonNegSingleFlonum -SingleFlonum (Un -NonNegSingleFlonum -SingleFlonumNan)) + (commutative-case -NonNegSingleFlonum -SingleFlonum) (map varop (list -NegSingleFlonum -NonPosSingleFlonum -SingleFlonum -InexactRealPosZero -InexactRealNegZero -InexactRealZero)) - (commutative-case -PosInexactReal (Un -NonNegInexactReal -NonPosInexactReal)) - (commutative-case -PosInexactReal -InexactReal (Un -PosInexactReal -InexactRealNan)) - (varop -NonNegInexactReal) - (commutative-case -NonNegInexactReal (Un -NonNegInexactReal -NonPosInexactReal)) - (commutative-case -NonNegInexactReal -InexactReal (Un -NonNegInexactReal -InexactRealNan)) + (commutative-case -PosInexactReal -InexactReal) + (commutative-case -NonNegInexactReal -InexactReal) (map varop (list -NegInexactReal -NonPosInexactReal -InexactReal -RealZero)) - (commutative-case -PosReal (Un -NonNegReal -NonPosReal)) - (varop -NonNegReal) - (commutative-case -NonNegReal (Un -NonNegInexactReal -NonPosInexactReal)) + (commutative-case -PosReal -Real) + (commutative-case -NonNegReal -Real) (map varop (list -NegReal -NonPosReal -Real)))] [min (from-cases (map varop (list -Zero -One)) @@ -1284,32 +1254,22 @@ (map varop (list -Rat -FlonumPosZero -FlonumNegZero -FlonumZero -PosFlonum -NonNegFlonum)) - (commutative-case -NegFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case -NegFlonum -Flonum (Un -NegFlonum -FlonumNan)) - (varop -NonPosFlonum) - (commutative-case -NonPosFlonum (Un -NonNegFlonum -NonPosFlonum)) - (commutative-case -NonPosFlonum -Flonum (Un -NonPosFlonum -FlonumNan)) + (commutative-case -NegFlonum -Flonum) + (commutative-case -NonPosFlonum -Flonum) (map varop (list -Flonum -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumZero -PosSingleFlonum -NonNegSingleFlonum)) - (commutative-case -NegSingleFlonum (Un -NonNegSingleFlonum -NonPosSingleFlonum)) - (commutative-case -NegSingleFlonum -SingleFlonum (Un -NegSingleFlonum -SingleFlonumNan)) - (varop -NonPosSingleFlonum) - (commutative-case -NonPosSingleFlonum (Un -NonNegSingleFlonum -NonPosSingleFlonum)) - (commutative-case -NonPosSingleFlonum -SingleFlonum (Un -NonPosSingleFlonum -SingleFlonumNan)) + (commutative-case -NegSingleFlonum -SingleFlonum) + (commutative-case -NonPosSingleFlonum -SingleFlonum) (map varop (list -SingleFlonum -InexactRealPosZero -InexactRealNegZero -InexactRealZero -PosInexactReal -NonNegInexactReal)) - (commutative-case -NegInexactReal (Un -NonNegInexactReal -NonPosInexactReal)) - (commutative-case -NegInexactReal -InexactReal (Un -NegInexactReal -InexactRealNan)) - (varop -NonPosInexactReal) - (commutative-case -NonPosInexactReal (Un -NonNegInexactReal -NonPosInexactReal)) - (commutative-case -NonPosInexactReal -InexactReal (Un -NonPosInexactReal -InexactRealNan)) + (commutative-case -NegInexactReal -InexactReal) + (commutative-case -NonPosInexactReal -InexactReal) (map varop (list -InexactReal -RealZero -PosReal -NonNegReal)) - (commutative-case -NegReal (Un -NonNegReal -NonPosReal)) - (varop -NonPosReal) - (commutative-case -NonPosReal (Un -NonNegReal -NonPosReal)) + (commutative-case -NegReal -Real) + (commutative-case -NonPosReal -Real) (varop -Real))] [add1 (from-cases @@ -1507,18 +1467,15 @@ (-Rat . -> . -NonNegRat) (-FlonumZero . -> . -FlonumZero) ((Un -PosFlonum -NegFlonum) . -> . -PosFlonum) - ((Un -NonNegFlonum -NonPosFlonum) . -> . -NonNegFlonum) - (-Flonum . -> . (Un -NonNegFlonum -FlonumNan)) ; can't guarantee NonNeg becauseof NaN + (-Flonum . -> . -NonNegFlonum) (-SingleFlonumZero . -> . -SingleFlonumZero) ((Un -PosSingleFlonum -NegSingleFlonum) . -> . -PosSingleFlonum) - ((Un -NonNegSingleFlonum -NonPosSingleFlonum) . -> . -NonNegSingleFlonum) - (-SingleFlonum . -> . (Un -NonNegSingleFlonum -SingleFlonumNan)) + (-SingleFlonum . -> . -NonNegSingleFlonum) (-InexactRealZero . -> . -InexactRealZero) ((Un -PosInexactReal -NegInexactReal) . -> . -PosInexactReal) - ((Un -NonNegInexactReal -NonPosInexactReal) . -> . -NonNegInexactReal) - (-InexactReal . -> . (Un -NonNegInexactReal -InexactRealNan)) + (-InexactReal . -> . -NonNegInexactReal) ((Un -PosReal -NegReal) . -> . -PosReal) - (-Real . -> . (Un -NonNegReal -InexactRealNan)))] + (-Real . -> . -NonNegReal))] ;; exactness [exact->inexact @@ -1671,15 +1628,12 @@ (-NonNegRat -Int . -> . -NonNegRat) (-Rat -Int . -> . -Rat) (-Rat -Rat . -> . -ExactNumber) - (-PosFlonum (Un -NegReal -PosReal) . -> . -PosFlonum) + (-PosFlonum -Real . -> . -PosFlonum) (-PosReal -Flonum . -> . -PosFlonum) - (-NonNegFlonum (Un -NegReal -PosReal) . -> . -NonNegFlonum) + (-NonNegFlonum -Real . -> . -NonNegFlonum) (-NonNegReal -Flonum . -> . -NonNegFlonum) - (-PosSingleFlonum (Un -SingleFlonum -NegRat -PosRat) . -> . -PosSingleFlonum) (-NonNegSingleFlonum (Un -SingleFlonum -NegRat -PosRat) . -> . -NonNegSingleFlonum) - (-PosInexactReal (Un -NegReal -PosReal) . -> . -PosInexactReal) (-NonNegInexactReal (Un -NegReal -PosReal) . -> . -NonNegInexactReal) - (-PosReal -Real . -> . -PosReal) (-NonNegReal -Real . -> . -NonNegReal) (-Flonum (Un -NegInt -PosInt) . -> . -Flonum) (-Flonum -Real . -> . N) @@ -1836,14 +1790,11 @@ (-> -Int -Nat) (unop -PosRat) (-> -Rat -NonNegRat) - (-> -NonNegFlonum -NonNegFlonum) ; possible underflow, no pos -> pos - (-> -Flonum (Un -NonNegFlonum -FlonumNan)) - (-> -NonNegSingleFlonum -NonNegSingleFlonum) - (-> -SingleFlonum (Un -NonNegSingleFlonum -SingleFlonumNan)) - (-> -NonNegInexactReal -NonNegInexactReal) - (-> -InexactReal (Un -NonNegInexactReal -InexactRealNan)) - (-> -NonNegReal -NonNegReal) - (-> -Real (Un -NonNegReal -InexactRealNan)) + ;; possible underflow, no pos -> pos + (-> -Flonum -NonNegFlonum) + (-> -SingleFlonum -NonNegSingleFlonum) + (-> -InexactReal -NonNegInexactReal) + (-> -Real -NonNegReal) (map unop (list -FloatComplex -SingleFlonumComplex -InexactComplex -ExactNumber N)))] [conjugate (from-cases @@ -1866,9 +1817,9 @@ -FloatComplex -SingleFlonumComplex -InexactComplex N)))] [cosh (from-cases ; no exact cases (map unop (list -FlonumNan -SingleFlonumNan)) - ((Un -Rat -Flonum) . -> . (Un -PosFlonum -FlonumNan)) - (-SingleFlonum . -> . (Un -PosSingleFlonum -SingleFlonumNan)) - (-InexactReal . -> . (Un -PosInexactReal -InexactRealNan)) + ((Un -Rat -Flonum) . -> . -PosFlonum) + (-SingleFlonum . -> . -PosSingleFlonum) + (-InexactReal . -> . -PosInexactReal) (-Real . -> . -PosReal) (map unop (list -FloatComplex -SingleFlonumComplex -InexactComplex N)))] [tanh (from-cases ; same as sinh @@ -1929,7 +1880,7 @@ (-> (Un -Rat -Flonum -SingleFlonum -InexactReal -Real) -Int))] [nan? (from-cases - (-> (Un -PosFlonum -NonPosFlonum -PosSingleFlonum -NonPosSingleFlonum -Rat) (-val #f)) + (-> -Rat (-val #f)) (-> (Un -FlonumNan -SingleFlonumNan) (-val #t)) (-> -Real B))] diff --git a/collects/typed-racket/types/numeric-tower.rkt b/collects/typed-racket/types/numeric-tower.rkt index 2d9d1cca..45051b90 100644 --- a/collects/typed-racket/types/numeric-tower.rkt +++ b/collects/typed-racket/types/numeric-tower.rkt @@ -131,6 +131,11 @@ (define -Rat (*Un -NegRat -Zero -PosRat)) ;; Floating-point numbers +;; NaN is included in all floating-point types +(define -FlonumNan (make-Base 'Float-Nan + #'(and/c flonum? (lambda (x) (eqv? x +nan.0))) + (lambda (x) (and (flonum? x) (eqv? x +nan.0))) + #'-FlonumNan)) (define -FlonumPosZero (make-Base 'Float-Positive-Zero #'(lambda (x) (eqv? x 0.0)) (lambda (x) (eqv? x 0.0)) @@ -139,25 +144,27 @@ #'(lambda (x) (eqv? x -0.0)) (lambda (x) (eqv? x -0.0)) #'-FlonumNegZero)) -(define -FlonumZero (*Un -FlonumPosZero -FlonumNegZero)) -(define -FlonumNan (make-Base 'Float-Nan - #'(and/c flonum? (lambda (x) (eqv? x +nan.0))) - (lambda (x) (and (flonum? x) (eqv? x +nan.0))) - #'-FlonumNan)) -(define -PosFlonum - (make-Base 'Positive-Float +(define -FlonumZero (*Un -FlonumPosZero -FlonumNegZero -FlonumNan)) +(define -PosFlonumNoNan + (make-Base 'Positive-Float-No-NaN #'(and/c flonum? positive?) (lambda (x) (and (flonum? x) (positive? x))) - #'-PosFlonum)) + #'-PosFlonumNoNan)) +(define -PosFlonum (*Un -PosFlonumNoNan -FlonumNan)) (define -NonNegFlonum (*Un -PosFlonum -FlonumZero)) -(define -NegFlonum - (make-Base 'Negative-Float +(define -NegFlonumNoNan + (make-Base 'Negative-Float-No-NaN #'(and/c flonum? negative?) (lambda (x) (and (flonum? x) (negative? x))) - #'-NegFlonum)) + #'-NegFlonumNoNan)) +(define -NegFlonum (*Un -NegFlonumNoNan -FlonumNan)) (define -NonPosFlonum (*Un -NegFlonum -FlonumZero)) -(define -Flonum (*Un -NegFlonum -FlonumNegZero -FlonumPosZero -PosFlonum -FlonumNan)) ; 64-bit floats +(define -Flonum (*Un -NegFlonumNoNan -FlonumNegZero -FlonumPosZero -PosFlonumNoNan -FlonumNan)) ; 64-bit floats ;; inexact reals can be flonums (64-bit floats) or 32-bit floats +(define -SingleFlonumNan (make-Base 'Single-Flonum-Nan + #'(and/c single-flonum? (lambda (x) (eqv? x +nan.f))) + (lambda (x) (and (single-flonum? x) (eqv? x +nan.f))) + #'-SingleFlonumNan)) (define -SingleFlonumPosZero ; disjoint from Flonum 0s (make-Base 'Single-Flonum-Positive-Zero ;; eqv? equates 0.0f0 with itself, but not eq? @@ -171,29 +178,28 @@ #'(and/c single-flonum? (lambda (x) (eqv? x -0.0f0))) (lambda (x) #f) #'-SingleFlonumNegZero)) -(define -SingleFlonumZero (*Un -SingleFlonumPosZero -SingleFlonumNegZero)) -(define -SingleFlonumNan (make-Base 'Single-Flonum-Nan - #'(and/c single-flonum? (lambda (x) (eqv? x +nan.f))) - (lambda (x) (and (single-flonum? x) (eqv? x +nan.f))) - #'-SingleFlonumNan)) +(define -SingleFlonumZero (*Un -SingleFlonumPosZero -SingleFlonumNegZero -SingleFlonumNan)) +(define -InexactRealNan (*Un -FlonumNan -SingleFlonumNan)) (define -InexactRealPosZero (*Un -SingleFlonumPosZero -FlonumPosZero)) (define -InexactRealNegZero (*Un -SingleFlonumNegZero -FlonumNegZero)) (define -InexactRealZero (*Un -InexactRealPosZero - -InexactRealNegZero)) -(define -InexactRealNan (*Un -FlonumNan -SingleFlonumNan)) -(define -PosSingleFlonum - (make-Base 'Positive-Single-Flonum + -InexactRealNegZero + -InexactRealNan)) +(define -PosSingleFlonumNoNan + (make-Base 'Positive-Single-Flonum-No-Nan #'(and/c single-flonum? positive?) (lambda (x) #f) - #'-PosSingleFlonum)) + #'-PosSingleFlonumNoNan)) +(define -PosSingleFlonum (*Un -PosSingleFlonumNoNan -SingleFlonumNan)) (define -PosInexactReal (*Un -PosSingleFlonum -PosFlonum)) (define -NonNegSingleFlonum (*Un -PosSingleFlonum -SingleFlonumZero)) (define -NonNegInexactReal (*Un -PosInexactReal -InexactRealZero)) -(define -NegSingleFlonum - (make-Base 'Negative-Single-Flonum +(define -NegSingleFlonumNoNan + (make-Base 'Negative-Single-Flonum-No-Nan #'(and/c single-flonum? negative?) (lambda (x) #f) - #'-NegSingleFlonum)) + #'-NegSingleFlonumNoNan)) +(define -NegSingleFlonum (*Un -NegSingleFlonumNoNan -SingleFlonumNan)) (define -NegInexactReal (*Un -NegSingleFlonum -NegFlonum)) (define -NonPosSingleFlonum (*Un -NegSingleFlonum -SingleFlonumZero)) (define -NonPosInexactReal (*Un -NegInexactReal -InexactRealZero))