Centralizing all kinds of numeral string management in numTok.ml.

Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent

In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.

Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.

7 files changed, 34 insertions, 31 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 6a436fbcb7..a39da96a53 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -723,7 +723,7 @@ let rec next_token ~diff_mode loc s =
         let ep = Stream.count s in
         IDENT id, set_loc_pos loc bp ep end
   | Some ('0'..'9') ->
-      let n = NumTok.parse s in
+      let n = NumTok.Unsigned.parse s in
       let ep = Stream.count s in
       comment_stop bp;
       (NUMERAL n, set_loc_pos loc bp ep)
@@ -813,7 +813,7 @@ let token_text : type c. c Tok.p -> string = function
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
   | PNUMERAL None -> "numeral"
-  | PNUMERAL (Some n) -> "'" ^ NumTok.to_string n ^ "'"
+  | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
   | PLEFTQMARK -> "LEFTQMARK"
@@ -888,6 +888,6 @@ let terminal s =
   else PKEYWORD s
 
 (* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-let terminal_numeral s = match NumTok.of_string s with
+let terminal_numeral s = match NumTok.Unsigned.parse_string s with
   | Some n -> PNUMERAL (Some n)
   | None -> failwith "numeral token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3ce6981879..2c1284c4db 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -50,7 +50,7 @@ val check_keyword : string -> unit
 val terminal : string -> string Tok.p
 
 (** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-val terminal_numeral : string -> NumTok.t Tok.p
+val terminal_numeral : string -> NumTok.Unsigned.t Tok.p
 
 (** The lexer of Coq: *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 3fd756e748..963f029766 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -174,7 +174,7 @@ GRAMMAR EXTEND Gram
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
-            | CPrim (Numeral (SPlus,n)) ->
+            | CPrim (Numeral (NumTok.SPlus,n)) ->
                 CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
@@ -248,7 +248,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id, None) }
@@ -355,12 +355,12 @@ GRAMMAR EXTEND Gram
         { (* Preserve parentheses around numerals so that constrintern does not
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
-          | CPatPrim (Numeral (SPlus,n)) ->
+          | CPatPrim (Numeral (NumTok.SPlus,n)) ->
               CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   fixannot:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 2bc1c11596..9c50109bb3 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -21,15 +21,18 @@ let _ = List.iter CLexer.add_keyword prim_kw
 
 let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
 
-let check_int loc = function
-  | { NumTok.int = i; frac = ""; exp = "" } -> i
-  | _ -> CErrors.user_err ~loc (Pp.str "This number is not an integer.")
-
-let my_int_of_string loc s =
+let my_int_of_string ?loc s =
   try
     int_of_string s
   with Failure _ ->
-    CErrors.user_err ~loc (Pp.str "This number is too large.")
+    CErrors.user_err ?loc (Pp.str "This number is too large.")
+
+let my_to_nat_string ?loc ispos s =
+  match NumTok.Unsigned.to_nat s with
+  | Some n -> n
+  | None ->
+    let pos = if ispos then "a natural" else "an integer" in
+    CErrors.user_err ?loc Pp.(str "This number is not " ++ str pos ++ str " number.")
 
 let test_pipe_closedcurly =
   let open Pcoq.Lookahead in
@@ -122,18 +125,18 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = bigint -> { my_int_of_string loc i } ] ]
+    [ [ i = bigint -> { my_int_of_string ~loc i } ] ]
   ;
   natural:
-    [ [ i = bignat -> { my_int_of_string loc i } ] ]
+    [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
   ;
   bigint:
-    [ [ i = NUMERAL -> { check_int loc i }
-      | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ]
+    [ [ i = NUMERAL -> { my_to_nat_string true ~loc i }
+      | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ]
   ;
   bignat:
-    [ [ i = NUMERAL -> { check_int loc i } ] ]
-  ;
+    [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ]
+ ;
   bar_cbrace:
     [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fccd096d11..b3f997e1b3 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -166,7 +166,7 @@ struct
   | _ -> None
 
   let lk_nat tok n strm = match stream_nth n strm with
-  | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+  | Tok.NUMERAL p when NumTok.Unsigned.is_nat p -> Some (n + 1)
   | _ -> None
 
   let rec lk_list lk_elem n strm =
diff --git a/parsing/tok.ml b/parsing/tok.ml
index ff4433f18c..b1ceab8822 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,7 +17,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.t option -> NumTok.t p
+  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -31,7 +31,7 @@ let pattern_strings : type c. c p -> string * string option =
   | PIDENT s -> "IDENT", s
   | PFIELD s -> "FIELD", s
   | PNUMERAL None -> "NUMERAL", None
-  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.to_string n)
+  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.Unsigned.sprint n)
   | PSTRING s -> "STRING", s
   | PLEFTQMARK -> "LEFTQMARK", None
   | PBULLET s -> "BULLET", s
@@ -43,7 +43,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.t
+  | NUMERAL of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -59,7 +59,7 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
   | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
   | PNUMERAL None, PNUMERAL None -> Some Util.Refl
-  | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.equal n1 n2 -> Some Util.Refl
+  | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl
   | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
   | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
   | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
@@ -73,7 +73,7 @@ let equal t1 t2 = match t1, t2 with
 | PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
 | IDENT s1, IDENT s2 -> string_equal s1 s2
 | FIELD s1, FIELD s2 -> string_equal s1 s2
-| NUMERAL n1, NUMERAL n2 -> NumTok.equal n1 n2
+| NUMERAL n1, NUMERAL n2 -> NumTok.Unsigned.equal n1 n2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -100,7 +100,7 @@ let extract_string diff_mode = function
     else s
   | PATTERNIDENT s -> s
   | FIELD s -> if diff_mode then "." ^ s else s
-  | NUMERAL n -> NumTok.to_string n
+  | NUMERAL n -> NumTok.Unsigned.sprint n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -124,7 +124,7 @@ let match_pattern (type c) (p : c p) : t -> c =
   let err () = raise Stream.Failure in
   let seq = string_equal in
   match p with
-  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.to_string n) -> s | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
   | PIDENT None -> (function IDENT s' -> s' | _ -> err ())
   | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
   | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())
@@ -132,7 +132,7 @@ let match_pattern (type c) (p : c p) : t -> c =
   | PFIELD None -> (function FIELD s -> s | _ -> err ())
   | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
   | PNUMERAL None -> (function NUMERAL s -> s | _ -> err ())
-  | PNUMERAL (Some n) -> let s = NumTok.to_string n in (function NUMERAL n' when s = NumTok.to_string n' -> n' | _ -> err ())
+  | PNUMERAL (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMERAL n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ())
   | PSTRING None -> (function STRING s -> s | _ -> err ())
   | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
   | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 6d0691a746..b556194eb3 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,7 +15,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.t option -> NumTok.t p
+  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -29,7 +29,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.t
+  | NUMERAL of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string