aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--parsing/pcoq.ml52
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--plugins/ltac/tacentries.ml6
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--user-contrib/Ltac2/tac2entries.ml2
-rw-r--r--vernac/egramcoq.ml67
-rw-r--r--vernac/egramml.ml2
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/vernacextend.ml2
10 files changed, 84 insertions, 58 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 72b7cb2f84..e723d4ea1b 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@ None@ @[(%a, %a)@]@]@ in@ "
+ fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ "
e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
let print_ast fmt ext =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 26afdcb9d5..92c3b7c6e8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -212,7 +212,8 @@ type 'a extend_statement =
'a single_extend_statement list
type extend_rule =
-| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
module EntryCommand = Dyn.Make ()
module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
@@ -231,33 +232,39 @@ let camlp5_entries = ref EntryDataMap.empty
(** Deletion *)
-let grammar_delete e reinit (pos,rls) =
+let grammar_delete e (pos,rls) =
List.iter
(fun (n,ass,lev) ->
List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
- (List.rev rls);
- match reinit with
- | Some (a,ext) ->
- let lev = match pos with
+ (List.rev rls)
+
+let grammar_delete_reinit e reinit (pos, rls) =
+ grammar_delete e (pos, rls);
+ 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,[]]
- | None -> ()
+ in
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
(** Extension *)
-let grammar_extend e reinit ext =
+let grammar_extend e ext =
let ext = of_coq_extend_statement ext in
- let undo () = grammar_delete e reinit ext in
+ let undo () = grammar_delete e ext in
let pos, ext = fix_extend_statement ext in
let redo () = G.safe_extend ~warning:None e pos ext in
camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
-let grammar_extend_sync e reinit ext =
- camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
+let grammar_extend_sync e ext =
+ camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
+ let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
+ G.safe_extend ~warning:None e pos ext
+
+let grammar_extend_sync_reinit e reinit ext =
+ camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
G.safe_extend ~warning:None e pos ext
@@ -278,8 +285,12 @@ let rec remove_grammars n =
if n>0 then
match !camlp5_state with
| [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
- | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
- grammar_delete g reinit (of_coq_extend_statement ext);
+ | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t ->
+ grammar_delete_reinit g reinit (of_coq_extend_statement ext);
+ camlp5_state := t;
+ remove_grammars (n-1)
+ | ByGrammar (ExtendRule (g, ext)) :: t ->
+ grammar_delete g (of_coq_extend_statement ext);
camlp5_state := t;
remove_grammars (n-1)
| ByEXTEND (undo,redo)::t ->
@@ -507,6 +518,12 @@ let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) ent
let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in
obj
+let iter_extend_sync = function
+ | ExtendRule (e, ext) ->
+ grammar_extend_sync e ext
+ | ExtendRuleReinit (e, reinit, ext) ->
+ grammar_extend_sync_reinit e reinit ext
+
let extend_grammar_command tag g =
let modify = GrammarInterpMap.find tag !grammar_interp in
let grammar_state = match !grammar_stack with
@@ -514,8 +531,7 @@ let extend_grammar_command tag g =
| (_, st) :: _ -> st
in
let (rules, st) = modify g grammar_state in
- let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
- let () = List.iter iter rules in
+ let () = List.iter iter_extend_sync rules in
let nb = List.length rules in
grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 404fbdb4fd..f2fc007a7b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -225,7 +225,7 @@ type 'a extend_statement =
Gramlib.Gramext.position option *
'a single_extend_statement list
-val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a 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. *)
@@ -242,7 +242,8 @@ type 'a grammar_command
marshallable. *)
type extend_rule =
-| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a 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 13a2f3b8c0..8b4520947b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -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, None, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
([r], state)
let tactic_grammar =
@@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
+ Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
(** Command *)
@@ -759,7 +759,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, None, rules)]) in
+ let () = Pcoq.grammar_extend e (None, [(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 1c66fee9b8..e95ac3b02b 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -889,7 +889,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr None (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+ Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
end
}
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d6db4a735c..70cba858c9 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -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, (None, [rule]))], st)
+ ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 72e6d41969..ead86bd12f 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -96,38 +96,38 @@ let create_pos = function
let find_position_gen current ensure assoc lev =
match lev with
| None ->
- current, (None, None, None, None)
+ current, (None, None, None, None)
| Some n ->
- let after = ref None in
- let init = ref None in
- let rec add_level q = function
- | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
- | (p,a,reinit)::l when Int.equal p n ->
- if reinit then
- let a' = create_assoc assoc in
- (init := Some (a',create_pos q); (p,a',false)::l)
- else if admissible_assoc (a,assoc) then
- raise Exit
- else
- error_level_assoc p a (Option.get assoc)
- | l -> after := q; (n,create_assoc assoc,ensure)::l
- in
- try
- let updated = add_level None current in
- let assoc = create_assoc assoc in
- begin match !init with
+ let after = ref None in
+ let init = ref None in
+ let rec add_level q = function
+ | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
+ | (p,a,reinit)::l when Int.equal p n ->
+ if reinit then
+ let a' = create_assoc assoc in
+ (init := Some (a',create_pos q); (p,a',false)::l)
+ else if admissible_assoc (a,assoc) then
+ raise Exit
+ else
+ error_level_assoc p a (Option.get assoc)
+ | l -> after := q; (n,create_assoc assoc,ensure)::l
+ in
+ try
+ let updated = add_level None current in
+ let assoc = create_assoc assoc in
+ begin match !init with
| None ->
(* Create the entry *)
- updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
+ updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
| _ ->
(* The reinit flag has been updated *)
- updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
- end
- with
- (* Nothing has changed *)
- Exit ->
- (* Just inherit the existing associativity and name (None) *)
- current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
+ updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
+ end
+ with
+ (* Nothing has changed *)
+ Exit ->
+ (* Just inherit the existing associativity and name (None) *)
+ current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
let rec list_mem_assoc_triple x = function
| [] -> false
@@ -505,7 +505,11 @@ let target_to_bool : type r. r target -> bool = function
let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = (pos, [(name, p4assoc, [])]) in
- ExtendRule (target_entry where forpat, reinit, empty)
+ match reinit with
+ | None ->
+ ExtendRule (target_entry where forpat, empty)
+ | Some reinit ->
+ ExtendRuleReinit (target_entry where forpat, reinit, empty)
let different_levels (custom,opt_level) (custom',string_level) =
match opt_level with
@@ -552,7 +556,12 @@ let extend_constr state forpat ng =
| MayRecRNo symbs -> Rule (symbs, act)
| MayRecRMay symbs -> Rule (symbs, act) in
name, p4assoc, [r] in
- let r = ExtendRule (entry, reinit, (pos, [rule])) in
+ let r = match reinit with
+ | None ->
+ ExtendRule (entry, (pos, [rule]))
+ | Some reinit ->
+ ExtendRuleReinit (entry, reinit, (pos, [rule]))
+ in
(accu @ empty_rules @ [r], state)
in
List.fold_left fold ([], state) ng.notgram_prods
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 62eb561f3c..2b1d99c7a9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -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, None, rules])
+ grammar_extend nt (None, [None, None, rules])
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 826e88cabf..2425f3d6c1 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -58,7 +58,7 @@ module Vernac_ =
Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
Rule (Next (Stop, Aentry vernac_control), act_vernac);
] in
- Pcoq.grammar_extend main_entry None (None, [None, None, rule])
+ Pcoq.grammar_extend main_entry (None, [None, None, rule])
let select_tactic_entry spec =
match spec with
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index e29086d726..f41df06f85 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -254,7 +254,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, None, rules)]) in
+ let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
e
in
let pr = arg.arg_printer in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:12:05 +0000