Simplifying the code of Entry.

5 files changed, 52 insertions, 96 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aef9b10b26..b8bc0483d3 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/parsing/entry.ml b/parsing/entry.ml
index 0519903d3d..b7c6c23fa6 100644
--- a/parsing/entry.ml
+++ b/parsing/entry.ml
@@ -9,51 +9,22 @@
 open Errors
 open Util
 
-type 'a t = string * string
-
-type repr = string * 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))
+type 'a t = string
 
 (** Entries are registered with a unique name *)
 
 let entries = ref String.Set.empty
 
-let create u name =
-  let uname = u ^ ":" ^ name in
+let create name =
   let () =
-    if String.Set.mem uname !entries then
-    anomaly (Pp.str ("Entry " ^ uname ^ " already defined"))
+    if String.Set.mem name !entries then
+    anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
   in
-  let () = entries := String.Set.add uname !entries in
-  (u, name)
-
-let dynamic name = ("", name)
+  let () = entries := String.Set.add name !entries in
+  name
 
-let unsafe_of_name (u, s) =
-  let uname = u ^ ":" ^ s in
-  assert (String.Set.mem uname !entries);
-  (u, s)
+let unsafe_of_name name =
+  assert (String.Set.mem name !entries);
+  name
 
-let repr (u, s) = (u, s)
+let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
index 97cd5b1105..4c73fe2049 100644
--- a/parsing/entry.mli
+++ b/parsing/entry.mli
@@ -11,34 +11,13 @@
 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. *)
+    unique names. They should be kept synchronized with the {!Pcoq} entries. *)
 
-type repr = string * 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
+val create : string -> 'a t
 (** Create an entry. They should be synchronized with the entries defined in
     {!Pcoq}. *)
 
 (** {5 Meta-programming} *)
 
-val repr : 'a t -> repr
-
-val unsafe_of_name : (string * string) -> 'a t
+val repr : 'a t -> string
+val unsafe_of_name : string -> 'a t
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index bf46fffffe..238b9edd44 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -198,40 +198,49 @@ 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 = Entry.universe
-
-let uprim   = Entry.uprim
-let uconstr = Entry.uconstr
-let utactic = Entry.utactic
-let uvernac = Entry.uvernac
-let get_univ = Entry.get_univ
+type gram_universe = string
 
 let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
   Hashtbl.create 97
 
+let create_universe u =
+  let table = Hashtbl.create 97 in
+  let () = Hashtbl.add utables u table in
+  u
+
+let uprim   = create_universe "prim"
+let uconstr = create_universe "constr"
+let utactic = create_universe "tactic"
+let uvernac = create_universe "vernac"
+
+let get_univ u =
+  if Hashtbl.mem utables u then u
+  else raise Not_found
+
 let get_utable u =
-  let u = Entry.univ_name u in
   try Hashtbl.find utables u
-  with Not_found ->
-    let table = Hashtbl.create 97 in
-    Hashtbl.add utables u table;
-    table
+  with Not_found -> assert false
 
 let get_entry u s =
   let utab = get_utable u in
   Hashtbl.find utab s
 
-let get_typed_entry e =
-  let (u, s) = Entry.repr e in
-  let u = Entry.get_univ u in
-  get_entry u s
+(** A table associating grammar to entries *)
+let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
+
+let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
+  Obj.magic (String.Map.find (Entry.repr e) !gtable)
+
+let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
+  assert (not (String.Map.mem (Entry.repr e) !gtable));
+  gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
 
 let new_entry etyp u s =
   let utab = get_utable u in
-  let uname = Entry.univ_name u in
-  let _ = Entry.create u s in
-  let ename = uname ^ ":" ^ s in
+  let ename = u ^ ":" ^ s in
+  let entry = Entry.create ename in
   let e = Gram.entry_create ename in
+  let () = set_grammar entry e in
   Hashtbl.add utab s (TypedEntry (etyp, e)); e
 
 let make_gen_entry u rawwit s = new_entry rawwit u s
@@ -251,8 +260,7 @@ let genarg_grammar = Grammar.obj
 let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
   let utab = get_utable u in
   if Hashtbl.mem utab s then
-    let u = Entry.univ_name u in
-    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists");
+    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists")
   else
     let e = new_entry etyp u s in
     let Rawwit t = etyp in
@@ -603,7 +611,6 @@ let compute_entry adjust forpat = function
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
   | ETOther (u,n) ->
-      let u = get_univ u in
       let e = get_entry u n in
       object_of_typed_entry e, None, true
 
@@ -696,11 +703,11 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
   | Aentry e ->
-    let e = get_typed_entry e in
-    Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
+    let e = get_grammar e in
+    Symbols.snterm (Gram.Entry.obj (weaken_entry e))
   | 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 e = get_grammar e in
+    Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
 
 let level_of_snterml e = int_of_string (Symbols.snterml_level e)
 
@@ -742,9 +749,7 @@ let coincide s pat off =
   done;
   !break
 
-let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
-| u :: s :: [] -> Entry.unsafe_of_name (u, s)
-| _ -> assert false
+let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
 
 let atactic n =
   if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e57da42cb3..c1c0187137 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -149,7 +149,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
 
-type gram_universe = Entry.universe
+type gram_universe
 
 val get_univ : string -> gram_universe
 
@@ -158,6 +158,7 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
+val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry