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.

9 files changed, 176 insertions, 44 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index fa19eb8ec4..7a14a4e708 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -48,13 +48,23 @@ type abstraction_kind = AbsLambda | AbsPi
 
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
-(** Representation of integer literals that appear in Coq scripts.
-    We now use raw strings of digits in base 10 (big-endian), and a separate
-    sign flag. Note that this representation is not unique, due to possible
-    multiple leading zeros, and -0 = +0 *)
+(** 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 = string
+type raw_numeral = NumTok.t
 
 type prim_token =
   | Numeral of sign * raw_numeral
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 338ffb706d..60610b92b8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -50,8 +50,8 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-(* Note: redundant Numeral representations such as -0 and +0 (or different
-   numbers of leading zeros) are considered different here. *)
+(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+   are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
 | Numeral (SPlus,n1), Numeral (SPlus,n2)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4866ff3db5..24b1362e6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -318,16 +318,11 @@ 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_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 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
@@ -337,10 +332,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
         mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
     | _ ->
 	match decompose_notation_key ntn, l with
-        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
-           mkprim (loc, Numeral (SMinus,x))
-        | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
-           mkprim (loc, Numeral (SPlus,x))
+        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+           begin match NumTok.of_string x with
+           | Some n -> mkprim (loc, Numeral (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))
+           | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
 let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
@@ -969,7 +968,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
   | GInt i ->
-     CPrim(Numeral (SPlus, Uint63.to_string i))
+     CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
 
   in insert_coercion coercion (CAst.make ?loc c)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 86fcf7fd56..8b93088515 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1489,6 +1489,7 @@ 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 merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 147eaf20dc..1262dbb181 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+NumTok
 Constrexpr
 Tactypes
 Stdarg
diff --git a/interp/notation.ml b/interp/notation.ml
index 6cb95db364..df8f6eb4f8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -506,9 +506,11 @@ module InnerPrimToken = struct
   let do_interp ?loc interp primtok =
     match primtok, interp with
     | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n)
-    | Numeral (s,n), BigNumInterp interp -> interp ?loc (ofNumeral s n)
+    | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }),
+      BigNumInterp interp -> interp ?loc (ofNumeral s n)
     | String s, StringInterp interp -> interp ?loc s
-    | _ -> raise Not_found
+    | (Numeral _ | String _),
+      (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
 
   type uninterpreter =
     | RawNumUninterp of (any_glob_constr -> rawnum option)
@@ -522,8 +524,10 @@ module InnerPrimToken = struct
     | _ -> false
 
   let mkNumeral n =
-    if Bigint.is_pos_or_zero n then Numeral (SPlus,Bigint.to_string n)
-    else Numeral (SMinus,Bigint.to_string (Bigint.neg 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)))
 
   let mkString = function
     | None -> None
@@ -560,8 +564,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_numeral
-  | Abstract of raw_numeral
+  | Warning of string
+  | Abstract of string
 
 type int_ty =
   { uint : Names.inductive;
@@ -571,11 +575,16 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
+type decimal_ty =
+  { int : int_ty;
+    decimal : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
 
 type string_target_kind =
   | ListByte
@@ -767,11 +776,24 @@ let coquint_of_rawnum uint str =
   in
   do_chars str (String.length str - 1) nil
 
-let coqint_of_rawnum inds (sign,str) =
+let coqint_of_rawnum inds sign str =
   let uint = coquint_of_rawnum inds.uint str 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 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
+    mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|])  (* DecimalExp *)
+
 let rawnum_of_coquint c =
   let rec of_uint_loop c buf =
     match Constr.kind c with
@@ -790,7 +812,7 @@ 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 Buffer.contents buf
+  else NumTok.int (Buffer.contents buf)
 
 let rawnum_of_coqint c =
   match Constr.kind c with
@@ -801,6 +823,19 @@ let rawnum_of_coqint 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
+  match Constr.kind c with
+  | App (_,[|i; f|]) -> of_ife i f None
+  | App (_,[|i; f; e|]) -> of_ife i f (Some e)
+  | _ -> raise NotAValidPrimToken
 
 (***********************************************************************)
 
@@ -887,32 +922,42 @@ let bigint_of_int63 c =
   | _ -> raise NotAValidPrimToken
 
 let big2raw n =
-  if Bigint.is_pos_or_zero n then (SPlus, Bigint.to_string n)
-  else (SMinus, Bigint.to_string (Bigint.neg 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
+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, n) when rawnum_compare n threshold >= 0 ->
+  | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" })
+       when rawnum_compare n threshold >= 0 ->
      warn_large_num o.ty_name
   | _ -> ()
   end;
-  let c = match fst o.to_kind with
-    | Int int_ty -> coqint_of_rawnum int_ty n
-    | UInt uint_ty when fst n == SPlus -> coquint_of_rawnum uint_ty (snd n)
-    | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
-    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
-    | Int63 -> interp_int63 ?loc (raw2big n)
+  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)
+    | (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
   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) threshold >= 0 ->
+  | Abstract threshold, Direct
+       when rawnum_compare (snd n).NumTok.int threshold >= 0 ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
      glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
@@ -928,6 +973,7 @@ let uninterp o n =
       | (UInt _, c) -> (SPlus, rawnum_of_coquint c)
       | (Z _, c) -> big2raw (bigint_of_z c)
       | (Int63, c) -> big2raw (bigint_of_int63 c)
+      | (Decimal _, c) -> rawnum_of_decimal c
     end o n
 end
 
@@ -1252,8 +1298,8 @@ let find_notation ntn sc =
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
-  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, n
-  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^n
+  | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
+  | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string 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 5423655229..57e2be16b9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -70,10 +70,10 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
-(** A numeral interpreter is the pair of an interpreter for **integer**
+(** A numeral interpreter is the pair of an interpreter for **decimal**
    numbers in terms and an optional interpreter in pattern, if
-   negative numbers are not supported, the interpreter must fail with
-   an appropriate error message *)
+   non integer or negative numbers are not supported, the interpreter
+   must fail with an appropriate error message *)
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
@@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
 
 type numnot_option =
   | Nop
-  | Warning of raw_numeral
-  | Abstract of raw_numeral
+  | Warning of string
+  | Abstract of string
 
 type int_ty =
   { uint : Names.inductive;
@@ -123,11 +123,16 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
+type decimal_ty =
+  { int : int_ty;
+    decimal : Names.inductive }
+
 type target_kind =
   | Int of int_ty (* Coq.Init.Decimal.int + uint *)
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+  | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
 
 type string_target_kind =
   | ListByte
diff --git a/interp/numTok.ml b/interp/numTok.ml
new file mode 100644
index 0000000000..cdc6ddb62b
--- /dev/null
+++ b/interp/numTok.ml
@@ -0,0 +1,52 @@
+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
diff --git a/interp/numTok.mli b/interp/numTok.mli
new file mode 100644
index 0000000000..46223c5faf
--- /dev/null
+++ b/interp/numTok.mli
@@ -0,0 +1,18 @@
+type t = {
+  int : string;  (** \[0-9\]+ *)
+  frac : string;  (** empty or \[0-9\]+ *)
+  exp : string  (** empty or \[eE\]\[+-\]?\[0-9\]+ *)
+}
+
+val equal : t -> t -> bool
+
+(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *)
+val int : string -> t
+
+val to_string : t -> string
+
+val of_string : string -> t option
+
+(** 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