Simplifying the code of Entry.

1 files changed, 34 insertions, 29 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index bf46fffff..238b9edd4 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)