[primitive floats] Add low level hexadecimal printing

9 files changed, 75 insertions, 30 deletions

diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst
new file mode 100644
index 0000000000..f3d85cadc6
--- /dev/null
+++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Add flag ``Printing Float`` to print primitive floats as hexadecimal
+  instead of decimal values. This is included in ``Set Printing All``.
+  (`#11986 <https://github.com/coq/coq/pull/11986>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 899173a83a..b2b68482ef 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,11 +1062,17 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
 decimal constants. This ensures that the composition
 :math:`\text{parse} \circ \text{print}` amounts to the identity.
 
-.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing]
+.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing]
 
    Not all decimal constants are floating-point values. This warning
    is generated when parsing such a constant (for instance ``0.1``).
 
+.. flag:: Printing Float
+
+   Turn this flag off (it is on by default) to deactivate decimal
+   printing of floating-point constants. They will then be printed
+   with an hexadecimal representation.
+
 .. example::
 
   .. coqtop:: all
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3f7bb6e330..bb91dc28da 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -888,12 +888,19 @@ 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 get_printing_float = Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Float"]
+    ~value:true
+
 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 s = Float64.(to_string f) in
+    let s =
+      let hex = !Flags.raw_print || not (get_printing_float ()) in
+      if hex then Float64.to_hex_string f else Float64.to_string f in
     let n = NumTok.Signed.of_string s in
     extern_prim_token_delimiter_if_required (Numeral n)
       "float" "float_scope" scopes
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 53fc13b04b..76005a3dc6 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -19,29 +19,27 @@ let is_nan (f : float) = f <> f
 let is_infinity f = f = infinity
 let is_neg_infinity f = f = neg_infinity
 
-(* 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] or an infinity 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.
    OCaml prints infinities as "inf" (resp. "-inf")
    but we want "infinity" (resp. "neg_infinity"). *)
-let to_string f =
+let to_string_raw fmt f =
   if is_nan f then "nan"
   else if is_infinity f then "infinity"
   else if is_neg_infinity f then "neg_infinity"
-  else to_string_raw f
+  else Printf.sprintf fmt f
+
+let to_hex_string = to_string_raw "%h"
+
+(* Printing a binary64 float in 17 decimal places and parsing it again
+   will yield the same float. *)
+let to_string = to_string_raw "%.17g"
 
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
 let compile f =
-  let s =
-    if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity"
-    else Printf.sprintf "%h" f in
-  Printf.sprintf "Float64.of_float (%s)" s
+  Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
 
 let of_float f = f
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index d43ff4553f..0afbfa89da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -19,9 +19,19 @@ val is_nan : t -> bool
 val is_infinity : t -> bool
 val is_neg_infinity : t -> bool
 
-val to_string : t -> string
 val of_string : string -> t
 
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f].  *)
+val to_string : t -> string
+
 val compile : t -> string
 
 val of_float : float -> t
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 9861a060ab..8e87fc13ca 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -28,8 +28,8 @@ let warn_inexact_float =
       Pp.strbrk
         (Printf.sprintf
            "The constant %s is not a binary64 floating-point value. \
-            A closest value will be used and unambiguously printed %s."
-           sn (Float64.to_string f)))
+            A closest value %s will be used and unambiguously printed %s."
+           sn (Float64.to_hex_string f) (Float64.to_string f)))
 
 let interp_float ?loc n =
   let sn = NumTok.Signed.to_string n in
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index dd8189c56f..539ec9b2bf 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,16 +1,18 @@
 File "stdin", line 25, characters 8-12:
 Warning: The constant 0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed 0.01. [inexact-float,parsing]
+value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 20-25:
 Warning: The constant -0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed -0.01. [inexact-float,parsing]
+value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 27-35:
 Warning: The constant 1.7e+308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 1.6999999999999999e+308.
-[inexact-float,parsing]
+closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed
+1.6999999999999999e+308. [inexact-float,parsing]
 File "stdin", line 25, characters 37-46:
 Warning: The constant -1.7e-308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed
 -1.7000000000000002e-308. [inexact-float,parsing]
 
 (** val infinity : Float64.t **)
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 4a5a700879..0b18e9a3d2 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -6,13 +6,13 @@
      : float
 File "stdin", line 9, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123%float
      : float
 File "stdin", line 10, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
@@ -28,13 +28,13 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 19, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123
      : float
 File "stdin", line 20, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
@@ -56,16 +56,24 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 30, characters 6-11:
 Warning: The constant 1e309 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed infinity.
+value infinity will be used and unambiguously printed infinity.
 [inexact-float,parsing]
 infinity
      : float
 File "stdin", line 31, characters 6-12:
 Warning: The constant -1e309 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed neg_infinity.
-[inexact-float,parsing]
+closest value neg_infinity will be used and unambiguously printed
+neg_infinity. [inexact-float,parsing]
 neg_infinity
      : float
+0x1p-1
+     : float
+0.5
+     : float
+0x1p-1
+     : float
+0.5
+     : float
 2
      : nat
 2%float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 36ffc27239..d3eb6d2e4c 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -30,6 +30,15 @@ Check -0xb.2cp-2.
 Check 1e309.
 Check -1e309.
 
+Set Printing All.
+Check 0.5.
+Unset Printing All.
+Check 0.5.
+Unset Printing Float.
+Check 0.5.
+Set Printing Float.
+Check 0.5.
+
 Open Scope nat_scope.
 
 Check 2.