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, 6 insertions, 1 deletions

diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index c3c35486d9..bdd78ea544 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -57,11 +57,16 @@ Primitive next_down := #float64_next_down.
 
 Local Open Scope float_scope.
 
-(* Special values *)
+(* Special values, needed for pretty-printing *)
 Definition infinity := Eval compute in div (of_int63 1) (of_int63 0).
 Definition neg_infinity := Eval compute in opp infinity.
 Definition nan := Eval compute in div (of_int63 0) (of_int63 0).
 
+Register infinity as num.float.infinity.
+Register neg_infinity as num.float.neg_infinity.
+Register nan as num.float.nan.
+
+(* Other special values *)
 Definition one := Eval compute in (of_int63 1).
 Definition zero := Eval compute in (of_int63 0).
 Definition neg_zero := Eval compute in (-zero).