Is there a way to create binary floats from hexadecimals?

Using Coq
1

Hi! Is there a way to create binary floating point numbers in Flocq from hexadecimals? For instance, if I want to create a binary 32 from 0x42000000, what is the best way to do so?

My initial idea was to convert the hexadecimal to binary, find the sign, exponent and mantissa, and use these to create the float manually. Is this the way to go, or is there a better approach?

For reference, this is how I am currently creating binary 32’s:

Goal Prec_gt_0 24.
Proof.
  reflexivity.
Qed.

Definition my_binary32 (exponent mantissa: Z): binary_float 24 128 :=
  binary_normalize 24 128 eq_refl eq_refl mode_NE mantissa exponent false.
2

You should have a look at the IEEE754.Bits module, especially the binary_float_of_bits function (or its instance b32_of_bits).

1 Like