Pretty-printing primitive float constants

* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function

Namely:

  let to_string_raw f = Printf.sprintf "%.17g" f
  let to_string f = if is_nan f then "nan" else to_string_raw f

Summary:

* printing a binary64 float in 17 decimal places and parsing it again
  will yield the same float, e.g.:

  let f1 = 1. +. (0x1p-53 +. 0x1p-105)
  let f2 = float_of_string (to_string f1)
  f1 = f2

* OCaml's string_of_float gives a sign to nan values which shouldn't be
  displayed as all NaNs are considered equal here.

2 files changed, 14 insertions, 3 deletions

diff --git a/kernel/float64.ml b/kernel/float64.ml
index 72f0d83359..5160d32892 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -16,9 +16,14 @@ let is_nan f = f <> f
 let is_infinity f = f = infinity
 let is_neg_infinity f = f = neg_infinity
 
-(* OCaml give a sign to nan values which should not be displayed as all nan are
- * considered equal *)
-let to_string f = if is_nan f then "nan" else string_of_float f
+(* Printing a binary64 float in 17 decimal places and parsing it again
+   will yield the same float. We assume [to_string_raw] is not given a
+   [nan] as input. *)
+let to_string_raw f = Printf.sprintf "%.17g" f
+
+(* OCaml gives a sign to nan values which should not be displayed as
+   all NaNs are considered equal here *)
+let to_string f = if is_nan f then "nan" else to_string_raw f
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
@@ -30,6 +35,8 @@ let compile f =
 
 let of_float f = f
 
+let sign f = copysign 1. f < 0.
+
 let opp = ( ~-. )
 let abs = abs_float
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 927594115e..acc3a556ab 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -14,6 +14,7 @@ Beware: NaNs have a sign and a payload, while they should be
 indistinguishable from Coq's perspective. *)
 type t
 
+(** Test functions for special values to avoid calling [classify] *)
 val is_nan : t -> bool
 val is_infinity : t -> bool
 val is_neg_infinity : t -> bool
@@ -25,6 +26,9 @@ val compile : t -> string
 
 val of_float : float -> t
 
+(** Return [true] for "-", [false] for "+". *)
+val sign : t -> bool
+
 val opp : t -> t
 val abs : t -> t