Add Proofview.tclWRAPFINALLY

This new primitive (which could be implemented in terms of `tclCASE`,
but which I believe encapsulates a useful unit of behavior) is needed
for correctly implementing both `with_strategy` and for implementing
multi-success support for the Ltac Profiler.

The basic function of this tactical is to allow wrapping multi-success
tactics with initialization and cleanup routines.  For example, if `tac`
is a multi-success tactic that writes its status to a log file, you
might want to wrap `tac` in "first open the log file" and then after it
runs "finally close the log file".  (Unfortunately, the way the monad is
set up doesn't allow passing data from the most recent run of the
initializer to the tactic, which suggests that perhaps there's something
a bit off about this abstraction.  Perhaps we should set up a ref cell
and that will hold the most recent return of the initializer and pass
this ref cell to the wrapped tactic?  But this can be done externally
without needing to modify the current API.  In any case, such data is
not needed in the case of the Ltac Profiler, where the initializer is
"update the current call stack and record the current start time" and
the finalizer is "update the call stack and record the end time", and
you want to have the start time be restarted when re-entering a tactic.
Nor is it needed for `with_strategy` which needs to update the global
conv_oracle so that it plays nicely with `abstract`.)

2 files changed, 27 insertions, 0 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..1d2c7d8729 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -297,6 +297,23 @@ let tclIFCATCH a s f =
     | Nil e -> f e
     | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
 
+(** [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]. *)
+let rec tclWRAPFINALLY before tac finally =
+  let open Logic_monad in
+  let open Proof in
+  before >>= fun v -> split tac >>= function
+  | Nil e -> finally v >>= fun () -> zero e
+  | Cons (ret,tac') -> plus
+                         (finally v >>= fun () -> return ret)
+                         (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
     with [e], [tclONCE t] also fails with [e]. *)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index d0a2b37a69..70513c8166 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -208,6 +208,16 @@ val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
     exception can be assumed non critical. *)
 val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
 
+(** [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]. *)
+val tclWRAPFINALLY : 'a tactic -> 'b tactic -> ('a -> unit tactic) -> 'b tactic
+
 (** [tclONCE t] behave like [t] except it has at most one success:
     [tclONCE t] stops after the first success of [t]. If [t] fails
     with [e], [tclONCE t] also fails with [e]. *)