Stream: Coq users

Topic: ✔ Printing of primitive floats

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" *)

Matthieu Sozeau (Sep 30 2022 at 11:45):

@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.v in 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: Apr 20 2024 at 10:02 UTC