Add a float shrinker

[jmid]

The Shrink module is missing a float shrinker. Part of the issue is figuring out what the shrinker should do, perhaps by researching the heuristics other frameworks use. For example, a halving heuristic is not going to work well for floats.

[c-cube]

good point, but I also have no idea on what well founded order on floats we could use. This needs someone to research the literature and implement it :)

[Gbury]

Maybe the shrinker could look at the floats' bit patterns rather than interpretation as a decimal number ? (and try and minimize the number of 1s in the bits for instance (which in effect should match low, or at least simple numbers ?))

[c-cube]

That doesn't seem very intuitive though (as in, doesn't "simplify" a counter-example much).

I wonder if we could start with something that subtract epsilon_float (taking care that it does yield a smaller float, though) and also tries to return [infinity, -. infinity, 0.] to get the "base" cases?

[jmid]

Would it be a viable strategy to shrink the 'mantissa' and 'exponent' separately? I suppose halving (or subtracting) could work for the exponent at least. E.g. 1.323 * 10^18 --> 1.323 * 10^9 or 1.323 * 10^-18 --> 1.323 * 10^-9 (edit: in binary the exponent is a power of two, but I think the idea still works) It is less clear to me how to simplify the mantissa (it should probably rewrite into something that shortens the decimal representation - rather than adding decimals... 🙂)