Pcoq entries are given a proper module.

Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.

10 files changed, 199 insertions, 55 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index de43efa67..1a2819feb 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -191,6 +191,7 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
+Entry
 Pcoq
 Printer
 Pptactic
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1d3d711ac..7b807a343 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -519,7 +519,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 let _ =
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+        (Loc.ghost,ConstrArgType,Aentry (Entry.unsafe_of_name ("constr","constr")),
 	 Some (Names.Id.of_string "c"))]
 
 (* Setting printer of unbound global reference *)
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 60ea0df02..7e4eea641 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -51,6 +51,7 @@ Constrexpr_ops
 Compat
 Tok
 Lexer
+Entry
 Pcoq
 G_prim
 G_tactic
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 20c83dfaf..5ec7510f7 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -58,6 +58,13 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi
   | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
-  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry ($str:u$, $str:s$) >>
-  | Pcoq.Aentryl ((u,s), l) -> <:expr< Pcoq.Aentryl ($str:u$, $str:s$) $mlexpr_of_int l$ >>
+  | Pcoq.Aentry e ->
+    begin match Entry.repr e with
+    | Entry.Dynamic s -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
+    | Entry.Static (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
+    end
+  | Pcoq.Aentryl (e, l) ->
+    begin match Entry.repr e with
+    | Entry.Dynamic s -> <:expr< Pcoq.Aentryl (Pcoq.name_of_entry $lid:s$) >>
+    | Entry.Static (u, s) -> <:expr< Pcoq.Aentryl (Entry.unsafe_of_name ($str:u$, $str:s$)) $mlexpr_of_int l$ >>
+    end
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 70151cef1..4709a7998 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -162,7 +162,11 @@ let is_constr_gram = function
 | GramTerminal _ -> false
 | GramNonTerminal (_, _, e, _) ->
   match e with
-  | Aentry ("constr", "constr") -> true
+  | Aentry e ->
+    begin match Entry.repr e with
+    | Entry.Static ("constr", "constr") -> true
+    | _ -> false
+    end
   | _ -> false
 
 let make_var = function
diff --git a/parsing/entry.ml b/parsing/entry.ml
new file mode 100644
index 000000000..97d601320
--- /dev/null
+++ b/parsing/entry.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Errors
+open Util
+
+type 'a t = string * string
+
+type repr =
+| Static of string * string
+| Dynamic of string
+
+type universe = string
+
+(* The univ_tab is not part of the state. It contains all the grammars that
+   exist or have existed before in the session. *)
+
+let univ_tab = (Hashtbl.create 7 : (string, unit) Hashtbl.t)
+
+let create_univ s =
+  Hashtbl.add univ_tab s (); s
+
+let univ_name s = s
+
+let uprim   = create_univ "prim"
+let uconstr = create_univ "constr"
+let utactic = create_univ "tactic"
+let uvernac = create_univ "vernac"
+
+let get_univ s =
+  try
+    Hashtbl.find univ_tab s; s
+  with Not_found ->
+    anomaly (Pp.str ("Unknown grammar universe: "^s))
+
+(** Entries are registered with a unique name *)
+
+let entries = ref String.Set.empty
+
+let create u name =
+  let uname = u ^ ":" ^ name in
+  let () =
+    if String.Set.mem uname !entries then
+    anomaly (Pp.str ("Entry " ^ uname ^ " already defined"))
+  in
+  let () = entries := String.Set.add uname !entries in
+  (u, name)
+
+let dynamic name = ("", name)
+
+let unsafe_of_name (u, s) =
+  let uname = u ^ ":" ^ s in
+  assert (String.Set.mem uname !entries);
+  (u, s)
+
+let repr = function
+| ("", u) -> Dynamic u
+| (u, s) -> Static (u, s)
diff --git a/parsing/entry.mli b/parsing/entry.mli
new file mode 100644
index 000000000..6854a5cb4
--- /dev/null
+++ b/parsing/entry.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Typed grammar entries *)
+
+type 'a t
+(** Typed grammar entries. We need to defined them here so that they are
+    marshallable and defined before the Pcoq.Gram module. They are basically
+    unique names made of a universe and an entry name. They should be kept
+    synchronized with the {!Pcoq} entries though. *)
+
+type repr =
+| Static of string * string
+| Dynamic of string
+(** Representation of entries. *)
+
+(** Table of Coq statically defined grammar entries *)
+
+type universe
+
+(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
+
+val get_univ : string -> universe
+val univ_name : universe -> string
+
+val uprim : universe
+val uconstr : universe
+val utactic : universe
+val uvernac : universe
+
+(** {5 Uniquely defined entries} *)
+
+val create : universe -> string -> 'a t
+(** Create an entry. They should be synchronized with the entries defined in
+    {!Pcoq}. *)
+
+(** {5 Meta-programming} *)
+
+val dynamic : string -> 'a t
+(** Dynamic entries. They refer to entries defined in the code source and may
+    only be used in meta-programming definitions from the grammar directory. *)
+
+val repr : 'a t -> repr
+
+val unsafe_of_name : (string * string) -> 'a t
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index a0cb83193..024d8607f 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,7 @@
 Tok
 Compat
 Lexer
+Entry
 Pcoq
 Egramml
 Egramcoq
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b244a021e..5b980b348 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -76,8 +76,8 @@ type ('self, _) entry_key =
 | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
-| Aentry : (string * string) -> ('self, 'a) entry_key
-| Aentryl : (string * string) * int -> ('self, 'a) entry_key
+| Aentry : 'a Entry.t -> ('self, 'a) entry_key
+| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
 
 type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
 
@@ -217,45 +217,58 @@ let map_entry f en =
 let parse_string f x =
   let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
 
-type gram_universe = string * (string, typed_entry) Hashtbl.t
+type gram_universe = Entry.universe
 
 let trace = ref false
 
-(* The univ_tab is not part of the state. It contains all the grammars that
-   exist or have existed before in the session. *)
+let uprim   = Entry.uprim
+let uconstr = Entry.uconstr
+let utactic = Entry.utactic
+let uvernac = Entry.uvernac
+let get_univ = Entry.get_univ
 
-let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t)
+let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
+  Hashtbl.create 97
 
-let create_univ s =
-  let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
-
-let uprim   = create_univ "prim"
-let uconstr = create_univ "constr"
-let utactic = create_univ "tactic"
-let uvernac = create_univ "vernac"
-
-let get_univ s =
-  try
-    Hashtbl.find univ_tab s
+let get_utable u =
+  let u = Entry.univ_name u in
+  try Hashtbl.find utables u
   with Not_found ->
-    anomaly (Pp.str ("Unknown grammar universe: "^s))
-
-let get_entry (u, utab) s = Hashtbl.find utab s
-
-let new_entry etyp (u, utab) s =
-  if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
-  let ename = u ^ ":" ^ s in
+    let table = Hashtbl.create 97 in
+    Hashtbl.add utables u table;
+    table
+
+let get_entry u s =
+  let utab = get_utable u in
+  Hashtbl.find utab s
+
+let get_typed_entry e =
+  let (u, s) = match Entry.repr e with
+  | Entry.Dynamic _ -> assert false
+  | Entry.Static (u, s) -> (u, s)
+  in
+  let u = Entry.get_univ u in
+  get_entry u s
+
+let new_entry etyp u s =
+  let utab = get_utable u in
+  let uname = Entry.univ_name u in
+  if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" uname s; flush stderr);
+  let _ = Entry.create u s in
+  let ename = uname ^ ":" ^ s in
   let e = in_typed_entry etyp (Gram.entry_create ename) in
   Hashtbl.add utab s e; e
 
-let create_entry (u, utab) s etyp =
+let create_entry u s etyp =
+  let utab = get_utable u in
   try
     let e = Hashtbl.find utab s in
+    let u = Entry.univ_name u in
     if not (argument_type_eq (type_of_typed_entry e) etyp) then
       failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
     e
   with Not_found ->
-    new_entry etyp (u, utab) s
+    new_entry etyp u s
 
 let create_constr_entry s =
   outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
@@ -266,8 +279,11 @@ let create_generic_entry s wit =
 (* [make_gen_entry] builds entries extensible by giving its name (a string) *)
 (* For entries extensible only via the ML name, Gram.entry_create is enough *)
 
-let make_gen_entry (u,univ) rawwit s =
-  let e = Gram.entry_create (u ^ ":" ^ s) in
+let make_gen_entry u rawwit s =
+  let univ = get_utable u in
+  let uname = Entry.univ_name u in
+  let e = Gram.entry_create (uname ^ ":" ^ s) in
+  let _ = Entry.create u s in
   Hashtbl.add univ s (inGramObj rawwit e); e
 
 (* Initial grammar entries *)
@@ -355,7 +371,7 @@ module Tactic =
       make_gen_entry utactic (rawwit wit_bindings) "bindings"
     let hypident = Gram.entry_create "hypident"
     let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
-    let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
+    let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval"
     let uconstr =
       make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
     let quantified_hypothesis =
@@ -707,11 +723,11 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
 	   Gram.action (fun _ l _ _loc -> l))]
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
-  | Aentry (u,s) ->
-    let e = get_entry (get_univ u) s in
+  | Aentry e ->
+    let e = get_typed_entry e in
     Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
-  | Aentryl ((u, s), n) ->
-    let e = get_entry (get_univ u) s in
+  | Aentryl (e, n) ->
+    let e = get_typed_entry e in
     Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n)
 
 let level_of_snterml e = int_of_string (Symbols.snterml_level e)
@@ -741,13 +757,18 @@ let type_of_entry u s =
   type_of_typed_entry (get_entry u s)
 
 let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
-| u :: s :: [] -> (u, s)
+| u :: s :: [] -> Entry.unsafe_of_name (u, s)
 | _ -> assert false
 
 let atactic n =
   if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
   else Aentryl (name_of_entry Tactic.tactic_expr, n)
 
+let try_get_entry u s =
+  (** Order the effects: type_of_entry can raise Not_found *)
+  let typ = type_of_entry u s in
+  Some typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s))
+
 let rec interp_entry_name static up_level s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
@@ -789,13 +810,13 @@ let rec interp_entry_name static up_level s sep =
         in
         (Some t, se)
       | None ->
-      try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found ->
-      try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found ->
-      try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found ->
+      try try_get_entry uprim s with Not_found ->
+      try try_get_entry uconstr s with Not_found ->
+      try try_get_entry utactic s with Not_found ->
 	if static then
 	  error ("Unknown entry "^s^".")
 	else
-	  None, Aentry ("",s) in
+	  None, Aentry (Entry.dynamic s) in
     let t =
       match t with
 	| Some t -> t
@@ -804,6 +825,6 @@ let rec interp_entry_name static up_level s sep =
 
 let list_entry_names () =
   let add_entry key (entry, _) accu = (key, entry) :: accu in
-  let ans = Hashtbl.fold add_entry (snd uprim) [] in
-  let ans = Hashtbl.fold add_entry (snd uconstr) ans in
-  Hashtbl.fold add_entry (snd utactic) ans
+  let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
+  let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
+  Hashtbl.fold add_entry (get_utable utactic) ans
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 959c039d3..18eb3eed3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -137,11 +137,7 @@ val parse_string : 'a Gram.entry -> string -> 'a
 val eoi_entry : 'a Gram.entry -> 'a Gram.entry
 val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
 
-(** Table of Coq statically defined grammar entries *)
-
-type gram_universe
-
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
+type gram_universe = Entry.universe
 
 val get_univ : string -> gram_universe
 
@@ -273,10 +269,10 @@ type ('self, _) entry_key =
 | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
-| Aentry : (string * string) -> ('self, 'a) entry_key
-| Aentryl : (string * string) * int -> ('self, 'a) entry_key
+| Aentry : 'a Entry.t -> ('self, 'a) entry_key
+| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
 
-val name_of_entry : 'a Gram.entry -> string * string
+val name_of_entry : 'a Gram.entry -> 'a Entry.t
 
 (** Binding general entry keys to symbols *)