Merge PR #21642: Ltac2.Control.reorder_goals

Reviewed-by: ppedrot
Ack-by: JasonGross
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

doc/changelog/06-Ltac2-language/21642-redoer-goals-Added.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  `Ltac2.Control.reorder_goals`
+  (`#21642 <https://github.com/rocq-prover/rocq/pull/21642>`_,
+  fixes `#20087 <https://github.com/rocq-prover/rocq/issues/20087>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -1081,6 +1081,30 @@ let () =
     Proofview.tclUNIT ()
   else throw Tac2ffi.err_notfound
 
+let is_permutation len l =
+  if not (Int.equal len (Array.length l)) then false else
+  let items = Array.make len false in
+  (* returns true iff [l] (seen as a 1-indexed list) maps ints in [1; len] to [1; len] injectively.
+     Thanks to pigeonhole theorem this means [l] is a permutation of [1; len]. *)
+  Array.for_all (fun x ->
+      if 1 <= x && x <= len && not items.(x-1) then
+        let () = items.(x-1) <- true in
+        true
+      else false)
+    l
+
+let () =
+  define "reorder_goals" (list int @-> tac unit) @@ fun l ->
+  Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+  let len = List.length gls in
+  let l = Array.of_list l in
+  if not (is_permutation len l) then
+    throw (err_invalid_arg (Pp.str "reorder_goals"))
+  else
+    let gls = Array.of_list gls in
+    let gls = List.init len (fun i -> gls.(l.(i) - 1)) in
+    Proofview.Unsafe.tclSETGOALS gls
+
 let () =
   define "unshelve" (thunk valexpr @-> tac valexpr) @@ fun t ->
   Proofview.with_shelf (thaw t) >>= fun (gls,v) ->

plugins/ltac2/tac2ffi.ml

@@ -277,21 +277,6 @@ let rocq_core n = Names.(KerName.make Tac2env.rocq_prefix (Id.of_string_soft n))
 
 let internal_err = rocq_core "Internal"
 
-let err_notfocussed =
-  LtacError (rocq_core "Not_focussed", [||])
-
-let err_outofbounds =
-  LtacError (rocq_core "Out_of_bounds", [||])
-
-let err_notfound =
-  LtacError (rocq_core "Not_found", [||])
-
-let err_matchfailure =
-  LtacError (rocq_core "Match_failure", [||])
-
-let err_division_by_zero =
-  LtacError (rocq_core "Division_by_zero", [||])
-
 let of_exninfo = of_ext val_exninfo
 let to_exninfo = to_ext val_exninfo
 
@@ -514,3 +499,21 @@ let reference = {
   r_of = of_reference;
   r_to = to_reference;
 }
+
+let err_notfocussed =
+  LtacError (rocq_core "Not_focussed", [||])
+
+let err_outofbounds =
+  LtacError (rocq_core "Out_of_bounds", [||])
+
+let err_notfound =
+  LtacError (rocq_core "Not_found", [||])
+
+let err_matchfailure =
+  LtacError (rocq_core "Match_failure", [||])
+
+let err_division_by_zero =
+  LtacError (rocq_core "Division_by_zero", [||])
+
+let err_invalid_arg msg =
+  LtacError (rocq_core "Invalid_argument", [|of_option of_pp (Some msg)|])

plugins/ltac2/tac2ffi.mli

@@ -275,3 +275,4 @@ val err_outofbounds : exn
 val err_notfound : exn
 val err_matchfailure : exn
 val err_division_by_zero : exn
+val err_invalid_arg : Pp.t -> exn

test-suite/ltac2/reorder_goals.v

@@ -0,0 +1,21 @@
+Require Import Ltac2.Ltac2.
+
+Axiom P : nat -> Prop.
+Axiom p : forall n, P n.
+
+Goal P 1 /\ P 2 /\ P 3 /\ P 4.
+Proof.
+  repeat split.
+  Fail 1:exact (p 3). (* sanity check: "exact (p n)" assert that the goal was originally goal n *)
+  all:Control.reorder_goals [1;3;4;2].
+  4: exact (p 2).
+  Fail all:Control.reorder_goals [1;2]. (* missing goal 3 *)
+  Fail all:Control.reorder_goals [1;2;3;3]. (* duplicated goal 3 *)
+  Fail all:Control.reorder_goals [1;4;3]. (* non existing goal 4 *)
+  all:Control.reorder_goals [3;2;1];
+    Control.dispatch [
+        (fun () => exact (p 4));
+        (fun () => exact (p 3));
+        (fun () => exact (p 1))
+      ].
+Qed.

theories/Ltac2/Control.v

@@ -88,6 +88,11 @@ Ltac2 @ external new_goal : evar -> unit := "rocq-runtime.plugins.ltac2" "new_go
     already defined in the current state, don't do anything. Panics if the
     evar is not in the current state. *)
 
+Ltac2 @external reorder_goals : int list -> unit := "rocq-runtime.plugins.ltac2" "reorder_goals".
+(** [reorder_goals l] reorders the goals according to (1-indexed) list [l]:
+    goal [i] after executing the tactic was goal [nth l (i-1)] before executing the tactic.
+    Throws if [l] is not a permutation of ints from [1] to [numgoals()]. *)
+
 Ltac2 @ external unshelve : (unit -> 'a) -> 'a := "rocq-runtime.plugins.ltac2" "unshelve".
 (** Runs the closure, then unshelves existential variables added to the
     shelf by its execution, prepending them to the current goal.