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].

2 files changed, 17 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e96e19015..63e58c278 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 8e47878fa..fe732c4b3 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]. *)