Adding a "time" tactical for benchmarking purposes. In case the tactic

backtracks, print time spent in each of successive calls.

2 files changed, 31 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a36d2675d6..6074a13d4c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -20,6 +20,7 @@
    There is also need of a list of the evars which initialised the proofview
    to be able to return information about the proofview. *)
 
+open Pp
 open Util
 
 (* Type of proofviews. *)
@@ -593,6 +594,32 @@ let tclTIMEOUT n t =
         Proof.ret res
     | Util.Inr e -> tclZERO e
 
+let tclTIME s t =
+  let (>>=) = Proof.bind in
+  let pr_time t1 t2 n msg =
+    let msg =
+      if n = 0 then
+        str msg
+      else
+        str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking")
+    in
+    msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
+             System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
+  let rec aux n t =
+    let tstart = System.get_time() in
+    Proof.split t >>= function
+    | Nil e ->
+      begin
+        let tend = System.get_time() in
+        pr_time tstart tend n "failure";
+        tclZERO e
+      end
+    | Cons (x,k) ->
+        let tend = System.get_time() in
+        pr_time tstart tend n "success";
+        tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
+  in aux 0 t
+
 let mark_as_unsafe =
   Proof.put (false,([],[]))
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0c75eb5aff..1aad0e090f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -271,6 +271,10 @@ exception Timeout
     In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
+(** [tclTIME s t] displays time for each atomic call to t, using s as an
+    identifying annotation if present *)
+val tclTIME : string option -> 'a tactic -> 'a tactic
+
 (** [mark_as_unsafe] signals that the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic