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

backtracks, print time spent in each of successive calls.

15 files changed, 81 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index 0fa460dca..6494173b5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -119,6 +119,7 @@ Tactics
   error messages.
 - Tactic "subst id" now supports id occurring in dependent local definitions.
 - Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities.
+- New tactical "time" to display time spent executing its argument.
 
 Program
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9f65c0ef0..8e588f4e6 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -102,6 +102,7 @@ is understood as
 & | & {\tt once} {\tacexprpref}\\
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
+& | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -401,7 +402,7 @@ Branching is left-associative.
 \subsubsection[First tactic to work]{First tactic to work\tacindex{first}
 \index{Tacticals!first@{\tt first}}}
 
-Backtracking branching may be too expansive. In this case we may
+Backtracking branching may be too expensive. In this case we may
 restrict to a local, left biased, branching and consider the first
 tactic to work (i.e. which does not fail) among a panel of tactics:
 \begin{quote}
@@ -537,6 +538,20 @@ phases, we strongly advise you to not leave any {\tt timeout} in
 final scripts. Note also that this tactical isn't available on
 the native Windows port of Coq.
 
+\subsubsection{Timing a tactic\tacindex{time}
+\index{Tacticals!time@{\tt time}}}
+
+A tactic execution can be timed:
+\begin{quote}
+ {\tt time} {\qstring} {\tacexpr}
+\end{quote}
+evaluates {\tacexpr}
+and displays the time the tactic expression ran, whether it fails or
+successes. In case of several successes, the time for each successive
+runs is displayed. Time is in seconds and is machine-dependent. The
+{\qstring} argument is optional. When provided, it is used to identify
+this particular occurrence of {\tt time}.
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let}
 \index{Ltac!let rec}
 \index{let!in Ltac}
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 530213b7c..493c0939a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,6 +209,7 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacDo of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacTimeout of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacTime of string option * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacRepeat of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacProgress of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacShowHyps of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/lib/system.ml b/lib/system.ml
index 6c357ee36..4188eb2b4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -279,3 +279,19 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
   str "," ++
   real (round (sstop -. sstart)) ++ str "s" ++
   str ")"
+
+let with_time time f x =
+  let tstart = get_time() in
+  let msg = if time then "" else "Finished transaction in " in
+  try
+    let y = f x in
+    let tend = get_time() in
+    let msg2 = if time then "" else " (successful)" in
+    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    y
+  with e ->
+    let tend = get_time() in
+    let msg = if time then "" else "Finished failing transaction in " in
+    let msg2 = if time then "" else " (failure)" in
+    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    raise e
diff --git a/lib/system.mli b/lib/system.mli
index 2e286a40c..9cfb1456f 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -67,3 +67,5 @@ type time
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
+
+val with_time : bool -> ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index f70a865d7..fd7091ec9 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -64,6 +64,7 @@ GEXTEND Gram
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
       | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
+      | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
       | IDENT "once"; ta = tactic_expr -> TacOnce ta
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f6c25d069..e51d7b3fd 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -865,6 +865,9 @@ let rec pr_tac inherited tac =
       hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++
              pr_tac (ltactical,E) t),
       ltactical
+  | TacTime (s,t) ->
+      hov 1 (str "time" ++ pr_opt str s ++ str " " ++ pr_tac (ltactical,E) t),
+      ltactical
   | TacRepeat t ->
       hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t),
       ltactical
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a36d2675d..6074a13d4 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 0c75eb5af..1aad0e090 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
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index f68f75359..bcff61e9c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -613,6 +613,8 @@ and intern_tactic_seq onlytac ist = function
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
   | TacTimeout (n,tac) ->
       ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
+  | TacTime (s,tac) ->
+      ist.ltacvars, TacTime (s,intern_tactic onlytac ist tac)
   | TacOr (tac1,tac2) ->
       ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
   | TacOnce tac ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9d8bc6843..bc7e02ed4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1023,6 +1023,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
+  | TacTime (s,tac) -> Tacticals.New.tclTIME s (interp_tactic ist tac)
   | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac)
   | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac)
   | TacOr (tac1,tac2) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4dd4b0aa8..d60356105 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -230,6 +230,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
   | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
   | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
+  | TacTime (s,tac) -> TacTime (s,subst_tactic subst tac)
   | TacTry tac -> TacTry (subst_tactic subst tac)
   | TacInfo tac -> TacInfo (subst_tactic subst tac)
   | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 966d355d4..22ca1f044 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -467,6 +467,9 @@ module New = struct
         | e -> Proofview.tclZERO e
       end
 
+  let tclTIME s t =
+    Proofview.tclTIME s t
+
   let nthDecl m gl =
     let hyps = Proofview.Goal.hyps gl in
     try
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 48fd44b4a..9c91638cf 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -212,6 +212,7 @@ module New : sig
   val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
+  val tclTIME : string option -> 'a tactic -> 'a tactic
 
   val nLastDecls  : [ `NF ] Proofview.Goal.t -> int -> named_context
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1d05f4e62..b98801ea7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1965,11 +1965,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacTime v ->
-	let tstart = System.get_time() in
-        aux_list ?locality ?polymorphism isprogcmd v;
-	let tend = System.get_time() in
-	let msg = if !Flags.time then "" else "Finished transaction in " in
-        msg_info (str msg ++ System.fmt_time_difference tstart tend)
+        System.with_time !Flags.time
+          (aux_list ?locality ?polymorphism isprogcmd) v;
     | VernacLoad (_,fname) -> vernac_load (aux false) fname
     | c -> 
         check_vernac_supports_locality c locality;