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

Fix filters of comparisons in the presence of NaN.

Browse Source 
Closes #112.
This commit is contained in:
Vincent St-Amour 2017-03-28 15:28:52 -05:00
parent 1f28ae53cd
commit 52b4507585
2 changed files with 70 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

114
typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
View File

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

8
typed-racket-test/fail/gh112.rkt Normal file
View File

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