Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.

1 files changed, 8 insertions, 4 deletions

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 9c5fe2a71d..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 = NUMERAL      -> { my_int_of_string loc i }
-      | "-"; i = NUMERAL -> { - 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 = NUMERAL -> { 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 = NUMERAL -> { i } ] ]
+    [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
 END