aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-ltac.tex39
-rw-r--r--doc/refman/RefMan-tac.tex10
-rw-r--r--engine/proofview.ml30
-rw-r--r--engine/proofview.mli10
-rw-r--r--intf/tacexpr.mli7
-rw-r--r--intf/vernacexpr.mli3
-rw-r--r--lib/cList.ml11
-rw-r--r--lib/cList.mli1
-rw-r--r--ltac/g_ltac.ml442
-rw-r--r--ltac/tacintern.ml2
-rw-r--r--ltac/tacinterp.ml1
-rw-r--r--proofs/pfedit.ml1
-rw-r--r--proofs/proof_global.ml8
-rw-r--r--tactics/tacticals.ml7
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--test-suite/success/goal_selector.v55
16 files changed, 212 insertions, 16 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index ffcb37134..722249191 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -25,6 +25,7 @@ problems.
\def\contexthyp{\textrm{\textsl{context\_hyp}}}
\def\tacarg{\nterm{tacarg}}
\def\cpattern{\nterm{cpattern}}
+\def\selector{\textrm{\textsl{selector}}}
The syntax of the tactic language is given Figures~\ref{ltac}
and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
@@ -104,6 +105,7 @@ is understood as
& | & {\tt exactly\_once} {\tacexprpref}\\
& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
& | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
+& | & {\selector} {\tt :} {\tacexprpref}\\
& | & {\tacexprinf} \\
\\
{\tacexprinf} & ::= &
@@ -203,7 +205,13 @@ is understood as
& $|$ & {\integer} {\tt \,<\,} {\integer}\\
& $|$ & {\integer} {\tt <=} {\integer}\\
& $|$ & {\integer} {\tt \,>\,} {\integer}\\
-& $|$ & {\integer} {\tt >=} {\integer}
+& $|$ & {\integer} {\tt >=} {\integer}\\
+\\
+\selector & ::= &
+ [{\ident}]\\
+& $|$ & {\integer}\\
+& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
+ {\tt ,}
\end{tabular}
\end{centerframe}
\caption{Syntax of the tactic language (continued)}
@@ -358,7 +366,36 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
\end{Variants}
+\subsubsection[Goal selectors]{Goal selectors\label{ltac:selector}
+\tacindex{\tt :}\index{Tacticals!:@{\tt :}}}
+
+We can restrict the application of a tactic to a subset of
+the currently focused goals with:
+\begin{quote}
+{\selector} {\tt :} {\tacexpr}
+\end{quote}
+When selecting several goals, the tactic {\tacexpr} is applied globally to
+all selected goals.
+
+\begin{Variants}
+ \item{} [{\ident}] {\tt :} {\tacexpr}
+
+ In this variant, {\tacexpr} is applied locally to a goal
+ previously named by the user.
+
+ \item {\num} {\tt :} {\tacexpr}
+
+ In this variant, {\tacexpr} is applied locally to the
+ {\num}-th goal.
+
+ \item $n_1$-$m_1$, \dots, $n_k$-$m_k$ {\tt :} {\tacexpr}
+
+ In this variant, {\tacexpr} is applied globally to the subset
+ of goals described by the given ranges. You can write a single
+ $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
+\end{Variants}
+\ErrMsg \errindex{No such goal}
\subsubsection[For loop]{For loop\tacindex{do}
\index{Tacticals!do@{\tt do}}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 54450fe7d..527226f68 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -42,14 +42,12 @@ language will be described in Chapter~\ref{TacticLanguage}.
\index{tactic@{\tac}}}
A tactic is applied as an ordinary command. It may be preceded by a
-goal selector: {\tt all} if the tactic is to be applied to every
-focused goal simultaneously, or a natural number $n$ if it is to be
-applied to the $n$-th goal. If no selector is specified, the default
+goal selector (see Section \ref{ltac:selector}).
+If no selector is specified, the default
selector (see Section \ref{default-selector}) is used.
\newcommand{\selector}{\nterm{selector}}
\begin{tabular}{lcl}
-{\selector} & := & {\tt all} | {\num}\\
{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
& $|$ & {\tac} {\tt .}
\end{tabular}
@@ -63,7 +61,9 @@ initial value is $1$, hence the tactics are, by default, applied to
the first goal. Using {\tt Set Default Goal Selector ``all''} will
make is so that tactics are, by default, applied to every goal
simultaneously. Then, to apply a tactic {\tt tac} to the first goal
-only, you can write {\tt 1:tac}.
+only, you can write {\tt 1:tac}. Although more selectors are available,
+only {\tt ``all''} or a single natural number are valid default
+goal selectors.
\subsection[\tt Test Default Goal Selector.]
{\tt Test Default Goal Selector.}
diff --git a/engine/proofview.ml b/engine/proofview.ml
index bcdd4da11..b8f49a9c8 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -388,6 +388,36 @@ let tclFOCUS_gen nosuchgoal i j t =
let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
+let tclFOCUSLIST l t =
+ let open Proof in
+ Comb.get >>= fun comb ->
+ let n = CList.length comb in
+ (* First, remove empty intervals, and bound the intervals to the number
+ of goals. *)
+ let sanitize (i, j) =
+ if i > j then None
+ else if i > n then None
+ else if j < 1 then None
+ else Some ((max i 1), (min j n))
+ in
+ let l = CList.map_filter sanitize l in
+ match l with
+ | [] -> tclZERO (NoSuchGoals 0)
+ | (mi, _) :: _ ->
+ (* Get the left-most goal to focus. This goal won't move, and we
+ will then place all the other goals to focus to the right. *)
+ let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+ (* [CList.goto] returns a zipper, so that
+ [(rev left) @ sub_right = comb]. *)
+ let left, sub_right = CList.goto (mi-1) comb in
+ let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+ let sub, right = CList.partitioni p sub_right in
+ let mj = mi - 1 + CList.length sub in
+ Comb.set (CList.rev_append left (sub @ right)) >>
+ tclFOCUS mi mj t
+
+
+
(** Like {!tclFOCUS} but selects a single goal by name. *)
let tclFOCUSID id t =
let open Proof in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 93ba55c61..bbf2d6bf7 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -239,6 +239,16 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
+(** [tclFOCUSLIST li t] applies [t] on the list of focused goals
+ described by [li]. Each element of [li] is a pair [(i, j)] denoting
+ the goals numbered from [i] to [j] (inclusive, starting from 1).
+ It will try to apply [t] to all the valid goals in any of these
+ intervals. If the set of such goals is not a single range, then it
+ will move goals such that it is a single range. (So, for
+ instance, [[1, 3-5]; idtac.] is not the identity.)
+ If the set of such goals is empty, it will fail. *)
+val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic
+
(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
{!tclFOCUS}. The goal is found by its name rather than its
number.*)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 379dd59d3..c15ef0dd4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -34,6 +34,12 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+type goal_selector =
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
type 'a core_induction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Id.t located
@@ -269,6 +275,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
+ | TacSelect of goal_selector * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
(* For syntax extensions *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index cfa30a4d5..faa5ba251 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -27,8 +27,9 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
to print a goal that is out of focus (or already solved) it doesn't
make sense to apply a tactic to it. Hence it the types may look very
similar, they do not seem to mean the same thing. *)
-type goal_selector =
+type goal_selector = Tacexpr.goal_selector =
| SelectNth of int
+ | SelectList of (int * int) list
| SelectId of Id.t
| SelectAll
diff --git a/lib/cList.ml b/lib/cList.ml
index ba592d13f..3a792d416 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -47,6 +47,8 @@ sig
('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
val filteri :
(int -> 'a -> bool) -> 'a list -> 'a list
+ val partitioni :
+ (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
val smartfilter : ('a -> bool) -> 'a list -> 'a list
val extend : bool list -> 'a -> 'a list -> 'a list
val count : ('a -> bool) -> 'a list -> int
@@ -486,6 +488,15 @@ let filteri p =
in
filter_i_rec 0
+let partitioni p =
+ let rec aux i = function
+ | [] -> [], []
+ | x :: l ->
+ let (l1, l2) = aux (succ i) l in
+ if p i x then (x :: l1, l2)
+ else (l1, x :: l2)
+ in aux 0
+
let rec sep_last = function
| [] -> failwith "sep_last"
| hd::[] -> (hd,[])
diff --git a/lib/cList.mli b/lib/cList.mli
index 9c7b815c1..b19d1a80f 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -89,6 +89,7 @@ sig
val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
'd list -> 'e list
val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+ val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
val smartfilter : ('a -> bool) -> 'a list -> 'a list
(** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 7c161e5cd..b1e3478c1 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -46,6 +46,7 @@ let new_entry name =
e
let selector = new_entry "vernac:selector"
+let toplevel_selector = new_entry "vernac:toplevel_selector"
let tacdef_body = new_entry "tactic:tacdef_body"
(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
@@ -73,7 +74,7 @@ let test_bracket_ident =
GEXTEND Gram
GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
- tactic_mode constr_may_eval constr_eval selector;
+ tactic_mode constr_may_eval constr_eval selector toplevel_selector;
tactic_then_last:
[ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
@@ -119,7 +120,8 @@ GEXTEND Gram
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
- TacAbstract (tc,Some s) ]
+ TacAbstract (tc,Some s)
+ | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ]
(*End of To do*)
| "2" RIGHTA
[ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
@@ -295,13 +297,31 @@ GEXTEND Gram
tactic:
[ [ tac = tactic_expr -> tac ] ]
;
+
+ range_selector:
+ [ [ n = natural ; "-" ; m = natural -> (n, m)
+ | n = natural -> (n, n) ] ]
+ ;
+ (* We unfold a range selectors list once so that we can make a special case
+ * for a unique SelectNth selector. *)
+ range_selector_or_nth:
+ [ [ n = natural ; "-" ; m = natural;
+ l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
+ SelectList ((n, m) :: Option.default [] l)
+ | n = natural;
+ l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
+ Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
+ ;
selector:
- [ [ n=natural; ":" -> Vernacexpr.SelectNth n
- | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
- | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
+ [ [ l = range_selector_or_nth; ":" -> l
+ | IDENT "all" ; ":" -> SelectAll ] ]
+ ;
+ toplevel_selector:
+ [ [ s = selector -> s
+ | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ]
;
tactic_mode:
- [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
+ [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
;
END
@@ -325,7 +345,7 @@ let _ = declare_int_option {
let vernac_solve n info tcom b =
let status = Proof_global.with_current_proof (fun etac p ->
let with_end_tac = if b then Some etac else None in
- let global = match n with SelectAll -> true | _ -> false in
+ let global = match n with SelectAll | SelectList _ -> true | _ -> false in
let info = Option.append info !print_info_trace in
let (p,status) =
Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
@@ -336,13 +356,19 @@ let vernac_solve n info tcom b =
p,status) in
if not status then Feedback.feedback Feedback.AddedAxiom
+let pr_range_selector (i, j) =
+ if Int.equal i j then int i
+ else int i ++ str "-" ++ int j
+
let pr_ltac_selector = function
| SelectNth i -> int i ++ str ":"
+| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
+ str "]" ++ str ":"
| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
| SelectAll -> str "all" ++ str ":"
VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
-| [ selector(s) ] -> [ s ]
+| [ toplevel_selector(s) ] -> [ s ]
END
let pr_ltac_info n = str "Info" ++ spc () ++ int n
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 7cda7d137..a72fb0d06 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -624,6 +624,8 @@ and intern_tactic_seq onlytac ist = function
| TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
| TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
| TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+ | TacSelect (sel, tac) ->
+ ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
(* For extensions *)
| TacAlias (loc,s,l) ->
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 649764da3..3716de251 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1256,6 +1256,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
strbrk "There is an \"Info\" command to replace it." ++fnl () ++
strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
eval_tactic ist tac
+ | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias (loc,s,l) ->
let (ids, body) = Tacenv.interp_alias s in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2863384b5..bf1da8ac0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -115,6 +115,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
let tac = match gi with
| Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
+ | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
| Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
| Vernacexpr.SelectAll -> tac
in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 36277bf58..61fe34750 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -664,15 +664,21 @@ let _ =
let default_goal_selector = ref (Vernacexpr.SelectNth 1)
let get_default_goal_selector () = !default_goal_selector
+let print_range_selector (i, j) =
+ if i = j then string_of_int i
+ else string_of_int i ^ "-" ^ string_of_int j
+
let print_goal_selector = function
| Vernacexpr.SelectAll -> "all"
| Vernacexpr.SelectNth i -> string_of_int i
+ | Vernacexpr.SelectList l -> "[" ^
+ String.concat ", " (List.map print_range_selector l) ^ "]"
| Vernacexpr.SelectId id -> Id.to_string id
let parse_goal_selector = function
| "all" -> Vernacexpr.SelectAll
| i ->
- let err_msg = "A selector must be \"all\" or a natural number." in
+ let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
if i < 0 then Errors.error err_msg;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 7f904a561..3d51623ea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -476,6 +476,13 @@ module New = struct
let tclPROGRESS t =
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
+ (* Select a subset of the goals *)
+ let tclSELECT = function
+ | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i
+ | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l
+ | Tacexpr.SelectId id -> Proofview.tclFOCUSID id
+ | Tacexpr.SelectAll -> fun tac -> tac
+
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma origsigma =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 0f926468b..cfdc2cffd 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -221,6 +221,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
+ val tclSELECT : goal_selector -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
new file mode 100644
index 000000000..91fb54d9a
--- /dev/null
+++ b/test-suite/success/goal_selector.v
@@ -0,0 +1,55 @@
+Inductive two : bool -> Prop :=
+| Zero : two false
+| One : two true.
+
+Ltac dup :=
+ let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial);
+ apply H; clear H.
+
+Lemma transform : two false <-> two true.
+Proof. split; intros _; constructor. Qed.
+
+Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
+Proof.
+ do 2 dup.
+ - repeat split.
+ 2, 4-99, 100-3:idtac.
+ 2-5:exact One.
+ par:exact Zero.
+ - repeat split.
+ 3-6:swap 1 4.
+ 1-5:swap 1 5.
+ 0-4:exact One.
+ all:exact Zero.
+ - repeat split.
+ 1, 3:exact Zero.
+ 1, 2, 3, 4: exact One.
+ - repeat split.
+ all:apply transform.
+ 2, 4, 6:apply transform.
+ all:apply transform.
+ 1-5:apply transform.
+ 1-6:exact One.
+Qed.
+
+Goal True -> True.
+Proof.
+ intros y; 1-2 : repeat idtac.
+ 1-1:match goal with y : _ |- _ => let x := y in idtac x end.
+ Fail 1-1:let x := y in idtac x.
+ 1:let x := y in idtac x.
+ exact I.
+Qed.
+
+Goal True /\ (True /\ True).
+Proof.
+ dup.
+ - split; 2: (split; exact I).
+ exact I.
+ - split; 2: split; exact I.
+Qed.
+
+Goal True -> exists (x : Prop), x.
+Proof.
+ intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:56:33 +0000