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

Include NaN in all floating-point types.

Browse Source 
Makes more closure properties hold, but weakens occurrence typing for
some comparisons involving flonums.

original commit: a6d5a98b61c033340c66b91dd53c18ea50db8c60
This commit is contained in:
Vincent St-Amour 2012-07-24 17:52:14 -04:00
parent 5c4b0895dd
commit 90741c2747
3 changed files with 193 additions and 236 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -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

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

@ -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
;; (* <float> 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 <float>) 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))]

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

@ -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))