aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml8
-rw-r--r--parsing/pcoq.ml10
-rw-r--r--parsing/pcoq.mli14
-rw-r--r--plugins/ltac/tacentries.ml20
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg19
-rw-r--r--user-contrib/Ltac2/tac2core.ml6
-rw-r--r--user-contrib/Ltac2/tac2entries.ml8
-rw-r--r--vernac/egramcoq.ml29
-rw-r--r--vernac/egramml.ml6
-rw-r--r--vernac/pvernac.ml4
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])
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:15:01 +0000