Merge PR #11703: Making of NumTok an API for numeral

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01

5 files changed, 14 insertions, 29 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5bfbe7a49a..5a26ac8827 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -125,7 +125,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | _ -> ElimOnConstr clbind
 
 let mkNumeral n =
-  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
+  Numeral (NumTok.Signed.of_int_string (string_of_int n))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 1dca8fd57b..442b40221b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -350,8 +350,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 (b,{NumTok.int = s; frac = ""; exp = ""}) ->
-             let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
+          | _, Constrexpr.Numeral n when NumTok.Signed.is_int n ->
+            int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
         | None -> raise Not_found
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index 23d4d63228..dadce9a9ea 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -22,9 +22,8 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 (*** Parsing for float in digital notation ***)
 
-let interp_float ?loc (sign,n) =
-  let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in
-  DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n)))
+let interp_float ?loc n =
+  DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n)))
 
 (* Pretty printing is already handled in constrextern.ml *)
 
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..e66dbe17b2 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -21,16 +21,16 @@ open Pcoq.Prim
 
 let pr_numnot_option = function
   | Nop -> mt ()
-  | Warning n -> str "(warning after " ++ str n ++ str ")"
-  | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+  | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
+  | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
 
 }
 
 VERNAC ARGUMENT EXTEND numnotoption
   PRINTED BY { pr_numnot_option }
 | [ ] -> { Nop }
-| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 7043653f7b..e0dc3d8989 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Glob_term
 open Bigint
-open Constrexpr
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -113,8 +112,8 @@ let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
 
 let glob_pow_pos = GlobRef.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 r_of_rawnum ?loc n =
+  let n,e = NumTok.Signed.to_bigint_and_exponent n in
   let izr z =
     DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
   let rmult r r' =
@@ -126,15 +125,7 @@ let r_of_rawnum ?loc (sign,n) =
     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 (String.concat "" (String.split_on_char '_' 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 *)
@@ -146,9 +137,7 @@ let r_of_rawnum ?loc (sign,n) =
 let rawnum_of_r c = match DAst.get c with
   | GApp (r, [a]) when is_gr r glob_IZR ->
      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)
+     NumTok.Signed.of_bigint 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])
@@ -161,11 +150,8 @@ let rawnum_of_r c = match DAst.get c with
            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 = "e" ^ se ^ Bigint.to_string e in
-             s, { NumTok.int = i; frac = ""; exp = e }
+             let e = if is_gr md glob_Rdiv then neg e else e in
+             NumTok.Signed.of_bigint_and_exponent i e
         | _ -> raise Non_closed_number
         end
      | _ -> raise Non_closed_number