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, 67 insertions, 21 deletions

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 =