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.

2 files changed, 33 insertions, 5 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 63e58c278..9f2ab30b6 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 fe732c4b3..5d093b43b 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]. *)