Merge PR #8064: Numeral notation (revisited again)

18 files changed, 604 insertions, 374 deletions

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dbbdbfa396..d779951180 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -52,8 +52,11 @@ let () =
 
 (* Rewriting orientation *)
 
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+  Mltop.declare_cache_obj
+    (fun () -> Metasyntax.add_token_obj "<-";
+               Metasyntax.add_token_obj "->")
+    "ltac_plugin"
 
 let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 0bb9ccb1d8..1f2c722b34 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -144,7 +144,7 @@ let add ~deprecation kn b t =
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
-  let (path, _, _) = KerName.repr path in
+  let path = KerName.modpath path in
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab
 
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 47a59ba631..5e36fbeb81 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -83,8 +83,18 @@ let make_ascii_string n =
 
 let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 let _ =
-  Notation.declare_string_interpreter "char_scope"
-    (ascii_path,ascii_module)
-    interp_ascii_string
-    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+  let sc = "char_scope" in
+  register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = sc;
+      pt_uid = sc;
+      pt_required = (ascii_path,ascii_module);
+      pt_refs = [static_glob_Ascii];
+      pt_in_match = true }
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
new file mode 100644
index 0000000000..ec14df3baa
--- /dev/null
+++ b/plugins/syntax/g_numeral.ml4
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+DECLARE PLUGIN "numeral_notation_plugin"
+
+open Numeral
+open Pp
+open Names
+open Vernacinterp
+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) numnotoption(o) ] ->
+    [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ]
+END
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index f10f98e23b..d3ffe936a9 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) =
   with Non_closed ->
     None
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 (* Actually declares the interpreter for int31 *)
-let _ = Notation.declare_numeral_interpreter int31_scope
-  (int31_path, int31_module)
-  interp_int31
-  ([DAst.make (GRef (int31_construct, None))],
-   uninterp_int31,
-   true)
+
+let _ =
+  register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = int31_scope;
+      pt_uid = int31_scope;
+      pt_required = (int31_path,int31_module);
+      pt_refs = [int31_construct];
+      pt_in_match = true }
diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml
deleted file mode 100644
index 0e202be47f..0000000000
--- a/plugins/syntax/n_syntax.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Names
-open Bigint
-open Positive_syntax_plugin.Positive_syntax
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "n_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(**********************************************************************)
-(* Parsing N via scopes                                               *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
-let glob_n = IndRef (n_kn,0)
-let path_of_N0 = ((n_kn,0),1)
-let path_of_Npos = ((n_kn,0),2)
-let glob_N0 = ConstructRef path_of_N0
-let glob_Npos = ConstructRef path_of_Npos
-
-let n_path = make_path binnums "N"
-
-let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
-  if not (Bigint.equal n zero) then
-    GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
-  else
-    GRef(glob_N0, None)
-
-let error_negative ?loc =
-  user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
-
-let n_of_int ?loc n =
-  if is_pos_or_zero n then n_of_binnat ?loc true n
-  else error_negative ?loc
-
-(**********************************************************************)
-(* Printing N via scopes                                              *)
-(**********************************************************************)
-
-let bignat_of_n n = DAst.with_val (function
-  | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
-  | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
-  | _ -> raise Non_closed_number
-  ) n
-
-let uninterp_n (AnyGlobConstr p) =
-  try Some (bignat_of_n p)
-  with Non_closed_number -> None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for N *)
-
-let _ = Notation.declare_numeral_interpreter "N_scope"
-  (n_path,binnums)
-  n_of_int
-  ([DAst.make @@ GRef (glob_N0, None);
-    DAst.make @@ GRef (glob_Npos, None)],
-  uninterp_n,
-  true)
diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack
deleted file mode 100644
index 4c56645f07..0000000000
--- a/plugins/syntax/n_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-N_syntax
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
deleted file mode 100644
index e158e0b516..0000000000
--- a/plugins/syntax/nat_syntax.ml
+++ /dev/null
@@ -1,85 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "nat_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* This file defines the printer for natural numbers in [nat] *)
-
-(*i*)
-open Pp
-open CErrors
-open Names
-open Glob_term
-open Bigint
-open Coqlib
-(*i*)
-
-(**********************************************************************)
-(* Parsing via scopes *)
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-
-let threshold = of_int 5000
-
-let warn_large_nat =
-  CWarnings.create ~name:"large-nat" ~category:"numbers"
-    (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++
-                 strbrk "working with large numbers in nat (observed threshold " ++
-                 strbrk "may vary from 5000 to 70000 depending on your system " ++
-                 strbrk "limits and on the command executed).")
-
-let nat_of_int ?loc n =
-  if is_pos_or_zero n then begin
-      if less_than threshold n then warn_large_nat ();
-      let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in
-      let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in
-      let rec mk_nat acc n =
-	if n <> zero then
-	  mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
-	else
-	  acc
-      in
-      mk_nat ref_O n
-    end
-  else
-      user_err ?loc ~hdr:"nat_of_int"
-       (str "Cannot interpret a negative number as a number of type nat")
-
-(************************************************************************)
-(* Printing via scopes *)
-
-exception Non_closed_number
-
-let rec int_of_nat x = DAst.with_val (function
-  | GApp (r, [a]) ->
-    begin match DAst.get r with
-    | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a)
-    | _ -> raise Non_closed_number
-    end
-  | GRef (z,_) when GlobRef.equal z glob_O -> zero
-  | _ -> raise Non_closed_number
-  ) x
-
-let uninterp_nat (AnyGlobConstr p) =
-  try
-    Some (int_of_nat p)
-  with
-    Non_closed_number -> None
-
-(************************************************************************)
-(* Declare the primitive parsers and printers *)
-
-let _ =
-  Notation.declare_numeral_interpreter "nat_scope"
-    (nat_path,datatypes_module_name)
-    nat_of_int
-    ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack
deleted file mode 100644
index 39bdd62f47..0000000000
--- a/plugins/syntax/nat_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Nat_syntax
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
new file mode 100644
index 0000000000..fee93593d0
--- /dev/null
+++ b/plugins/syntax/numeral.ml
@@ -0,0 +1,478 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Constr
+
+(** * 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 from
+    our own ad-hoc [constr_of_glob] or from conversions such
+    as [coqint_of_rawnum].
+*)
+
+let eval_constr env sigma (c : Constr.t) =
+  let c = EConstr.of_constr c in
+  let sigma,t = Typing.type_of env sigma c in
+  let c' = Vnorm.cbv_vm env sigma c t in
+  EConstr.Unsafe.to_constr c'
+
+(* For testing with "compute" instead of "vm_compute" :
+let eval_constr env sigma (c : Constr.t) =
+  let c = EConstr.of_constr c in
+  let c' = Tacred.compute env sigma c in
+  EConstr.Unsafe.to_constr c'
+*)
+
+let eval_constr_app env sigma c1 c2 =
+  eval_constr env sigma (mkApp (c1,[| c2 |]))
+
+exception NotANumber
+
+let warn_large_num =
+  CWarnings.create ~name:"large-number" ~category:"numbers"
+    (fun ty ->
+      strbrk "Stack overflow or segmentation fault happens when " ++
+      strbrk "working with large numbers in " ++ pr_qualid ty ++
+      strbrk " (threshold may vary depending" ++
+      strbrk " on your system limits and on the command executed).")
+
+let warn_abstract_large_num =
+  CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
+    (fun (ty,f) ->
+      strbrk "To avoid stack overflow, large numbers in " ++
+      pr_qualid ty ++ strbrk " are interpreted as applications of " ++
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+
+let warn_abstract_large_num_no_op =
+  CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
+    (fun f ->
+      strbrk "The 'abstract after' directive has no effect when " ++
+      strbrk "the parsing function (" ++
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
+      strbrk "option type.")
+
+(** Comparing two raw numbers (base 10, big-endian, non-negative).
+    A bit nasty, but not critical: only used to decide when a
+    number is considered as large (see warnings above). *)
+
+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 [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
+  | (q, false) ->
+      let c = mkConstruct (posty, 2) in (* xO *)
+      mkApp (c, [| pos_of_bigint posty q |])
+  | (q, true) when not (Bigint.equal q Bigint.zero) ->
+      let c = mkConstruct (posty, 1) in (* xI *)
+      mkApp (c, [| pos_of_bigint posty q |])
+  | (q, true) ->
+      mkConstruct (posty, 3) (* xH *)
+
+let rec bigint_of_pos c = match Constr.kind c with
+  | Construct ((_, 3), _) -> (* xH *) Bigint.one
+  | App (c, [| d |]) ->
+      begin match Constr.kind c with
+      | Construct ((_, n), _) ->
+          begin match n with
+          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
+          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+          | n -> assert false (* no other constructor of type positive *)
+          end
+      | x -> raise NotANumber
+      end
+  | x -> raise NotANumber
+
+(** Now, [Z] from/to bigint *)
+
+let z_of_bigint { z_ty; pos_ty } n =
+  if Bigint.equal n Bigint.zero then
+    mkConstruct (z_ty, 1) (* Z0 *)
+  else
+    let (s, n) =
+      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
+      else (3, Bigint.neg n) (* Zneg *)
+    in
+    let c = mkConstruct (z_ty, s) in
+    mkApp (c, [| pos_of_bigint pos_ty n |])
+
+let bigint_of_z z = match Constr.kind z with
+  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+  | App (c, [| d |]) ->
+      begin match Constr.kind c with
+      | Construct ((_, n), _) ->
+          begin match n with
+          | 2 -> (* Zpos *) bigint_of_pos d
+          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+          | n -> assert false (* no other constructor of type Z *)
+          end
+      | _ -> raise NotANumber
+      end
+  | _ -> raise NotANumber
+
+(** 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. *)
+
+let rec constr_of_glob env sigma g = match DAst.get g with
+  | Glob_term.GRef (ConstructRef c, _) ->
+      let sigma,c = Evd.fresh_constructor_instance env sigma c in
+      sigma,mkConstructU c
+  | Glob_term.GApp (gc, gcl) ->
+      let sigma,c = constr_of_glob env sigma gc in
+      let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
+      sigma,mkApp (c, Array.of_list cl)
+  | _ ->
+      raise NotANumber
+
+let rec glob_of_constr ?loc c = match Constr.kind c with
+  | App (c, ca) ->
+      let c = glob_of_constr ?loc c in
+      let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in
+      DAst.make ?loc (Glob_term.GApp (c, cel))
+  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
+  | 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))
+  | _ -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+           (strbrk "Unexpected term " ++
+              Printer.pr_constr_env env sigma c ++
+              strbrk " while parsing a numeral notation.")
+
+let no_such_number ?loc ty =
+  CErrors.user_err ?loc
+   (str "Cannot interpret this number as a value of type " ++
+    pr_qualid 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 -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (strbrk "Unexpected non-option term " ++
+             Printer.pr_constr_env env sigma c ++
+             strbrk " while parsing a numeral notation.")
+
+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 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 *)
+
+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 =
+  { to_kind : conversion_kind;
+    to_ty : GlobRef.t;
+    of_kind : conversion_kind;
+    of_ty : GlobRef.t;
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
+    warning : numnot_option }
+
+let interp o ?loc n =
+  begin match o.warning with
+  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+     warn_large_num o.num_ty
+  | _ -> ()
+  end;
+  let c = match fst o.to_kind with
+    | Int int_ty -> coqint_of_rawnum int_ty n
+    | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
+    | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
+    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big 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 (fst n) threshold >= 0 ->
+     warn_abstract_large_num (o.num_ty,o.to_ty);
+     glob_of_constr ?loc (mkApp (to_ty,[|c|]))
+  | _ ->
+     let res = eval_constr_app env sigma 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) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
+  let of_ty = EConstr.Unsafe.to_constr of_ty in
+  try
+    let sigma,n = constr_of_glob env sigma n in
+    let c = eval_constr_app env sigma of_ty 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 _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+  | NotANumber -> None (* all other functions except big2raw *)
+
+(* Here we only register the interp and uninterp functions
+   for a particular Numeral Notation (determined by a unique
+   string). The actual activation of the notation will be done
+   later (cf. Notation.enable_prim_token_interpretation).
+   This registration of interp/uninterp must be added in the
+   libstack, otherwise this won't work through a Require. *)
+
+let load_numeral_notation _ (_, (uid,opts)) =
+  Notation.register_rawnumeral_interpretation
+    ~allow_overwrite:true uid (interp opts, uninterp opts)
+
+let cache_numeral_notation x = load_numeral_notation 1 x
+
+(* TODO: substitution ?
+   TODO: uid pas stable par substitution dans opts
+ *)
+
+let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj =
+  Libobject.declare_object {
+    (Libobject.default_object "NUMERAL NOTATION") with
+    Libobject.cache_function = cache_numeral_notation;
+    Libobject.load_function = load_numeral_notation }
+
+let get_constructors ind =
+  let mib,oib = Global.lookup_inductive ind in
+  let mc = oib.Declarations.mind_consnames in
+  Array.to_list
+    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+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
+
+let locate_ind q =
+  try unsafe_locate_ind q
+  with Not_found -> Nametab.error_global_not_found q
+
+let locate_z () =
+  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 has_type f ty =
+  let (sigma, env) = Pfedit.get_current_context () in
+  let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
+  try let _ = Constrintern.interp_constr env sigma c in true
+  with Pretype_errors.PretypeError _ -> false
+
+let type_error_to f ty loadZ =
+  CErrors.user_err
+    (pr_qualid f ++ str " should go from Decimal.int to " ++
+     pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
+     (if loadZ then str " (require BinNums first)." else str "."))
+
+let type_error_of g ty loadZ =
+  CErrors.user_err
+    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
+     str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
+     str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
+     (if loadZ then str " (require BinNums first)." else str "."))
+
+let vernac_numeral_notation local ty f g scope opts =
+  let int_ty = locate_int () in
+  let z_pos_ty = locate_z () in
+  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let to_ty = Smartlocate.global_with_alias f in
+  let of_ty = Smartlocate.global_with_alias g in
+  let cty = mkRefC ty in
+  let app x y = mkAppC (x,[y]) in
+  let cref q = mkRefC 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
+  let constructors = get_constructors tyc in
+  (* Check the type of f *)
+  let to_kind =
+    if has_type f (arrow cint cty) then Int int_ty, Direct
+    else if has_type f (arrow cint (opt cty)) then Int int_ty, Option
+    else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct
+    else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
+    else
+      match z_pos_ty with
+      | Some z_pos_ty ->
+         if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
+         else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
+         else type_error_to f ty false
+      | None -> type_error_to f ty true
+  in
+  (* Check the type of g *)
+  let of_kind =
+    if has_type g (arrow cty cint) then Int int_ty, Direct
+    else if has_type g (arrow cty (opt cint)) then Int int_ty, Option
+    else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct
+    else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
+    else
+      match z_pos_ty with
+      | Some z_pos_ty ->
+         if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
+         else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
+         else type_error_of g ty false
+      | None -> type_error_of g ty true
+  in
+  let o = { to_kind; to_ty; of_kind; of_ty;
+            num_ty = ty;
+            warning = opts }
+  in
+  (match opts, to_kind with
+   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
+   | _ -> ());
+  (* TODO: un hash suffit-il ? *)
+  let uid = Marshal.to_string o [] in
+  let i = Notation.(
+       { pt_local = local;
+         pt_scope = scope;
+         pt_uid = uid;
+         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_refs = constructors;
+         pt_in_match = true })
+  in
+  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
+  Notation.enable_prim_token_interpretation i
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
new file mode 100644
index 0000000000..83ede6f48f
--- /dev/null
+++ b/plugins/syntax/numeral.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Libnames
+open Constrexpr
+open Vernacexpr
+
+(** * Numeral notation *)
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
new file mode 100644
index 0000000000..f4d9cae3ff
--- /dev/null
+++ b/plugins/syntax/numeral_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+Numeral
+G_numeral
diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml
deleted file mode 100644
index 0c82e47445..0000000000
--- a/plugins/syntax/positive_syntax.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Util
-open Names
-open Bigint
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "positive_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_number
-
-(**********************************************************************)
-(* Parsing positive via scopes                                        *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let positive_path = make_path binnums "positive"
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
-let glob_positive = IndRef (positive_kn,0)
-let path_of_xI = ((positive_kn,0),1)
-let path_of_xO = ((positive_kn,0),2)
-let path_of_xH = ((positive_kn,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
-
-let pos_of_bignat ?loc x =
-  let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
-  let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
-  let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
-  let rec pos_of x =
-    match div2_with_rest x with
-      | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
-      | (q,true) -> ref_xH
-  in
-  pos_of x
-
-let error_non_positive ?loc =
-  user_err ?loc ~hdr:"interp_positive"
-   (str "Only strictly positive numbers in type \"positive\".")
-
-let interp_positive ?loc n =
-  if is_strictly_pos n then pos_of_bignat ?loc n
-  else error_non_positive ?loc
-
-(**********************************************************************)
-(* Printing positive via scopes                                       *)
-(**********************************************************************)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let rec bignat_of_pos x = DAst.with_val (function
-  | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _)                when GlobRef.equal a glob_xH -> Bigint.one
-  | _ -> raise Non_closed_number
-  ) x
-
-let uninterp_positive (AnyGlobConstr p) =
-  try
-    Some (bignat_of_pos p)
-  with Non_closed_number ->
-    None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for positive *)
-(************************************************************************)
-
-let _ = Notation.declare_numeral_interpreter "positive_scope"
-  (positive_path,binnums)
-  interp_positive
-  ([DAst.make @@ GRef (glob_xI, None);
-    DAst.make @@ GRef (glob_xO, None);
-    DAst.make @@ GRef (glob_xH, None)],
-   uninterp_positive,
-   true)
diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack
deleted file mode 100644
index ac8f3c425c..0000000000
--- a/plugins/syntax/positive_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Positive_syntax
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 94aa143350..04946c158b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) =
   with Non_closed_number ->
     None
 
-let _ = Notation.declare_numeral_interpreter "R_scope"
-  (r_path,["Coq";"Reals";"Rdefinitions"])
-  r_of_int
-  ([DAst.make @@ GRef (glob_IZR, None)],
-    uninterp_r,
-    false)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let r_scope = "R_scope"
+
+let _ =
+  register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = r_scope;
+      pt_uid = r_scope;
+      pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
+      pt_refs = [glob_IZR];
+      pt_in_match = false }
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index c22869f4d6..640bcfde91 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -64,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) =
   with
    Non_closed_string -> None
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 let _ =
-  Notation.declare_string_interpreter "string_scope"
-    (string_path,["Coq";"Strings";"String"])
-    interp_string
-    ([DAst.make @@ GRef (static_glob_String,None);
-      DAst.make @@ GRef (static_glob_EmptyString,None)],
-     uninterp_string, true)
+  let sc = "string_scope" in
+  register_string_interpretation sc (interp_string,uninterp_string);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = sc;
+      pt_uid = sc;
+      pt_required = (string_path,["Coq";"Strings";"String"]);
+      pt_refs = [static_glob_String; static_glob_EmptyString];
+      pt_in_match = true }
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
deleted file mode 100644
index 2534162e36..0000000000
--- a/plugins/syntax/z_syntax.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Bigint
-open Positive_syntax_plugin.Positive_syntax
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "z_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(**********************************************************************)
-(* Parsing Z via scopes                                               *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
-let glob_z = IndRef (z_kn,0)
-let path_of_ZERO = ((z_kn,0),1)
-let path_of_POS = ((z_kn,0),2)
-let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = ConstructRef path_of_ZERO
-let glob_POS = ConstructRef path_of_POS
-let glob_NEG = ConstructRef path_of_NEG
-
-let z_of_int ?loc n =
-  if not (Bigint.equal n zero) then
-    let sgn, n =
-      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
-  else
-    DAst.make ?loc @@ GRef(glob_ZERO, None)
-
-(**********************************************************************)
-(* Printing Z via scopes                                              *)
-(**********************************************************************)
-
-let bigint_of_z z = DAst.with_val (function
-  | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
-  | _ -> raise Non_closed_number
-  ) z
-
-let uninterp_z (AnyGlobConstr p) =
-  try
-    Some (bigint_of_z p)
-  with Non_closed_number -> None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for Z *)
-
-let _ = Notation.declare_numeral_interpreter "Z_scope"
-  (z_path,binnums)
-  z_of_int
-  ([DAst.make @@ GRef (glob_ZERO, None);
-    DAst.make @@ GRef (glob_POS, None);
-    DAst.make @@ GRef (glob_NEG, None)],
-  uninterp_z,
-  true)
diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack
deleted file mode 100644
index 411260c04c..0000000000
--- a/plugins/syntax/z_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Z_syntax