Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).

1 files changed, 44 insertions, 36 deletions

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index caba4db4fc..19a15fd1df 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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"
@@ -16,7 +18,6 @@ open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Constr
-open Misctypes
 
 (** * Numeral notation *)
 
@@ -24,7 +25,7 @@ open Misctypes
 
     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
+    that starts with the right constructor but might be partially
     applied.
 
     At least [c] is known to be evar-free, since it comes from
@@ -55,7 +56,7 @@ 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_reference ty ++
+      strbrk "working with large numbers in " ++ pr_qualid ty ++
       strbrk " (threshold may vary depending" ++
       strbrk " on your system limits and on the command executed).")
 
@@ -64,11 +65,11 @@ let warn_abstract_large_num =
     (fun (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 " ++
+      pr_qualid 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
+    A bit nasty, but not critical: only used to decide when a
     number is considered as large (see warnings above). *)
 
 exception Comp of int
@@ -233,18 +234,24 @@ 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 "Numeral.interp: unexpected constr")
+  | _ -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++
+           Printer.pr_constr_env env sigma c)
 
 let no_such_number ?loc ty =
   CErrors.user_err ?loc
    (str "Cannot interpret this number as a value of type " ++
-    pr_reference ty)
+    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 -> CErrors.anomaly (str "Numeral.interp: option expected")
+  | x -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++
+           Printer.pr_constr_env env sigma c)
 
 let uninterp_option c =
   match Constr.kind c with
@@ -276,7 +283,7 @@ type numeral_notation_obj =
     to_ty : constr;
     of_kind : conversion_kind;
     of_ty : constr;
-    num_ty : Libnames.reference; (* for warnings / error messages *)
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
 let interp o ?loc n =
@@ -322,7 +329,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
 
 let load_numeral_notation _ (_, (uid,opts)) =
   Notation.register_rawnumeral_interpretation
-    uid (interp opts, uninterp opts)
+    ~allow_overwrite:true uid (interp opts, uninterp opts)
 
 let cache_numeral_notation x = load_numeral_notation 1 x
 
@@ -355,7 +362,7 @@ let unsafe_locate_ind q =
 
 let locate_ind q =
   try unsafe_locate_ind q
-  with Not_found -> Nametab.error_global_not_found (CAst.make q)
+  with Not_found -> Nametab.error_global_not_found q
 
 let locate_z () =
   try
@@ -367,35 +374,33 @@ let locate_int () =
   { uint = locate_ind q_uint;
     int = locate_ind q_int }
 
-let locate_globref r =
-  let q = qualid_of_reference r in
-  try Nametab.locate CAst.(q.v)
+let locate_globref q =
+  try Nametab.locate q
   with Not_found -> Nametab.error_global_not_found q
 
-let locate_constant r =
-  let q = qualid_of_reference r in
-  try Nametab.locate_constant CAst.(q.v)
+let locate_constant q =
+  try Nametab.locate_constant q
   with Not_found -> Nametab.error_global_not_found q
 
 let has_type f ty =
   let (sigma, env) = Pfedit.get_current_context () in
-  let c = mkCastC (mkRefC f, CastConv ty) 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_reference f ++ str " should go from Decimal.int to " ++
-     pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++
-     fnl () ++ str "Instead of int, the types uint or Z could be used" ++
-     (if loadZ then str " (load Z first)." else str "."))
+    (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_reference g ++ str " should go from " ++ pr_reference ty ++
-     str " to Decimal.int or (option int)." ++ fnl () ++
-     str "Instead of int, the types uint or Z could be used" ++
-     (if loadZ then str " (load Z first)." else str "."))
+    (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 ty f g scope opts =
   let int_ty = locate_int () in
@@ -405,7 +410,7 @@ let vernac_numeral_notation ty f g scope opts =
   let of_ty = mkConst (locate_constant g) in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
-  let cref q = mkRefC (CAst.make (Qualid q)) in
+  let cref q = mkRefC q in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
@@ -420,17 +425,20 @@ let vernac_numeral_notation ty f g scope opts =
        get_constructors ind
     | IndRef _ ->
        CErrors.user_err
-         (str "The inductive type " ++ pr_reference ty ++
-          str " cannot be polymorphic here for the moment")
+         (str "The inductive type " ++ pr_qualid ty ++
+          str " cannot be used in numeral notations because" ++
+          str " support for polymorphic inductive types is not yet implemented")
     | ConstRef _ | ConstructRef _ | VarRef _ ->
        CErrors.user_err
-        (pr_reference ty ++ str " is not an inductive type")
+        (pr_qualid ty ++ str " is not an inductive type")
   in
   (* Check the type of f *)
   let to_kind =
     if Global.is_polymorphic (Nametab.global f) then
       CErrors.user_err
-        (pr_reference f ++ str " cannot be polymorphic for the moment")
+        (str "The function " ++ pr_qualid f ++ str " cannot be used" ++
+         str " in numeral notations because support for polymorphic" ++
+         str " printing and parsing functions is not yet implemented.")
     else 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
@@ -447,7 +455,7 @@ let vernac_numeral_notation ty f g scope opts =
   let of_kind =
     if Global.is_polymorphic (Nametab.global g) then
       CErrors.user_err
-        (pr_reference g ++ str " cannot be polymorphic for the moment")
+        (pr_qualid g ++ str " cannot be polymorphic for the moment")
     else 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