Merge PR #8464: Fix numeral notations

14 files changed, 459 insertions, 380 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index a6a14efc87..02c7812e21 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -379,23 +379,364 @@ module InnerPrimToken = struct
 
 end
 
-(* The following two tables of (un)interpreters will *not* be synchronized.
-   But their indexes will be checked to be unique *)
+(* The following two tables of (un)interpreters will *not* be
+   synchronized.  But their indexes will be checked to be unique.
+   These tables contain primitive token interpreters which are
+   registered in plugins, such as string and ascii syntax.  It is
+   essential that only plugins add to these tables, and that
+   vernacular commands do not.  See
+   https://github.com/coq/coq/issues/8401 for details of what goes
+   wrong when vernacular commands add to these tables. *)
 let prim_token_interpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t)
 
 let prim_token_uninterpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
 
+(*******************************************************)
+(* Numeral notation interpretation                     *)
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : 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 *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+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 }
+
+module Numeral = struct
+(** * 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 " ++
+      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+
+(** 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 *)
+
+(** 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 *)
+
+(** 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 env sigma c = match Constr.kind c with
+  | App (c, ca) ->
+      let c = glob_of_constr ?loc env sigma c in
+      let cel = List.map (glob_of_constr ?loc env sigma) (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))
+  | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
+
+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 env sigma c =
+  match Constr.kind c with
+  | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
+  | App (_None, [| _ |]) -> no_such_number ?loc ty
+  | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
+
+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)
+
+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 env sigma (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 env sigma res
+     | Option -> interp_option o.num_ty ?loc env sigma 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 *)
+end
+
+(* A [prim_token_infos], which is synchronized with the document
+   state, either contains a unique id pointing to an unsynchronized
+   prim token function, or a numeral notation object describing how to
+   interpret and uninterpret.  We provide [prim_token_infos] because
+   we expect plugins to provide their own interpretation functions,
+   rather than going through numeral notations, which are available as
+   a vernacular. *)
+
+type prim_token_interp_info =
+    Uid of prim_token_uid
+  | NumeralNotation of numeral_notation_obj
+
+type prim_token_infos = {
+  pt_local : bool; (** Is this interpretation local? *)
+  pt_scope : scope_name; (** Concerned scope *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+  pt_required : required_module; (** Module that should be loaded first *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
+  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
 (* Table from scope_name to backtrack-able informations about interpreters
    (in particular interpreter unique id). *)
 let prim_token_interp_infos =
-  ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t)
+  ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t)
 
 (* Table from global_reference to backtrack-able informations about
    prim_token uninterpretation (in particular uninterpreter unique id). *)
 let prim_token_uninterp_infos =
-  ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t)
+  ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t)
 
 let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
@@ -425,23 +766,14 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter
   register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
-type prim_token_infos = {
-  pt_local : bool; (** Is this interpretation local? *)
-  pt_scope : scope_name; (** Concerned scope *)
-  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
-  pt_required : required_module; (** Module that should be loaded first *)
-  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
-  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
-}
-
 let cache_prim_token_interpretation (_,infos) =
+  let ptii = infos.pt_interp_info in
   let sc = infos.pt_scope in
-  let uid = infos.pt_uid in
   check_scope ~tolerant:true sc;
   prim_token_interp_infos :=
-    String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
+    String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
   List.iter (fun r -> prim_token_uninterp_infos :=
-                        GlobRef.Map.add r (sc,uid,infos.pt_in_match)
+                        GlobRef.Map.add r (sc,ptii,infos.pt_in_match)
                           !prim_token_uninterp_infos)
             infos.pt_refs
 
@@ -479,7 +811,7 @@ let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   enable_prim_token_interpretation
     { pt_local = local;
       pt_scope = sc;
-      pt_uid = uid;
+      pt_interp_info = Uid uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
@@ -489,7 +821,7 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   enable_prim_token_interpretation
     { pt_local = local;
       pt_scope = sc;
-      pt_uid = uid;
+      pt_interp_info = Uid uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
@@ -605,9 +937,12 @@ let find_prim_token check_allowed ?loc p sc =
     pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in
+  let (spdir,info) = String.Map.find sc !prim_token_interp_infos in
   check_required_module ?loc sc spdir;
-  let interp = Hashtbl.find prim_token_interpreters uid in
+  let interp = match info with
+    | Uid uid -> Hashtbl.find prim_token_interpreters uid
+    | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+  in
   let pat = InnerPrimToken.do_interp ?loc interp p in
   check_allowed pat;
   pat, ((dirpath (fst spdir),DirPath.empty),"")
@@ -783,8 +1118,11 @@ let uninterp_prim_token c =
   | None -> raise Notation_ops.No_match
   | Some r ->
      try
-       let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
-       let uninterp = Hashtbl.find prim_token_uninterpreters uid in
+       let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
+       let uninterp = match info with
+         | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+         | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+       in
        match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
        | None -> raise Notation_ops.No_match
        | Some n -> (sc,n)
@@ -799,12 +1137,16 @@ let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
     try
       let uid = snd (String.Map.find scope !prim_token_interp_infos) in
-      let interp = Hashtbl.find prim_token_interpreters uid in
       let open InnerPrimToken in
-      match n, interp with
-      | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
-      | String _, StringInterp _ -> true
-      | _ -> false
+      match n, uid with
+      | Numeral _, NumeralNotation _ -> true
+      | _, NumeralNotation _ -> false
+      | _, Uid uid ->
+        let interp = Hashtbl.find prim_token_interpreters uid in
+        match n, interp with
+        | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+        | String _, StringInterp _ -> true
+        | _ -> false
     with Not_found -> false
   in
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index 6e59c0fd70..734198bbf6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -102,10 +102,51 @@ val register_bignumeral_interpretation :
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
+(** * Numeral notation *)
+
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : 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 *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+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 }
+
+type prim_token_interp_info =
+    Uid of prim_token_uid
+  | NumeralNotation of numeral_notation_obj
+
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5e36fbeb81..53153198f9 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -94,7 +94,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = 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
index ec14df3baa..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
+open Notation
 open Numeral
 open Pp
 open Names
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index d3ffe936a9..e34a401c2c 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -108,7 +108,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = int31_scope;
-      pt_uid = int31_scope;
+      pt_interp_info = Uid int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
       pt_in_match = true }
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index fee93593d0..10a0af0b8f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -15,351 +15,18 @@ open Libnames
 open Globnames
 open Constrexpr
 open Constrexpr_ops
-open Constr
+open Notation
 
 (** * 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 " ++
+      Nametab.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
@@ -464,15 +131,12 @@ let vernac_numeral_notation local ty f g scope opts =
   (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.(
+  let i =
        { pt_local = local;
          pt_scope = scope;
-         pt_uid = uid;
+         pt_interp_info = NumeralNotation o;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
-         pt_in_match = true })
+         pt_in_match = true }
   in
-  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
-  Notation.enable_prim_token_interpretation i
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 83ede6f48f..f96b8321f8 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -9,14 +9,9 @@
 (************************************************************************)
 
 open Libnames
-open Constrexpr
 open Vernacexpr
+open Notation
 
 (** * 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/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 04946c158b..49497aef54 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -143,7 +143,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
-      pt_uid = r_scope;
+      pt_interp_info = 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 640bcfde91..7478c1e978 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -75,7 +75,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];
       pt_in_match = true }
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e8ca719932..613581ade7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,7 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
diff --git a/test-suite/vio/numeral.v b/test-suite/vio/numeral.v
new file mode 100644
index 0000000000..f28355bb29
--- /dev/null
+++ b/test-suite/vio/numeral.v
@@ -0,0 +1,21 @@
+Lemma foo : True.
+Proof.
+Check 0 : nat.
+Check 0 : nat.
+exact I.
+Qed.
+
+Lemma bar : True.
+Proof.
+pose (0 : nat).
+exact I.
+Qed.
+
+Require Import Coq.Strings.Ascii.
+Open Scope char_scope.
+
+Lemma baz : True.
+Proof.
+pose "s".
+exact I.
+Qed.
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 504e7095b0..7cf4e64805 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,6 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
       wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+  | Notation.NumeralNotationError(ctx,sigma,te) ->
+      wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
       wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
   | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a4650cfd92..e7b2a0e8a6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1315,3 +1315,13 @@ let explain_reduction_tactic_error = function
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' (Evd.from_env env') e
+
+let explain_numeral_notation_error env sigma = function
+  | Notation.UnexpectedTerm c ->
+    (strbrk "Unexpected term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")
+  | Notation.UnexpectedNonOptionTerm c ->
+    (strbrk "Unexpected non-option term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 91caddcf13..02b3c45501 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -46,3 +46,5 @@ val explain_module_internalization_error :
 
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+
+val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t