Introduce a Pcoq.Entry module for functions that ought to be exported.

We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.

Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.

2 files changed, 132 insertions, 104 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 93d65df2f..6726603e6 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -88,11 +88,10 @@ module type S =
   type action = Gramext.g_action
   type coq_parsable
 
-  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+  val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
 
   val comment_state : coq_parsable -> ((int * int) * string) list
 
@@ -107,7 +106,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
-  let parsable ?(file=Loc.ToplevelInput) c =
+  let coq_parsable ?(file=Loc.ToplevelInput) c =
     let state = ref (CLexer.init_lexer_state file) in
     CLexer.set_lexer_state !state;
     let a = parsable c in
@@ -132,7 +131,23 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   let comment_state (p,state) =
     CLexer.get_comment_state !state
 
-  let entry_print ft x = Entry.print ft x
+end
+
+module Parsable =
+struct
+  type t = G.coq_parsable
+  let make = G.coq_parsable
+  let comment_state = G.comment_state
+end
+
+module Entry =
+struct
+
+  type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+
+  let create = G.Entry.create
+  let parse = G.entry_parse
+  let print = G.Entry.print
 
 end
 
@@ -347,14 +362,14 @@ let make_rule r = [None, None, r]
 (** An entry that checks we reached the end of the input. *)
 
 let eoi_entry en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
+  let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
   let act = Gram.action (fun _ x loc -> x) in
   uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 let map_entry f en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
+  let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
   let act = Gram.action (fun x loc -> f x) in
   uncurry (Gram.extend e) (None, make_rule [symbs, act]);
@@ -364,7 +379,7 @@ let map_entry f en =
    (use eoi_entry) *)
 
 let parse_string f x =
-  let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
+  let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm)
 
 type gram_universe = string
 
@@ -385,14 +400,14 @@ let get_univ u =
 
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let e = Gram.entry_create ename in
+  let e = Entry.create ename in
   e
 
 let make_gen_entry u s = new_entry u s
 
 module GrammarObj =
 struct
-  type ('r, _, _) obj = 'r Gram.entry
+  type ('r, _, _) obj = 'r Entry.t
   let name = "grammar"
   let default _ = None
 end
@@ -402,7 +417,7 @@ module Grammar = Register(GrammarObj)
 let register_grammar = Grammar.register0
 let genarg_grammar = Grammar.obj
 
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
   let e = new_entry u s in
   let Rawwit t = etyp in
   let () = Grammar.register0 t e in
@@ -414,38 +429,38 @@ module Prim =
   struct
     let gec_gen n = make_gen_entry uprim n
 
-    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Entry.t table *)
     (* Typically for tactic or vernac extensions *)
     let preident = gec_gen "preident"
     let ident = gec_gen "ident"
     let natural = gec_gen "natural"
     let integer = gec_gen "integer"
-    let bigint = Gram.entry_create "Prim.bigint"
+    let bigint = Entry.create "Prim.bigint"
     let string = gec_gen "string"
-    let lstring = Gram.entry_create "Prim.lstring"
+    let lstring = Entry.create "Prim.lstring"
     let reference = make_gen_entry uprim "reference"
-    let by_notation = Gram.entry_create "by_notation"
-    let smart_global = Gram.entry_create "smart_global"
+    let by_notation = Entry.create "by_notation"
+    let smart_global = Entry.create "smart_global"
 
     (* parsed like ident but interpreted as a term *)
     let var = gec_gen "var"
 
-    let name = Gram.entry_create "Prim.name"
-    let identref = Gram.entry_create "Prim.identref"
-    let univ_decl = Gram.entry_create "Prim.univ_decl"
-    let ident_decl = Gram.entry_create "Prim.ident_decl"
-    let pattern_ident = Gram.entry_create "pattern_ident"
-    let pattern_identref = Gram.entry_create "pattern_identref"
+    let name = Entry.create "Prim.name"
+    let identref = Entry.create "Prim.identref"
+    let univ_decl = Entry.create "Prim.univ_decl"
+    let ident_decl = Entry.create "Prim.ident_decl"
+    let pattern_ident = Entry.create "pattern_ident"
+    let pattern_identref = Entry.create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
-    let base_ident = Gram.entry_create "Prim.base_ident"
+    let base_ident = Entry.create "Prim.base_ident"
 
-    let qualid = Gram.entry_create "Prim.qualid"
-    let fullyqualid = Gram.entry_create "Prim.fullyqualid"
-    let dirpath = Gram.entry_create "Prim.dirpath"
+    let qualid = Entry.create "Prim.qualid"
+    let fullyqualid = Entry.create "Prim.fullyqualid"
+    let dirpath = Entry.create "Prim.dirpath"
 
-    let ne_string = Gram.entry_create "Prim.ne_string"
-    let ne_lstring = Gram.entry_create "Prim.ne_lstring"
+    let ne_string = Entry.create "Prim.ne_string"
+    let ne_lstring = Entry.create "Prim.ne_lstring"
 
   end
 
@@ -453,7 +468,7 @@ module Constr =
   struct
     let gec_constr = make_gen_entry uconstr
 
-    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Entry.t table *)
     let constr = gec_constr "constr"
     let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
@@ -464,29 +479,29 @@ module Constr =
     let universe_level = make_gen_entry uconstr "universe_level"
     let sort = make_gen_entry uconstr "sort"
     let sort_family = make_gen_entry uconstr "sort_family"
-    let pattern = Gram.entry_create "constr:pattern"
+    let pattern = Entry.create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
-    let closed_binder = Gram.entry_create "constr:closed_binder"
-    let binder = Gram.entry_create "constr:binder"
-    let binders = Gram.entry_create "constr:binders"
-    let open_binders = Gram.entry_create "constr:open_binders"
-    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
-    let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
-    let record_declaration = Gram.entry_create "constr:record_declaration"
-    let appl_arg = Gram.entry_create "constr:appl_arg"
+    let closed_binder = Entry.create "constr:closed_binder"
+    let binder = Entry.create "constr:binder"
+    let binders = Entry.create "constr:binders"
+    let open_binders = Entry.create "constr:open_binders"
+    let binders_fixannot = Entry.create "constr:binders_fixannot"
+    let typeclass_constraint = Entry.create "constr:typeclass_constraint"
+    let record_declaration = Entry.create "constr:record_declaration"
+    let appl_arg = Entry.create "constr:appl_arg"
   end
 
 module Module =
   struct
-    let module_expr = Gram.entry_create "module_expr"
-    let module_type = Gram.entry_create "module_type"
+    let module_expr = Entry.create "module_expr"
+    let module_type = Entry.create "module_type"
   end
 
 let epsilon_value f e =
   let r = Rule (Next (Stop, e), fun x _ -> f x) in
   let ext = of_coq_extend_statement (None, [None, None, [r]]) in
-  let entry = G.entry_create "epsilon" in
+  let entry = Gram.entry_create "epsilon" in
   let () = uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
@@ -591,7 +606,7 @@ let () =
 
 (** Registering extra grammar *)
 
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ae4f5cab6..029c43713 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -24,21 +24,34 @@ module Gram : sig
   include Grammar.S with type te = Tok.t
 
   type 'a entry = 'a Entry.e
+  [@@ocaml.deprecated "Use [Pcoq.Entry.t]"]
 
-  type coq_parsable
+  [@@@ocaml.warning "-3"]
 
-  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
-
-  (* Get comment parsing information from the Lexer *)
-  val comment_state : coq_parsable -> ((int * int) * string) list
+  [@@ocaml.deprecated "Use [Pcoq.Entry.create]"]
 
   val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
 
+  [@@@ocaml.warning "+3"]
+
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
+module Parsable :
+sig
+  type t
+  val make : ?file:Loc.source -> char Stream.t -> t
+  (* Get comment parsing information from the Lexer *)
+  val comment_state : t -> ((int * int) * string) list
+end
+
+module Entry : sig
+  type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+  val create : string -> 'a t
+  val parse : 'a t -> Parsable.t -> 'a
+  val print : Format.formatter -> 'a t -> unit
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using
@@ -120,86 +133,86 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
 (** Parse a string *)
 
-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
+val parse_string : 'a Entry.t -> string -> 'a
+val eoi_entry : 'a Entry.t -> 'a Entry.t
+val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
 
 type gram_universe
 
 val get_univ : string -> gram_universe
 val create_universe : string -> gram_universe
 
-val new_entry : gram_universe -> string -> 'a Gram.entry
+val new_entry : gram_universe -> string -> 'a Entry.t
 
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
 
 
-val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
-val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
 
 val create_generic_entry : gram_universe -> string ->
-  ('a, rlevel) abstract_argument_type -> 'a Gram.entry
+  ('a, rlevel) abstract_argument_type -> 'a Entry.t
 
 module Prim :
   sig
     open Names
     open Libnames
-    val preident : string Gram.entry
-    val ident : Id.t Gram.entry
-    val name : lname Gram.entry
-    val identref : lident Gram.entry
-    val univ_decl : universe_decl_expr Gram.entry
-    val ident_decl : ident_decl Gram.entry
-    val pattern_ident : Id.t Gram.entry
-    val pattern_identref : lident Gram.entry
-    val base_ident : Id.t Gram.entry
-    val natural : int Gram.entry
-    val bigint : Constrexpr.raw_natural_number Gram.entry
-    val integer : int Gram.entry
-    val string : string Gram.entry
-    val lstring : lstring Gram.entry
-    val reference : qualid Gram.entry
-    val qualid : qualid Gram.entry
-    val fullyqualid : Id.t list CAst.t Gram.entry
-    val by_notation : (string * string option) Gram.entry
-    val smart_global : qualid or_by_notation Gram.entry
-    val dirpath : DirPath.t Gram.entry
-    val ne_string : string Gram.entry
-    val ne_lstring : lstring Gram.entry
-    val var : lident Gram.entry
+    val preident : string Entry.t
+    val ident : Id.t Entry.t
+    val name : lname Entry.t
+    val identref : lident Entry.t
+    val univ_decl : universe_decl_expr Entry.t
+    val ident_decl : ident_decl Entry.t
+    val pattern_ident : Id.t Entry.t
+    val pattern_identref : lident Entry.t
+    val base_ident : Id.t Entry.t
+    val natural : int Entry.t
+    val bigint : Constrexpr.raw_natural_number Entry.t
+    val integer : int Entry.t
+    val string : string Entry.t
+    val lstring : lstring Entry.t
+    val reference : qualid Entry.t
+    val qualid : qualid Entry.t
+    val fullyqualid : Id.t list CAst.t Entry.t
+    val by_notation : (string * string option) Entry.t
+    val smart_global : qualid or_by_notation Entry.t
+    val dirpath : DirPath.t Entry.t
+    val ne_string : string Entry.t
+    val ne_lstring : lstring Entry.t
+    val var : lident Entry.t
   end
 
 module Constr :
   sig
-    val constr : constr_expr Gram.entry
-    val constr_eoi : constr_expr Gram.entry
-    val lconstr : constr_expr Gram.entry
-    val binder_constr : constr_expr Gram.entry
-    val operconstr : constr_expr Gram.entry
-    val ident : Id.t Gram.entry
-    val global : qualid Gram.entry
-    val universe_level : Glob_term.glob_level Gram.entry
-    val sort : Glob_term.glob_sort Gram.entry
-    val sort_family : Sorts.family Gram.entry
-    val pattern : cases_pattern_expr Gram.entry
-    val constr_pattern : constr_expr Gram.entry
-    val lconstr_pattern : constr_expr Gram.entry
-    val closed_binder : local_binder_expr list Gram.entry
-    val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
-    val binders : local_binder_expr list Gram.entry (* list of binder *)
-    val open_binders : local_binder_expr list Gram.entry
-    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry
-    val typeclass_constraint : (lname * bool * constr_expr) Gram.entry
-    val record_declaration : constr_expr Gram.entry
-    val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry
+    val constr : constr_expr Entry.t
+    val constr_eoi : constr_expr Entry.t
+    val lconstr : constr_expr Entry.t
+    val binder_constr : constr_expr Entry.t
+    val operconstr : constr_expr Entry.t
+    val ident : Id.t Entry.t
+    val global : qualid Entry.t
+    val universe_level : Glob_term.glob_level Entry.t
+    val sort : Glob_term.glob_sort Entry.t
+    val sort_family : Sorts.family Entry.t
+    val pattern : cases_pattern_expr Entry.t
+    val constr_pattern : constr_expr Entry.t
+    val lconstr_pattern : constr_expr Entry.t
+    val closed_binder : local_binder_expr list Entry.t
+    val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
+    val binders : local_binder_expr list Entry.t (* list of binder *)
+    val open_binders : local_binder_expr list Entry.t
+    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+    val typeclass_constraint : (lname * bool * constr_expr) Entry.t
+    val record_declaration : constr_expr Entry.t
+    val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
   end
 
 module Module :
   sig
-    val module_expr : module_ast Gram.entry
-    val module_type : module_ast Gram.entry
+    val module_expr : module_ast Entry.t
+    val module_type : module_ast Entry.t
   end
 
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
@@ -209,7 +222,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 type gram_reinit = gram_assoc * gram_position
 (** Type of reinitialization data *)
 
-val grammar_extend : 'a Gram.entry -> gram_reinit option ->
+val grammar_extend : 'a Entry.t -> gram_reinit option ->
   'a Extend.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
@@ -225,7 +238,7 @@ type 'a grammar_command
     marshallable. *)
 
 type extend_rule =
-| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,
@@ -255,7 +268,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag
 
 (** Registering grammars by name *)
 
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list