From 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 3 Aug 2014 19:18:21 +0200 Subject: Experimentally adding an option for automatically erasing an hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context). --- tactics/contradiction.ml | 4 +- tactics/equality.ml | 45 +++++++---- tactics/equality.mli | 8 +- tactics/extratactics.ml4 | 6 +- tactics/inv.ml | 8 +- tactics/tacintern.ml | 27 ++++--- tactics/tacinterp.ml | 54 ++++++++----- tactics/tacsubst.ml | 17 ++-- tactics/tactics.ml | 203 ++++++++++++++++++++++++++++++----------------- tactics/tactics.mli | 23 ++++-- 10 files changed, 251 insertions(+), 144 deletions(-) (limited to 'tactics') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 805ecc3ebb..96e8e60bba 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -94,7 +94,9 @@ let contradiction_term (c,lbind as cl) = let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then - Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption) + Tacticals.New.tclTHEN + (elim false None cl None) + (Tacticals.New.tclTRY assumption) else Proofview.tclORELSE begin diff --git a/tactics/equality.ml b/tactics/equality.ml index a23ae4e82f..7343aa532a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -460,6 +460,17 @@ let general_multi_rewrite l2r with_evars ?tac c cl = (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps +let apply_special_clear_request clear_flag f = + Proofview.Goal.raw_enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try + let sigma,(c,bl) = f env sigma in + apply_clear_request clear_flag (use_clear_hyp_by_default ()) c + with + e when catchable_exception e -> tclIDTAC + end + type delayed_open_constr_with_bindings = env -> evar_map -> evar_map * constr with_bindings @@ -484,7 +495,9 @@ let general_multi_multi_rewrite with_evars l cl tac = in let rec loop = function | [] -> Proofview.tclUNIT () - | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l) + | (l2r,m,clear_flag,c)::l -> + tclTHENFIRST + (tclTHEN (doN l2r c m) (apply_special_clear_request clear_flag c)) (loop l) in loop l let rewriteLR = general_rewrite true AllOccurrences true true @@ -963,7 +976,7 @@ let discrEverywhere with_evars = *) let discr_tac with_evars = function | None -> discrEverywhere with_evars - | Some c -> onInductionArg (discr with_evars) c + | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c let discrConcl = discrClause false onConcl let discrHyp id = discrClause false (onHyp id) @@ -1296,13 +1309,15 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) -let postInjEqTac ipats c n = +let use_clear_hyp_by_default () = false + +let postInjEqTac clear_flag ipats c n = match ipats with | Some ipats -> let clear_tac = - if use_injection_pattern_l2r_order () && isVar c - then tclTRY (clear [destVar c]) - else tclIDTAC in + let dft = + use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in + tclTRY (apply_clear_request clear_flag dft c) in let intro_tac = if use_injection_pattern_l2r_order () then intros_pattern_bound n MoveLast ipats @@ -1310,20 +1325,20 @@ let postInjEqTac ipats c n = tclTHEN clear_tac intro_tac | None -> tclIDTAC -let injEq ipats = +let injEq clear_flag ipats = let l2r = if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false in - injEqThen (fun c i -> postInjEqTac ipats c i) l2r + injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r -let inj ipats with_evars = onEquality with_evars (injEq ipats) +let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats) let injClause ipats with_evars = function - | None -> onNegatedEquality with_evars (injEq ipats) + | None -> onNegatedEquality with_evars (injEq None ipats) | Some c -> onInductionArg (inj ipats with_evars) c let injConcl = injClause None false None -let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) +let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> @@ -1341,10 +1356,12 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = end let dEqThen with_evars ntac = function - | None -> onNegatedEquality with_evars (decompEqThen ntac) - | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c + | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c -let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ()) +let dEq with_evars = + dEqThen with_evars (fun clear_flag c x -> + (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decompe_eq tac data cl = Proofview.Goal.raw_enter begin fun gl -> diff --git a/tactics/equality.mli b/tactics/equality.mli index 82e30b9401..2993c8d3a4 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -64,7 +64,7 @@ type delayed_open_constr_with_bindings = env -> evar_map -> evar_map * constr with_bindings val general_multi_multi_rewrite : - evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> + evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic @@ -78,14 +78,14 @@ val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic val inj : intro_pattern_expr Loc.located list option -> evars_flag -> - constr with_bindings -> unit Proofview.tactic + clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : intro_pattern_expr Loc.located list option -> evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic -val injHyp : Id.t -> unit Proofview.tactic +val injHyp : clear_flag -> Id.t -> unit Proofview.tactic val injConcl : unit Proofview.tactic val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic +val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8cf1e531dd..a7d95c5e89 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -65,8 +65,8 @@ TACTIC EXTEND replace_term END let induction_arg_of_quantified_hyp = function - | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Loc.ghost,id) + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a @@ -74,7 +74,7 @@ let induction_arg_of_quantified_hyp = function let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (ElimOnConstr c.it)) + c.sigma (Some (None,ElimOnConstr c.it)) TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> diff --git a/tactics/inv.ml b/tactics/inv.ml index ee875ce27d..36affb5412 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -308,9 +308,11 @@ let projectAndApply thin id eqname names depids = | _ -> tac id end in - let deq_trailer id _ neqns = + let deq_trailer id clear_flag _ neqns = tclTHENLIST - [(if not (List.is_empty names) then clear [id] else tclIDTAC); + [apply_clear_request clear_flag + (not (List.is_empty names) || use_clear_hyp_by_default ()) + (mkVar id); (tclMAP_i neqns (fun idopt -> tclTRY (tclTHEN (intro_move idopt MoveLast) @@ -325,7 +327,7 @@ let projectAndApply thin id eqname names depids = (* and apply a trailer which again try to substitute *) (fun id -> dEqThen false (deq_trailer id) - (Some (ElimOnConstr (mkVar id,NoBindings)))) + (Some (None,ElimOnConstr (mkVar id,NoBindings)))) id let nLastDecls i tac = diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index e2f87062ef..80711cf815 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -270,18 +270,21 @@ let intern_bindings ist = function let intern_constr_with_bindings ist (c,bl) = (intern_constr ist c, intern_bindings ist bl) +let intern_constr_with_bindings_arg ist (clear,c) = + (clear,intern_constr_with_bindings ist c) + (* TODO: catch ltac vars *) let intern_induction_arg ist = function - | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) -> + | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c) + | clear,ElimOnAnonHyp n as x -> x + | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) match intern_constr ist (CRef (Ident (dloc,id), None)) with - | GVar (loc,id),_ -> ElimOnIdent (loc,id) - | c -> ElimOnConstr (c,NoBindings) + | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id) + | c -> clear,ElimOnConstr (c,NoBindings) else - ElimOnIdent (loc,id) + clear,ElimOnIdent (loc,id) let short_name = function | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) @@ -371,8 +374,8 @@ let intern_red_expr ist = function | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r -let intern_in_hyp_as ist lf (id,ipat) = - (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat) +let intern_in_hyp_as ist lf (clear,id,ipat) = + (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat) let intern_hyp_list ist = List.map (intern_hyp ist) @@ -459,12 +462,12 @@ let rec intern_atomic lf ist x = intern_move_location ist hto) | TacExact c -> TacExact (intern_constr ist c) | TacApply (a,ev,cb,inhyp) -> - TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb, + TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, Option.map (intern_in_hyp_as ist lf) inhyp) | TacElim (ev,cb,cbo) -> - TacElim (ev,intern_constr_with_bindings ist cb, + TacElim (ev,intern_constr_with_bindings_arg ist cb, Option.map (intern_constr_with_bindings ist) cbo) - | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb) + | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb) | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in @@ -555,7 +558,7 @@ let rec intern_atomic lf ist x = | TacRewrite (ev,l,cl,by) -> TacRewrite (ev, - List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l, + List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings_arg ist c)) l, clause_app (intern_hyp_location ist) cl, Option.map (intern_pure_tactic ist) by) | TacInversion (inv,hyp) -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b52a3e7e94..0432b08ec5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -768,8 +768,8 @@ and interp_intro_pattern_list_as_list ist env = function List.map (interp_intro_pattern ist env) l) | l -> List.map (interp_intro_pattern ist env) l -let interp_in_hyp_as ist env (id,ipat) = - (interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat) +let interp_in_hyp_as ist env (clear,id,ipat) = + (clear,interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat) let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n @@ -812,11 +812,19 @@ let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, c = interp_open_constr ist env sigma c in sigma, (c,bl) +let interp_constr_with_bindings_arg ist env sigma (keep,c) = + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, (keep,c) + let interp_open_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in let sigma, c = interp_open_constr ist env sigma c in sigma, (c, bl) +let interp_open_constr_with_bindings_arg ist env sigma (keep,c) = + let sigma, c = interp_open_constr_with_bindings ist env sigma c in + sigma,(keep,c) + let loc_of_bindings = function | NoBindings -> Loc.ghost | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) @@ -829,22 +837,26 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in sigma, (loc,cb) +let interp_open_constr_with_bindings_arg_loc ist env sigma (keep,c) = + let sigma, c = interp_open_constr_with_bindings_loc ist env sigma c in + sigma,(keep,c) + let interp_induction_arg ist gl arg = let env = pf_env gl and sigma = project gl in match arg with - | ElimOnConstr c -> - ElimOnConstr (interp_constr_with_bindings ist env sigma c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) -> + | keep,ElimOnConstr c -> + keep,ElimOnConstr (interp_constr_with_bindings ist env sigma c) + | keep,ElimOnAnonHyp n as x -> x + | keep,ElimOnIdent (loc,id) -> let error () = user_err_loc (loc, "", strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl - then ElimOnIdent (loc,id') + then keep,ElimOnIdent (loc,id') else - (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings)) + (try keep,ElimOnConstr (sigma,(constr_of_id env id',NoBindings)) with Not_found -> user_err_loc (loc,"", pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")) @@ -862,18 +874,18 @@ let interp_induction_arg ist gl arg = let id = out_gen (topwit wit_var) v in try_cast_id id else if has_type v (topwit wit_int) then - ElimOnAnonHyp (out_gen (topwit wit_int) v) + keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> ElimOnConstr (sigma,(c,NoBindings)) + | Some c -> keep,ElimOnConstr (sigma,(c,NoBindings)) with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - ElimOnIdent (loc,id) + keep,ElimOnIdent (loc,id) else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in let (sigma,c) = interp_constr ist env sigma c in - ElimOnConstr (sigma,(c,NoBindings)) + keep,ElimOnConstr (sigma,(c,NoBindings)) (* Associates variables with values and gives the remaining variables and values *) @@ -1544,7 +1556,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, l = - List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb in let tac = match cl with | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l) @@ -1552,25 +1564,25 @@ and interp_atomic ist tac : unit Proofview.tactic = (fun l -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in - let (id,cl) = interp_in_hyp_as ist env cl in - Tactics.apply_in a ev id l cl + let (clear,id,cl) = interp_in_hyp_as ist env cl in + Tactics.apply_in a ev clear id l cl end) in Tacticals.New.tclWITHHOLES ev tac sigma l end - | TacElim (ev,cb,cbo) -> + | TacElim (ev,(keep,cb),cbo) -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in - Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo + Tacticals.New.tclWITHHOLES ev (Tactics.elim ev keep cb) sigma cbo end - | TacCase (ev,cb) -> + | TacCase (ev,(keep,cb)) -> Proofview.Goal.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in - Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb + Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev keep) sigma cb end | TacFix (idopt,n) -> Proofview.Goal.raw_enter begin fun gl -> @@ -1824,9 +1836,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> Proofview.Goal.raw_enter begin fun gl -> - let l = List.map (fun (b,m,c) -> + let l = List.map (fun (b,m,(keep,c)) -> let f env sigma = interp_open_constr_with_bindings ist env sigma c in - (b,m,f)) l in + (b,m,keep,f)) l in let env = Proofview.Goal.env gl in let cl = interp_clause ist env cl in Equality.general_multi_multi_rewrite ev l cl diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 428061463e..0ff4fe9b8a 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -44,10 +44,13 @@ let subst_bindings subst = function let subst_glob_with_bindings subst (c,bl) = (subst_glob_constr subst c, subst_bindings subst bl) +let subst_glob_with_bindings_arg subst (clear,c) = + (clear,subst_glob_with_bindings subst c) + let subst_induction_arg subst = function - | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent id as x -> x + | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c) + | clear,ElimOnAnonHyp n as x -> x + | clear,ElimOnIdent id as x -> x let subst_and_short_name f (c,n) = (* assert (n=None); *)(* since tacdef are strictly globalized *) @@ -135,11 +138,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x | TacExact c -> TacExact (subst_glob_constr subst c) | TacApply (a,ev,cb,cl) -> - TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl) + TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl) | TacElim (ev,cb,cbo) -> - TacElim (ev,subst_glob_with_bindings subst cb, + TacElim (ev,subst_glob_with_bindings_arg subst cb, Option.map (subst_glob_with_bindings subst) cbo) - | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb) + | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb) | TacFix (idopt,n) as x -> x | TacMutualFix (id,n,l) -> TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) @@ -194,7 +197,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacRewrite (ev,l,cl,by) -> TacRewrite (ev, List.map (fun (b,m,c) -> - b,m,subst_glob_with_bindings subst c) l, + b,m,subst_glob_with_bindings_arg subst c) l, cl,Option.map (subst_tactic subst) by) | TacInversion (DepInversion (k,c,l),hyp) -> TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb6894fefa..2de4e26f3f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -99,6 +99,19 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> apply_solve_class_goals:=a); } +let clear_hyp_by_default = ref false + +let use_clear_hyp_by_default () = !clear_hyp_by_default + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "default clearing of hypotheses after use"; + optkey = ["Default";"Clearing";"Used";"Hypotheses"]; + optread = (fun () -> !clear_hyp_by_default) ; + optwrite = (fun b -> clear_hyp_by_default := b) } + (*********************************************) (* Tactics *) (*********************************************) @@ -159,6 +172,16 @@ let thin l gl = with Evarutil.ClearDependencyError (id,err) -> error_clear_dependency (pf_env gl) id err +let apply_clear_request clear_flag dft c = + let check_isvar c = + if not (isVar c) then + error "keep/clear modifiers apply only to hypothesis names." in + let clear = match clear_flag with + | None -> dft && isVar c + | Some clear -> check_isvar c; clear in + if clear then Proofview.V82.tactic (thin [destVar c]) + else Tacticals.New.tclIDTAC + let internal_cut_gen b d t gl = try internal_cut b d t gl with Evarutil.ClearDependencyError (id,err) -> @@ -167,8 +190,8 @@ let internal_cut_gen b d t gl = let internal_cut = internal_cut_gen false let internal_cut_replace = internal_cut_gen true -let internal_cut_rev_gen b d t gl = - try internal_cut_rev b d t gl +let internal_cut_rev_gen b id t gl = + try internal_cut_rev b id t gl with Evarutil.ClearDependencyError (id,err) -> error_clear_dependency (pf_env gl) id err @@ -678,31 +701,36 @@ let rec intros_move = function or a term with bindings *) let onOpenInductionArg tac = function - | ElimOnConstr cbl -> - tac cbl - | ElimOnAnonHyp n -> + | clear_flag,ElimOnConstr cbl -> + tac clear_flag cbl + | clear_flag,ElimOnAnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) - (Tacticals.New.onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings)))) - | ElimOnIdent (_,id) -> + (Tacticals.New.onLastHyp + (fun c -> tac clear_flag (Evd.empty,(c,NoBindings)))) + | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (tac (Evd.empty,(mkVar id,NoBindings))) + (tac clear_flag (Evd.empty,(mkVar id,NoBindings))) let onInductionArg tac = function - | ElimOnConstr cbl -> - tac cbl - | ElimOnAnonHyp n -> - Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac (c,NoBindings))) - | ElimOnIdent (_,id) -> + | clear_flag,ElimOnConstr cbl -> + tac clear_flag cbl + | clear_flag,ElimOnAnonHyp n -> + Tacticals.New.tclTHEN + (intros_until_n n) + (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) + | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) - Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings)) + Tacticals.New.tclTHEN + (try_intros_until_id_check id) + (tac clear_flag (mkVar id,NoBindings)) let map_induction_arg f = function - | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl) - | ElimOnAnonHyp n -> ElimOnAnonHyp n - | ElimOnIdent id -> ElimOnIdent id + | clear_flag,ElimOnConstr (sigma,(c,bl)) -> clear_flag,ElimOnConstr (f (sigma,c),bl) + | clear_flag,ElimOnAnonHyp n as x -> x + | clear_flag,ElimOnIdent id as x -> x (**************************) (* Cut tactics *) @@ -782,13 +810,19 @@ let check_unresolved_evars_of_metas clenv = | _ -> ()) (meta_list clenv.evd) +let clear_of_flag flag = + match flag with + | None -> true (* default for apply in *) + | Some b -> b + (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last ones (resp [n] first ones if [sidecond_first] is [true]) being the [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl = +let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv gl = + let with_clear = clear_of_flag clear_flag in let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in let clenv = if with_classes then @@ -800,10 +834,15 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c if not with_evars && occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in + let id' = if with_clear then id else fresh_id [] id gl in + let exact_tac = refine_no_check new_hyp_prf in tclTHEN (tclEVARS clenv.evd) - ((if sidecond_first then assert_replacing else cut_replacing) - id new_hyp_typ (refine_no_check new_hyp_prf)) gl + (if sidecond_first then + tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac + else + tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac) + gl (********************************************) (* Elimination tactics *) @@ -900,16 +939,20 @@ let general_elim_clause_gen elimtac indclause elim gl = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl -let general_elim with_evars (c, lbindc) elim gl = +let general_elim with_evars clear_flag (c, lbindc) elim gl = let ct = pf_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in - general_elim_clause_gen elimtac indclause elim gl + tclTHEN + (general_elim_clause_gen elimtac indclause elim) + (Proofview.V82.of_tactic + (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) + gl (* Case analysis tactics *) -let general_case_analysis_in_context with_evars (c,lbindc) gl = +let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl = let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let sort = elimination_sort_of_goal gl in let sigma, elim = @@ -918,19 +961,21 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl = else pf_apply build_case_analysis_scheme_default gl mind sort in tclTHEN (tclEVARS sigma) - (general_elim with_evars (c,lbindc) + (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl -let general_case_analysis with_evars (c,lbindc as cx) = +let general_case_analysis with_evars clear_flag (c,lbindc as cx) = match kind_of_term c with | Var id when lbindc == NoBindings -> Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.V82.tactic (general_case_analysis_in_context with_evars cx)) + (Proofview.V82.tactic + (general_case_analysis_in_context with_evars clear_flag cx)) | _ -> - Proofview.V82.tactic (general_case_analysis_in_context with_evars cx) + Proofview.V82.tactic + (general_case_analysis_in_context with_evars clear_flag cx) -let simplest_case c = general_case_analysis false (c,NoBindings) +let simplest_case c = general_case_analysis false None (c,NoBindings) (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) @@ -951,39 +996,39 @@ let find_eliminator c gl = evd, {elimindex = None; elimbody = (c,NoBindings); elimrename = Some (true, constructors_nrealdecls ind)} -let default_elim with_evars (c,_ as cx) = +let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE (Proofview.Goal.raw_enter begin fun gl -> let evd, elim = find_eliminator c gl in Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) - (Proofview.V82.tactic (general_elim with_evars cx elim)) + (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim)) end) begin function | IsRecord -> (* For records, induction principles aren't there by default anymore. Instead, we do a case analysis instead. *) - general_case_analysis with_evars cx + general_case_analysis with_evars clear_flag cx | e -> Proofview.tclZERO e end -let elim_in_context with_evars c = function +let elim_in_context with_evars clear_flag c = function | Some elim -> Proofview.V82.tactic - (general_elim with_evars c {elimindex = Some (-1); elimbody = elim; + (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim; elimrename = None}) - | None -> default_elim with_evars c + | None -> default_elim with_evars clear_flag c -let elim with_evars (c,lbindc as cx) elim = +let elim with_evars clear_flag (c,lbindc as cx) elim = match kind_of_term c with | Var id when lbindc == NoBindings -> Tacticals.New.tclTHEN (try_intros_until_id_check id) - (elim_in_context with_evars cx elim) + (elim_in_context with_evars clear_flag cx elim) | _ -> - elim_in_context with_evars cx elim + elim_in_context with_evars clear_flag cx elim (* The simplest elimination tactic, with no substitutions at all. *) -let simplest_elim c = default_elim false (c,NoBindings) +let simplest_elim c = default_elim false None (c,NoBindings) (* Elimination in hypothesis *) (* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y) @@ -1019,7 +1064,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i ( if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" (str "Nothing to rewrite in " ++ pr_id id ++ str"."); - clenv_refine_in with_evars id elimclause'' gl + clenv_refine_in with_evars None id elimclause'' gl let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1117,7 +1162,7 @@ let solve_remaining_apply_goals gl = with Not_found -> tclIDTAC gl else tclIDTAC gl -let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = +let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 = let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the @@ -1153,21 +1198,26 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = Loc.raise loc exn in try_red_apply thm_ty0 in - tclTHEN (try_main_apply with_destruct c) solve_remaining_apply_goals gl0 + tclTHENLIST [ + try_main_apply with_destruct c; + solve_remaining_apply_goals; + Proofview.V82.of_tactic + (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) + ] gl0 let rec apply_with_bindings_gen b e = function | [] -> tclIDTAC - | [cb] -> general_apply b b e cb - | cb::cbl -> - tclTHENLAST (general_apply b b e cb) (apply_with_bindings_gen b e cbl) + | [k,cb] -> general_apply b b e k cb + | (k,cb)::cbl -> + tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl) -let apply_with_bindings cb = apply_with_bindings_gen false false [dloc,cb] +let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)] -let eapply_with_bindings cb = apply_with_bindings_gen false true [dloc,cb] +let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)] -let apply c = apply_with_bindings_gen false false [dloc,(c,NoBindings)] +let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))] -let eapply c = apply_with_bindings_gen false true [dloc,(c,NoBindings)] +let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))] let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1212,15 +1262,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl = in aux (pf_apply make_clenv_binding gl (d,thm) lbind) -let apply_in_once sidecond_first with_delta with_destruct with_evars id - (loc,(d,lbind)) gl0 = +let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag + id (clear_flag,(loc,(d,lbind))) gl0 = let flags = if with_delta then elim_flags () else elim_no_delta_flags () in let t' = pf_get_hyp_typ gl0 id in let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in let rec aux with_destruct c gl = try let clause = apply_in_once_main flags innerclause (c,lbind) gl in - clenv_refine_in ~sidecond_first with_evars id clause gl + tclTHEN + (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause) + (Proofview.V82.of_tactic + (apply_clear_request clear_flag false c)) + gl with e when with_destruct -> let e = Errors.push e in descend_in_conjunctions aux (fun _ -> raise e) c gl @@ -1435,7 +1489,7 @@ let constructor_tac with_evars expctdnumopt i lbind = (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in let cons = mkConstructU cons in - let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in + let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in (Tacticals.New.tclTHENLIST [Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac]) end @@ -1770,23 +1824,23 @@ let tclMAPFIRST tacfun l = List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT()) let general_apply_in sidecond_first with_delta with_destruct with_evars - id lemmas ipat = + with_clear id lemmas ipat = if sidecond_first then (* Skip the side conditions of the applied lemma *) Tacticals.New.tclTHENLAST (tclMAPLAST - (apply_in_once sidecond_first with_delta with_destruct with_evars id) + (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id) lemmas) (as_tac id ipat) else Tacticals.New.tclTHENFIRST (tclMAPFIRST - (apply_in_once sidecond_first with_delta with_destruct with_evars id) + (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id) lemmas) (as_tac id ipat) -let apply_in simple with_evars id lemmas ipat = - general_apply_in false simple simple with_evars id lemmas ipat +let apply_in simple with_evars clear_flag id lemmas ipat = + general_apply_in false simple simple with_evars clear_flag id lemmas ipat (*****************************) (* Tactics abstracting terms *) @@ -3283,7 +3337,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl = let elimc = mkCast (elimc, DEFAULTcast, elimt) in elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl -let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names +let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names inhyps = Proofview.Goal.enter begin fun gl -> let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in @@ -3295,18 +3349,19 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [ induction_tac with_evars elim (hyp0,lbind) typ0; tclTRY (unfold_body hyp0); - thin [hyp0] + Proofview.V82.of_tactic + (apply_clear_request clear_flag true (mkVar hyp0)) ]) in apply_induction_in_context (Some (hyp0,inhyps)) elim indvars names induct_tac end -let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps = +let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names (hyp0,lbind) inhyps = Proofview.Goal.enter begin fun gl -> let sigma, elim_info = find_induction_type isrec elim hyp0 gl in Tacticals.New.tclTHENLIST [Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0); - (induction_from_context isrec with_evars elim_info + (induction_from_context clear_flag isrec with_evars elim_info (hyp0,lbind) names inhyps)] end @@ -3358,7 +3413,7 @@ let clear_unselected_context id inhyps cls gl = thin ids gl | None -> tclIDTAC gl -let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = +let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in @@ -3369,7 +3424,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = Tacticals.New.tclTHEN (Proofview.V82.tactic (clear_unselected_context id inhyps cls)) (induction_with_atomization_of_ind_arg - isrec with_evars elim names (id,lbind) inhyps) + clear_flag isrec with_evars elim names (id,lbind) inhyps) | _ -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -3385,7 +3440,8 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = (letin_tac_gen with_eq (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None) (induction_with_atomization_of_ind_arg - isrec with_evars elim names (id,lbind) inhyps) + (Some true) + isrec with_evars elim names (id,lbind) inhyps) end end @@ -3447,7 +3503,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) = if Int.equal (List.length lc) 1 && not ifi then (* standard induction *) onOpenInductionArg - (fun c -> induction_gen isrec with_evars elim names c cls) + (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim names c cls) (List.hd lc) else begin (* functional induction *) @@ -3467,7 +3523,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) = (* Hook to recover standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) onInductionArg - (fun (c,lbind) -> + (fun _clear_flag (c,lbind) -> if lbind != NoBindings then error "'with' clause not supported here."; induction_gen_l isrec with_evars elim names [c]) (List.hd lc) @@ -3475,7 +3531,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) = let newlc = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) - | ElimOnConstr (x,NoBindings) -> x + | _clear_flag,ElimOnConstr (x,NoBindings) -> x | _ -> error "Don't know where to find some argument.") lc in induction_gen_l isrec with_evars elim names newlc @@ -3910,10 +3966,15 @@ module Simple = struct generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous)) cl) - let apply c = apply_with_bindings_gen false false [Loc.ghost,(c,NoBindings)] - let eapply c = apply_with_bindings_gen false true [Loc.ghost,(c,NoBindings)] - let elim c = elim false (c,NoBindings) None - let case c = general_case_analysis false (c,NoBindings) + let apply c = + apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))] + let eapply c = + apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))] + let elim c = elim false None (c,NoBindings) None + let case c = general_case_analysis false None (c,NoBindings) + + let apply_in id c = + apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c2403d97a8..f58e218bec 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -93,9 +93,13 @@ val try_intros_until : or a term with bindings *) val onInductionArg : - (constr with_bindings -> unit Proofview.tactic) -> + (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings induction_arg -> unit Proofview.tactic +(** Tell if a used hypothesis should be cleared by default or not *) + +val use_clear_hyp_by_default : unit -> bool + (** {6 Introduction tactics with eliminations. } *) val intro_pattern : Id.t move_location -> intro_pattern_expr -> unit Proofview.tactic @@ -157,6 +161,7 @@ val unfold_constr : global_reference -> tactic val clear : Id.t list -> tactic val clear_body : Id.t list -> tactic val keep : Id.t list -> tactic +val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> tactic @@ -174,7 +179,7 @@ val apply : constr -> tactic val eapply : constr -> tactic val apply_with_bindings_gen : - advanced_flag -> evars_flag -> constr with_bindings located list -> tactic + advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic @@ -182,8 +187,8 @@ val eapply_with_bindings : constr with_bindings -> tactic val cut_and_apply : constr -> unit Proofview.tactic val apply_in : - advanced_flag -> evars_flag -> Id.t -> - constr with_bindings located list -> + advanced_flag -> evars_flag -> clear_flag -> Id.t -> + (clear_flag * constr with_bindings located) list -> intro_pattern_expr located option -> unit Proofview.tactic (** {6 Elimination tactics. } *) @@ -245,16 +250,17 @@ type eliminator = { elimbody : constr with_bindings } -val general_elim : evars_flag -> +val general_elim : evars_flag -> clear_flag -> constr with_bindings -> eliminator -> tactic val general_elim_clause : evars_flag -> unify_flags -> identifier option -> clausenv -> eliminator -> unit Proofview.tactic -val default_elim : evars_flag -> constr with_bindings -> unit Proofview.tactic +val default_elim : evars_flag -> clear_flag -> constr with_bindings -> + unit Proofview.tactic val simplest_elim : constr -> unit Proofview.tactic val elim : - evars_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic + evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic val simple_induct : quantified_hypothesis -> unit Proofview.tactic @@ -266,7 +272,7 @@ val induction : evars_flag -> (** {6 Case analysis tactics. } *) -val general_case_analysis : evars_flag -> constr with_bindings -> unit Proofview.tactic +val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val simplest_case : constr -> unit Proofview.tactic val simple_destruct : quantified_hypothesis -> unit Proofview.tactic @@ -384,6 +390,7 @@ module Simple : sig val eapply : constr -> tactic val elim : constr -> unit Proofview.tactic val case : constr -> unit Proofview.tactic + val apply_in : identifier -> constr -> unit Proofview.tactic end -- cgit v1.2.3