diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 75 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 |
2 files changed, 56 insertions, 21 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index db7d2e4a13..1d3239ef68 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -72,11 +72,26 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "injection left-to-right pattern order"; + optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; optkey = ["Injection";"L2R";"Pattern";"Order"]; optread = (fun () -> !injection_pattern_l2r_order) ; optwrite = (fun b -> injection_pattern_l2r_order := b) } +let injection_in_context = ref false + +let use_injection_in_context () = + !injection_in_context + && Flags.version_strictly_greater Flags.V8_5 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "injection in context"; + optkey = ["Structural";"Injection"]; + optread = (fun () -> !injection_in_context) ; + optwrite = (fun b -> injection_in_context := b) } + (* Rewriting tactics *) let tclNOTSAMEGOAL tac = @@ -1381,27 +1396,41 @@ 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 use_clear_hyp_by_default () = false - -let postInjEqTac with_evars clear_flag ipats c n = - match ipats with - | Some ipats -> - let clear_tac = - 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 intro_patterns_bound_to with_evars n MoveLast ipats - else intro_patterns_to with_evars MoveLast ipats in - tclTHEN clear_tac intro_tac - | None -> apply_clear_request clear_flag false c - -let injEq with_evars clear_flag ipats = - let l2r = - if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false +let get_previous_hyp_position id gl = + let rec aux dest = function + | [] -> raise (RefinerError (NoSuchHyp id)) + | d :: right -> + let hyp = Context.Named.Declaration.get_id d in + if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r + aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + +let injEq ?(old=false) with_evars clear_flag ipats = + (* Decide which compatibility mode to use *) + let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with + | None when not old && use_injection_in_context () -> + Some [], true, true, true + | None -> None, false, false, false + | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in + (* Built the post tactic depending on compatibility mode *) + let post_tac c n = + match ipats_style with + | Some ipats -> + Proofview.Goal.enter { enter = begin fun gl -> + let destopt = match kind_of_term c with + | Var id -> get_previous_hyp_position id gl + | _ -> MoveLast in + let clear_tac = + tclTRY (apply_clear_request clear_flag dft_clear_flag c) in + (* Try should be removal if dependency were treated *) + let intro_tac = + if bounded_intro + then intro_patterns_bound_to with_evars n destopt ipats + else intro_patterns_to with_evars destopt ipats in + tclTHEN clear_tac intro_tac + end } + | None -> tclIDTAC in + injEqThen post_tac l2r let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats) @@ -1409,6 +1438,10 @@ let injClause ipats with_evars = function | None -> onNegatedEquality with_evars (injEq with_evars None ipats) | Some c -> onInductionArg (inj ipats with_evars) c +let simpleInjClause with_evars = function + | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c + let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id))) diff --git a/tactics/equality.mli b/tactics/equality.mli index 1122615c3d..47cb6b82fd 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -79,6 +79,8 @@ val injClause : intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val injHyp : clear_flag -> Id.t -> unit Proofview.tactic val injConcl : unit Proofview.tactic +val simpleInjClause : evars_flag -> + constr with_bindings destruction_arg option -> unit Proofview.tactic val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic |