aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml47
-rw-r--r--intf/tacexpr.mli17
-rw-r--r--parsing/egramcoq.ml16
-rw-r--r--parsing/egramcoq.mli4
-rw-r--r--printing/pptactic.ml42
-rw-r--r--printing/pptactic.mli8
-rw-r--r--tactics/tacenv.ml24
-rw-r--r--tactics/tacenv.mli21
-rw-r--r--tactics/tacintern.ml4
-rw-r--r--tactics/tacinterp.ml5
-rw-r--r--tactics/tacsubst.ml6
-rw-r--r--tactics/tactics.mllib1
-rw-r--r--toplevel/metasyntax.ml44
13 files changed, 132 insertions, 67 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 12de0bcbe..e56f7a34e 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -125,9 +125,8 @@ let make_one_printing_rule se (pt,_,e) =
let level = mlexpr_of_int 0 in (* only level 0 supported here *)
let loc = MLast.loc_of_expr e in
let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
- <:expr< { Pptactic.pptac_key = $se$;
- pptac_args = $make_tags loc pt$;
- pptac_prods = ($level$, $prods$) } >>
+ <:expr< ($se$, { Pptactic.pptac_args = $make_tags loc pt$;
+ pptac_prods = ($level$, $prods$) }) >>
let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
@@ -203,7 +202,7 @@ let declare_tactic loc s c cl =
(Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
(Errors.print e)) ];
Egramml.extend_tactic_grammar $se$ $gl$;
- List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
+ List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >>
]
open Pcaml
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0ddf58b74..87af636b4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -178,8 +178,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacExtend of Loc.t * string * 'lev generic_argument list
(* For syntax extensions *)
- | TacAlias of Loc.t * string *
- (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr)
+ | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
(** Possible arguments of a tactic definition *)
@@ -250,14 +249,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
(** Globalized tactics *)
-and g_trm = glob_constr_and_expr
-and g_pat = glob_constr_and_expr * constr_pattern
-and g_cst = evaluable_global_reference and_short_name or_var
-and g_ind = inductive or_var
-and g_ref = ltac_constant located or_var
-and g_nam = Id.t located
+type g_trm = glob_constr_and_expr
+type g_pat = glob_constr_and_expr * constr_pattern
+type g_cst = evaluable_global_reference and_short_name or_var
+type g_ind = inductive or_var
+type g_ref = ltac_constant located or_var
+type g_nam = Id.t located
-and glob_tactic_expr =
+type glob_tactic_expr =
(g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr
type glob_atomic_tactic_expr =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 34e0dcdef..a6ac42cf1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -246,15 +246,13 @@ let get_tactic_entry n =
(** State of the grammar extensions *)
type tactic_grammar = {
- tacgram_key : string;
tacgram_level : int;
tacgram_prods : grammar_prod_item list;
- tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
}
type all_grammar_command =
| Notation of Notation.level * notation_grammar
- | TacticGrammar of tactic_grammar
+ | TacticGrammar of KerName.t * tactic_grammar
(* Declaration of the tactic grammar rule *)
@@ -262,19 +260,19 @@ let head_is_ident tg = match tg.tacgram_prods with
| GramTerminal _::_ -> true
| _ -> false
-let add_tactic_entry tg =
+let add_tactic_entry kn tg =
let entry, pos = get_tactic_entry tg.tacgram_level in
let rules =
if Int.equal tg.tacgram_level 0 then begin
if not (head_is_ident tg) then
error "Notation for simple tactic must start with an identifier.";
let mkact loc l =
- (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in
+ (TacAlias (loc,kn,l):raw_atomic_tactic_expr) in
make_rule mkact tg.tacgram_prods
end
else
let mkact loc l =
- (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in
+ (TacAtom(loc,TacAlias(loc,kn,l)):raw_tactic_expr) in
make_rule mkact tg.tacgram_prods in
synchronize_level_positions ();
grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
@@ -285,14 +283,14 @@ let (grammar_state : (int * all_grammar_command) list ref) = ref []
let extend_grammar gram =
let nb = match gram with
| Notation (_,a) -> extend_constr_notation a
- | TacticGrammar g -> add_tactic_entry g in
+ | TacticGrammar (kn, g) -> add_tactic_entry kn g in
grammar_state := (nb,gram) :: !grammar_state
let extend_constr_grammar pr ntn =
extend_grammar (Notation (pr, ntn))
-let extend_tactic_grammar ntn =
- extend_grammar (TacticGrammar ntn)
+let extend_tactic_grammar kn ntn =
+ extend_grammar (TacticGrammar (kn, ntn))
let recover_constr_grammar ntn prec =
let filter = function
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 9ae49f718..19e8ee8f6 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -41,10 +41,8 @@ type notation_grammar = {
}
type tactic_grammar = {
- tacgram_key : string;
tacgram_level : int;
tacgram_prods : grammar_prod_item list;
- tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
}
(** {5 Adding notations} *)
@@ -52,7 +50,7 @@ type tactic_grammar = {
val extend_constr_grammar : Notation.level -> notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
-val extend_tactic_grammar : tactic_grammar -> unit
+val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
(** Add a tactic notation rule to the parsing system. *)
val recover_constr_grammar : notation -> Notation.level -> notation_grammar
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 2ce3eba06..f52e10979 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -30,18 +30,21 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
type grammar_terminals = string option list
type pp_tactic = {
- pptac_key : string;
pptac_args : argument_type list;
pptac_prods : int * grammar_terminals;
}
- (* Extensions *)
+(* ML Extensions *)
let prtac_tab = Hashtbl.create 17
-let declare_extra_tactic_pprule pt =
- Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods)
+(* Tactic notations *)
+let prnotation_tab = Hashtbl.create 17
-let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
+let declare_ml_tactic_pprule key pt =
+ Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+
+let declare_notation_tactic_pprule kn pt =
+ Hashtbl.add prnotation_tab (kn, pt.pptac_args) pt.pptac_prods
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
@@ -268,6 +271,15 @@ let pr_extend_gen pr_gen lev s l =
with Not_found ->
str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+let pr_alias_gen pr_gen lev s l =
+ try
+ let tags = List.map genarg_tag l in
+ let (lev',pl) = Hashtbl.find prnotation_tab (s,tags) in
+ let p = pr_tacarg_using_rule pr_gen (pl,l) in
+ if lev' > lev then surround p else p
+ with Not_found ->
+ KerName.print s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+
let pr_raw_extend prc prlc prtac prpat =
pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
let pr_glob_extend prc prlc prtac prpat =
@@ -275,6 +287,13 @@ let pr_glob_extend prc prlc prtac prpat =
let pr_extend prc prlc prtac prpat =
pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+let pr_raw_alias prc prlc prtac prpat =
+ pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+let pr_glob_alias prc prlc prtac prpat =
+ pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+let pr_alias prc prlc prtac prpat =
+ pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+
(**********************************************************************)
(* The tactic printer *)
@@ -543,13 +562,14 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
let make_pr_tac pr_tac_level
(pr_constr,pr_lconstr,pr_pat,pr_lpat,
- pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders, pr_gen) =
+ pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,pr_alias,strip_prod_binders, pr_gen) =
(* some shortcuts *)
let pr_bindings = pr_bindings pr_lconstr pr_constr in
let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
+let pr_alias = pr_alias pr_constr pr_lconstr pr_tac_level pr_pat in
let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
let pr_constrarg c = spc () ++ pr_constr c in
@@ -623,8 +643,8 @@ let rec pr_atom0 = function
and pr_atom1 = function
| TacExtend (loc,s,l) ->
pr_with_comments loc (pr_extend 1 s l)
- | TacAlias (loc,s,l,_) ->
- pr_with_comments loc (pr_extend 1 s (List.map snd l))
+ | TacAlias (loc,kn,l) ->
+ pr_with_comments loc (pr_alias 1 kn (List.map snd l))
(* Basic tactics *)
| TacIntroPattern [] as t -> pr_atom0 t
@@ -912,9 +932,9 @@ let rec pr_tac inherited tac =
pr_tac (lcomplete,E) t, lcomplete
| TacId l ->
str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
- | TacAtom (loc,TacAlias (_,s,l,_)) ->
+ | TacAtom (loc,TacAlias (_,kn,l)) ->
pr_with_comments loc
- (pr_extend (level_of inherited) s (List.map snd l)),
+ (pr_alias (level_of inherited) kn (List.map snd l)),
latom
| TacAtom (loc,t) ->
pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
@@ -971,6 +991,7 @@ let raw_printers =
pr_reference,
pr_or_metaid pr_lident,
pr_raw_extend,
+ pr_raw_alias,
strip_prod_binders_expr,
Genprint.generic_raw_print)
@@ -994,6 +1015,7 @@ let pr_glob_tactic_level env =
pr_ltac_or_var (pr_located pr_ltac_constant),
pr_lident,
pr_glob_extend,
+ pr_glob_alias,
strip_prod_binders_glob_constr,
Genprint.generic_glb_print)
in
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 59a3fc830..47640afa6 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -8,6 +8,7 @@
open Pp
open Genarg
+open Names
open Constrexpr
open Tacexpr
open Proof_type
@@ -48,15 +49,12 @@ val declare_extra_genarg_pprule :
type grammar_terminals = string option list
type pp_tactic = {
- pptac_key : string;
pptac_args : argument_type list;
pptac_prods : int * grammar_terminals;
}
- (** if the boolean is false then the extension applies only to old syntax *)
-val declare_extra_tactic_pprule : pp_tactic -> unit
-
-val exists_extra_tactic_pprule : string -> argument_type list -> bool
+val declare_ml_tactic_pprule : string -> pp_tactic -> unit
+val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
val pr_raw_generic :
(constr_expr -> std_ppcmds) ->
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
new file mode 100644
index 000000000..1a277c740
--- /dev/null
+++ b/tactics/tacenv.ml
@@ -0,0 +1,24 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Pp
+open Names
+open Tacexpr
+
+type alias = KerName.t
+
+let alias_map = Summary.ref ~name:"tactic-alias"
+ (KNmap.empty : (DirPath.t * glob_tactic_expr) KNmap.t)
+
+let register_alias key dp tac =
+ alias_map := KNmap.add key (dp, tac) !alias_map
+
+let interp_alias key =
+ try KNmap.find key !alias_map
+ with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
new file mode 100644
index 000000000..8fada3920
--- /dev/null
+++ b/tactics/tacenv.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Tacexpr
+
+(** This module centralizes the various ways of registering tactics. *)
+
+type alias = KerName.t
+(** Type of tactic alias, used in the [TacAlias] node. *)
+
+val register_alias : alias -> DirPath.t -> glob_tactic_expr -> unit
+(** Register a tactic alias. *)
+
+val interp_alias : alias -> (DirPath.t * glob_tactic_expr)
+(** Recover the the body of an alias. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 42ea649ec..edbec7a04 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -634,9 +634,9 @@ let rec intern_atomic lf ist x =
| TacExtend (loc,opn,l) ->
!assert_tactic_installed opn;
TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
- | TacAlias (loc,s,l,(dir,body)) ->
+ | TacAlias (loc,s,l) ->
let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
- TacAlias (loc,s,l,(dir,body))
+ TacAlias (loc,s,l)
and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 248a5d36b..e6afbbaf7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2231,7 +2231,8 @@ and interp_atomic ist tac =
Proofview.V82.tclEVARS sigma <*>
tac args ist
end
- | TacAlias (loc,s,l,(_,body)) ->
+ | TacAlias (loc,s,l) ->
+ let (_, body) = Tacenv.interp_alias s in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let rec f x =
@@ -2332,7 +2333,7 @@ and interp_atomic ist tac =
Proofview.Goal.return (Id.Map.add x v accu)
in
List.fold_right addvar l (Proofview.Goal.return ist.lfun) >>= fun lfun ->
- let trace = push_trace (loc,LtacNotationCall s) ist in
+ let trace = push_trace (loc,LtacNotationCall (KerName.to_string s)) ist in
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7c968865a..7491c9a8f 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -219,9 +219,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* For extensions *)
| TacExtend (_loc,opn,l) ->
TacExtend (dloc,opn,List.map (subst_genarg subst) l)
- | TacAlias (_,s,l,(dir,body)) ->
- TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
- (dir,subst_tactic subst body))
+ | TacAlias (_,s,l) ->
+ let s = subst_kn subst s in
+ TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 7b91665ad..f1227c234 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,6 +15,7 @@ Equality
Contradiction
Inv
Leminv
+Tacenv
Tacsubst
Taccoerce
Tacintern
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4bce9b73e..b2493a2a1 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,26 +65,37 @@ type tactic_grammar_obj = {
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
tacobj_tacpp : Pptactic.pp_tactic;
+ tacobj_body : DirPath.t * Tacexpr.glob_tactic_expr
}
-let cache_tactic_notation (_, tobj) =
- Egramcoq.extend_tactic_grammar tobj.tacobj_tacgram;
- Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp
+let cache_tactic_notation ((_, key), tobj) =
+ let (dp, body) = tobj.tacobj_body in
+ Tacenv.register_alias key dp body;
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+ Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
-let subst_tactic_parule subst tg =
- let dir, tac = tg.tacgram_tactic in
- { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); }
+let open_tactic_notation i ((_, key), tobj) =
+ if Int.equal i 1 && not tobj.tacobj_local then
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+
+let load_tactic_notation i ((_, key), tobj) =
+ let (dp, body) = tobj.tacobj_body in
+ (** Only add the printing and interpretation rules. *)
+ Tacenv.register_alias key dp body;
+ Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
+ if Int.equal i 1 && not tobj.tacobj_local then
+ Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
- { tobj with
- tacobj_tacgram = subst_tactic_parule subst tobj.tacobj_tacgram; }
+ let dir, tac = tobj.tacobj_body in
+ { tobj with tacobj_body = (dir, Tacsubst.subst_tactic subst tac); }
-let classify_tactic_notation tacobj =
- if tacobj.tacobj_local then Dispose else Substitute tacobj
+let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = (fun i o -> if Int.equal i 1 then cache_tactic_notation o);
+ open_function = open_tactic_notation;
+ load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
classify_function = classify_tactic_notation}
@@ -98,31 +109,24 @@ let rec tactic_notation_key = function
| _ :: l -> tactic_notation_key l
| [] -> "terminal_free_notation"
-let rec next_key_away key t =
- if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
- else key
-
let add_tactic_notation (local,n,prods,e) =
let prods = List.map (interp_prod_item n) prods in
let tags = make_tags prods in
- let key = next_key_away (tactic_notation_key prods) tags in
let pprule = {
- Pptactic.pptac_key = key;
- pptac_args = tags;
+ Pptactic.pptac_args = tags;
pptac_prods = (n, List.map make_terminal_status prods);
} in
let ids = List.fold_left cons_production_parameter [] prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
let parule = {
- tacgram_key = key;
tacgram_level = n;
tacgram_prods = prods;
- tacgram_tactic = (Lib.cwd (), tac);
} in
let tacobj = {
tacobj_local = local;
tacobj_tacgram = parule;
tacobj_tacpp = pprule;
+ tacobj_body = (Lib.cwd (), tac);
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:06:40 +0000