diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_interp.ml | 4 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 90 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.mli | 2 |
3 files changed, 42 insertions, 54 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index beda24629..209d5f52f 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -149,8 +149,8 @@ let decompose_eq env id = let get_eq_typ info env = let last_id = match info.pm_last with - Anonymous -> error "no previous equality" - | Name id -> id in + None -> error "no previous equality" + | Some (id,_) -> id in let typ = decompose_eq env last_id in typ diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 4ac92fbae..3bb641165 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -92,18 +92,27 @@ let mk_evd metalist gls = let add_one (meta,typ) evd = meta_declare meta typ evd in List.fold_right add_one metalist evd0 + +let set_last cpl gls = + let info = get_its_info gls in + tclTHEN + begin + match info.pm_last with + Some (lid,false) -> tclTRY (clear [lid]) + | _ -> tclIDTAC + end + begin + tcl_change_info + {info with + pm_last=Some cpl } + end gls (* start a proof *) let start_proof_tac gls= let gl=sig_it gls in - let info={pm_last=Anonymous; + let info={pm_last=None; pm_partial_goal=mkMeta 1; - pm_hyps= - begin - let hyps = pf_ids_of_hyps gls in - List.fold_right Idset.add hyps Idset.empty - end; pm_subgoals= [1,gl.evar_concl]; pm_stack=[]} in {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, @@ -459,8 +468,8 @@ let instr_cut mkstat _thus _then cut gls0 = let items_ = if _then then match info.pm_last with - Anonymous -> error "no previous statement to use" - | Name id -> (mkVar id)::items + None -> error "no previous statement to use" + | Some (id,_) -> (mkVar id)::items else items in prepare_goal items_ gls in let method_tac gls = @@ -471,19 +480,18 @@ let instr_cut mkstat _thus _then cut gls0 = (Tacinterp.eval_tactic tac) gls in let just_tac gls = justification (tclTHEN items_tac method_tac) gls in - let c_id = match cut.cut_stat.st_label with + let (c_id,_) as cpl = match cut.cut_stat.st_label with Anonymous -> - pf_get_new_id (id_of_string "_fact") gls0 - | Name id -> id in + pf_get_new_id (id_of_string "_fact") gls0,false + | Name id -> id,true in let c_stat = mkstat info cut.cut_stat.st_it in let thus_tac gls= if _thus then thus_tac (mkVar c_id) c_stat gls else tclIDTAC gls in - let ninfo = {info with pm_last=Name c_id} in tclTHENS (internal_cut c_id c_stat) [tclTHEN tcl_erase_info just_tac; - tclTHEN (tcl_change_info ninfo) thus_tac] gls0 + tclTHEN (set_last cpl) thus_tac] gls0 (* iterated equality *) let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) @@ -504,8 +512,8 @@ let instr_rew _thus rew_side cut gls0 = let info = get_its_info gls0 in let last_id = match info.pm_last with - Anonymous -> error "no previous equality" - | Name id -> id in + None -> error "no previous equality" + | Some (id,_) -> id in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -519,11 +527,10 @@ let instr_rew _thus rew_side cut gls0 = (Tacinterp.eval_tactic tac) gls in let just_tac gls = justification (tclTHEN items_tac method_tac) gls in - let c_id = match cut.cut_stat.st_label with + let (c_id,_) as cpl = match cut.cut_stat.st_label with Anonymous -> - pf_get_new_id (id_of_string "_eq") gls0 - | Name id -> id in - let ninfo = {info with pm_last=Name c_id} in + pf_get_new_id (id_of_string "_eq") gls0,false + | Name id -> id,true in let thus_tac new_eq gls= if _thus then thus_tac (mkVar c_id) new_eq gls @@ -535,14 +542,14 @@ let instr_rew _thus rew_side cut gls0 = [tclTHEN tcl_erase_info (tclTHENS (transitivity lhs) [just_tac;exact_check (mkVar last_id)]); - tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + tclTHEN (set_last cpl) (thus_tac new_eq)] gls0 | Rhs -> let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in tclTHENS (internal_cut c_id new_eq) [tclTHEN tcl_erase_info (tclTHENS (transitivity rhs) [exact_check (mkVar last_id);just_tac]); - tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + tclTHEN (set_last cpl) (thus_tac new_eq)] gls0 @@ -550,9 +557,9 @@ let instr_rew _thus rew_side cut gls0 = let instr_claim _thus st gls0 = let info = get_its_info gls0 in - let id = match st.st_label with - Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 - | Name id -> id in + let (id,_) as cpl = match st.st_label with + Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false + | Name id -> id,true in let thus_tac gls= if _thus then thus_tac (mkVar id) st.st_it gls @@ -562,10 +569,9 @@ let instr_claim _thus st gls0 = (if _thus then Focus_claim else Claim)::info.pm_stack; pm_partial_goal=mkMeta 1; pm_subgoals = [1,st.st_it]} in - let ninfo2 = {info with pm_last=Name id} in tclTHENS (internal_cut id st.st_it) [tcl_change_info ninfo1; - tclTHEN (tcl_change_info ninfo2) thus_tac] gls0 + tclTHEN (set_last cpl) thus_tac] gls0 (* tactics for assume *) @@ -576,11 +582,6 @@ let reset_concl gls = pm_partial_goal=mkMeta 1; pm_subgoals= [1,gls.it.evar_concl]} gls -let set_last id gls = - let info = get_its_info gls in - tcl_change_info - {info with - pm_last=Name id} gls let intro_pm id gls= let info = get_its_info gls in @@ -590,20 +591,14 @@ let intro_pm id gls= | _ -> error "Goal is split" let push_intro_tac coerce nam gls = - let hid = + let (hid,_) as cpl = match nam with - Anonymous -> pf_get_new_id (id_of_string "_hyp") gls - | Name id -> id in - let mark_id gls0 = - let info = get_its_info gls0 in - let ninfo = {info with - pm_last = Name hid; - pm_hyps = Idset.add hid info.pm_hyps } in - tcl_change_info ninfo gls0 in + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false + | Name id -> id,true in tclTHENLIST [intro_pm hid; coerce hid; - mark_id] + set_last cpl] gls let assume_tac hyps gls = @@ -695,14 +690,7 @@ let pm_rename_hyp id hid gls = let rec consider_match may_intro introduced available expected gls = match available,expected with [],[] -> - if not may_intro then set_last (List.hd introduced) gls - else - let info = get_its_info gls in - let nameset=List.fold_right Idset.add introduced info.pm_hyps in - tcl_change_info {info with - pm_last = Name (List.hd introduced); - pm_hyps = nameset} gls | _,[] -> error "last statements do not match a complete hypothesis" (* should tell which ones *) | [],hyps -> @@ -715,7 +703,7 @@ let rec consider_match may_intro introduced available expected gls = (fun _ -> error "not enough sub-hypotheses to match statements") gls - end + end else error "not enough sub-hypotheses to match statements" (* should tell which ones *) @@ -724,11 +712,11 @@ let rec consider_match may_intro introduced available expected gls = begin match st.st_label with Anonymous -> - consider_match may_intro (id::introduced) rest_ids rest + consider_match may_intro ((id,false)::introduced) rest_ids rest | Name hid -> tclTHENLIST [pm_rename_hyp id hid; - consider_match may_intro (hid::introduced) rest_ids rest] + consider_match may_intro ((hid,true)::introduced) rest_ids rest] end begin (fun gls -> diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index ba8dc7b66..0d51cf979 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -112,7 +112,7 @@ val hrec_for: val consider_match : bool -> - Names.Idset.elt list -> + (Names.Idset.elt*bool) list -> Names.Idset.elt list -> (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> Proof_type.tactic |