diff options
| -rw-r--r-- | engine/proofview.ml | 17 | ||||
| -rw-r--r-- | engine/proofview.mli | 10 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 21 |
3 files changed, 19 insertions, 29 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 1d2c7d8729..2e036be9e3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -297,23 +297,6 @@ 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 70513c8166..d0a2b37a69 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -208,16 +208,6 @@ 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]. *) diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 44cb531e51..0dbf16a821 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -330,15 +330,32 @@ let exit_tactic ~count_call start_time c = feedback_results parent 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]. *) +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 do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in (* We do an early check to [is_profiling] so that we save the - overhead of [Proofview.tclWRAPFINALLY] when profiling is not set + overhead of [tclWRAPFINALLY] when profiling is not set *) Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function | false -> tac | true -> - Proofview.tclWRAPFINALLY + tclWRAPFINALLY (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then match call_trace, Local.(!stack) with |