Add a tactic [swap i j] to swap the position of goals [i] and [j].

If [i] or [j] is negative goals are counted from the end.

3 files changed, 38 insertions, 5 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 63e58c278f..9f2ab30b65 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -655,19 +655,41 @@ let give_up =
   Proof.set {initial with comb=[]} >>
   Proof.put (false,([],initial.comb))
 
+(** [goodmod p m] computes the representative of [p] modulo [m] in the
+    interval [[0,m-1]].*)
+let goodmod p m =
+  let p' = p mod m in
+  (* if [n] is negative [n mod l] is negative of absolute value less
+     than [l], so [(n mod l)+l] is the representative of [n] in the
+     interval [[0,l-1]].*)
+  if p' < 0 then p'+m else p'
+
 let cycle n =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun initial ->
   let l = List.length initial.comb in
-  let n' = n mod l in
-  (* if [n] is negative [n mod l] is negative of absolute value less
-     than [l], so [(n mod l)+l] is the representative of [n] in the
-     interval [[0,l-1]].*)
-  let n' = if n' < 0 then n'+l else n' in
+  let n' = goodmod n l in
   let (front,rear) = List.chop n' initial.comb in
   Proof.set {initial with comb=rear@front}
 
+let swap i j =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  let l = List.length initial.comb in
+  let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
+  let i = goodmod i l and j = goodmod j l in
+  let comb =
+    CList.map_i begin fun k x ->
+      match k with
+      | k when Int.equal k i -> CList.nth initial.comb j
+      | k when Int.equal k j -> CList.nth initial.comb i
+      | _ -> x
+    end 0 initial.comb
+  in
+  Proof.set {initial with comb}
+
 (*** Commands ***)
 
 let in_proofview p k =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index fe732c4b37..5d093b43b5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -270,6 +270,12 @@ val give_up : unit tactic
     is negative, then it puts the [n] last goals first.*)
 val cycle : int -> unit tactic
 
+(** [swap i j] swaps the position of goals number [i] and [j]
+    (negative numbers can be used to address goals from the end. Goals
+    are indexed from [1]. For simplicity index [0] corresponds to goal
+    [1] as well, rather than raising an error. *)
+val swap : int -> int -> unit tactic
+
 exception Timeout
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 635904cc7e..d0993b66ea 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -876,3 +876,8 @@ END
 TACTIC EXTEND cycle
 | [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ]
 END
+
+(* swaps goals number [i] and [j] *)
+TACTIC EXTEND swap
+| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap (out_arg i) (out_arg j) ]
+END