## 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?

:)

#### 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).

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: Jun 18 2024 at 21:01 UTC