On 06/05/2012 03:57 PM, Vincent St-Amour wrote:
At Tue, 05 Jun 2012 15:45:09 -0600,
Neil Toronto wrote:
Vincent, is there a quick way for me to test whether the types I give
the new functions are sound?
I recently added redex-based random testing for TR's float types. It's
in collects/tests/typed-racket/tr-random-testing.rkt.
Currently, it only tests flonum (i.e. double precision) operations and
types, but it should be easy to expand to single-flonums.
Thanks! I've adapted it and will commit the changes with the ones to
racket/math.
I've managed to make it always find a counterexample. But there are only
a few single-flonum -> flonum issues. Most of them are because I've
changed the random-flonum-generating code to sometimes generate *very*
small random numbers. Here's the counterexample I found earlier today
that motivated that change to the random testing:
#lang typed/racket
(require/typed
unstable/flonum
[+min.0 Positive-Float]) ; the smallest positive flonum
> +min.0
- : Float [generalized from Positive-Float]
4.9406564584125e-324
> (sqr +min.0)
- : Float [generalized from Positive-Float]
0.0
I'm not comfortable messing with those precise primitive types yet, so
I'll let you handle that. When I push my commits tomorrow,
tr-random-testing.rkt will fail. After you've fixed the erroneous types,
I'll be able to use your fixes to figure out the right types for the
functions I added to racket/math.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
