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