aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--gramlib/grammar.ml102
-rw-r--r--gramlib/grammar.mli21
-rw-r--r--parsing/pcoq.ml264
-rw-r--r--parsing/pcoq.mli40
-rw-r--r--plugins/ltac/tacentries.ml8
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--user-contrib/Ltac2/tac2core.ml2
-rw-r--r--user-contrib/Ltac2/tac2entries.ml6
-rw-r--r--user-contrib/Ltac2/tac2entries.mli2
-rw-r--r--vernac/egramcoq.ml14
-rw-r--r--vernac/egramml.ml8
-rw-r--r--vernac/egramml.mli4
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/vernacextend.ml6
-rw-r--r--vernac/vernacextend.mli2
16 files changed, 182 insertions, 303 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 70e400c29b..17f81c555c 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -266,7 +266,7 @@ let print_rule fmt r =
let print_entry fmt e =
let print_position_opt fmt pos = print_opt fmt print_position pos in
let print_rules fmt rules = print_list fmt print_rule rules in
- fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ "
+ fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.G.pos=%a; data=%a}@]@]@ in@ "
e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
let print_ast fmt ext =
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 818608674e..0eed42f290 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -80,12 +80,21 @@ module type S = sig
module Unsafe : sig
val clear_entry : 'a Entry.t -> unit
end
- val safe_extend : warning:(string -> unit) option ->
- 'a Entry.t -> Gramext.position option ->
- (string option * Gramext.g_assoc option * 'a Production.t list)
- list ->
- unit
- val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+
+ type 'a single_extend_statement =
+ string option * Gramext.g_assoc option * 'a Production.t list
+
+ type 'a extend_statement =
+ { pos : Gramext.position option
+ ; data : 'a single_extend_statement list
+ }
+
+ val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+ val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+ val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+
+ val mk_rule : 'a pattern list -> string Rules.t
(* Used in custom entries, should tweak? *)
val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
@@ -1659,13 +1668,18 @@ module Unsafe = struct
end
-let safe_extend ~warning (e : 'a Entry.t) pos
- (r :
- (string option * Gramext.g_assoc option * 'a ty_production list)
- list) =
- extend_entry ~warning e pos r
+type 'a single_extend_statement =
+ string option * Gramext.g_assoc option * 'a ty_production list
+
+type 'a extend_statement =
+ { pos : Gramext.position option
+ ; data : 'a single_extend_statement list
+ }
+
+let safe_extend ~warning (e : 'a Entry.t) { pos; data } =
+ extend_entry ~warning e pos data
-let safe_delete_rule e r =
+let safe_delete_rule e (TProd (r,_act)) =
let AnyS (symbols, _) = get_symbols r in
delete_rule e symbols
@@ -1673,4 +1687,68 @@ let level_of_nonterm sym = match sym with
| Snterml (_,l) -> Some l
| _ -> None
+exception SelfSymbol
+
+let rec generalize_symbol :
+ type a tr s. (s, tr, a) Symbol.t -> (s, norec, a) ty_symbol =
+ function
+ | Stoken tok ->
+ Stoken tok
+ | Slist1 e ->
+ Slist1 (generalize_symbol e)
+ | Slist1sep (e, sep, b) ->
+ let e = generalize_symbol e in
+ let sep = generalize_symbol sep in
+ Slist1sep (e, sep, b)
+ | Slist0 e ->
+ Slist0 (generalize_symbol e)
+ | Slist0sep (e, sep, b) ->
+ let e = generalize_symbol e in
+ let sep = generalize_symbol sep in
+ Slist0sep (e, sep, b)
+ | Sopt e ->
+ Sopt (generalize_symbol e)
+ | Sself ->
+ raise SelfSymbol
+ | Snext ->
+ raise SelfSymbol
+ | Snterm e ->
+ Snterm e
+ | Snterml (e, l) ->
+ Snterml (e, l)
+ | Stree r ->
+ Stree (generalize_tree r)
+and generalize_tree : type a tr s .
+ (s, tr, a) ty_tree -> (s, norec, a) ty_tree = fun r ->
+ match r with
+ | Node (fi, n) ->
+ let fi = match fi with
+ | NoRec3 -> NoRec3
+ | MayRec3 -> raise SelfSymbol
+ in
+ let n = match n with
+ | { node; son; brother } ->
+ let node = generalize_symbol node in
+ let son = generalize_tree son in
+ let brother = generalize_tree brother in
+ { node; son; brother }
+ in
+ Node (fi, n)
+ | LocAct _ as r -> r
+ | DeadEnd as r -> r
+
+let generalize_symbol s =
+ try Some (generalize_symbol s)
+ with SelfSymbol -> None
+
+let rec mk_rule tok =
+ match tok with
+ | [] ->
+ let stop_e = Rule.stop in
+ TRules (stop_e, fun _ -> (* dropped anyway: *) "")
+ | tkn :: rem ->
+ let TRules (r, f) = mk_rule rem in
+ let r = Rule.next_norec r (Symbol.token tkn) in
+ TRules (r, fun _ -> f)
+
end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 4ac85bd358..4280181109 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -90,16 +90,23 @@ module type S = sig
val clear_entry : 'a Entry.t -> unit
end
- val safe_extend : warning:(string -> unit) option ->
- 'a Entry.t -> Gramext.position option ->
- (string option * Gramext.g_assoc option * 'a Production.t list)
- list ->
- unit
- val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+ type 'a single_extend_statement =
+ string option * Gramext.g_assoc option * 'a Production.t list
+
+ type 'a extend_statement =
+ { pos : Gramext.position option
+ ; data : 'a single_extend_statement list
+ }
+
+ val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+ val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+ val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+
+ val mk_rule : 'a pattern list -> string Rules.t
(* Used in custom entries, should tweak? *)
val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
-
end
(** Signature type of the functor [Grammar.GMake]. The types and
functions are almost the same than in generic interface, but:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8f7d6d1966..e10e4bb8dd 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -10,7 +10,6 @@
open CErrors
open Util
-open Extend
open Genarg
open Gramlib
@@ -19,47 +18,16 @@ open Gramlib
type norec = Gramlib.Grammar.norec
type mayrec = Gramlib.Grammar.mayrec
-type ('self, 'trec, 'a) symbol =
-| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
-| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
- -> ('self, 'trec, 'a list) symbol
-| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
- -> ('self, 'trec, 'a list) symbol
-| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol
-| Aself : ('self, mayrec, 'self) symbol
-| Anext : ('self, mayrec, 'self) symbol
-| Aentry : 'a entry -> ('self, norec, 'a) symbol
-| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol
-| Arules : 'a rules list -> ('self, norec, 'a) symbol
-
-and ('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
-
-and '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
-
module G : sig
include Grammar.S
with type te = Tok.t
and type 'c pattern = 'c Tok.p
- and type 'a pattern = 'a Tok.p
- and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
- and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
- and type 'a Rules.t = 'a rules
- and type 'a Production.t = 'a production_rule
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
+ val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+ val mk_rule : 'a Tok.p list -> string Rules.t
end with type 'a Entry.t = 'a Extend.entry = struct
@@ -88,6 +56,12 @@ end with type 'a Entry.t = 'a Extend.entry = struct
let tokens = G_.tokens
+ type 'a single_extend_statement = 'a G_.single_extend_statement
+ type 'a extend_statement = 'a G_.extend_statement =
+ { pos : Gramlib.Gramext.position option
+ ; data : 'a single_extend_statement list
+ }
+
module Entry = struct
include G_.Entry
@@ -105,164 +79,17 @@ end with type 'a Entry.t = 'a Extend.entry = struct
end
- module Symbol = struct
- type ('self, 'trec, 'a) t = ('self, 'trec, 'a) symbol
- let token tok = Atoken tok
- let list0 e = Alist0 e
- let list0sep e s _ = Alist0sep (e,s)
- let list1 e = Alist1 e
- let list1sep e s _ = Alist1sep (e,s)
- let opt e = Aopt e
- let self = Aself
- let next = Anext
- let nterm e = Aentry e
- let nterml e s = Aentryl (e,s)
- let rules ~warning:_ r = Arules r
- end
-
- module Rule = struct
- type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) rule
- let stop = Stop
- let next a b = Next (a,b)
- let next_norec a b = NextNoRec (a,b)
- end
-
- module Rules = struct
- type 'a t = 'a rules
- let make a f = Rules(a,f)
- end
-
- module Production = struct
- type 'a t = 'a production_rule
- let make a f = Rule(a,f)
- end
-
- module Unsafe = struct
- let clear_entry = G_.Unsafe.clear_entry
- end
-
- (** FIXME: This is a hack around a deficient camlp5 API *)
- type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G_.Rule.t * 'f -> 'a any_production
-
- let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G_.Symbol.t =
- function
- | Atoken t -> G_.Symbol.token t
- | Alist1 s ->
- let s = symbol_of_prod_entry_key s in
- G_.Symbol.list1 s
- | Alist1sep (s,sep) ->
- let s = symbol_of_prod_entry_key s in
- let sep = symbol_of_prod_entry_key sep in
- G_.Symbol.list1sep s sep false
- | Alist0 s ->
- let s = symbol_of_prod_entry_key s in
- G_.Symbol.list0 s
- | Alist0sep (s,sep) ->
- let s = symbol_of_prod_entry_key s in
- let sep = symbol_of_prod_entry_key sep in
- G_.Symbol.list0sep s sep false
- | Aopt s ->
- let s = symbol_of_prod_entry_key s in
- G_.Symbol.opt s
- | Aself -> G_.Symbol.self
- | Anext -> G_.Symbol.next
- | Aentry e -> G_.Symbol.nterm e
- | Aentryl (e, n) -> G_.Symbol.nterml e n
- | Arules rs ->
- let warning msg = Feedback.msg_warning Pp.(str msg) in
- G_.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs)
-
- and symbol_of_rule : type s tr a r. (s, tr, a, r) rule -> (s, tr, a, r) G_.Rule.t = function
- | Stop ->
- G_.Rule.stop
- | Next (r, s) ->
- let r = symbol_of_rule r in
- let s = symbol_of_prod_entry_key s in
- G_.Rule.next r s
- | NextNoRec (r, s) ->
- let r = symbol_of_rule r in
- let s = symbol_of_prod_entry_key s in
- G_.Rule.next_norec r s
-
- and symbol_of_rules : type a. a rules -> a G_.Rules.t = function
- | Rules (r, act) ->
- let symb = symbol_of_rule r in
- G_.Rules.make symb act
-
- let of_coq_production_rule : type a. a production_rule -> a any_production = function
- | Rule (toks, act) ->
- AnyProduction (symbol_of_rule toks, act)
-
- let of_coq_single_extend_statement (lvl, assoc, rule) =
- (lvl, assoc, List.map of_coq_production_rule rule)
-
- let of_coq_extend_statement (pos, st) =
- (pos, List.map of_coq_single_extend_statement st)
-
- let fix_extend_statement (pos, st) =
- let fix_single_extend_statement (lvl, assoc, rules) =
- let fix_production_rule (AnyProduction (s, act)) = G_.Production.make s act in
- (lvl, assoc, List.map fix_production_rule rules)
- in
- (pos, List.map fix_single_extend_statement st)
-
- let safe_extend ~warning e pos ext =
- let pos, ext = of_coq_extend_statement (pos,ext) in
- let pos, ext = fix_extend_statement (pos, ext) in
- G_.safe_extend ~warning e pos ext
-
- let safe_delete_rule e r =
- let r = symbol_of_rule r in
- G_.safe_delete_rule e r
-
- let level_of_nonterm = function
- | Aentryl (_,l) -> Some l
- | _ -> None
-
- exception SelfSymbol
- let rec generalize_symbol :
- type a tr s. (s, tr, a) symbol -> (s, norec, a) 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
-
- let generalize_symbol s =
- 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)
+ module Symbol = G_.Symbol
+ module Rule = G_.Rule
+ module Rules = G_.Rules
+ module Production = G_.Production
+ module Unsafe = G_.Unsafe
+
+ let safe_extend = G_.safe_extend
+ let safe_delete_rule = G_.safe_delete_rule
+ let level_of_nonterm = G_.level_of_nonterm
+ let generalize_symbol = G_.generalize_symbol
+ let mk_rule = G_.mk_rule
end
module Parsable = struct
@@ -349,21 +176,9 @@ end
(** Type of reinitialization data *)
type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
-type 'a single_extend_statement =
- string option *
- (* Level *)
- Gramlib.Gramext.g_assoc option *
- (* Associativity *)
- 'a production_rule list
- (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
- Gramlib.Gramext.position option *
- 'a single_extend_statement list
-
type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
module EntryCommand = Dyn.Make ()
module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
@@ -382,39 +197,38 @@ let camlp5_entries = ref EntryDataMap.empty
(** Deletion *)
-let grammar_delete e (pos,rls) =
+let grammar_delete e { G.pos; data } =
List.iter
(fun (n,ass,lev) ->
- List.iter (fun (Rule(pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
- (List.rev rls)
+ List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev))
+ (List.rev data)
-let grammar_delete_reinit e reinit (pos, rls) =
- grammar_delete e (pos, rls);
+let grammar_delete_reinit e reinit ({ G.pos; data } as d)=
+ grammar_delete e d;
let a, ext = reinit in
let lev = match pos with
| Some (Gramext.Level n) -> n
| _ -> assert false
in
let warning msg = Feedback.msg_warning Pp.(str msg) in
- (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
+ let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in
+ G.safe_extend ~warning:(Some warning) e ext
(** Extension *)
-let grammar_extend e (pos,ext) =
- let undo () = grammar_delete e (pos,ext) in
- let redo () = G.safe_extend ~warning:None e pos ext in
+let grammar_extend e ext =
+ let undo () = grammar_delete e ext in
+ let redo () = G.safe_extend ~warning:None e ext in
camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
let grammar_extend_sync e ext =
camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
- let pos, ext = ext in
- G.safe_extend ~warning:None e pos ext
+ G.safe_extend ~warning:None e ext
let grammar_extend_sync_reinit e reinit ext =
camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
- let pos, ext = ext in
- G.safe_extend ~warning:None e pos ext
+ G.safe_extend ~warning:None e ext
(** The apparent parser of Coq; encapsulate G to keep track
of the extensions. *)
@@ -467,7 +281,8 @@ let eoi_entry en =
let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in
let act = fun _ x loc -> x in
let warning msg = Feedback.msg_warning Pp.(str msg) in
- Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
+ let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+ Gram.safe_extend ~warning:(Some warning) e ext;
e
let map_entry f en =
@@ -475,7 +290,8 @@ let map_entry f en =
let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
let act = fun x loc -> f x in
let warning msg = Feedback.msg_warning Pp.(str msg) in
- Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
+ let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+ Gram.safe_extend ~warning:(Some warning) e ext;
e
(* Parse a string, does NOT check if the entire string was read
@@ -620,12 +436,12 @@ module Module =
let module_type = Entry.create "module_type"
end
-let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
+let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) =
let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in
- let ext = [None, None, [r]] in
let entry = G.Entry.make "epsilon" in
let warning msg = Feedback.msg_warning Pp.(str msg) in
- let () = G.safe_extend ~warning:(Some warning) entry None ext in
+ let ext = { G.pos = None; data = [None, None, [r]] } in
+ let () = G.safe_extend ~warning:(Some warning) entry ext in
try Some (parse_string entry "") with _ -> None
(** Synchronized grammar extensions *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e7e3e9442b..f83109d39a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -223,51 +223,26 @@ 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 'a rules
-type 'a production_rule
-
module G : sig
include Gramlib.Grammar.S
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
+ val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+ val mk_rule : 'a Tok.p list -> string Rules.t
end with type 'a Entry.t = 'a Entry.t
and type te = Tok.t
and type 'a pattern = 'a Tok.p
- and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
- and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
- and type 'a Rules.t = 'a rules
- and type 'a Production.t = 'a production_rule
-val epsilon_value : ('a -> 'self) -> ('self, _, 'a) symbol -> 'self option
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option
(** {5 Extending the parser without synchronization} *)
-type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
-(** Type of reinitialization data *)
-
-type 'a single_extend_statement =
- string option *
- (* Level *)
- Gramlib.Gramext.g_assoc option *
- (* Associativity *)
- 'a production_rule list
- (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
- Gramlib.Gramext.position option *
- 'a single_extend_statement list
-
-val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a G.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
an undo. *)
@@ -283,9 +258,12 @@ type 'a grammar_command
(** Type of synchronized parsing extensions. The ['a] type should be
marshallable. *)
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
+(** Type of reinitialization data *)
+
type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.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,
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 6b83590b1d..eed7f07b2e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
- let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in
([r], state)
let tactic_grammar =
@@ -421,7 +421,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
- Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
+ Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]}
(** Command *)
@@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
e
| Vernacextend.Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8b3203c8dd..477672ebdb 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -861,7 +861,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+ Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
end
}
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 547ca0c2ed..0946c88228 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1590,7 +1590,7 @@ 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, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule
let rec make_seq_rule = function
| [] ->
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index c5f081eab9..7c4971db8c 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) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
@@ -611,7 +611,7 @@ type synext = {
type krule =
| KRule :
- (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule *
+ (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t *
((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
let rec get_rule (tok : scope_rule token list) : krule = match tok with
@@ -643,7 +643,7 @@ let perform_notation syn st =
| Some lev -> Some (string_of_int lev)
in
let rule = (lev, None, [rule]) in
- ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
+ ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 4938e96cae..1efac697aa 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) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 43029f4d53..88bcf1d477 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -332,8 +332,8 @@ let make_sep_rules = function
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
+| MayRecNo : ('s, norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('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
@@ -458,8 +458,8 @@ 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, norec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('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 G.Rule.stop
@@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function
| ForPattern -> true
let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
- let empty = (pos, [(name, p4assoc, [])]) in
+ let empty = { G.pos; data = [(name, p4assoc, [])] } in
match reinit with
| None ->
ExtendRule (target_entry where forpat, empty)
@@ -562,9 +562,9 @@ let extend_constr state forpat ng =
name, p4assoc, [r] in
let r = match reinit with
| None ->
- ExtendRule (entry, (pos, [rule]))
+ ExtendRule (entry, { G.pos; data = [rule]})
| Some reinit ->
- ExtendRuleReinit (entry, reinit, (pos, [rule]))
+ ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]})
in
(accu @ empty_rules @ [r], state)
in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 175217803f..00a239f56e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,13 +19,13 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item
+ ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
type ('self, 'tr, _, '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 ->
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.G.Symbol.t * 'b ty_arg option ->
('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule
type ('self, 'r) any_ty_rule =
@@ -44,7 +44,7 @@ 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) Pcoq.rule = function
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function
| TyStop -> Pcoq.G.Rule.stop
| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s, l) in
let rules = [make_rule mkact gl] in
- grammar_extend nt (None, [None, None, rules])
+ grammar_extend nt { G.pos=None; data=[None, None, rules]}
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index e6e4748b59..77198452b9 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) Pcoq.symbol) Loc.located -> 's grammar_prod_item
+ ('s, _, 'a) Pcoq.G.Symbol.t) 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 Pcoq.production_rule
+ 'a grammar_prod_item list -> 'a Pcoq.G.Production.t
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 27b8a5bda2..9a9c96064d 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -57,7 +57,7 @@ module 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])
+ Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]})
let select_tactic_entry spec =
match spec with
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index fc6ece27cd..ac4d33c926 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,7 +166,7 @@ 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, Pcoq.norec, a) Pcoq.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.G.Symbol.t =
let open Extend in function
| 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
@@ -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 Pcoq.production_rule list
+| Arg_rules of 'a Pcoq.G.Production.t list
type 'a vernac_argument = {
arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
@@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg =
e
| Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e {Pcoq.G.pos=None; data=[(None, None, rules)]} in
e
in
let pr = arg.arg_printer in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0acb5f43f9..4d9537b6ff 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 Pcoq.production_rule list
+| Arg_rules of 'a Pcoq.G.Production.t 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. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:05:17 +0000