From d29b487f7c50fd8332cb1cfc144f70bc7db595d9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 3 Jul 2014 12:43:28 +0200
Subject: Adding a "time" tactical for benchmarking purposes. In case the
 tactic backtracks, print time spent in each of successive calls.

---
 proofs/proofview.ml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'proofs/proofview.ml')

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,([],[]))
 
-- 
cgit v1.2.3