Print a warning when parsing non floating-point values.

For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.

1 files changed, 49 insertions, 1 deletions

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 *)