[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.

4 files changed, 38 insertions, 58 deletions

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5e04959e9a..52d92d87c0 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -826,12 +826,11 @@ END
 
 let () =
 
-let open Extend in
 let open Tok in
 let (++) r s = Next (r, s) in
 let rules = [
   Rule (
-    Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident,
+    Stop ++ Pcoq.G.Symbol.nterm test_dollar_ident ++ Pcoq.G.Symbol.token (PKEYWORD "$") ++ Pcoq.G.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
@@ -840,7 +839,7 @@ let rules = [
   );
 
   Rule (
-    Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
+    Stop ++ Pcoq.G.Symbol.nterm test_ampersand_ident ++ Pcoq.G.Symbol.token (PKEYWORD "&") ++ Pcoq.G.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
@@ -849,8 +848,8 @@ let rules = [
   );
 
   Rule (
-    Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
-      Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
+    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 ")"),
     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 38b05bed6b..2edbcc38f5 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0))
 let add_generic_scope s entry arg =
   let parse = function
   | [] ->
-    let scope = Extend.Aentry entry in
+    let scope = Pcoq.G.Symbol.nterm entry in
     let act x = CAst.make @@ CTacExt (arg, x) in
     Tac2entries.ScopeRule (scope, act)
   | arg -> scope_fail s arg
@@ -1442,14 +1442,14 @@ open CAst
 
 let () = add_scope "keyword" begin function
 | [SexprStr {loc;v=s}] ->
-  let scope = Extend.Atoken (Tok.PKEYWORD s) in
+  let scope = Pcoq.G.Symbol.token (Tok.PKEYWORD s) in
   Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
 | arg -> scope_fail "keyword" arg
 end
 
 let () = add_scope "terminal" begin function
 | [SexprStr {loc;v=s}] ->
-  let scope = Extend.Atoken (CLexer.terminal s) in
+  let scope = Pcoq.G.Symbol.token (CLexer.terminal s) in
   Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
 | arg -> scope_fail "terminal" arg
 end
@@ -1457,13 +1457,13 @@ end
 let () = add_scope "list0" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Alist0 scope in
+  let scope = Pcoq.G.Symbol.list0 scope in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr {v=str}] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let sep = Extend.Atoken (CLexer.terminal str) in
-  let scope = Extend.Alist0sep (scope, sep) in
+  let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in
+  let scope = Pcoq.G.Symbol.list0sep scope sep false in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "list0" arg
@@ -1472,13 +1472,13 @@ end
 let () = add_scope "list1" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Alist1 scope in
+  let scope = Pcoq.G.Symbol.list1 scope in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr {v=str}] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let sep = Extend.Atoken (CLexer.terminal str) in
-  let scope = Extend.Alist1sep (scope, sep) in
+  let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in
+  let scope = Pcoq.G.Symbol.list1sep scope sep false in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "list1" arg
@@ -1487,7 +1487,7 @@ end
 let () = add_scope "opt" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Aopt scope in
+  let scope = Pcoq.G.Symbol.opt scope in
   let act opt = match opt with
   | None ->
     CAst.make @@ CTacCst (AbsKn (Other Core.c_none))
@@ -1500,7 +1500,7 @@ end
 
 let () = add_scope "self" begin function
 | [] ->
-  let scope = Extend.Aself in
+  let scope = Pcoq.G.Symbol.self in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "self" arg
@@ -1508,7 +1508,7 @@ end
 
 let () = add_scope "next" begin function
 | [] ->
-  let scope = Extend.Anext in
+  let scope = Pcoq.G.Symbol.next in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "next" arg
@@ -1517,12 +1517,12 @@ end
 let () = add_scope "tactic" begin function
 | [] ->
   (* Default to level 5 parsing *)
-  let scope = Extend.Aentryl (tac2expr, "5") in
+  let scope = Pcoq.G.Symbol.nterml tac2expr "5" in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt {loc;v=n}] as arg ->
   let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
-  let scope = Extend.Aentryl (tac2expr, string_of_int n) in
+  let scope = Pcoq.G.Symbol.nterml tac2expr (string_of_int n) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "tactic" arg
@@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg ->
         arg
     in
     let act e = Tac2quote.of_constr ~delimiters e in
-    Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act)
+    Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm Pcoq.Constr.constr, act)
   )
 
 let add_expr_scope name entry f =
   add_scope name begin function
-  | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f)
+  | [] -> Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm entry, f)
   | arg -> scope_fail name arg
   end
 
@@ -1578,28 +1578,7 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)
 
-open Extend
-exception SelfSymbol
-
-let rec generalize_symbol :
-  type a tr s. (s, tr, a) Extend.symbol -> (s, Extend.norec, a) Extend.symbol = function
-| Atoken tok -> Atoken tok
-| Alist1 e -> Alist1 (generalize_symbol e)
-| Alist1sep (e, sep) ->
-  let e = generalize_symbol e in
-  let sep = generalize_symbol sep in
-  Alist1sep (e, sep)
-| Alist0 e -> Alist0 (generalize_symbol e)
-| Alist0sep (e, sep) ->
-  let e = generalize_symbol e in
-  let sep = generalize_symbol sep in
-  Alist0sep (e, sep)
-| Aopt e -> Aopt (generalize_symbol e)
-| Aself -> raise SelfSymbol
-| Anext -> raise SelfSymbol
-| Aentry e -> Aentry e
-| Aentryl (e, l) -> Aentryl (e, l)
-| Arules r -> Arules r
+open Pcoq
 
 type _ converter =
 | CvNil : (Loc.t -> raw_tacexpr) converter
@@ -1611,14 +1590,19 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function
 | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
 
 type seqrule =
-| Seqrule : (Tac2expr.raw_tacexpr, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
 
 let rec make_seq_rule = function
 | [] ->
   Seqrule (Stop, CvNil)
 | tok :: rem ->
   let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
-  let scope = generalize_symbol scope in
+  let scope =
+    match Pcoq.G.generalize_symbol scope with
+    | None ->
+      CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+    | Some scope -> scope
+  in
   let Seqrule (r, c) = make_seq_rule rem in
   let r = NextNoRec (r, scope) in
   let f = match tok with
@@ -1629,11 +1613,8 @@ let rec make_seq_rule = function
 
 let () = add_scope "seq" begin fun toks ->
   let scope =
-    try
-      let Seqrule (r, c) = make_seq_rule (List.rev toks) in
-      Arules [Rules (r, apply c [])]
-    with SelfSymbol ->
-      CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+    let Seqrule (r, c) = make_seq_rule (List.rev toks) in
+    Pcoq.G.Symbol.rules ~warning:None [Rules (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 e9945794d3..d5d5bad987 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -558,7 +558,7 @@ type 'a token =
 | TacNonTerm of Name.t * 'a
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
@@ -583,7 +583,7 @@ let parse_scope = function
     CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
 | SexprStr {v=str} ->
   let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
-  ScopeRule (Extend.Atoken (Tok.PIDENT (Some str)), (fun _ -> v_unit))
+  ScopeRule (Pcoq.G.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit))
 | tok ->
   let loc = loc_of_token tok in
   CErrors.user_err ?loc (str "Invalid parsing token")
@@ -611,19 +611,19 @@ type synext = {
 
 type krule =
 | KRule :
-  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule *
   ((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 (Extend.Stop, fun k loc -> k loc [])
+| [] -> KRule (Pcoq.Stop, fun k loc -> k loc [])
 | TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
   let KRule (rule, act) = get_rule tok in
-  let rule = Extend.Next (rule, scope) in
+  let rule = Pcoq.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 = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in
+  let rule = Pcoq.Next (rule, Pcoq.G.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 = Extend.Rule (rule, act mk) in
+  let rule = Pcoq.Rule (rule, act mk) in
   let lev = match syn.synext_lev with
   | None -> None
   | Some lev -> Some (string_of_int lev)
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index fed43a4dd5..4938e96cae 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
 (** {5 Notations} *)
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule