Merge PR #11859: Warn when non exactly parsing non floating-point

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd

7 files changed, 115 insertions, 4 deletions

diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst
new file mode 100644
index 0000000000..224ffdbe9b
--- /dev/null
+++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  In primitive floats, print a warning when parsing a decimal value
+  that is not exactly a binary64 floating-point number.
+  For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
+  (`#11859 <https://github.com/coq/coq/pull/11859>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 39f2ccec29..acdd4408ed 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,6 +1062,11 @@ 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]
+
+   Not all decimal constants are floating-point values. This warning
+   is generated when parsing such a constant (for instance ``0.1``).
+
 .. example::
 
   .. coqtop:: all
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 299f53e8ab..53fc13b04b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -21,12 +21,19 @@ 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] as input. *)
+   [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 *)
-let to_string f = if is_nan f then "nan" else to_string_raw f
+   all NaNs are considered equal here.
+   OCaml prints infinities as "inf" (resp. "-inf")
+   but we want "infinity" (resp. "neg_infinity"). *)
+let to_string 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
+
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index dadce9a9ea..e0a9906689 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -22,8 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 (*** Parsing for float in digital notation ***)
 
+let warn_inexact_float =
+  CWarnings.create ~name:"inexact-float" ~category:"parsing"
+    (fun (sn, f) ->
+      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)))
+
 let interp_float ?loc n =
-  DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n)))
+  let sn = NumTok.Signed.to_string n in
+  let f = Float64.of_string sn in
+  (* return true when f is not exactly equal to n,
+     this is only used to decide whether or not to display a warning
+     and does not play any actual role in the parsing *)
+  let inexact () = match Float64.classify f with
+    | Float64.(PInf | NInf | NaN) -> true
+    | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n)
+    | Float64.(PNormal | NNormal | PSubn | NSubn) ->
+       let m, e =
+         let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in
+         let i = NumTok.UnsignedNat.to_string i in
+         let f = match f with
+           | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
+         let e = match e with
+           | None -> "0" | Some e -> NumTok.SignedNat.to_string e in
+         Bigint.of_string (i ^ f),
+         (try int_of_string e with Failure _ -> 0) - String.length f in
+       let m', e' =
+         let m', e' = Float64.frshiftexp f in
+         let m' = Float64.normfr_mantissa m' in
+         let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in
+         Bigint.of_string (Uint63.to_string m'),
+         e' in
+       let c2, c5 = Bigint.(of_int 2, of_int 5) in
+       (* check m*5^e <> m'*2^e' *)
+       let check m e m' e' =
+         not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in
+       (* check m*5^e*2^e' <> m' *)
+       let check' m e e' m' =
+         not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in
+       (* we now have to check m*10^e <> m'*2^e' *)
+       if e >= 0 then
+         if e <= e' then check m e m' (e' - e)
+         else check' m e (e - e') m'
+       else  (* e < 0 *)
+         if e' <= e then check m' (-e) m (e - e')
+         else check' m' (-e) (e' - e) m in
+  if inexact () then warn_inexact_float ?loc (sn, f);
+  DAst.make ?loc (GFloat f)
 
 (* Pretty printing is already handled in constrextern.ml *)
 
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index cfd6633752..dd8189c56f 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,3 +1,17 @@
+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]
+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]
+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]
+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
+-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 668a55977d..7941d2e647 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -4,8 +4,16 @@
      : float
 (-2.5)%float
      : 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]
 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
+-2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
 (2 + 2)%float
@@ -18,14 +26,34 @@
      : float
 -2.5
      : 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]
 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
+-2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
 2 + 2
      : float
 2.5 + 2.5
      : float
+File "stdin", line 24, characters 6-11:
+Warning: The constant 1e309 is not a binary64 floating-point value. A closest
+value will be used and unambiguously printed infinity.
+[inexact-float,parsing]
+infinity
+     : float
+File "stdin", line 25, 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]
+neg_infinity
+     : float
 2
      : nat
 2%float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 85f611352c..eca712db10 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -21,6 +21,9 @@ Check (-2.5e-123).
 Check (2 + 2).
 Check (2.5 + 2.5).
 
+Check 1e309.
+Check -1e309.
+
 Open Scope nat_scope.
 
 Check 2.