diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 45 | ||||
| -rw-r--r-- | tactics/equality.mli | 8 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 8 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 27 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 54 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 17 | ||||
| -rw-r--r-- | tactics/tactics.ml | 203 | ||||
| -rw-r--r-- | tactics/tactics.mli | 23 |
10 files changed, 251 insertions, 144 deletions
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 |