search

ocaml / Zarith

The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.
Other
231 stars 70 forks source link

more precise bounds for of_float conversion to small ints #137

Closed antoinemine closed 1 year ago

antoinemine commented 1 year ago

This patch changes the bounds used in of_float to decide whether the double can fit into an OCaml 64-bit int.

The previous bounds were conservative: some doubles that could fit in a 64-bit OCaml int were converted to a GMP int instead. It was safe as ml_z_reduce converted it back to a OCaml int. But it was wasteful. The new bounds should be tight and correspond exactly the the smallest/greatest double that can fit in a 64-bit OCaml int.

xavierleroy commented 1 year ago

Please pardon my stupidity, but could you give me a reason why the new bound is correct (and tight) and why the old bound was not tight (and correct) ? In similar cases in the past, I found Gappa (https://gappa.gitlabpages.inria.fr/) very useful to prove such bounds, and even to find them.

antoinemine commented 1 year ago

My reasoning is: 0x3ffffffffffffe00 is exactly representable as a double (2^53-1)*2^9 = (2-2^-52) * 2^61 as it is 1.1...1 * 2^61 with 52 ones after the 1.. The double just after 0x3ffffffffffffe00 is 0x4000000000000000, or 2^62, which does not fit an OCaml int.

For the negative side, it's easier as -0x4000000000000000 is exactly representable as a double, but also the smallest number that fits an OCaml int.

xavierleroy commented 1 year ago

OK, it makes sense. Thanks for the explanation.