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

Fix occurrence typing when comparing Byte and Positive-Rationa.

Browse Source 
Closes PR14568.

original commit: 8b6d3e9117667ccd5cdde9dabea0c2a843e7fb63
This commit is contained in:
Vincent St-Amour 2014-06-13 21:59:56 -07:00
parent 2170e9f6d6
commit 97ac1da181
3 changed files with 39 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1178,7 +1178,7 @@
(-> -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))))
(-> -PosRat -Byte B : (-FS -top (-filter -PosByte 0)))
(-> -PosRat -Byte B : (-FS -top (-filter -PosByte 1)))
(-> -Byte -Nat B : (-FS (-filter -Byte 1) -top))
(-> -Nat -Byte B : (-FS -top (-and (-filter -Byte 0) (-filter -PosByte 1))))
(-> -NonNegRat -Byte B : (-FS -top (-filter -PosByte 1)))

20
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/pr14568.rkt Normal file
View File

@ -0,0 +1,20 @@
#;
(exn-pred 1)
#lang typed/racket
(: rational->fle (-> Exact-Rational (Values Flonum Flonum)))
(define (rational->fle r)
(let-values ([(s r) (values (sgn r) (abs r))])
(define e
(- (integer-length (numerator r))
(integer-length (denominator r))))
(let loop ([r (/ r (expt 2 e))] [e e])
(cond [(< r 1) (loop (* r 2) (- e 1))]
[(>= r 2) (loop (/ r 2) (+ e 1))]
[else
(ann r Positive-Byte) ; should not typecheck
(values (* (real->double-flonum s)
(real->double-flonum r)) ; optimizer changes to ->fl
(real->double-flonum e))]))))
(rational->fle 1/7) ; optimization causes contract violation

18
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr14568.rkt Normal file
View File

@ -0,0 +1,18 @@
#lang typed/racket
(: rational->fle (-> Exact-Rational (Values Flonum Flonum)))
(define (rational->fle r)
(let-values ([(s r) (values (sgn r) (abs r))])
(define e
(- (integer-length (numerator r))
(integer-length (denominator r))))
(let loop ([r (/ r (expt 2 e))] [e e])
(cond [(< r 1) (loop (* r 2) (- e 1))]
[(>= r 2) (loop (/ r 2) (+ e 1))]
[else
;; (ann r Positive-Byte) ; wrongly typechecks
(values (* (real->double-flonum s)
(real->double-flonum r)) ; optimizer changes to ->fl
(real->double-flonum e))]))))
(rational->fle 1/7) ; optimization causes contract violation