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.

6 files changed, 119 insertions, 6 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 589df6af07..0a1371413a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -752,6 +752,30 @@ let extended_glob_local_binder_of_decl loc = function
 let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
 
 (**********************************************************************)
+(* mapping special floats                                             *)
+
+(* this helper function is copied from notation.ml as it's not exported *)
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_infinity () = qualid_of_ref "num.float.infinity"
+let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
+let q_nan () = qualid_of_ref "num.float.nan"
+
+let extern_float f scopes =
+  if Float64.is_nan f then CRef(q_nan (), None)
+  else if Float64.is_infinity f then CRef(q_infinity (), None)
+  else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
+  else
+    let sign = if Float64.sign f then SMinus else SPlus in
+    let s = Float64.(to_string (abs f)) in
+    match NumTok.of_string s with
+    | None -> assert false
+    | Some n ->
+       extern_prim_token_delimiter_if_required (Numeral (sign, n))
+       "float" "float_scope" scopes
+
+(**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
@@ -972,8 +996,7 @@ let rec extern inctx scopes vars r =
        (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
-  | GFloat f ->
-     CPrim(String (Float64.to_string f))
+  | GFloat f -> extern_float f (snd scopes)
 
   in insert_coercion coercion (CAst.make ?loc c)
 
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
 
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..f67119020e
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.5e+20%float
+     : float
+(-2.4999999999999999e-20)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.5e+20
+     : float
+-2.4999999999999999e-20
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..1caa0bb444
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,34 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+Check 2.5e20%float.
+Check (-2.5e-20)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e20.
+Check (-2.5e-20).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.
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).