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

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

8 files changed, 425 insertions, 208 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 8732b0e2c6..21f682ac0e 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -57,26 +57,8 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
-(** Representation of decimal literals that appear in Coq scripts.
-   We now use raw strings following the format defined by
-   [NumTok.t] and a separate sign flag.
-
-   Note that this representation is not unique, due to possible
-   multiple leading or trailing zeros, and -0 = +0, for instances.
-   The reason to keep the numeral exactly as it was parsed is that
-   specific notations can be declared for specific numerals
-   (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
-   [Notation "2e1" := ...]). Those notations, which override the
-   generic interpretation as numeral, use the same representation of
-   numeral using the Numeral constructor. So the latter should be able
-   to record the form of the numeral which exactly matches the
-   notation. *)
-
-type sign = SPlus | SMinus
-type raw_numeral = NumTok.t
-
 type prim_token =
-  | Numeral of sign * raw_numeral
+  | Numeral of NumTok.Signed.t
   | String of string
 
 type instance_expr = Glob_term.glob_level list
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index da5b8d9132..d4369e9bd1 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -48,10 +48,9 @@ let names_of_local_binders bl =
    are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral (SPlus,n1), Numeral (SPlus,n2)
-| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2
+| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2
 | String s1, String s2 -> String.equal s1 s2
-| (Numeral ((SPlus|SMinus),_) | String _), _ -> false
+| (Numeral _ | String _), _ -> false
 
 let explicitation_eq ex1 ex2 = match ex1, ex2 with
 | ExplByPos (i1, id1), ExplByPos (i2, id2) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a16825b5c9..7a14ca3e48 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -354,27 +354,21 @@ let drop_implicits_in_patt cst nb_expl args =
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
-let is_zero s =
-  let rec aux i =
-    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
-  in aux 0
-let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
-
 let make_notation_gen loc ntn mknot mkprim destprim l bl =
   match snd ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) ->
+    | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
         assert (bl=[]);
         mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
         | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
-           begin match NumTok.of_string x with
-           | Some n -> mkprim (loc, Numeral (SMinus,n))
+           begin match NumTok.Unsigned.parse_string x with
+           | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | (InConstrEntrySomeLevel,[Terminal x]), [] ->
-           begin match NumTok.of_string x with
-           | Some n -> mkprim (loc, Numeral (SPlus,n))
+           begin match NumTok.Unsigned.parse_string x with
+           | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
@@ -899,13 +893,10 @@ let extern_float f scopes =
   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 sign = if Float64.sign f then SMinus else SPlus in
-    let s = Float64.(to_string (abs f)) in
-    match NumTok.of_string s with
-    | None -> assert false
-    | Some n ->
-       extern_prim_token_delimiter_if_required (Numeral (sign, n))
-       "float" "float_scope" scopes
+    let s = 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
 
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
@@ -1085,7 +1076,7 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GInt i ->
      extern_prim_token_delimiter_if_required
-       (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+       (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
   | GFloat f -> extern_float f (snd scopes)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index abacadc43a..a071ba7ec9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,7 @@ open Notation_ops
 open Notation
 open Inductiveops
 open Context.Rel.Declaration
+open NumTok
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
@@ -1585,12 +1586,6 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let is_zero s =
-  let rec aux i =
-    Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1))
-  in aux 0
-let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
-
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
@@ -1614,11 +1609,11 @@ let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
 let is_non_zero c = match c with
-| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p)
+| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p)
+| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
diff --git a/interp/notation.ml b/interp/notation.ml
index 4b73189ad3..6291a88bb0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -21,6 +21,7 @@ open Notation_term
 open Glob_term
 open Glob_ops
 open Context.Named.Declaration
+open NumTok
 
 (*i*)
 
@@ -335,7 +336,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
 type required_module = full_path * string list
-type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
+type rawnum = NumTok.Signed.t
 
 type prim_token_uid = string
 
@@ -358,17 +359,13 @@ module InnerPrimToken = struct
     | StringInterp f, StringInterp f' -> f == f'
     | _ -> false
 
-  let ofNumeral s n =
-    let n = String.(concat "" (split_on_char '_' n)) in
-    match s with
-    | SPlus -> Bigint.of_string n
-    | SMinus -> Bigint.neg (Bigint.of_string n)
-
   let do_interp ?loc interp primtok =
     match primtok, interp with
-    | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n)
-    | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }),
-      BigNumInterp interp -> interp ?loc (ofNumeral s n)
+    | Numeral n, RawNumInterp interp -> interp ?loc n
+    | Numeral n, BigNumInterp interp ->
+      (match NumTok.Signed.to_bigint n with
+       | Some n -> interp ?loc n
+       | None -> raise Not_found)
     | String s, StringInterp interp -> interp ?loc s
     | (Numeral _ | String _),
       (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
@@ -385,10 +382,7 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    if Bigint.is_pos_or_zero n then
-      Numeral (SPlus,NumTok.int (Bigint.to_string n))
-    else
-      Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg n)))
+    Numeral (NumTok.Signed.of_bigint n)
 
   let mkString = function
     | None -> None
@@ -425,8 +419,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of string
-  | Abstract of string
+  | Warning of NumTok.UnsignedNat.t
+  | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
   { uint : Names.inductive;
@@ -567,7 +561,7 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
     Some (to_raw (fst o.of_kind, c))
   with
   | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
-  | NotAValidPrimToken -> None (* all other functions except big2raw *)
+  | NotAValidPrimToken -> None (* all other functions except NumTok.Signed.of_bigint *)
 
 end
 
@@ -600,26 +594,6 @@ let warn_abstract_large_num =
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
 
-(** Comparing two raw numbers (base 10, big-endian, non-negative).
-    A bit nasty, but not critical: only used to decide when a
-    number is considered as large (see warnings above). *)
-
-exception Comp of int
-
-let rec rawnum_compare s s' =
- let l = String.length s and l' = String.length s' in
- if l < l' then - rawnum_compare s' s
- else
-   let d = l-l' in
-   try
-     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
-     for i = d to l-1 do
-       let c = pervasives_compare s.[i] s'.[i-d] in
-       if c != 0 then raise (Comp c)
-     done;
-     0
-   with Comp c -> c
-
 (***********************************************************************)
 
 (** ** Conversion between Coq [Decimal.int] and internal raw string *)
@@ -634,32 +608,31 @@ let char_of_digit n =
   assert (2<=n && n<=11);
   Char.chr (n-2 + Char.code '0')
 
-let coquint_of_rawnum uint str =
+let coquint_of_rawnum uint n =
   let nil = mkConstruct (uint,1) in
+  match n with None -> nil | Some n ->
+  let str = NumTok.UnsignedNat.to_string n in
   let rec do_chars s i acc =
     if i < 0 then acc
-    else if s.[i] == '_' then do_chars s (i-1) acc else
+    else
       let dg = mkConstruct (uint, digit_of_char s.[i]) in
       do_chars s (i-1) (mkApp(dg,[|acc|]))
   in
   do_chars str (String.length str - 1) nil
 
-let coqint_of_rawnum inds sign str =
-  let uint = coquint_of_rawnum inds.uint str in
+let coqint_of_rawnum inds (sign,n) =
+  let uint = coquint_of_rawnum inds.uint (Some n) in
   let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
   mkApp (mkConstruct (inds.int, pos_neg), [|uint|])
 
-let coqdecimal_of_rawnum inds sign n =
-  let i, f, e = NumTok.(n.int, n.frac, n.exp) in
-  let i = coqint_of_rawnum inds.int sign i in
+let coqdecimal_of_rawnum inds n =
+  let i, f, e = NumTok.Signed.to_decimal_and_exponent n in
+  let i = coqint_of_rawnum inds.int i in
   let f = coquint_of_rawnum inds.int.uint f in
-  if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|])  (* Decimal *)
-  else
-    let sign, e = match e.[1] with
-      | '-' -> SMinus, String.sub e 2 (String.length e - 2)
-      | '+' -> SPlus, String.sub e 2 (String.length e - 2)
-      | _ -> SPlus, String.sub e 1 (String.length e - 1) in
-    let e = coqint_of_rawnum inds.int sign e in
+  match e with
+  | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|])  (* Decimal *)
+  | Some e ->
+    let e = coqint_of_rawnum inds.int e in
     mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|])  (* DecimalExp *)
 
 let rawnum_of_coquint c =
@@ -680,26 +653,23 @@ let rawnum_of_coquint c =
     (* To avoid ambiguities between Nil and (D0 Nil), we choose
        to not display Nil alone as "0" *)
     raise NotAValidPrimToken
-  else NumTok.int (Buffer.contents buf)
+  else NumTok.UnsignedNat.of_string (Buffer.contents buf)
 
 let rawnum_of_coqint c =
   match Constr.kind c with
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c')
-      | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c')
+      | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c')
+      | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c')
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
 let rawnum_of_decimal c =
   let of_ife i f e =
-    let sign, n = rawnum_of_coqint i in
-    let f =
-      try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in
-    let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with
-      | SPlus, e -> "e+" ^ e.NumTok.int
-      | SMinus, e -> "e-" ^ e.NumTok.int in
-    sign,{ n with NumTok.frac = f; exp = e } in
+    let n = rawnum_of_coqint i in
+    let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in
+    let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in
+    NumTok.Signed.of_decimal_and_exponent n f e in
   match Constr.kind c with
   | App (_,[|i; f|]) -> of_ife i f None
   | App (_,[|i; f; e|]) -> of_ife i f (Some e)
@@ -789,43 +759,31 @@ let bigint_of_int63 c =
   | Int i -> Bigint.of_string (Uint63.to_string i)
   | _ -> raise NotAValidPrimToken
 
-let big2raw n =
-  if Bigint.is_pos_or_zero n then
-    (SPlus, NumTok.int (Bigint.to_string n))
-  else
-    (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n)))
-
-let raw2big s n = match s with
-  | SPlus -> Bigint.of_string n
-  | SMinus -> Bigint.neg (Bigint.of_string n)
-
 let interp o ?loc n =
   begin match o.warning, n with
-  | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" })
-       when rawnum_compare n threshold >= 0 ->
+  | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_large_num o.ty_name
   | _ -> ()
   end;
-  let c = match fst o.to_kind, n with
-    | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       coqint_of_rawnum int_ty s n
-    | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) ->
-       coquint_of_rawnum uint_ty n
-    | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       z_of_bigint z_pos_ty (raw2big s n)
-    | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
-       interp_int63 ?loc (raw2big s n)
+  let c = match fst o.to_kind, NumTok.Signed.to_int n with
+    | Int int_ty, Some n ->
+       coqint_of_rawnum int_ty n
+    | UInt uint_ty, Some (SPlus, n) ->
+       coquint_of_rawnum uint_ty (Some n)
+    | Z z_pos_ty, Some n ->
+       z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
+    | Int63, Some n ->
+       interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
     | (Int _ | UInt _ | Z _ | Int63), _ ->
        no_such_prim_token "number" ?loc o.ty_name
-    | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n
+    | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
   let to_ty = EConstr.Unsafe.to_constr to_ty in
   match o.warning, snd o.to_kind with
-  | Abstract threshold, Direct
-       when rawnum_compare (snd n).NumTok.int threshold >= 0 ->
+  | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
      glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
@@ -837,10 +795,10 @@ let interp o ?loc n =
 let uninterp o n =
   PrimTokenNotation.uninterp
     begin function
-      | (Int _, c) -> rawnum_of_coqint c
-      | (UInt _, c) -> (SPlus, rawnum_of_coquint c)
-      | (Z _, c) -> big2raw (bigint_of_z c)
-      | (Int63, c) -> big2raw (bigint_of_int63 c)
+      | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
+      | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
+      | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c)
+      | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c)
       | (Decimal _, c) -> rawnum_of_decimal c
     end o n
 end
@@ -1162,8 +1120,8 @@ let find_notation ntn sc =
   NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
-  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
-  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n
+  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
+  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
diff --git a/interp/notation.mli b/interp/notation.mli
index 8fcf9dc5dc..892eba8d11 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -81,7 +81,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
-type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
+type rawnum = NumTok.Signed.t
 
 (** The unique id string below will be used to refer to a particular
     registered interpreter/uninterpreter of numeral or string notation.
@@ -116,8 +116,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of string
-  | Abstract of string
+  | Warning of NumTok.UnsignedNat.t
+  | Abstract of NumTok.UnsignedNat.t
 
 type int_ty =
   { uint : Names.inductive;
diff --git a/interp/numTok.ml b/interp/numTok.ml
index c11acdc8bd..e254e9e972 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -8,55 +8,243 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type t = {
-  int : string;
-  frac : string;
-  exp : string
-}
-
-let equal n1 n2 =
-  String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
-
-let int s = { int = s; frac = ""; exp = "" }
-
-let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
-
-let parse =
-  let buff = ref (Bytes.create 80) in
-  let store len x =
-    let open Bytes in
-    if len >= length !buff then
-      buff := cat !buff (create (length !buff));
-    set !buff len x;
-    succ len in
-  let get_buff len = Bytes.sub_string !buff 0 len in
-  (* reads [0-9_]* *)
-  let rec number len s = match Stream.peek s with
-    | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s
-    | _ -> len in
-  fun s ->
-  let i = get_buff (number 0 s) in
-  let f =
-    match Stream.npeek 2 s with
-    | '.' :: (('0'..'9' | '_') as c) :: _ ->
-       Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
-    | _ -> "" in
-  let e =
-    match (Stream.npeek 2 s) with
-    | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
-       Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
-    | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
-       begin match Stream.npeek 3 s with
-       | _ :: _ :: ('0'..'9' as c) :: _ ->
-          Stream.junk s; Stream.junk s; Stream.junk s;
-          get_buff (number (store (store (store 0 e) sign) c) s)
-       | _ -> ""
-       end
-    | _ -> "" in
-  { int = i; frac = f; exp = e }
-
-let of_string s =
-  if s = "" || s.[0] < '0' || s.[0] > '9' then None else
-    let strm = Stream.of_string (s ^ "  ") in
-    let n = parse strm in
-    if Stream.count strm >= String.length s then Some n else None
+(** We keep the string to preserve the user representation,
+    e.g. "e"/"E" or the presence of leading 0s, or the presence of a +
+    in the exponent *)
+
+module UnsignedNat =
+struct
+  type t = string
+  let of_string s =
+    assert (String.length s > 0);
+    assert (s.[0] >= '0' && s.[0] <= '9');
+    s
+  let to_string s =
+    String.(concat "" (split_on_char '_' s))
+
+  let sprint s = s
+  let print s = Pp.str (sprint s)
+
+  (** Comparing two raw numbers (base 10, big-endian, non-negative).
+      A bit nasty, but not critical: used e.g. to decide when a number
+      is considered as large (see threshold warnings in notation.ml). *)
+
+  exception Comp of int
+
+  let rec compare s s' =
+    let l = String.length s and l' = String.length s' in
+    if l < l' then - compare s' s
+    else
+      let d = l-l' in
+      try
+        for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
+        for i = d to l-1 do
+          let c = Util.pervasives_compare s.[i] s'.[i-d] in
+          if c != 0 then raise (Comp c)
+        done;
+        0
+      with Comp c -> c
+
+   let is_zero s =
+     compare s "0" = 0
+end
+
+type sign = SPlus | SMinus
+
+module SignedNat =
+struct
+  type t = sign * UnsignedNat.t
+  let of_string s =
+    assert (String.length s > 0);
+    let sign,n =
+      match s.[0] with
+      | '-' -> (SMinus,String.sub s 1 (String.length s - 1))
+      | '+' -> (SPlus,String.sub s 1 (String.length s - 1))
+      | _ -> (SPlus,s) in
+    (sign,UnsignedNat.of_string n)
+  let to_string (sign,n) =
+    (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
+  let to_bigint n = Bigint.of_string (to_string n)
+  let of_bigint n =
+    let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+    (sign, Bigint.to_string n)
+end
+
+module Unsigned =
+struct
+
+  type t = {
+    int : string;  (** \[0-9\]\[0-9_\]* *)
+    frac : string;  (** empty or \[0-9_\]+ *)
+    exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+  }
+
+  let equal n1 n2 =
+    String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
+
+  let parse =
+    let buff = ref (Bytes.create 80) in
+    let store len x =
+      let open Bytes in
+      if len >= length !buff then
+        buff := cat !buff (create (length !buff));
+      set !buff len x;
+      succ len in
+    let get_buff len = Bytes.sub_string !buff 0 len in
+    (* reads [0-9_]* *)
+    let rec number len s = match Stream.peek s with
+      | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
+      | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
+      | _ -> len in
+    fun s ->
+    let i = get_buff (number 0 s) in
+    assert (i <> "");
+    let f =
+      match Stream.npeek 2 s with
+      | '.' :: (('0'..'9' | '_') as c) :: _ ->
+         Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
+      | _ -> "" in
+    let e =
+      match (Stream.npeek 2 s) with
+      | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+         Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
+      | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+         begin match Stream.npeek 3 s with
+         | _ :: _ :: ('0'..'9' as c) :: _ ->
+            Stream.junk s; Stream.junk s; Stream.junk s;
+            get_buff (number (store (store (store 0 e) sign) c) s)
+         | _ -> ""
+         end
+      | _ -> "" in
+    { int = i; frac = f; exp = e }
+
+  let sprint n =
+    n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
+
+  let print n =
+    Pp.str (sprint n)
+
+  let parse_string s =
+    if s = "" || s.[0] < '0' || s.[0] > '9' then None else
+      let strm = Stream.of_string (s ^ "  ") in
+      let n = parse strm in
+      if Stream.count strm >= String.length s then Some n else None
+
+  let of_string s =
+    match parse_string s with
+    | None -> assert false
+    | Some s -> s
+
+  let to_string =
+    sprint (* We could remove the '_' but not necessary for float_of_string *)
+
+  let to_nat = function
+    | { int = i; frac = ""; exp = "" } -> Some i
+    | _ -> None
+
+  let is_nat = function
+    | { int = _; frac = ""; exp = "" } -> true
+    | _ -> false
+
+end
+
+open Unsigned
+
+module Signed =
+struct
+
+  type t = sign * Unsigned.t
+
+  let equal (s1,n1) (s2,n2) =
+    s1 = s2 && equal n1 n2
+
+  let is_zero = function
+    | (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac
+    | _ -> false
+
+  let of_decimal_and_exponent (sign,int) f e =
+    let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in
+    let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in
+    sign, { int; frac; exp }
+
+  let to_decimal_and_exponent (sign, { int; frac; exp }) =
+    let e =
+      if exp = "" then None else
+        Some (match exp.[1] with
+        | '-' -> SMinus, String.sub exp 2 (String.length exp - 2)
+        | '+' -> SPlus, String.sub exp 2 (String.length exp - 2)
+        | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in
+    let f = if frac = "" then None else Some frac in
+    (sign, int), f, e
+
+  let of_nat i =
+    (SPlus,{ int = i; frac = ""; exp = "" })
+
+  let of_int (s,i) =
+    (s,{ int = i; frac = ""; exp = "" })
+
+  let of_int_string s = of_int (SignedNat.of_string s)
+
+  let to_int = function
+    | (s, { int = i; frac = ""; exp = "" }) -> Some (s,i)
+    | _ -> None
+
+  let is_int n = match to_int n with None -> false | Some _ -> true
+
+  let sprint (s,i) =
+    (match s with SPlus -> "" | SMinus -> "-") ^ Unsigned.sprint i
+
+  let print i =
+    Pp.str (sprint i)
+
+  let parse_string s =
+    if s = "" || s = "-" || s = "+" ||
+       (s.[0] < '0' || s.[0] > '9') && ((s.[0] <> '-' && s.[0] <> '+') || s.[1] < '0' || s.[1] > '9') then None else
+      let strm = Stream.of_string (s ^ "  ") in
+      let sign = match s.[0] with
+        | '-' -> (Stream.junk strm; SMinus)
+        | '+' -> (Stream.junk strm; SPlus)
+        | _ -> SPlus in
+      let n = parse strm in
+      if Stream.count strm >= String.length s then Some (sign,n) else None
+
+  let of_string s =
+    assert (s <> "");
+    let sign,u = match s.[0] with
+    | '-' -> (SMinus, String.sub s 1 (String.length s - 1))
+    | '+' -> (SPlus, String.sub s 1 (String.length s - 1))
+    | _ -> (SPlus, s) in
+    (sign, Unsigned.of_string u)
+
+  let to_string (sign,u) =
+    (match sign with SPlus -> "" | SMinus -> "-") ^ Unsigned.to_string u
+
+  let to_bigint = function
+    | (sign, { int = n; frac = ""; exp = "" }) ->
+      Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n))
+    | _ -> None
+
+  let of_bigint n =
+    let sign, int = SignedNat.of_bigint n in
+    (sign, { int; frac = ""; exp = "" })
+
+  let to_bigint_and_exponent (s, { int; frac; exp }) =
+    let s = match s with SPlus -> "" | SMinus -> "-" in
+    let int = UnsignedNat.to_string int in
+    let frac = UnsignedNat.to_string frac in
+    let i = Bigint.of_string (s ^ int ^ frac) in
+    let e =
+      let e = if exp = "" then Bigint.zero else match exp.[1] with
+      | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))
+      | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))))
+      | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in
+      Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in
+    (i,e)
+
+  let of_bigint_and_exponent i e =
+    of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e))
+
+  let is_bigger_int_than (s, { int; frac; exp }) i =
+    frac = "" && exp = "" && UnsignedNat.compare int i >= 0
+
+end
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 141f1be889..ea289df237 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -8,21 +8,125 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type t = {
-  int : string;  (** \[0-9\]\[0-9_\]* *)
-  frac : string;  (** empty or \[0-9_\]+ *)
-  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
-}
+(** Numerals in different forms: signed or unsigned, possibly with
+    fractional part and exponent.
 
-val equal : t -> t -> bool
+    Numerals are represented using raw strings of decimal
+    literals and a separate sign flag.
 
-(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *)
-val int : string -> t
+    Note that this representation is not unique, due to possible
+    multiple leading or trailing zeros, and -0 = +0, for instances.
+    The reason to keep the numeral exactly as it was parsed is that
+    specific notations can be declared for specific numerals
+    (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
+    [Notation "2e1" := ...]). Those notations override the generic
+    interpretation as numeral. So, one has to record the form of the
+    numeral which exactly matches the notation. *)
 
-val to_string : t -> string
+type sign = SPlus | SMinus
 
-val of_string : string -> t option
+(** {6 String representation of a natural number } *)
 
-(** Precondition: the first char on the stream is a digit (\[0-9\]).
-    Precondition: at least two extra chars after the numeral to parse. *)
-val parse : char Stream.t -> t
+module UnsignedNat :
+sig
+  type t
+  val of_string : string -> t
+    (** Convert from a non-empty sequence of digits (which may contain "_") *)
+
+  val to_string : t -> string
+    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val compare : t -> t -> int
+end
+
+(** {6 String representation of a signed natural number } *)
+
+module SignedNat :
+sig
+  type t = sign * UnsignedNat.t
+  val of_string : string -> t
+    (** Convert from a non-empty sequence of digits which may contain "_" *)
+
+  val to_string : t -> string
+    (** Convert to a non-empty sequence of digit that does not contain "_" *)
+
+  val to_bigint : t -> Bigint.bigint
+  val of_bigint : Bigint.bigint -> t
+end
+
+(** {6 Unsigned decimal numerals } *)
+
+module Unsigned :
+sig
+  type t
+  val equal : t -> t -> bool
+  val is_nat : t -> bool
+  val to_nat : t -> string option
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val parse : char Stream.t -> t
+    (** Parse a positive Coq numeral.
+        Precondition: the first char on the stream is already known to be a digit (\[0-9\]).
+        Precondition: at least two extra chars after the numeral to parse.
+
+        The recognized syntax is:
+        - integer part: \[0-9\]\[0-9_\]*
+        - decimal part: empty or .\[0-9_\]+
+        - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+
+  val parse_string : string -> t option
+    (** Parse the string as a positive Coq numeral, if possible *)
+
+end
+
+(** {6 Signed decimal numerals } *)
+
+module Signed :
+sig
+  type t = sign * Unsigned.t
+  val equal : t -> t -> bool
+  val is_zero : t -> bool
+  val of_nat : UnsignedNat.t -> t
+  val of_int : SignedNat.t -> t
+  val to_int : t -> SignedNat.t option
+  val is_int : t -> bool
+
+  val sprint : t -> string
+  val print : t -> Pp.t
+    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+
+  val parse_string : string -> t option
+    (** Parse the string as a signed Coq numeral, if possible *)
+
+  val of_int_string : string -> t
+    (** Convert from a string in the syntax of OCaml's int/int64 *)
+
+  val of_string : string -> t
+    (** Convert from a string in the syntax of OCaml's string_of_float *)
+
+  val to_string : t -> string
+    (** Returns a string in the syntax of OCaml's float_of_string *)
+
+  val of_bigint : Bigint.bigint -> t
+  val to_bigint : t -> Bigint.bigint option
+    (** Convert from and to bigint when the denotation of a bigint *)
+
+  val of_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
+  val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
+    (** n, p and q such that the number is n.p*10^q *)
+
+  val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint
+  val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t
+    (** n and p such that the number is n*10^p *)
+
+  val is_bigger_int_than : t -> UnsignedNat.t -> bool
+    (** Test if an integer whose absolute value is bounded *)
+
+end