Jerome Hugues (Dec 12 2022 at 20:30): Jerome Hugues (Dec 12 2022 at 20:30):Hi,
I need to turn strings with float numbers, e.g. 1.02 or 1.01e-1 into decimal (from Coq.Init.Decimal) or floats. I understand there might be rounding issues with the latter, and this is OK for the demo I planned.
What is not clear is what the most direct approach is and whether or not some existing code exists.
Parsing a string from a decimal (e.g. 1.02) should be straightforward using int_of_string and the like.
I am confused at the last leg: going from decimal to a float.
Any hint to share? Thanks!
Karl Palmskog (Dec 12 2022 at 20:34):floating points and strings were recently discussed here, maybe helpful?
Jerome Hugues (Dec 12 2022 at 20:39):Thanks. That's for string_of_float though. I am curious about what could be float_of_string. I'll dig some of the links there.
Pierre Roux (Dec 13 2022 at 08:25):@Jerome Hugues the file in https://github.com/coq/coq/issues/14782#issuecomment-906480643 should contain a solution.
Note that to do pretty much anything with floats, it is advised to use the dedicated library Flocq. The Floats module in the stdlib is only intended to provide access to primitive floats in the kernel, which is only useful for fast floating-point computations inside Coq (to implement reflexive tactics for instance).
Jerome Hugues (Dec 13 2022 at 12:50):Thanks @Pierre Roux , this is much appreciated. Why is this not part of Flocq or similar library?
Would this make sense?
Pierre Roux (Dec 13 2022 at 13:24):Yes, it should be integrated in Flocq.
Last updated: Oct 04 2023 at 23:01 UTC