Add goal range selectors.

You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.

2 files changed, 41 insertions, 0 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index bcdd4da11..d1970abc9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -388,6 +388,37 @@ 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
+    (* Sort the list to 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 l = CList.sort compare l in
+    match l with
+      | [] -> tclZERO (NoSuchGoals 0)
+      | (mi, _) :: _ ->
+          let left, sub_right = CList.goto (mi-1) comb in
+          let p x = CList.exists (fun (i, j) -> i <= x && x <= j) l in
+          (* Since there is no [CList.partitioni], we do it manually. *)
+          let sub = CList.filteri (fun x _ -> p (x + mi)) sub_right in
+          let right = CList.filteri (fun x _ -> not (p (x + mi))) 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 7996b7969..2f8394e84 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)] denothing
+    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.*)