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.

1 files changed, 4 insertions, 0 deletions

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