[parsing] Make grammar extension type private.

After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.

6 files changed, 64 insertions, 54 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5dae389a62..ba542101c8 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -325,51 +325,56 @@ let is_binder_level custom (custom',from) e = match e with
 | _ -> false
 
 let make_sep_rules = function
-  | [tk] -> Atoken tk
+  | [tk] ->
+    Pcoq.G.Symbol.token tk
   | tkl ->
-  let rec mkrule : 'a Tok.p list -> 'a rules = function
-  | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "")
-  | tkn :: rem ->
-    let Rules (r, f) = mkrule rem in
-    let r = NextNoRec (r, Atoken tkn) in
-    Rules (r, fun _ -> f)
-  in
-  let r = mkrule (List.rev tkl) in
-  Arules [r]
+    let rec mkrule : 'a Tok.p list -> 'a rules = function
+      | [] ->
+        Rules (Stop, fun _ -> (* dropped anyway: *) "")
+      | tkn :: rem ->
+        let Rules (r, f) = mkrule rem in
+        let r = NextNoRec (r, Pcoq.G.Symbol.token tkn) in
+        Rules (r, fun _ -> f)
+    in
+    let r = mkrule (List.rev tkl) in
+    Pcoq.G.Symbol.rules ~warning:None [r]
 
 type ('s, 'a) mayrec_symbol =
 | MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol
 | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
-  if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200"))
-  else if is_self custom from p then MayRecMay Aself
+  if is_binder_level custom from p
+  then
+    (* Prevent self *)
+    MayRecNo (Pcoq.G.Symbol.nterml (target_entry custom forpat) "200")
+  else if is_self custom from p then MayRecMay Pcoq.G.Symbol.self
   else
     let g = target_entry custom forpat in
     let lev = adjust_level custom assoc from p in
     begin match lev with
-    | DefaultLevel -> MayRecNo (Aentry g)
-    | NextLevel -> MayRecMay Anext
-    | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev))
+    | DefaultLevel -> MayRecNo (Pcoq.G.Symbol.nterm g)
+    | NextLevel -> MayRecMay Pcoq.G.Symbol.next
+    | NumLevel lev -> MayRecNo (Pcoq.G.Symbol.nterml g (string_of_int lev))
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
 | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
 | TTConstrList (s, typ', [], forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Alist1 s)
-  | MayRecMay s -> MayRecMay (Alist1 s) end
+  | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1 s)
+  | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1 s) end
 | TTConstrList (s, typ', tkl, forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
-  | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
-| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
-| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder))
-| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
-| TTName -> MayRecNo (Aentry Prim.name)
-| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
-| TTBigint -> MayRecNo (Aentry Prim.bignat)
-| TTReference -> MayRecNo (Aentry Constr.global)
+  | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false)
+  | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) end
+| TTPattern p -> MayRecNo (Pcoq.G.Symbol.nterml Constr.pattern (string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Pcoq.G.Symbol.list1 (Pcoq.G.Symbol.nterm Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Pcoq.G.Symbol.list1sep (Pcoq.G.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
+| TTName -> MayRecNo (Pcoq.G.Symbol.nterm Prim.name)
+| TTOpenBinderList -> MayRecNo (Pcoq.G.Symbol.nterm Constr.open_binders)
+| TTBigint -> MayRecNo (Pcoq.G.Symbol.nterm Prim.bignat)
+| TTReference -> MayRecNo (Pcoq.G.Symbol.nterm Constr.global)
 
 let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
@@ -461,16 +466,16 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
     ty_eval rem f { env with constrs; constrlists; }
 
 type ('s, 'a, 'r) mayrec_rule =
-| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, norec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
 
 let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
 | TyStop -> MayRecRNo Stop
 | TyMark (_, _, _, r) -> ty_erase r
 | TyNext (rem, TyTerm tok) ->
    begin match ty_erase rem with
-   | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok))
-   | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end
+   | MayRecRNo rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok))
+   | MayRecRMay rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) end
 | TyNext (rem, TyNonTerm (_, _, s, _)) ->
    begin match ty_erase rem, s with
    | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
@@ -522,7 +527,13 @@ let rec pure_sublevels' assoc from forpat level = function
    let rem = pure_sublevels' assoc from forpat level rem in
    let push where p rem =
      match symbol_of_target where p assoc from forpat with
-     | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem
+     | MayRecNo sym ->
+       (match Pcoq.G.level_of_nonterm sym with
+        | None -> rem
+        | Some i ->
+          if different_levels (fst from,level) (where,i) then
+            (where,int_of_string i) :: rem
+          else rem)
      | _ -> rem in
    (match e with
    | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 793aad6b24..bcd8de1ff4 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -24,9 +24,9 @@ type 's grammar_prod_item =
 type 'a ty_arg = ('a -> raw_generic_argument)
 
 type ('self, 'tr, _, 'r) ty_rule =
-| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule
-| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option ->
-  ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule
+| TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.symbol * 'b ty_arg option ->
+  ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function
 | [] -> AnyTyRule TyStop
 | GramTerminal s :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let tok = Atoken (CLexer.terminal s) in
+  let tok = Pcoq.G.Symbol.token (CLexer.terminal s) in
   let r = TyNext (rem, tok, None) in
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
@@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
-let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Extend.rule = function
-| TyStop -> Extend.Stop
-| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function
+| TyStop -> Pcoq.Stop
+| TyNext (rem, tok, _) -> Pcoq.Next (ty_erase rem, tok)
 
 type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
@@ -62,7 +62,7 @@ let make_rule f prod =
   let symb = ty_erase ty_rule in
   let f loc l = f loc (List.rev l) in
   let act = ty_eval ty_rule f in
-  Extend.Rule (symb, act)
+  Pcoq.Rule (symb, act)
 
 let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
 | TUentry a -> ExtraArg a
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 7f6656b079..e6e4748b59 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
-      ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
+      ('s, _, 'a) Pcoq.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   extend_name -> vernac_expr Pcoq.Entry.t option ->
@@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena
 
 val make_rule :
   (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
-  'a grammar_prod_item list -> 'a Extend.production_rule
+  'a grammar_prod_item list -> 'a Pcoq.production_rule
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 08625b41a6..aebded72f8 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -51,12 +51,11 @@ module Vernac_ =
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
-      let open Extend in
       let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
-        Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
-        Rule (Next (Stop, Aentry vernac_control), act_vernac);
+        Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi);
+        Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac);
       ] in
       Pcoq.grammar_extend main_entry (None, [None, None, rule])
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 0e8202da9f..fc6ece27cd 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c
     | Some Refl -> untype_command ty (f v) args
   end
 
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.symbol =
   let open Extend in function
-| TUlist1 l -> Alist1 (untype_user_symbol l)
-| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUlist0 l -> Alist0 (untype_user_symbol l)
-| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUopt o -> Aopt (untype_user_symbol o)
-| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a))
-| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i)
+| TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
+| TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
+| TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o)
+| TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+| TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
 
 let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
 | TyNil -> []
@@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext =
 
 type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
-| Arg_rules of 'a Extend.production_rule list
+| Arg_rules of 'a Pcoq.production_rule list
 
 type 'a vernac_argument = {
   arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 90c00415d4..0acb5f43f9 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -111,7 +111,7 @@ type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
   (** This is used because CAMLP5 parser can be dumb about rule factorization,
       which sometimes requires two entries to be the same. *)
-| Arg_rules of 'a Extend.production_rule list
+| Arg_rules of 'a Pcoq.production_rule list
   (** There is a discrepancy here as we use directly extension rules and thus
     entries instead of ty_user_symbol and thus arguments as roots. *)