From 29697585836c6e0e4d91e28a13c3f40d2137208b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 May 2016 18:23:32 +0200 Subject: Fix bug #4707: clearbody much slower in 8.5pl1. We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time. --- tactics/tactics.ml | 56 ++++++++++++++++++++++++++++++++---------------------- 1 file changed, 33 insertions(+), 23 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 28aed8a10e..63d3c694ea 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1789,17 +1789,17 @@ let on_the_bodies = function | [id] -> str " depends on the body of " ++ pr_id id | l -> str " depends on the bodies of " ++ pr_sequence pr_id l -let check_is_type env ty msg = - Proofview.tclEVARMAP >>= fun sigma -> +exception DependsOnBody of Id.t option + +let check_is_type env sigma ty = let evdref = ref sigma in try let _ = Typing.sort_of env evdref ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + raise (DependsOnBody None) -let check_decl env (_, c, ty) msg = - Proofview.tclEVARMAP >>= fun sigma -> +let check_decl env sigma (id, c, ty) = let evdref = ref sigma in try let _ = Typing.sort_of env evdref ty in @@ -1807,14 +1807,15 @@ let check_decl env (_, c, ty) msg = | None -> () | Some c -> Typing.check env evdref c ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + raise (DependsOnBody (Some id)) let clear_body ids = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let sigma = Proofview.Goal.sigma gl in let ctx = named_context env in let map (id, body, t as decl) = match body with | None -> @@ -1828,23 +1829,32 @@ let clear_body ids = let ctx = List.map map ctx in let base_env = reset_context env in let env = push_named_context ctx base_env in - let check_hyps = - let check env (id, _, _ as decl) = - let msg _ = Tacticals.New.tclZEROMSG - (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids) + let check = + try + let check (env, sigma) decl = + (** Do no recheck hypotheses that do not depend *) + let sigma = + if List.exists (fun id -> occur_var_in_decl env id decl) ids then + check_decl env sigma decl + else sigma + in + (push_named decl env, sigma) in - check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env) - in - let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in - Proofview.tclIGNORE checks - in - let check_concl = - let msg _ = Tacticals.New.tclZEROMSG - (str "Conclusion" ++ on_the_bodies ids) - in - check_is_type env concl msg + let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in + let sigma = + if List.exists (fun id -> occur_var env id concl) ids then + check_is_type env sigma concl + else sigma + in + Proofview.Unsafe.tclEVARS sigma + with DependsOnBody where -> + let msg = match where with + | None -> str "Conclusion" ++ on_the_bodies ids + | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids + in + Tacticals.New.tclZEROMSG msg in - check_hyps <*> check_concl <*> + check <*> Proofview.Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end -- cgit v1.2.3 From 27689bac62f85c039517cbd003f8ea74cb9b4aa7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 24 Apr 2016 18:22:53 +0200 Subject: In Regular Subst Tactic mode, ensure that the order of hypotheses is preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. --- tactics/equality.ml | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index f72a72f46d..819a995db1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1595,6 +1595,17 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) +let regular_subst_tactic = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let unfold_body x = Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) @@ -1642,23 +1653,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = - List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) -> + List.rev (pi3 (List.fold_right (fun (id,b,_ as dcl) (dest,deps,allhyps) -> if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then - ((if b = None then deps else id::deps), id::allhyps) + let id_dest = if !regular_subst_tactic then dest else MoveLast in + (dest,(if b = None then deps else id::deps), (id_dest,id)::allhyps) else - (deps,allhyps)) + (MoveBefore id,deps,allhyps)) hyps - ([x],[]))) in + (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) let depconcl = occur_var env x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [revert dephyps; + [revert (List.map snd dephyps); general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); - (tclMAP intro_using dephyps)] + (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) @@ -1709,17 +1721,6 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -let regular_subst_tactic = ref false - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "more regular behavior of tactic subst"; - optkey = ["Regular";"Subst";"Tactic"]; - optread = (fun () -> !regular_subst_tactic); - optwrite = (:=) regular_subst_tactic } - let subst_all ?(flags=default_subst_tactic_flags ()) () = if !regular_subst_tactic then -- cgit v1.2.3