From 52b450758524464213bf341785db007a10719b18 Mon Sep 17 00:00:00 2001 From: Vincent St-Amour Date: Tue, 28 Mar 2017 15:28:52 -0500 Subject: [PATCH] Fix filters of comparisons in the presence of NaN. Closes #112. --- .../base-env/base-env-numeric.rkt | 114 ++++++++++-------- typed-racket-test/fail/gh112.rkt | 8 ++ 2 files changed, 70 insertions(+), 52 deletions(-) create mode 100644 typed-racket-test/fail/gh112.rkt diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index 82a3d4bc..685b42af 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -596,43 +596,53 @@ ;; There's a repetitive pattern in the types of each comparison operator. ;; As explained below, this is because props don't do intersections. - (define (<-type-pattern base pos non-neg neg non-pos [zero -RealZero]) - (list (-> base zero B : (-PS (-is-type 0 neg) (-is-type 0 non-neg))) - (-> zero base B : (-PS (-is-type 1 pos) (-is-type 1 non-pos))) - (-> base -PosReal B : (-PS -tt (-is-type 0 pos))) - (-> base -NonNegReal B : (-PS -tt (-is-type 0 non-neg))) - (-> -NonNegReal base B : (-PS (-is-type 1 pos) -tt)) - (-> base -NonPosReal B : (-PS (-is-type 0 neg) -tt)) - (-> -NegReal base B : (-PS -tt (-is-type 1 neg))) - (-> -NonPosReal base B : (-PS -tt (-is-type 1 non-pos))))) - (define (>-type-pattern base pos non-neg neg non-pos [zero -RealZero]) - (list (-> base zero B : (-PS (-is-type 0 pos) (-is-type 0 non-pos))) - (-> zero base B : (-PS (-is-type 1 neg) (-is-type 1 non-neg))) - (-> base -NonNegReal B : (-PS (-is-type 0 pos) -tt)) - (-> -PosReal base B : (-PS -tt (-is-type 1 pos))) - (-> -NonNegReal base B : (-PS -tt (-is-type 1 non-neg))) - (-> -NonPosReal base B : (-PS (-is-type 1 neg) -tt)) - (-> base -NegReal B : (-PS -tt (-is-type 0 neg))) - (-> base -NonPosReal B : (-PS -tt (-is-type 0 non-pos))))) + ;; Cases that may include NaN don't learn anything when a comparison returns + ;; false, because anything at all compared to NaN is always false. + (define (<-type-pattern base pos non-neg neg non-pos [zero -RealZero] + #:no-false-props? [no-false-props? #f]) + (define (-PS* t f) (-PS t (if no-false-props? -tt f))) + (list (-> base zero B : (-PS* (-is-type 0 neg) (-is-type 0 non-neg))) + (-> zero base B : (-PS* (-is-type 1 pos) (-is-type 1 non-pos))) + (-> base -PosReal B : (-PS* -tt (-is-type 0 pos))) + (-> base -NonNegReal B : (-PS* -tt (-is-type 0 non-neg))) + (-> -NonNegReal base B : (-PS* (-is-type 1 pos) -tt)) + (-> base -NonPosReal B : (-PS* (-is-type 0 neg) -tt)) + (-> -NegReal base B : (-PS* -tt (-is-type 1 neg))) + (-> -NonPosReal base B : (-PS* -tt (-is-type 1 non-pos))))) + (define (>-type-pattern base pos non-neg neg non-pos [zero -RealZero] + #:no-false-props? [no-false-props? #f]) + (define (-PS* t f) (-PS t (if no-false-props? -tt f))) + (list (-> base zero B : (-PS* (-is-type 0 pos) (-is-type 0 non-pos))) + (-> zero base B : (-PS* (-is-type 1 neg) (-is-type 1 non-neg))) + (-> base -NonNegReal B : (-PS* (-is-type 0 pos) -tt)) + (-> -PosReal base B : (-PS* -tt (-is-type 1 pos))) + (-> -NonNegReal base B : (-PS* -tt (-is-type 1 non-neg))) + (-> -NonPosReal base B : (-PS* (-is-type 1 neg) -tt)) + (-> base -NegReal B : (-PS* -tt (-is-type 0 neg))) + (-> base -NonPosReal B : (-PS* -tt (-is-type 0 non-pos))))) ;; this is > with flipped props - (define (<=-type-pattern base pos non-neg neg non-pos [zero -RealZero]) - (list (-> base zero B : (-PS (-is-type 0 non-pos) (-is-type 0 pos))) - (-> zero base B : (-PS (-is-type 1 non-neg) (-is-type 1 neg))) - (-> base -NonNegReal B : (-PS -tt (-is-type 0 pos))) - (-> -PosReal base B : (-PS (-is-type 1 pos) -tt)) - (-> -NonNegReal base B : (-PS (-is-type 1 non-neg) -tt)) - (-> -NonPosReal base B : (-PS -tt (-is-type 1 neg))) - (-> base -NegReal B : (-PS (-is-type 0 neg) -tt)) - (-> base -NonPosReal B : (-PS (-is-type 0 non-pos) -tt)))) - (define (>=-type-pattern base pos non-neg neg non-pos [zero -RealZero]) - (list (-> base zero B : (-PS (-is-type 0 non-neg) (-is-type 0 neg))) - (-> zero base B : (-PS (-is-type 1 non-pos) (-is-type 1 pos))) - (-> base -PosReal B : (-PS (-is-type 0 pos) -tt)) - (-> base -NonNegReal B : (-PS (-is-type 0 non-neg) -tt)) - (-> -NonNegReal base B : (-PS -tt (-is-type 1 pos))) - (-> base -NonPosReal B : (-PS -tt (-is-type 0 neg))) - (-> -NegReal base B : (-PS (-is-type 1 neg) -tt)) - (-> -NonPosReal base B : (-PS (-is-type 1 non-pos) -tt)))) + (define (<=-type-pattern base pos non-neg neg non-pos [zero -RealZero] + #:no-false-props? [no-false-props? #f]) + (define (-PS* t f) (-PS t (if no-false-props? -tt f))) + (list (-> base zero B : (-PS* (-is-type 0 non-pos) (-is-type 0 pos))) + (-> zero base B : (-PS* (-is-type 1 non-neg) (-is-type 1 neg))) + (-> base -NonNegReal B : (-PS* -tt (-is-type 0 pos))) + (-> -PosReal base B : (-PS* (-is-type 1 pos) -tt)) + (-> -NonNegReal base B : (-PS* (-is-type 1 non-neg) -tt)) + (-> -NonPosReal base B : (-PS* -tt (-is-type 1 neg))) + (-> base -NegReal B : (-PS* (-is-type 0 neg) -tt)) + (-> base -NonPosReal B : (-PS* (-is-type 0 non-pos) -tt)))) + (define (>=-type-pattern base pos non-neg neg non-pos [zero -RealZero] + #:no-false-props? [no-false-props? #f]) + (define (-PS* t f) (-PS t (if no-false-props? -tt f))) + (list (-> base zero B : (-PS* (-is-type 0 non-neg) (-is-type 0 neg))) + (-> zero base B : (-PS* (-is-type 1 non-pos) (-is-type 1 pos))) + (-> base -PosReal B : (-PS* (-is-type 0 pos) -tt)) + (-> base -NonNegReal B : (-PS* (-is-type 0 non-neg) -tt)) + (-> -NonNegReal base B : (-PS* -tt (-is-type 1 pos))) + (-> base -NonPosReal B : (-PS* -tt (-is-type 0 neg))) + (-> -NegReal base B : (-PS* (-is-type 1 neg) -tt)) + (-> -NonPosReal base B : (-PS* (-is-type 1 non-pos) -tt)))) (define (negation-pattern pos neg non-neg non-pos) (list (-> pos neg) @@ -806,10 +816,10 @@ ;; In the meantime, repetition is hard to avoid. (<-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) - (<-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal) + (<-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum #:no-false-props? #t) + (<-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum #:no-false-props? #t) + (<-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal #:no-false-props? #t) + (<-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal #:no-false-props? #t) (->* (list R R) R B))] [> (from-cases (-> -One -Int B : (-PS (-is-type 1 -NonPosInt) (-is-type 1 -PosInt))) @@ -855,10 +865,10 @@ (-> -NegInfinity -Real B : -false-propset) (>-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) - (>-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal) + (>-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum #:no-false-props? #t) + (>-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum #:no-false-props? #t) + (>-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal #:no-false-props? #t) + (>-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal #:no-false-props? #t) (->* (list R R) R B))] [<= (from-cases (-> -Int -One B : (-PS (-is-type 0 (Un -NonPosInt -One)) (-is-type 0 -PosInt))) @@ -903,10 +913,10 @@ (-> -Real -NegInfinity B : (-PS (-is-type 0 -NegInfinity) (-not-type 0 -NegInfinity))) (<=-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) - (<=-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal) + (<=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum #:no-false-props? #t) + (<=-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum #:no-false-props? #t) + (<=-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal #:no-false-props? #t) + (<=-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal #:no-false-props? #t) (->* (list R R) R B))] [>= (from-cases (-> -One -Int B : (-PS (-is-type 1 (Un -One -NonPosInt)) (-is-type 1 -PosInt))) @@ -951,10 +961,10 @@ (-> -NegInfinity -Real B : (-PS (-is-type 1 -NegInfinity) (-not-type 1 -NegInfinity))) (>=-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) - (>=-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal) + (>=-type-pattern -Flonum -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum #:no-false-props? #t) + (>=-type-pattern -SingleFlonum -PosSingleFlonum -NonNegSingleFlonum -NegSingleFlonum -NonPosSingleFlonum #:no-false-props? #t) + (>=-type-pattern -InexactReal -PosInexactReal -NonNegInexactReal -NegInexactReal -NonPosInexactReal #:no-false-props? #t) + (>=-type-pattern -Real -PosReal -NonNegReal -NegReal -NonPosReal #:no-false-props? #t) (->* (list R R) R B))] [* (from-cases diff --git a/typed-racket-test/fail/gh112.rkt b/typed-racket-test/fail/gh112.rkt new file mode 100644 index 00000000..002f4bb4 --- /dev/null +++ b/typed-racket-test/fail/gh112.rkt @@ -0,0 +1,8 @@ +#lang typed/racket + +(ann + (let ([x : Flonum -5.0]) + (if (< x (ann +nan.0 Positive-Flonum)) + 1.0 + x)) + Positive-Flonum) ; -5 is *not* positive