The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 writes:

> Floats would be next, using Flocq on Coq's side.

The following is a quick and dirty way to extract floats from Flocq. I'm
sure there are much nicer and safer ways to do it.

(* number *)
Require Import ExtrOcamlZInt.
Extract Inductive Fappli_IEEE.binary_float => float [
  "(fun s -> if s then (0.) else (-0.))"
  "(fun s -> if s then infinity else neg_infinity)"
  "nan"
  "(fun (s, m, e) -> let f = ldexp (float_of_int m) e in if s then f else 
-.f)"
].
Extract Constant number_comparable => "(=)".
Extract Constant number_add => "(+.)".
Extract Constant number_mult => "( *. )".
Extract Constant number_div => "(/.)".
Extract Constant number_of_int => float_of_int.
(* The following functions make pattern matches with floats and will thus be 
removed. *)
Extraction Inline Fappli_IEEE.Bplus Fappli_IEEE.binary_normalize 
Fappli_IEEE_bits.b64_plus.
Extraction Inline Fappli_IEEE.Bmult Fappli_IEEE.Bmult_FF 
Fappli_IEEE_bits.b64_mult.
Extraction Inline Fappli_IEEE.Bdiv Fappli_IEEE_bits.b64_div.

Alan