diff options
author | Jason Gross <jgross@mit.edu> | 2017-12-12 12:00:25 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-12-14 18:02:41 -0500 |
commit | 29644bf0814945cbf2b4388b8f8bd19f109503a0 (patch) | |
tree | ca37a531989f7c329d78dda769f1f54dc7617ea3 | |
parent | b270ad686075e5579dc3826fafdc324ea339785c (diff) |
Make [abstract] nodes show up in the Ltac profile
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 12 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/tacsubst.ml | 2 | ||||
-rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.out | 14 | ||||
-rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.v | 8 | ||||
-rw-r--r-- | test-suite/output/bug5778.out | 4 | ||||
-rw-r--r-- | test-suite/output/bug5778.v | 7 |
10 files changed, 52 insertions, 15 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ebf6e450b..8dd4199e3 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -125,9 +125,9 @@ GEXTEND Gram | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta (*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) + | IDENT "abstract"; tc = NEXT -> TacAbstract (Loc.tag ~loc:!@loc (tc,None)) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) + TacAbstract (Loc.tag ~loc:!@loc (tc,Some s)) | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] (*End of To do*) | "2" RIGHTA @@ -401,12 +401,12 @@ VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default END let is_anonymous_abstract = function - | TacAbstract (_,None) -> true - | TacSolve [TacAbstract (_,None)] -> true + | TacAbstract (_,(_,None)) -> true + | TacSolve [TacAbstract (_,(_,None))] -> true | _ -> false let rm_abstract = function - | TacAbstract (t,_) -> t - | TacSolve [TacAbstract (t,_)] -> TacSolve [t] + | TacAbstract (_,(t,_)) -> t + | TacSolve [TacAbstract (_,(t,_))] -> TacSolve [t] | x -> x let is_explicit_terminator = function TacSolve _ -> true | _ -> false diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e5ff47356..c9676ac6f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -881,9 +881,9 @@ let pr_goal_selector ~toplevel s = let rec pr_tac inherited tac = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with - | TacAbstract (t,None) -> + | TacAbstract (_,(t,None)) -> keyword "abstract " ++ pr_tac (labstract,L) t, labstract - | TacAbstract (t,Some s) -> + | TacAbstract (_,(t,Some s)) -> hov 0 ( keyword "abstract" ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index ccd555b61..a98752e26 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -249,7 +249,7 @@ and 'a gen_tactic_expr = | TacProgress of 'a gen_tactic_expr | TacShowHyps of 'a gen_tactic_expr | TacAbstract of - 'a gen_tactic_expr * Id.t option + ('a gen_tactic_expr * Id.t option) Loc.located | TacId of 'n message_token list | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ebffde441..acdbc7d79 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -584,8 +584,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l) | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac) - | TacAbstract (tac,s) -> - ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s) + | TacAbstract (loc,(tac,s)) -> + ist.ltacvars, TacAbstract (loc,(intern_pure_tactic ist tac,s)) | TacThen (t1,t2) -> let lfun', t1 = intern_tactic_seq onlytac ist t1 in let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ded902a8f..dccb7cb75 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end - | TacAbstract (tac,ido) -> + | TacAbstract (loc,(t,ido)) -> + let call = LtacMLCall tac in + push_trace(loc,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:TacAbstract" trace + (catch_error_tac trace begin Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end + (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) + end end) | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 79bf3685e..2b4dd2a27 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -192,7 +192,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacId _ | TacFail _ as x -> x | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr) | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr) - | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s) + | TacAbstract (loc,(tac,s)) -> TacAbstract (loc,(subst_tactic subst tac,s)) | TacThen (t1,t2) -> TacThen (subst_tactic subst t1, subst_tactic subst t2) | TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl) diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out new file mode 100644 index 000000000..c60c5abdd --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -0,0 +1,14 @@ +total time: 0.964s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep' -------------------------------- 100.0% 100.0% 1 0.964s +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.964s + └─constructor ------------------------- 0.0% 0.0% 1 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v new file mode 100644 index 000000000..10a76309e --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. abstract (sleep; constructor). +Defined. diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out new file mode 100644 index 000000000..91ceb1b58 --- /dev/null +++ b/test-suite/output/bug5778.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call +failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 000000000..0dcd76aef --- /dev/null +++ b/test-suite/output/bug5778.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. |