diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 13 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 1 |
3 files changed, 17 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index c478bd6635..da1937ef3d 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -579,6 +579,19 @@ let tclTIMEOUT n t = Proof.ret res | Util.Inr e -> tclZERO e +let tclTIME t = + let (>>=) = Proof.bind in + let (>>) = Proof.seq in + let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in + Proof.current >>= fun env -> + Proof.get >>= fun initial -> + Proof.lift begin + Proofview_monad.NonLogical.time !Flags.time (Proof.run t env initial) + end >>= function ((res,s),m) -> + Proof.set s >> + Proof.put m >> + Proof.ret res + let mark_as_unsafe = Proof.put (false,([],[])) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6a2d815114..df833a04ff 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -261,6 +261,9 @@ exception Timeout In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic +(** [tclTIME t] displays time for each atomic call to t *) +val tclTIME : 'a tactic -> 'a tactic + (** [mark_as_unsafe] signals that the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 4d4e4470c0..8139d3026b 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -38,6 +38,7 @@ module NonLogical : sig val raise : exn -> 'a t val catch : 'a t -> (exn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t + val time : bool -> 'a t -> 'a t (* [run] performs effects. *) |