Merge PR #6381: A version of [time] that works on constr evaluation

6 files changed, 98 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 24f3580787..c155bb52f4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,8 @@ Tactics
 - Tactic "decide equality" now able to manage constructors which
   contain proofs.
 - Added tactics reset ltac profile, show ltac profile (and variants)
+- Added tactics restart_timer, finish_timing, and time_constr as an
+  experimental way of timing Ltac's evaluation phase
 
 Vernacular Commands
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 00430c07f6..89f0b5ae11 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -709,6 +709,55 @@ 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{Timing a tactic that evaluates to a term\tacindex{time\_constr}\tacindex{restart\_timer}\tacindex{finish\_timing}
+\index{Tacticals!time\_constr@{\tt time\_constr}}}
+\index{Tacticals!restart\_timer@{\tt restart\_timer}}
+\index{Tacticals!finish\_timing@{\tt finish\_timing}}
+
+Tactic expressions that produce terms can be timed with the experimental tactic
+\begin{quote}
+ {\tt time\_constr} {\tacexpr}
+\end{quote}
+which evaluates {\tacexpr\tt{ ()}}
+and displays the time the tactic expression evaluated, assuming successful evaluation.
+Time is in seconds and is machine-dependent.
+
+This tactic currently does not support nesting, and will report times based on the innermost execution.
+This is due to the fact that it is implemented using the tactics
+\begin{quote}
+ {\tt restart\_timer} {\qstring}
+\end{quote}
+and
+\begin{quote}
+ {\tt finish\_timing} ({\qstring}) {\qstring}
+\end{quote}
+which (re)set and display an optionally named timer, respectively.
+The parenthsized {\qstring} argument to {\tt finish\_timing} is also
+optional, and determines the label associated with the timer for
+printing.
+
+By copying the definition of {\tt time\_constr} from the standard
+library, users can achive support for a fixed pattern of nesting by
+passing different {\qstring} parameters to {\tt restart\_timer} and
+{\tt finish\_timing} at each level of nesting.  For example:
+
+\begin{coq_example}
+Ltac time_constr1 tac :=
+  let eval_early := match goal with _ => restart_timer "(depth 1)" end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in
+  ret.
+
+Goal True.
+  let v := time_constr
+             ltac:(fun _ =>
+                     let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in
+                     let y := time_constr1 ltac:(fun _ => eval compute in x) in
+                     y) in
+  pose v.
+Abort.
+\end{coq_example}
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}}
 \index{Ltac!let rec@\texttt{let rec}}
 \index{let@\texttt{let}!in Ltac}
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5e3b7cf775..1615465281 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -397,6 +397,27 @@ let reset_profile () =
   reset_profile_tmp ();
   data := SM.empty
 
+(* ****************************** Named timers ****************************** *)
+
+let timer_data = ref M.empty
+
+let timer_name = function
+  | Some v -> v
+  | None -> ""
+
+let restart_timer name =
+  timer_data := M.add (timer_name name) (System.get_time ()) !timer_data
+
+let get_timer name =
+  try M.find (timer_name name) !timer_data
+  with Not_found -> System.get_time ()
+
+let finish_timing ~prefix name =
+  let tend = System.get_time () in
+  let tstart = get_timer name in
+  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+                    System.fmt_time_difference tstart tend)
+
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index feb7773526..adedf7ee91 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -52,6 +52,10 @@ val print_results_tactic : string -> unit
 
 val reset_profile : unit -> unit
 
+val restart_timer : string option -> unit
+
+val finish_timing : prefix:string -> string option -> unit
+
 val do_print_results_at_close : unit -> unit
 
 (* The collected statistics for a tactic. The timing data is collected over all
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 58e3a3a57e..9864ffeb65 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -27,6 +27,12 @@ let tclSHOW_PROFILE ~cutoff =
 let tclSHOW_PROFILE_TACTIC s =
    Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s))
 
+let tclRESTART_TIMER s =
+   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s))
+
+let tclFINISH_TIMING ?(prefix="Timer") (s : string option) =
+   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s))
+
 TACTIC EXTEND start_ltac_profiling
 | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
 END
@@ -45,6 +51,15 @@ TACTIC EXTEND show_ltac_profile
 | [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ]
 END
 
+TACTIC EXTEND restart_timer
+| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ]
+END
+
+TACTIC EXTEND finish_timing
+| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ]
+| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ]
+END
+
 VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
   [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ]
 END
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 5d0e7602a9..47a971ef09 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -306,3 +306,10 @@ Ltac inversion_sigma_step :=
     => induction_sigma_in_using H @eq_sigT2_rect
   end.
 Ltac inversion_sigma := repeat inversion_sigma_step.
+
+(** A version of [time] that works for constrs *)
+Ltac time_constr tac :=
+  let eval_early := match goal with _ => restart_timer end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
+  ret.