Adds a cycle tactic to reorder goals in a loop.

[cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].

3 files changed, 22 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e96e19015a..63e58c278f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -655,6 +655,19 @@ let give_up =
   Proof.set {initial with comb=[]} >>
   Proof.put (false,([],initial.comb))
 
+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 (front,rear) = List.chop n' initial.comb in
+  Proof.set {initial with comb=rear@front}
+
 (*** Commands ***)
 
 let in_proofview p k =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 8e47878fa2..fe732c4b37 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -266,6 +266,10 @@ val unshelve : Goal.goal list -> proofview -> proofview
    with given up goals cannot be closed. *)
 val give_up : unit tactic
 
+(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
+    is negative, then it puts the [n] last goals first.*)
+val cycle : 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 fa2ac37126..635904cc7e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -871,3 +871,8 @@ TACTIC EXTEND give_up
 | [ "give_up" ] ->
     [ Proofview.give_up ]
 END
+
+(* cycles [n] goals *)
+TACTIC EXTEND cycle
+| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle (out_arg n) ]
+END