Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint

 This way, we could fully bypass bigint.ml.

 The previous mechanism of parsing/printing Z is kept for now.
 Currently, the conversion functions accepted by Numeral Notation foo
 may have the following types.

 for parsing:

   int -> foo
   int -> option foo
   uint -> foo
   uint -> option foo
   Z -> foo
   Z -> option foo

 for printing:

   foo -> int
   foo -> option int
   foo -> uint
   foo -> option uint
   foo -> Z
   foo -> option Z

 Notes:

  - The Declare ML Module is directly done in Prelude
  - When doing a Numeral Notation, having the Z datatype around
    isn't mandatory anymore (but the error messages suggest that
    it can still be used).
  - An option (abstract after ...) allows to keep large numbers in
    an abstract form such as (Nat.of_uint 123456) instead of reducing
    to (S (S (S ...))) and ending immediately with Stack Overflow.
  - After checking with Matthieu, there is now a explicit check
    and an error message in case of polymorphic inductive types

1 files changed, 289 insertions, 97 deletions

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index b4c6a06ab0..cb99904b6e 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -20,15 +20,35 @@ open Misctypes
 
 (** * Numeral notation *)
 
+(** Reduction
+
+    The constr [c] below isn't necessarily well-typed, since we
+    built it via an [mkApp] of a conversion function on a term
+    that starts with the right constructor, but might be partially
+    applied.
+
+    At least [c] is known to be evar-free, since it comes for
+    our own ad-hoc [constr_of_glob] or from conversions such
+    as [coqint_of_rawnum].
+*)
+
 let eval_constr (c : Constr.t) =
   let env = Global.env () in
-  let j = Arguments_renaming.rename_typing env c in
+  let j = Typeops.infer env c in
   let c'=
     Vnorm.cbv_vm env (Evd.from_env env)
                  (EConstr.of_constr j.Environ.uj_val)
                  (EConstr.of_constr j.Environ.uj_type)
   in EConstr.Unsafe.to_constr c'
 
+(* For testing with "compute" instead of "vm_compute" :
+let eval_constr (c : constr) =
+ let (sigma, env) = Lemmas.get_current_context () in
+ Tacred.compute env sigma c
+*)
+
+let eval_constr_app c1 c2 = eval_constr (mkApp (c1,[| c2 |]))
+
 exception NotANumber
 
 let warning_big_num ty =
@@ -37,11 +57,103 @@ let warning_big_num ty =
   strbrk " (threshold may vary depending" ++
   strbrk " on your system limits and on the command executed)."
 
-type conversion_function =
-  | Direct of Constant.t
-  | Option of Constant.t
+let warning_abstract_num ty f =
+  let (sigma, env) = Pfedit.get_current_context () in
+  strbrk "To avoid stack overflow, large numbers in " ++
+  pr_reference ty ++ strbrk " are interpreted as applications of " ++
+  Printer.pr_constr_env env sigma f ++ strbrk "."
+
+(** Comparing two raw numbers (base 10, big-endian, non-negative).
+    A bit nasty, but not critical : only used to decide when a
+    nat number is considered as large. *)
+
+exception Comp of int
+
+let rec rawnum_compare s s' =
+ let l = String.length s and l' = String.length s' in
+ if l < l' then - rawnum_compare s' s
+ else
+   let d = l-l' in
+   try
+     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
+     for i = d to l-1 do
+       let c = Pervasives.compare s.[i] s'.[i-d] in
+       if c != 0 then raise (Comp c)
+     done;
+     0
+   with Comp c -> c
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [Decimal.int] and internal raw string *)
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
+
+let digit_of_char c =
+  assert ('0' <= c && c <= '9');
+  Char.code c - Char.code '0' + 2
+
+let char_of_digit n =
+  assert (2<=n && n<=11);
+  Char.chr (n-2 + Char.code '0')
+
+let coquint_of_rawnum uint str =
+  let nil = mkConstruct (uint,1) in
+  let rec do_chars s i acc =
+    if i < 0 then acc
+    else
+      let dg = mkConstruct (uint, digit_of_char s.[i]) in
+      do_chars s (i-1) (mkApp(dg,[|acc|]))
+  in
+  do_chars str (String.length str - 1) nil
+
+let coqint_of_rawnum inds (str,sign) =
+  let uint = coquint_of_rawnum inds.uint str in
+  mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
+
+let rawnum_of_coquint c =
+  let rec of_uint_loop c buf =
+    match Constr.kind c with
+    | Construct ((_,1), _) (* Nil *) -> ()
+    | App (c, [|a|]) ->
+       (match Constr.kind c with
+        | Construct ((_,n), _) (* D0 to D9 *) ->
+           let () = Buffer.add_char buf (char_of_digit n) in
+           of_uint_loop a buf
+        | _ -> raise NotANumber)
+    | _ -> raise NotANumber
+  in
+  let buf = Buffer.create 64 in
+  let () = of_uint_loop c buf in
+  if Int.equal (Buffer.length buf) 0 then
+    (* To avoid ambiguities between Nil and (D0 Nil), we choose
+       to not display Nil alone as "0" *)
+    raise NotANumber
+  else Buffer.contents buf
+
+let rawnum_of_coqint c =
+  match Constr.kind c with
+  | App (c,[|c'|]) ->
+     (match Constr.kind c with
+      | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
+      | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
+      | _ -> raise NotANumber)
+  | _ -> raise NotANumber
+
+
+(***********************************************************************)
 
-(** Conversion between Coq's [Positive] and our internal bigint *)
+(** ** Conversion between Coq [Z] and internal bigint *)
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : Names.inductive }
+
+(** First, [positive] from/to bigint *)
 
 let rec pos_of_bigint posty n =
   match Bigint.div2_with_rest n with
@@ -68,19 +180,9 @@ let rec bigint_of_pos c = match Constr.kind c with
       end
   | x -> raise NotANumber
 
-(** Conversion between Coq's [Z] and our internal bigint *)
-
-type z_pos_ty =
-  { z_ty : Names.inductive;
-    pos_ty : Names.inductive }
+(** Now, [Z] from/to bigint *)
 
-let maybe_warn (thr,msg) n =
-  if Bigint.is_pos_or_zero n && not (Bigint.equal thr Bigint.zero) &&
-     Bigint.less_than thr n
-  then Feedback.msg_warning msg
-
-let z_of_bigint { z_ty; pos_ty } warn n =
-  maybe_warn warn n;
+let z_of_bigint { z_ty; pos_ty } n =
   if Bigint.equal n Bigint.zero then
     mkConstruct (z_ty, 1) (* Z0 *)
   else
@@ -105,7 +207,7 @@ let bigint_of_z z = match Constr.kind z with
       end
   | _ -> raise NotANumber
 
-(** The uinterp function below work at the level of [glob_constr]
+(** The uninterp function below work at the level of [glob_constr]
     which is too low for us here. So here's a crude conversion back
     to [constr] for the subset that concerns us. *)
 
@@ -127,53 +229,91 @@ let rec glob_of_constr ?loc c = match Constr.kind c with
   | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> CErrors.anomaly (str "interp_big_int: unexpected constr")
-
-let interp_big_int zposty ty warn of_z ?loc bi =
-  match of_z with
-  | Direct f ->
-     let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in
-     glob_of_constr ?loc (eval_constr c)
-  | Option f ->
-     let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in
-     match Constr.kind (eval_constr c) with
-     | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
-     | App (_None, [| _ |]) ->
-        CErrors.user_err ?loc
-         (str "Cannot interpret this number as a value of type " ++
-          pr_reference ty)
-     | x -> CErrors.anomaly (str "interp_big_int: option expected")
-
-let uninterp_big_int to_z (Glob_term.AnyGlobConstr c) =
-  try
-    let t = constr_of_glob c in
-    match to_z with
-    | Direct g ->
-       let r = eval_constr (mkApp (mkConst g, [| t |])) in
-       Some (bigint_of_z r)
-    | Option g ->
-       let r = eval_constr (mkApp (mkConst g, [| t |])) in
-       match Constr.kind r with
-       | App (_Some, [| _; x |]) -> Some (bigint_of_z x)
-       | x -> None
-  with
-  | Type_errors.TypeError _ -> None (* cf. eval_constr *)
-  | NotANumber -> None (* cf constr_of_glob or bigint_of_z *)
+  | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr")
+
+let no_such_number ?loc ty =
+  CErrors.user_err ?loc
+   (str "Cannot interpret this number as a value of type " ++
+    pr_reference ty)
+
+let interp_option ty ?loc c =
+  match Constr.kind c with
+  | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
+  | App (_None, [| _ |]) -> no_such_number ?loc ty
+  | x -> CErrors.anomaly (str "Numeral.interp: option expected")
+
+let uninterp_option c =
+  match Constr.kind c with
+  | App (_Some, [| _; x |]) -> x
+  | _ -> raise NotANumber
+
+let big2raw n =
+  if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
+  else (Bigint.to_string (Bigint.neg n), false)
+
+let raw2big (n,s) =
+  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
+type target_kind = Int | UInt | Z
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
 
 type numeral_notation_obj =
   { num_ty : Libnames.reference;
-    z_pos_ty : z_pos_ty;
-    of_z : conversion_function;
-    to_z : conversion_function;
+    z_pos_ty : z_pos_ty option;
+    int_ty : int_ty;
+    to_kind : conversion_kind;
+    to_ty : constr;
+    of_kind : conversion_kind;
+    of_ty : constr;
     scope : Notation_term.scope_name;
     constructors : Glob_term.glob_constr list;
-    warning : Bigint.bigint * Pp.t;
+    warning : numnot_option;
     path : Libnames.full_path }
 
+let interp o ?loc n =
+  begin match o.warning with
+  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+     Feedback.msg_warning (warning_big_num o.num_ty)
+  | _ -> ()
+  end;
+  let c = match fst o.to_kind with
+    | Int -> coqint_of_rawnum o.int_ty n
+    | UInt when snd n -> coquint_of_rawnum o.int_ty.uint (fst n)
+    | UInt (* n <= 0 *) -> no_such_number ?loc o.num_ty
+    | Z -> z_of_bigint (Option.get o.z_pos_ty) (raw2big n)
+  in
+  match o.warning, snd o.to_kind with
+  | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
+     Feedback.msg_warning (warning_abstract_num o.num_ty o.to_ty);
+     glob_of_constr ?loc (mkApp (o.to_ty,[|c|]))
+  | _ ->
+     let res = eval_constr_app o.to_ty c in
+     match snd o.to_kind with
+     | Direct -> glob_of_constr ?loc res
+     | Option -> interp_option o.num_ty ?loc res
+
+let uninterp o (Glob_term.AnyGlobConstr n) =
+  try
+    let c = eval_constr_app o.of_ty (constr_of_glob n) in
+    let c = if snd o.of_kind == Direct then c else uninterp_option c in
+    match fst o.of_kind with
+    | Int -> Some (rawnum_of_coqint c)
+    | UInt -> Some (rawnum_of_coquint c, true)
+    | Z -> Some (big2raw (bigint_of_z c))
+  with
+  | Type_errors.TypeError _ -> None (* cf. eval_constr_app *)
+  | NotANumber -> None (* all other functions except big2raw *)
+
 let load_numeral_notation _ (_, o) =
-  Notation.declare_numeral_interpreter o.scope (o.path, [])
-   (interp_big_int o.z_pos_ty o.num_ty o.warning o.of_z)
-   (o.constructors, uninterp_big_int o.to_z, true)
+  Notation.declare_rawnumeral_interpreter o.scope (o.path, [])
+  (interp o)
+  (o.constructors, uninterp o, true)
 
 let cache_numeral_notation o = load_numeral_notation 1 o
 
@@ -193,19 +333,30 @@ let get_constructors ind =
            (Glob_term.GRef (ConstructRef (ind, j + 1), None)))
        mc)
 
-let locate_ind s =
-  let q = qualid_of_string s in
-  try
-    match Nametab.locate q with
-    | IndRef i -> i
-    | _ -> raise Not_found
-  with Not_found -> Nametab.error_global_not_found (CAst.make q)
+let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
+let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
+let q_int = qualid_of_string "Coq.Init.Decimal.int"
+let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
+let q_option = qualid_of_string "Coq.Init.Datatypes.option"
+
+let unsafe_locate_ind q =
+  match Nametab.locate q with
+  | IndRef i -> i
+  | _ -> raise Not_found
 
-(** TODO: we should ensure that BinNums is loaded (or autoload it ?) *)
+let locate_ind q =
+  try unsafe_locate_ind q
+  with Not_found -> Nametab.error_global_not_found (CAst.make q)
 
 let locate_z () =
-  { z_ty = locate_ind "Coq.Numbers.BinNums.Z";
-    pos_ty = locate_ind "Coq.Numbers.BinNums.positive"; }
+  try
+    Some { z_ty = unsafe_locate_ind q_z;
+           pos_ty = unsafe_locate_ind q_positive }
+  with Not_found -> None
+
+let locate_int () =
+  { uint = locate_ind q_uint;
+    int = locate_ind q_int }
 
 let locate_globref r =
   let q = qualid_of_reference r in
@@ -223,66 +374,107 @@ let has_type f ty =
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
 
-let vernac_numeral_notation ty f g scope waft =
+let vernac_numeral_notation ty f g scope opts =
+  let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
   let tyc = locate_globref ty in
-  let fc = locate_constant f in
-  let gc = locate_constant g in
-  let cty = mkRefC (CAst.(make (Qualid (qualid_of_reference ty).v)))
-  in
+  let to_ty = mkConst (locate_constant f) in
+  let of_ty = mkConst (locate_constant g) in
+  let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
-  let cref s = mkIdentC (Id.of_string s) in
+  let cref q = mkRefC (CAst.make (Qualid q)) in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
+  let cZ = cref q_z in
+  let cint = cref q_int in
+  let cuint = cref q_uint in
+  let coption = cref q_option in
+  let opt r = app coption r in
   (* Check that [ty] is an inductive type *)
   let constructors = match tyc with
-    | IndRef ind -> get_constructors ind
+    | IndRef ind when not (Global.is_polymorphic tyc) ->
+       get_constructors ind
+    | IndRef _ ->
+       CErrors.user_err
+         (str "The inductive type " ++ pr_reference ty ++
+          str " cannot be polymorphic here for the moment")
     | ConstRef _ | ConstructRef _ | VarRef _ ->
        CErrors.user_err
         (pr_reference ty ++ str " is not an inductive type")
   in
-  (* Is "f" of type "Z -> ty" or "Z -> option ty" ? *)
-  let of_z =
-    if has_type f (arrow (cref "Z") cty) then
-      Direct fc
-    else if has_type f (arrow (cref "Z") (app (cref "option") cty)) then
-      Option fc
+  (* Check the type of f *)
+  let to_kind =
+    if has_type f (arrow cint cty) then Int, Direct
+    else if has_type f (arrow cint (opt cty)) then Int, Option
+    else if has_type f (arrow cuint cty) then UInt, Direct
+    else if has_type f (arrow cuint (opt cty)) then UInt, Option
+    else if Option.is_empty z_pos_ty then
+      CErrors.user_err
+        (pr_reference f ++ str " should goes from Decimal.int or uint to " ++
+         pr_reference ty ++ str " or (option " ++ pr_reference ty ++
+         str ")." ++ fnl () ++
+         str "Instead of int, the type Z could also be used (load it first).")
+    else if has_type f (arrow cZ cty) then Z, Direct
+    else if has_type f (arrow cZ (opt cty)) then Z, Option
     else
        CErrors.user_err
-        (pr_reference f ++ str " should goes from Z to " ++
+        (pr_reference f ++ str " should goes from Decimal.int or uint or Z to "
+         ++
          pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")")
   in
-  (* Is "g" of type "ty -> Z" or "ty -> option Z" ? *)
-  let to_z =
-    if has_type g (arrow cty (cref "Z")) then
-      Direct gc
-    else if has_type g (arrow cty (app (cref "option") (cref "Z"))) then
-      Option gc
+  (* Check the type of g *)
+  let of_kind =
+    if has_type g (arrow cty cint) then Int, Direct
+    else if has_type g (arrow cty (opt cint)) then Int, Option
+    else if has_type g (arrow cty cuint) then UInt, Direct
+    else if has_type g (arrow cty (opt cuint)) then UInt, Option
+    else if Option.is_empty z_pos_ty then
+      CErrors.user_err
+        (pr_reference g ++ str " should goes from " ++
+         pr_reference ty ++
+         str " to Decimal.int or (option int) or uint." ++ fnl () ++
+         str "Instead of int, the type Z could also be used (load it first).")
+    else if has_type g (arrow cty cZ) then Z, Direct
+    else if has_type g (arrow cty (opt cZ)) then Z, Option
     else
       CErrors.user_err
         (pr_reference g ++ str " should goes from " ++
-         pr_reference ty ++ str " to Z or (option Z)")
+         pr_reference ty ++
+         str " to Decimal.int or (option int) or uint or Z or (option Z)")
   in
   Lib.add_anonymous_leaf
     (inNumeralNotation
        { num_ty = ty;
          z_pos_ty;
-         of_z;
-         to_z;
+         int_ty;
+         to_kind;
+         to_ty;
+         of_kind;
+         of_ty;
          scope;
          constructors;
-         warning = (Bigint.of_int waft, warning_big_num ty);
+         warning = opts;
          path = Nametab.path_of_global tyc })
 
+open Ltac_plugin
 open Stdarg
+open Pcoq.Prim
+
+let pr_numnot_option _ _ _ = function
+  | Nop -> mt ()
+  | Warning n -> str "(warning after " ++ str n ++ str ")"
+  | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+
+ARGUMENT EXTEND numnotoption
+  PRINTED BY pr_numnot_option
+| [ ] -> [ Nop ]
+| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ]
+| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ]
+END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) ] ->
-    [ let waft = 0 in
-      vernac_numeral_notation ty f g (Id.to_string sc) waft ]
-  | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) "(" "warning" "after" int(waft) ")" ] ->
-    [ vernac_numeral_notation ty f g (Id.to_string sc) waft ]
+      ident(sc) numnotoption(o) ] ->
+    [ vernac_numeral_notation ty f g (Id.to_string sc) o ]
 END