suzanne.soy/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.
This commit is contained in:
Vincent St-Amour 2012-07-24 17:52:14 -04:00
parent b1fbbafd91
commit a6d5a98b61
4 changed files with 318 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))]

125
collects/typed-racket/optimizer/tool/TODO Normal file
View File

@ -0,0 +1,125 @@
OC TODO
Oh, also the optimization-coach-callback should probably not erase the
user's interactions (what it currently does).
Instead, it would be better to do something like what check syntax
does, namely create another control embedded in the window that
contains the error message (and a "hide" button).
Robby
tool-tips instead of popups
have highlights to the end of lines
to capture right-clicks properly, maybe ask canvas directly if event is in
the right place. I dunno.
The way things are set up in the editor, there are kind of "two
regions" of coordinates. The editor knows only about those pixels that
go as far as the widest line in the editor. After that, you have to
use the canvas% object that the editor is inside. I forget how all
this goes, but I think you should try poking around in the canvas when
you get #f back or something like that. -- Robby
maybe look at ryan's code: macro-debugger/syntax-brower/text.rkt, ~l382
move to toplevel collect once we figure out long-term way to invoke OC
at that point, move docs to their own document
that involves changing a #:tag, or something, that Robby put there
for inlining, ignore when fuel is too low, etc. what we say we do in the paper
for each pop-up entry, have button: "show me where" that circles (not
highlights) the piece of code in the defs window
merge opts too, have goodness measure, and multiple shades of green
when merging opts, highlight (in green, in popup) the specific
operations that are optimized
set-clickback can do highlighting, there's a style delta arg
good to know if I go back to sth like that
run OC in a separate place, using the online compilation API?
inlining recommendations: point to racket/performance-hint ?
TR recommendations: point to exact->inexact, flsqrt, etc
add a link/button to popups that circles code (of a popup entry) in defs win
have inliner logs be in sexp format
-> argh, paths are not readable
paper says we use ratio of inlinings and missed inlining. we currently
just use subtractions
also, all kinds of opts share the same scale
checkboxes to enable / disable each may alleviate the problem
better integrate inliner logging with what matthew already had?
;; TODO should have o-o-f that missed by only a little count for less. we mention in paper
;; TODO also, change recommendation depending on how close the misses were, give an idea of how much the function needs to be reduced
move structs defs from optimizer/logging.rkt to PR. and maybe other things too
;; TODO don't show checkbox for TR opts when not in TR
;; TODO ignore all loops (heck, maybe even identifiers that contain
"loop", since they pretty much only ever add noise
-> (months after original comment): is it still as bad with
unrollings considered separately? yeah, probably
+ ;; TODO -> so maybe, if there are unrollings at all, don't say anything at all!
;; TODO other heuristic: discard events that have to do with identifiers
not in the program (or better, not in the region that would be
highlighted). would get rid of procs introduces by macros (for-loop,
stuff from match, etc.)
;; `f' is a loop. We ignore anything beyond the first inlining
;; in `g'.
+ ;; TODO ignore beyond, or ignore the whole thing? currently, the latter is implemented
(apply
append
(for/list ([site (in-list inlining-sites)]
+;; TODO information is better targeted w/o inliner info. The problem is that
+;; inlining basically highlights entire functions, and pretty much all of them.
+;; This means that any finer grained regions in the function get merged.
+;; TODO solution: highlight only function name -- i.e. (define (_f_ x) ...)
+;; or, if lambda, highlight the lambda itself. etc.
+;; TODO OOPS: doesn't work with stuff like for-loop, which is introduced by expansion
+;; TODO maybe a better solution is better handling of nesting. show nested regions
+;; (with the inner one being redder, or red as opposed to green, etc.), and only when
+;; clicking on the inner one do you get the whole thing (inner and outer)
we can use unrollings to determine whether a function is a loop or not!
conservative, but sounds like it would work!
if a function is unrolled, we assume it's a loop.
THEN
if we're in a loop, we can do more aggressive recommentations:
- struct -> vector
- hoist parameter-using funcs (e.g. print / random, if not passed the
port / prng arg, will implicitly do a parameter lookup. _but_, they
can also be passed the port / prng. if you're in a loop, you probably
want to lookup the param once, outside the loop, then pass it to print
/ random)
future opts to report:
hidden parameterizations (e.g. write, when called, looks up value for
current-output-port, if you call it in a loop, you look up value n times.
write also takes an extra port argument. if you look up current-output-port
yourself once outside the loop, then pass that to write every time, win.)
where closures get allocated

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