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

7 files changed, 41 insertions, 42 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index b81d89edf9..42ca5f8c05 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -318,10 +318,6 @@ let rec ident_tail loc len s = match Stream.peek s with
           warn_unrecognized_unicode ~loc (u,id); len
       | _ -> len
 
-let rec number len s = match Stream.peek s with
-  | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
-  | _ -> len
-
 let warn_comment_terminator_in_string =
   CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
          (fun () ->
@@ -706,15 +702,11 @@ let rec next_token ~diff_mode loc s =
       let id = get_buff len in
       comment_stop bp;
       (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
-  | Some ('0'..'9' as c) ->
-      Stream.junk s;
-      let len =
-        try number (store 0 c) s with
-          Stream.Failure -> raise (Stream.Error "")
-      in
+  | Some ('0'..'9') ->
+      let n = NumTok.parse s in
       let ep = Stream.count s in
       comment_stop bp;
-      (INT (get_buff len), set_loc_pos loc bp ep)
+      (NUMERAL n, set_loc_pos loc bp ep)
   | Some '\"' ->
       Stream.junk s;
       let (loc, len) =
@@ -796,8 +788,8 @@ let token_text : type c. c Tok.p -> string = function
   | PKEYWORD t -> "'" ^ t ^ "'"
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
-  | PINT None -> "integer"
-  | PINT (Some s) -> "'" ^ s ^ "'"
+  | PNUMERAL None -> "numeral"
+  | PNUMERAL (Some n) -> "'" ^ NumTok.to_string n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
   | PLEFTQMARK -> "LEFTQMARK"
@@ -846,12 +838,6 @@ module LexerDiff = MakeLexer (struct let mode = true end)
 let is_ident_not_keyword s =
   is_ident s && not (is_keyword s)
 
-let is_number s =
-  let rec aux i =
-    Int.equal (String.length s) i ||
-    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
-  in aux 0
-
 let strip s =
   let len =
     let rec loop i len =
@@ -875,5 +861,9 @@ let terminal s =
   let s = strip s in
   let () = match s with "" -> failwith "empty token." | _ -> () in
   if is_ident_not_keyword s then PIDENT (Some s)
-  else if is_number s then PINT (Some s)
   else PKEYWORD s
+
+(* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
+let terminal_numeral s = match NumTok.of_string s with
+  | Some n -> PNUMERAL (Some n)
+  | None -> failwith "numeral token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 9df3e45f49..464bcf614d 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -46,9 +46,12 @@ val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
 
-(** When string is neither an ident nor an int, returns a keyword. *)
+(** When string is not an ident, returns a keyword. *)
 val terminal : string -> string Tok.p
 
+(** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
+val terminal_numeral : string -> NumTok.t Tok.p
+
 (** The lexer of Coq: *)
 
 module Lexer :
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 6f73a3e4ed..0586dda555 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -226,7 +226,7 @@ GRAMMAR EXTEND Gram
       | c=match_constr -> { c }
       | "("; c = operconstr LEVEL "200"; ")" ->
         { (match c.CAst.v with
-            | CPrim (Numeral (n,true)) ->
+            | CPrim (Numeral (SPlus,n)) ->
                 CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; "|}" -> { c }
@@ -305,7 +305,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) }
       | s=sort   -> { CAst.make ~loc @@  CSort s }
-      | n=INT    -> { CAst.make ~loc @@ CPrim (Numeral (n,true)) }
+      | n=NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (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) }
@@ -413,18 +413,18 @@ GRAMMAR EXTEND Gram
       | "_" -> { CAst.make ~loc @@ CPatAtom None }
       | "("; p = pattern LEVEL "200"; ")" ->
           { (match p.CAst.v with
-            | CPatPrim (Numeral (n,true)) ->
+            | CPatPrim (Numeral (SPlus,n)) ->
                  CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p) }
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           { let p =
             match p with
-            | { CAst.v = CPatPrim (Numeral (n,true)) } ->
+            | { CAst.v = CPatPrim (Numeral (SPlus,n)) } ->
                  CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc @@ CPatCast (p, ty) }
-      | n = INT    -> { CAst.make ~loc @@ CPatPrim (Numeral (n,true)) }
+      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   impl_ident_tail:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 6247a12640..80dd997860 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -21,6 +21,10 @@ 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 =
   try
     int_of_string s
@@ -110,13 +114,13 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = INT      -> { my_int_of_string loc i }
-      | "-"; i = INT -> { - my_int_of_string loc i } ] ]
+    [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
+      | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
   ;
   natural:
-    [ [ i = INT -> { my_int_of_string loc i } ] ]
+    [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
   ;
   bigint: (* Negative numbers are dealt with elsewhere *)
-    [ [ i = INT -> { i } ] ]
+    [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e361f0d00f..5d8897cb47 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -157,7 +157,7 @@ module Prim :
     val pattern_identref : lident Entry.t
     val base_ident : Id.t Entry.t
     val natural : int Entry.t
-    val bigint : Constrexpr.raw_natural_number Entry.t
+    val bigint : string Entry.t
     val integer : int Entry.t
     val string : string Entry.t
     val lstring : lstring Entry.t
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 186d0502fc..71e2d4aa80 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
-  | PINT : string option -> string p
+  | PNUMERAL : NumTok.t option -> NumTok.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -30,7 +30,8 @@ let pattern_strings : type c. c p -> string * string option =
   | PPATTERNIDENT s -> "PATTERNIDENT", s
   | PIDENT s -> "IDENT", s
   | PFIELD s -> "FIELD", s
-  | PINT s -> "INT", s
+  | PNUMERAL None -> "NUMERAL", None
+  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.to_string n)
   | PSTRING s -> "STRING", s
   | PLEFTQMARK -> "LEFTQMARK", None
   | PBULLET s -> "BULLET", s
@@ -42,7 +43,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | INT of string
+  | NUMERAL of NumTok.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -57,7 +58,8 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
   | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
-  | PINT s1, PINT 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
   | 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
@@ -71,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
-| INT s1, INT s2 -> string_equal s1 s2
+| NUMERAL n1, NUMERAL n2 -> NumTok.equal n1 n2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -98,7 +100,7 @@ let extract_string diff_mode = function
     else s
   | PATTERNIDENT s -> s
   | FIELD s -> if diff_mode then "." ^ s else s
-  | INT s -> s
+  | NUMERAL n -> NumTok.to_string n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -122,15 +124,15 @@ 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' | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.to_string 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 ())
   | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ())
   | PFIELD None -> (function FIELD s -> s | _ -> err ())
   | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
-  | PINT None -> (function INT s -> s | _ -> err ())
-  | PINT (Some s) -> (function INT 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 ())
   | 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 678877720d..a5fb5ad9cd 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
-  | PINT : string option -> string p
+  | PNUMERAL : NumTok.t option -> NumTok.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
-  | INT of string
+  | NUMERAL of NumTok.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string