Matthieu Sozeau (Sep 30 2022 at 11:44): Matthieu Sozeau (Sep 30 2022 at 11:44):It seems I don't understand the spec_float type enough:
Definition string_of_float (f : PrimFloat.float) : string :=
match Prim2SF f with
| S754_zero sign => "0f"
| S754_infinity sign => if sign then "neg_infinity" else "infinity"
| S754_nan => "nan"
| S754_finite sign p z =>
let abs := string_of_positive p ++ "E" ++ string_of_Z z in
if sign then "-" ++ abs else abs
end.
Eval compute in string_of_float (0.23%float).
(* "8286623314361713E-55" *)
@Guillaume Melquiond @Pierre Roux any idea what I'm doing wrong?
Pierre Roux (Sep 30 2022 at 12:01):It's a power of two: 8286623314361713*2^-55 ~= .22995379697353753575
Paolo Giarrusso (Sep 30 2022 at 12:06):Is http://kurtstephens.com/files/p372-steele.pdf the "right" pretty-printing algorithm?
Matthieu Sozeau (Sep 30 2022 at 12:16):Ah thanks, that explains it!
Pierre Roux (Sep 30 2022 at 12:17):@Paolo Giarrusso Depends your specification but indeed, printing binary values in a decimal format with some accuracy while "looking good" and doing so efficiently is non trivial.
Matthieu Sozeau (Sep 30 2022 at 12:19):I guess I'd rather want to print the exact hex value
Pierre Roux (Sep 30 2022 at 12:20):At some point, there was a plan to implement the parsing/printing of floats in gallina so we would have had some code, maybe @Guillaume Melquiond remembers more details?
Pierre Roux (Sep 30 2022 at 12:20):Printing exact value in hexadecimal format is much easier indeed.
Matthieu Sozeau (Sep 30 2022 at 12:21):Would you know right of the bat how to do it?
Matthieu Sozeau (Sep 30 2022 at 12:21)::)
Guillaume Melquiond (Sep 30 2022 at 12:23):I don't remember the details. The only thing I know of is the existence of examples/Print17.v in Flocq. But you surely know as well since you wrote it.
Matthieu Sozeau (Sep 30 2022 at 12:24):I don't see how to access easily the "bits" of a primitive float, which is really all I need as I want to interoperate with C
Pierre Roux (Sep 30 2022 at 12:26):I would say "0x" ++ Numbers.HexadecimalString.string_of_uint (uint_of_positive p) ++ "p" ++ Numbers.DecimalString.string_of_int (int_of_Z z) or something like that
Guillaume Melquiond (Sep 30 2022 at 12:27):If you can afford a small detour, then you can use functions such as PrimFloat.frshiftexp and PrimFloat.normfr_mantissa.
Matthieu Sozeau (Sep 30 2022 at 12:28):Sure, it's only going to be used on constants that appear in compiled code, so I guess that's not a huge matter
Matthieu Sozeau (Sep 30 2022 at 12:29):@Pierre Roux what about the "sign" I get from S754_finite ?
Pierre Roux (Sep 30 2022 at 12:29):Can't this file of Flocq help: https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/IEEE754/Bits.v
I think it's the one used by CompCert (but never used it so I don't know the details)
Pierre Roux (Sep 30 2022 at 12:30):Matthieu Sozeau said:
Pierre Roux what about the "sign" I get from
S754_finite?
The bit is the boolean (1 for true (negative) and 0 for false (positive))
Pierre Roux (Sep 30 2022 at 12:31):Guillaume Melquiond said:
I don't remember the details. The only thing I know of is the existence of
examples/Print17.vin Flocq. But you surely know as well since you wrote it.
I have some vague remembrance of code written by Andrew Appel that we had to somehow integrate, but I don't remember the details.
Matthieu Sozeau (Sep 30 2022 at 12:37):Do you mean I should output -0x... if the sign bit is set?
Matthieu Sozeau (Sep 30 2022 at 12:39):I didn't know that 0x...p... format, is that standard?
Pierre Roux (Sep 30 2022 at 12:52):That's the format of printf (%h in OCaml, %a in C).
Matthieu Sozeau (Sep 30 2022 at 12:55):Nice, thanks!
Guillaume Melquiond (Sep 30 2022 at 15:02):Pierre Roux said:
Can't this file of Flocq help: https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/IEEE754/Bits.v
Yes. It gives you the in-memory representation of a floating-point number. But if you are targeting C anyway, just outputting numbers in hexadecimal format 0x...p... seems like the simplest.
If you don't want to deal with hexa, you can also output it as string_of_positive p ++ ". * 0x1p" ++ string_of_Z z and let the C compiler do its magic.
Matthieu Sozeau (Sep 30 2022 at 15:49):Hexa is fine and seems to work well, thanks for the help guys!
Notification Bot (Sep 30 2022 at 15:49):Matthieu Sozeau has marked this topic as resolved.
Last updated: Sep 30 2023 at 05:01 UTC