diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-03 12:43:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-13 18:02:57 +0200 |
| commit | d29b487f7c50fd8332cb1cfc144f70bc7db595d9 (patch) | |
| tree | a80671a48c3db293d46f5d8d2a929486a4d02e13 /tactics | |
| parent | d90205f6284b998a8fc50b295d2d790d2580ea26 (diff) | |
Adding a "time" tactical for benchmarking purposes. In case the tactic
backtracks, print time spent in each of successive calls.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
5 files changed, 8 insertions, 0 deletions
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 |