[parsing] Make grammar rules 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.

10 files changed, 65 insertions, 59 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 5d1f0a876f..70e400c29b 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -217,13 +217,13 @@ let rec print_prod fmt p =
 
 and print_extrule fmt (tkn, vars, body) =
   let tkn = List.rev tkn in
-  fprintf fmt "@[Pcoq.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
+  fprintf fmt "@[Pcoq.G.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
 
 and print_symbols ~norec fmt = function
-| [] -> fprintf fmt "Pcoq.Stop"
+| [] -> fprintf fmt "Pcoq.G.Rule.stop"
 | tkn :: tkns ->
-  let c = if norec then "Pcoq.NextNoRec" else "Pcoq.Next" in
-  fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn
+  let c = if norec then "Pcoq.G.Rule.next_norec" else "Pcoq.G.Rule.next" in
+  fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn
 
 and print_symbol fmt tkn = match tkn with
 | SymbToken (t, s) ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 5601dcb474..8f7d6d1966 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -59,6 +59,7 @@ module G : sig
   val comment_state : Parsable.t -> ((int * int) * string) list
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
   val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
+  val mk_rule : 'a Tok.p list -> string rules
 
 end with type 'a Entry.t = 'a Extend.entry = struct
 
@@ -253,6 +254,15 @@ end with type 'a Entry.t = 'a Extend.entry = struct
     try Some (generalize_symbol s)
     with SelfSymbol -> None
 
+  let rec mk_rule tok =
+    match tok with
+    | [] ->
+      let stop_e = Stop in
+      Rules (stop_e, fun _ -> (* dropped anyway: *) "")
+    | tkn :: rem ->
+      let Rules (r, f) = mk_rule rem in
+      let r = Rule.next_norec r (Symbol.token tkn) in
+      Rules (r, fun _ -> f)
 end
 
 module Parsable = struct
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 63a4c1dd58..e7e3e9442b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -224,20 +224,13 @@ module Module :
 (** {5 Type-safe grammar extension} *)
 
 type ('self, 'trec, 'a) symbol
+type ('self, 'trec, _, 'r) rule
 
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type ('self, 'trec, _, 'r) rule =
-| Stop : ('self, norec, 'r, 'r) rule
-| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule
-| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule
-
-type 'a rules =
-  | Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
-
-type 'a production_rule =
-  | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
+type 'a rules
+type 'a production_rule
 
 module G : sig
 
@@ -245,6 +238,7 @@ module G : sig
 
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
   val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
+  val mk_rule : 'a Tok.p list -> string rules
 
 end with type 'a Entry.t = 'a Entry.t
      and type te = Tok.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 53b5386375..6b83590b1d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -406,15 +406,21 @@ let create_ltac_quotation name cast (e, l) =
   let level = None in
   let assoc = None in
   let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Pcoq.G.Symbol.token (CLexer.terminal name)),
-      Pcoq.G.Symbol.token (CLexer.terminal ":")),
-      Pcoq.G.Symbol.token (CLexer.terminal "(")),
-      entry),
-      Pcoq.G.Symbol.token (CLexer.terminal ")"))
+    Pcoq.G.(
+      Rule.next
+        (Rule.next
+           (Rule.next
+              (Rule.next
+                 (Rule.next
+                    Rule.stop
+                    (Symbol.token (CLexer.terminal name)))
+                 (Symbol.token (CLexer.terminal ":")))
+              (Symbol.token (CLexer.terminal "(")))
+           entry)
+        (Symbol.token (CLexer.terminal ")")))
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
+  let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
   Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
 
 (** Command *)
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 52d92d87c0..8b3203c8dd 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -827,10 +827,11 @@ END
 let () =
 
 let open Tok in
-let (++) r s = Next (r, s) in
+let (++) r s = Pcoq.G.Rule.next r s in
 let rules = [
-  Rule (
-    Stop ++ Pcoq.G.Symbol.nterm test_dollar_ident ++ Pcoq.G.Symbol.token (PKEYWORD "$") ++ Pcoq.G.Symbol.nterm Prim.ident,
+  Pcoq.G.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident)
     begin fun id _ _ loc ->
       let id = Loc.tag ~loc id in
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
@@ -838,8 +839,9 @@ let rules = [
     end
   );
 
-  Rule (
-    Stop ++ Pcoq.G.Symbol.nterm test_ampersand_ident ++ Pcoq.G.Symbol.token (PKEYWORD "&") ++ Pcoq.G.Symbol.nterm Prim.ident,
+  Pcoq.G.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident)
     begin fun id _ _ loc ->
       let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
@@ -847,9 +849,10 @@ let rules = [
     end
   );
 
-  Rule (
-    Stop ++ Pcoq.G.Symbol.token (PIDENT (Some "ltac2")) ++ Pcoq.G.Symbol.token (PKEYWORD ":") ++
-      Pcoq.G.Symbol.token (PKEYWORD "(") ++ Pcoq.G.Symbol.nterm tac2expr ++ Pcoq.G.Symbol.token (PKEYWORD ")"),
+  Pcoq.G.(
+    Production.make
+      (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
+       Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
     begin fun _ tac _ _ _ loc ->
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2edbcc38f5..547ca0c2ed 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1594,7 +1594,7 @@ type seqrule =
 
 let rec make_seq_rule = function
 | [] ->
-  Seqrule (Stop, CvNil)
+  Seqrule (Pcoq.G.Rule.stop, CvNil)
 | tok :: rem ->
   let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
   let scope =
@@ -1604,7 +1604,7 @@ let rec make_seq_rule = function
     | Some scope -> scope
   in
   let Seqrule (r, c) = make_seq_rule rem in
-  let r = NextNoRec (r, scope) in
+  let r = Pcoq.G.Rule.next_norec r scope in
   let f = match tok with
   | SexprStr _ -> None (* Leave out mere strings *)
   | _ -> Some f
@@ -1614,7 +1614,7 @@ let rec make_seq_rule = function
 let () = add_scope "seq" begin fun toks ->
   let scope =
     let Seqrule (r, c) = make_seq_rule (List.rev toks) in
-    Pcoq.G.Symbol.rules ~warning:None [Rules (r, apply c [])]
+    Pcoq.G.(Symbol.rules ~warning:None [Rules.make r (apply c [])])
   in
   Tac2entries.ScopeRule (scope, (fun e -> e))
 end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d5d5bad987..c5f081eab9 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -615,15 +615,15 @@ type krule =
   ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
 
 let rec get_rule (tok : scope_rule token list) : krule = match tok with
-| [] -> KRule (Pcoq.Stop, fun k loc -> k loc [])
+| [] -> KRule (Pcoq.G.Rule.stop, fun k loc -> k loc [])
 | TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
   let KRule (rule, act) = get_rule tok in
-  let rule = Pcoq.Next (rule, scope) in
+  let rule = Pcoq.G.Rule.next rule scope in
   let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
   KRule (rule, act)
 | TacTerm t :: tok ->
   let KRule (rule, act) = get_rule tok in
-  let rule = Pcoq.Next (rule, Pcoq.G.Symbol.token (CLexer.terminal t)) in
+  let rule = Pcoq.G.(Rule.next rule (Symbol.token (CLexer.terminal t))) in
   let act k _ = act k in
   KRule (rule, act)
 
@@ -637,7 +637,7 @@ let perform_notation syn st =
     let bnd = List.map map args in
     CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
-  let rule = Pcoq.Rule (rule, act mk) in
+  let rule = Pcoq.G.Production.make rule (act mk) in
   let lev = match syn.synext_lev with
   | None -> None
   | Some lev -> Some (string_of_int lev)
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index ba542101c8..43029f4d53 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -328,15 +328,7 @@ let make_sep_rules = function
   | [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, Pcoq.G.Symbol.token tkn) in
-        Rules (r, fun _ -> f)
-    in
-    let r = mkrule (List.rev tkl) in
+    let r = Pcoq.G.mk_rule (List.rev tkl) in
     Pcoq.G.Symbol.rules ~warning:None [r]
 
 type ('s, 'a) mayrec_symbol =
@@ -470,18 +462,18 @@ type ('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
+| TyStop -> MayRecRNo G.Rule.stop
 | TyMark (_, _, _, r) -> ty_erase r
 | TyNext (rem, TyTerm tok) ->
    begin match ty_erase rem with
-   | MayRecRNo rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok))
-   | MayRecRMay rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) end
+   | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok))
+   | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end
 | TyNext (rem, TyNonTerm (_, _, s, _)) ->
    begin match ty_erase rem, s with
-   | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end
+   | MayRecRNo rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRNo rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRMay rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
+   | MayRecRMay rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) end
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -564,8 +556,9 @@ let extend_constr state forpat ng =
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule =
       let r = match ty_erase r with
-        | MayRecRNo symbs -> Rule (symbs, act)
-        | MayRecRMay symbs -> Rule (symbs, act) in
+        | MayRecRNo symbs -> Pcoq.G.Production.make symbs act
+        | MayRecRMay symbs -> Pcoq.G.Production.make symbs act
+      in
       name, p4assoc, [r] in
     let r = match reinit with
       | None ->
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index bcd8de1ff4..175217803f 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -45,8 +45,8 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 
 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)
+| TyStop -> Pcoq.G.Rule.stop
+| TyNext (rem, tok, _) -> Pcoq.G.Rule.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
-  Pcoq.Rule (symb, act)
+  Pcoq.G.Production.make 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/pvernac.ml b/vernac/pvernac.ml
index aebded72f8..27b8a5bda2 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -54,8 +54,8 @@ module Vernac_ =
       let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
-        Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi);
-        Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac);
+        Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
+        Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
       ] in
       Pcoq.grammar_extend main_entry (None, [None, None, rule])