Add goal range selectors.

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

6 files changed, 62 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.*)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc..029ee8a48 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -29,6 +29,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    similar, they do not seem to mean the same thing. *)
 type goal_selector =
   | SelectNth of int
+  | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 3579fc10f..7de394435 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -295,9 +295,15 @@ GEXTEND Gram
   tactic:
     [ [ tac = tactic_expr -> tac ] ]
   ;
+
+  range_selector:
+    [ [ n = natural ; "-" ; m = natural -> (n, m)
+      | n = natural -> (n, n) ] ]
+  ;
   selector:
     [ [ n=natural; ":" -> Vernacexpr.SelectNth n
       | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
+      | "[" ; l = LIST1 range_selector SEP "," ; "]" ; ":" -> Vernacexpr.SelectList l
       | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
   ;
   tactic_mode:
@@ -336,8 +342,15 @@ 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 i = j then int i
+  else int i ++ str "-" ++ int j
+
 let pr_ltac_selector = function
 | SelectNth i -> int i ++ str ":"
+(* Special case to distinguish between 1: and 1-1: *)
+| SelectList [(i, j)] when i = j -> int i ++ str "-" ++ int j
+| SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l
 | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
 | SelectAll -> str "all" ++ str ":"
 
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..be353b10a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -664,9 +664,15 @@ 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