Add big_int_of_float

[liyishuai]

No description provided.

[antoinemine]

I see that BigInt has no (or no longer) a big_int_of_float. @xavierleroy, do you know why, and whether we should add it to this file in Zarith?

@liyishuai, the Big_int module in Zarith is only here for API compatibility with the legacy code using Big_int from OCaml. Is there any reason why to use this API in recent code? Why not use the native Zarith API in ExtractQC, i.e. Z.of_float? It seems strange to me to support an enriched legacy API instead of the original one...

[liyishuai]

Z.of_float would refer to the Z module extracted from Coq's Zarith, and there's no mechanism to avoid the name conflict with OCaml Zarith yet. See coq/coq#8252 (comment)

[xavierleroy]

I see that BigInt has no (or no longer) a big_int_of_float. @xavierleroy, do you know why, and whether we should add it to this file in Zarith?

As far as I can remember, until recently I was not comfortable with FP arithmetic and thought that conversions from "inexact" FP numbers to "exact" big integers made no sense. ("Inexact numbers" and "exact numbers" are Scheme terminology, even though Scheme does have "inexact to exact" conversions.) So, that's probably why I chose to leave out big_int_of_float.

Should we add it today? We do have Z.of_float, so the cat is out of the box and we could just as well have it as big_int_of_float.

This said, I think the use of FP numbers in QuickChick/QuickChick#245 is misplaced. What QuickChick wants is a randomly-generated Z.t, and going through FP arithmetic to get it is questionable.

[xavierleroy]

Z.of_float would refer to the Z module extracted from Coq's Zarith, and there's no mechanism to avoid the name conflict with OCaml Zarith yet.

Yes, there is. Add to your project an OCaml file CamlLibraries.ml containing module Z = Z, and use CamlLibraries.Z.foo instead of Z.foo in your Extract Inlined Constant declarations.

Or, use Extract Constant xxx => "QuickcheckRuntime.xxx" (not inlined!) and write a QuickcheckRuntime.ml file with all the auxiliary functions written in OCaml in an environment where you have full control on open statements.

[liyishuai]

This said, I think the use of FP numbers in QuickChick/QuickChick#245 is misplaced. What QuickChick wants is a randomly-generated Z.t, and going through FP arithmetic to get it is questionable.

If there is some Random.State.z : t -> Z.t -> Z.t then indeed I should use that function immediately.

Yes, there is. Add to your project an OCaml file CamlLibraries.ml containing module Z = Z, and use CamlLibraries.Z.foo instead of Z.foo in your Extract Inlined Constant declarations.

Or, use Extract Constant xxx => "QuickcheckRuntime.xxx" (not inlined!) and write a QuickcheckRuntime.ml file with all the auxiliary functions written in OCaml in an environment where you have full control on open statements.

These methods require the extracted code to link with OCaml file, which is painful for Coq plugins. That's why coq/coq#8252 removed that external Big.ml file (which nobody used), and extracted Z and N to code that can be directly linked to the Zartih library here.

[antoinemine]

OK. The original need for this seems gone, and we don't need to add the function for compatibility reasons as it's not in Big_int anyway, but I'll merge anyway so that we have a more consistent Big_int API...