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.

1 files changed, 63 insertions, 0 deletions

diff --git a/parsing/entry.ml b/parsing/entry.ml
new file mode 100644
index 0000000000..97d601320d
--- /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)