Fix a bug with with_strategy, behavior on multisuccess tactics

Copy tclWRAPFINALLY to tactics.ml

As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't export
it from Proofview, because it seems somehow not primitive enough.  But
we don't export it from Tactics because it is more of a tactical than a
tactic.  But we don't export it from Tacticals because all of the
non-New tacticals there operate on `tactic`, not `Proofview.tactic`, and
all of the `New` tacticals that deal with multi-success things are
focussing, i.e., apply their arguments on each goal separately (and it
even says so in the comment on `New`), whereas it's important that
`tclWRAPFINALLY` doesn't introduce extra focussing.

3 files changed, 101 insertions, 37 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 350881f72d..c1b1076102 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5045,49 +5045,77 @@ let unify ?(state=TransparentState.full) x y =
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+    entry-point of [tac] and passes the result of [before] to
+    [finally], which is then run at each exit-point of [tac],
+    regardless of whether it succeeds or fails.  Said another way, if
+    [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+    ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+    [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+    e].  Note that if [tac] succeeds [n] times before finally failing,
+    [before] and [finally] are both run [n+1] times (once around each
+    succuess, and once more around the final failure). *)
+(* We should probably export this somewhere, but it's not clear
+   where. As per
+   https://github.com/coq/coq/pull/12197#discussion_r418480525 and
+   https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't
+   export it from Proofview, because it seems somehow not primitive
+   enough.  We don't export it from this file because it is more of a
+   tactical than a tactic.  But we also don't export it from Tacticals
+   because all of the non-New tacticals there operate on `tactic`, not
+   `Proofview.tactic`, and all of the `New` tacticals that deal with
+   multi-success things are focussing, i.e., apply their arguments on
+   each goal separately (and it even says so in the comment on `New`),
+   whereas it's important that `tclWRAPFINALLY` doesn't introduce
+   extra focussing. *)
+let rec tclWRAPFINALLY before tac finally =
+  let open Proofview in
+  let open Proofview.Notations in
+  before >>= fun v -> tclCASE tac >>= function
+  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Next (ret, tac') -> tclOR
+                          (finally v >>= fun () -> tclUNIT ret)
+                          (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
 let with_set_strategy lvl_ql k =
   let glob_key r =
     match r with
     | GlobRef.ConstRef sp -> ConstKey sp
     | GlobRef.VarRef id -> VarKey id
     | _ -> user_err Pp.(str
-        "cannot set an inductive type or a constructor as transparent") in
+                          "cannot set an inductive type or a constructor as transparent") in
   let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in
-  Proofview.tclENV >>= fun env ->
-  let orig_kl = List.map (fun (_lvl, k) ->
-      (Conv_oracle.get_strategy (Environ.oracle env) k, k))
-      kl in
-  (* Because the global env might be desynchronized from the proof-local
-     env, we need to update the global env to have this tactic play
-     nicely with abstract.
-     TODO: When abstract no longer depends on Global, delete this variable
-       let-in *)
-  let orig_kl_global = List.map (fun (_lvl, k) ->
-      (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k))
-      kl in
-  let env = List.fold_left (fun env (lvl, k) ->
-    Environ.set_oracle env
-      (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
-  (* TODO: When abstract no longer depends on Global, replace this
-       [Proofview.Goal.enter] block with [Proofview.Unsafe.tclSETENV env] *)
-  Proofview.Goal.enter begin
-    fun _ ->
-      List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl;
-      Proofview.Unsafe.tclSETENV env
-  end <*>
-  k <*>
-  Proofview.tclENV >>= fun env ->
-  let env = List.fold_left (fun env (lvl, k) ->
-      Environ.set_oracle env
-        (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
-  Proofview.Unsafe.tclSETENV env <*>
-  (* TODO: When abstract no longer depends on Global, remove this
-       [Proofview.Goal.enter] block *)
-  Proofview.Goal.enter begin
-    fun _ ->
-      List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global;
-      Proofview.tclUNIT ()
-  end
+  tclWRAPFINALLY
+    (Proofview.tclENV >>= fun env ->
+     let orig_kl = List.map (fun (_lvl, k) ->
+         (Conv_oracle.get_strategy (Environ.oracle env) k, k))
+         kl in
+     (* Because the global env might be desynchronized from the proof-local
+        env, we need to update the global env to have this tactic play
+        nicely with abstract.
+        TODO: When abstract no longer depends on Global, delete this variable
+        let-in *)
+     let orig_kl_global = List.map (fun (_lvl, k) ->
+         (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k))
+         kl in
+     let env = List.fold_left (fun env (lvl, k) ->
+         Environ.set_oracle env
+           (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
+     Proofview.Unsafe.tclSETENV env <*>
+     Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+         List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*>
+     Proofview.tclUNIT (orig_kl, orig_kl_global))
+    k
+    (fun (orig_kl, orig_kl_global) ->
+       (* TODO: When abstract no longer depends on Global, remove this
+          [Proofview.tclLIFT] block *)
+       Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+           List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*>
+       Proofview.tclENV >>= fun env ->
+       let env = List.fold_left (fun env (lvl, k) ->
+           Environ.set_oracle env
+             (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
+       Proofview.Unsafe.tclSETENV env)
 
 module Simple = struct
   (** Simplified version of some of the above tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fb4367f3aa..b6eb48a3d9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -439,7 +439,7 @@ val declare_intro_decomp_eq :
    locally to the tactic argument *)
 val with_set_strategy :
   (Conv_oracle.level * Names.GlobRef.t list) list ->
-  unit Proofview.tactic -> unit Proofview.tactic
+  'a Proofview.tactic -> 'a Proofview.tactic
 
 (** {6 Simple form of basic tactics. } *)
 
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index 4f761fb470..e0d0252a47 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -149,6 +149,42 @@ Proof using Type.
        reflexivity).
 Time Timeout 5 Qed.
 
+(* test that the strategy is correctly reverted after closing the goal completely *)
+Goal id 0 = 0.
+  assert (id 0 = 0) by with_strategy expand [id] reflexivity.
+  Fail unfold id.
+  reflexivity.
+Qed.
+
+(* test that the strategy is correctly reverted after failure *)
+Goal id 0 = 0.
+  let id' := id in
+  (try with_strategy expand [id] fail); assert_fails unfold id'.
+  Fail unfold id.
+  (* a more complicated test involving a success and then a failure after backtracking *)
+  let id' := id in
+  ((with_strategy expand [id] (unfold id' + fail)) + idtac);
+    lazymatch goal with |- id 0 = 0 => idtac end;
+    assert_fails unfold id'.
+  Fail unfold id.
+  reflexivity.
+Qed.
+
+(* test multi-success *)
+Goal id (fact 100) = fact 100.
+  Timeout 1
+          (with_strategy -1 [id] (((idtac + (abstract reflexivity))); fail)).
+  Undo.
+  Timeout 1
+          let id' := id in
+          (with_strategy -1 [id] (((idtac + (unfold id'; reflexivity))); fail)).
+  Undo.
+  Timeout 1
+          (with_strategy -1 [id] (idtac + (abstract reflexivity))); fail. (* should not time out *)
+  Undo.
+  with_strategy -1 [id] abstract reflexivity.
+Defined.
+
 (* check that module substitutions happen correctly *)
 Module F.
   Definition id {T} := @id T.