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?

It's a power of two: 8286623314361713*2^-55 ~= .22995379697353753575

Is http://kurtstephens.com/files/p372-steele.pdf the "right" pretty-printing algorithm?

Ah thanks, that explains it!

@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.

I guess I'd rather want to print the exact hex value

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?

Printing exact value in hexadecimal format is much easier indeed.

Would you know right of the bat how to do it?

:)

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

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

If you can afford a small detour, then you can use functions such as `PrimFloat.frshiftexp`

and `PrimFloat.normfr_mantissa`

.

Sure, it's only going to be used on constants that appear in compiled code, so I guess that's not a huge matter

@Pierre Roux what about the "sign" I get from `S754_finite`

?

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)

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

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.

Do you mean I should output `-0x...`

if the sign bit is set?

I didn't know that `0x...p...`

format, is that standard?

That's the format of printf (`%h`

in OCaml, `%a`

in C).

Nice, thanks!

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.

Hexa is fine and seems to work well, thanks for the help guys!

Matthieu Sozeau has marked this topic as resolved.

Last updated: Sep 30 2023 at 05:01 UTC