Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01

5 files changed, 105 insertions, 33 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
-              | IDENT _ | INT _ ->
+              | IDENT _ | NUMERAL _ ->
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 38bc58a659..e12bf36339 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -141,6 +141,11 @@ Ltac IZR_tac t :=
   match t with
   | R0 => constr:(0%Z)
   | R1 => constr:(1%Z)
+  | IZR (Z.pow_pos 10 ?p) =>
+    match isPcst p with
+    | true => constr:(Z.pow_pos 10 p)
+    | _ => constr:(InitialRing.NotConstant)
+    end
   | IZR ?u =>
     match isZcst u with
     | true => u
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..7cd62f4ead 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -224,20 +224,20 @@ let test_ssrslashnum b1 b2 strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "/" ->
       (match Util.stream_nth 1 strm with
-      | Tok.INT _ when b1 ->
+      | Tok.NUMERAL _ when b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
          | Tok.KEYWORD "/" ->
              if not b2 then () else begin
                match Util.stream_nth 3 strm with
-               | Tok.INT _ -> ()
+               | Tok.NUMERAL _ -> ()
                | _ -> raise Stream.Failure
              end
          | _ -> raise Stream.Failure)
       | Tok.KEYWORD "/" when not b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 3 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -248,7 +248,7 @@ let test_ssrslashnum b1 b2 strm =
   | Tok.KEYWORD "//" when not b1 ->
          (match Util.stream_nth 1 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.INT _ when b2 ->
+         | Tok.NUMERAL _ when b2 ->
            (match Util.stream_nth 2 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -360,8 +360,8 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral (s,b) ->
-             let n = int_of_string s in if b then n else -n
+          | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) ->
+             let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
           | _ -> raise Not_found
           end
         | None -> raise Not_found
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 525056e5f1..ec8c2338fb 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -56,17 +56,24 @@ let locate_z () =
     }, mkRefC q_z)
   else None
 
-let locate_int () =
+let locate_decimal () =
   let int = "num.int.type" in
   let uint = "num.uint.type" in
-  if Coqlib.has_ref int && Coqlib.has_ref uint
+  let dec = "num.decimal.type" in
+  if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec
   then
     let q_int = qualid_of_ref int in
     let q_uint = qualid_of_ref uint in
-    Some ({
+    let q_dec = qualid_of_ref dec in
+    let int_ty = {
         int = unsafe_locate_ind q_int;
         uint = unsafe_locate_ind q_uint;
-    }, mkRefC q_int, mkRefC q_uint)
+      } in
+    let dec_ty = {
+        int = int_ty;
+        decimal = unsafe_locate_ind q_dec;
+      } in
+    Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec)
   else None
 
 let locate_int63 () =
@@ -86,16 +93,16 @@ let type_error_to f ty =
   CErrors.user_err
     (pr_qualid f ++ str " should go from Decimal.int to " ++
      pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let type_error_of g ty =
   CErrors.user_err
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
-     str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
+     str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
 let vernac_numeral_notation env sigma local ty f g scope opts =
-  let int_ty = locate_int () in
+  let dec_ty = locate_decimal () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -110,11 +117,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
   let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
-    match int_ty with
-    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    match dec_ty with
+    | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+    | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -127,11 +136,13 @@ let vernac_numeral_notation env sigma local ty f g scope opts =
   in
   (* Check the type of g *)
   let of_kind =
-    match int_ty with
-    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    match dec_ty with
+    | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+    | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct
+    | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index d90b7d754c..b9062dd16b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -13,6 +13,7 @@ open Names
 open Globnames
 open Glob_term
 open Bigint
+open Constrexpr
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -104,22 +105,76 @@ let r_modpath = MPfile (make_dir rdefinitions)
 let r_path = make_path rdefinitions "R"
 
 let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-
-let r_of_int ?loc z =
-  DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
+
+let binintdef = ["Coq";"ZArith";"BinIntDef"]
+let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
+
+let glob_pow_pos = ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
+
+let r_of_rawnum ?loc (sign,n) =
+  let n, f, e = NumTok.(n.int, n.frac, n.exp) in
+  let izr z =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
+  let rmult r r' =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in
+  let rdiv r r' =
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
+  let pow10 e =
+    let ten = z_of_int ?loc (Bigint.of_int 10) in
+    let e = pos_of_bignat e in
+    DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in
+  let n =
+    let n = Bigint.of_string (n ^ f) in
+    let n = match sign with SPlus -> n | SMinus -> Bigint.(neg n) in
+    izr (z_of_int ?loc n) in
+  let e =
+    let e = if e = "" then Bigint.zero else match e.[1] with
+      | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2))
+      | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2))))
+      | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in
+    Bigint.(sub e (of_int (String.length f))) in
+  if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
+  else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
+  else n  (* e = 0 *)
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_r c = match DAst.get c with
+let rawnum_of_r c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_IZR ->
-      bigint_of_z a
+     let n = bigint_of_z a in
+     let s, n =
+       if is_strictly_neg n then SMinus, neg n else SPlus, n in
+     s, NumTok.int (to_string n)
+  | GApp (md,  [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
+     begin match DAst.get l, DAst.get r with
+     | GApp (i, [l]), GApp (i', [r])
+          when is_gr i glob_IZR && is_gr i' glob_IZR ->
+        begin match DAst.get r with
+        | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
+           let t = bigint_of_z t in
+           if not (Bigint.(equal t (of_int 10))) then
+             raise Non_closed_number
+           else
+             let i = bigint_of_z l in
+             let e = bignat_of_pos e in
+             let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in
+             let i = Bigint.to_string i in
+             let se = if is_gr md glob_Rdiv then "-" else "" in
+             let e = se ^ Bigint.to_string e in
+             s, { NumTok.int = i; frac = ""; exp = e }
+        | _ -> raise Non_closed_number
+        end
+     | _ -> raise Non_closed_number
+     end
   | _ -> raise Non_closed_number
 
 let uninterp_r (AnyGlobConstr p) =
   try
-    Some (bigint_of_r p)
+    Some (rawnum_of_r p)
   with Non_closed_number ->
     None
 
@@ -131,11 +186,11 @@ let at_declare_ml_module f x =
 let r_scope = "R_scope"
 
 let _ =
-  register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+  register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r);
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
       pt_interp_info = Uid r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
-      pt_refs = [glob_IZR];
+      pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv];
       pt_in_match = false }