diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 839 |
1 files changed, 410 insertions, 429 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 67d1d41a..9c58f06e 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *) +(* $Id$ *) open Util open Pp @@ -28,6 +28,7 @@ open Tactics open Tacticals open Term open Termops +open Namegen open Reductionops open Goptions @@ -36,27 +37,27 @@ open Goptions let get_its_info gls = get_info gls.it -let get_strictness,set_strictness = +let get_strictness,set_strictness = let strictness = ref false in (fun () -> (!strictness)),(fun b -> strictness:=b) let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "strict mode"; - optkey = (SecondaryTable ("Strict","Proofs")); + optkey = ["Strict";"Proofs"]; optread = get_strictness; optwrite = set_strictness } -let tcl_change_info_gen info_gen = +let tcl_change_info_gen info_gen = (fun gls -> - let gl =sig_it gls in - {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, - function + let gl =sig_it gls in + {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, + function [pftree] -> {pftree with goal=gl; - ref=Some (Prim Change_evars,[pftree])} + ref=Some (Prim Change_evars,[pftree])} | _ -> anomaly "change_info : Wrong number of subtrees") let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls @@ -78,27 +79,27 @@ let is_good_inductive env ind = let check_not_per pts = if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then match get_stack pts with - Per (_,_,_,_)::_ -> + Per (_,_,_,_)::_ -> error "You are inside a proof per cases/induction.\n\ Please \"suppose\" something or \"end\" it now." | _ -> () let mk_evd metalist gls = let evd0= create_goal_evar_defs (sig_sig gls) in - let add_one (meta,typ) evd = + let add_one (meta,typ) evd = meta_declare meta typ evd in List.fold_right add_one metalist evd0 -let is_tmp id = (string_of_id id).[0] = '_' +let is_tmp id = (string_of_id id).[0] = '_' -let tmp_ids gls = +let tmp_ids gls = let ctx = pf_hyps gls in - match ctx with + match ctx with [] -> [] - | _::q -> List.filter is_tmp (ids_of_named_context q) + | _::q -> List.filter is_tmp (ids_of_named_context q) -let clean_tmp gls = - let clean_id id0 gls0 = +let clean_tmp gls = + let clean_id id0 gls0 = tclTRY (clear [id0]) gls0 in let rec clean_all = function [] -> tclIDTAC @@ -114,30 +115,30 @@ let assert_postpone id t = let start_proof_tac gls= let gl=sig_it gls in let info={pm_stack=[]} in - {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, - function + {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, + function [pftree] -> {pftree with goal=gl; - ref=Some (Decl_proof true,[pftree])} + ref=Some (Decl_proof true,[pftree])} | _ -> anomaly "Dem : Wrong number of subtrees" -let go_to_proof_mode () = - Pfedit.mutate +let go_to_proof_mode () = + Pfedit.mutate (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts)) (* closing gaps *) let daimon_tac gls = set_daimon_flag (); - ({it=[];sigma=sig_sig gls}, - function + ({it=[];sigma=sig_sig gls}, + function [] -> {open_subgoals=0; goal=sig_it gls; - ref=Some (Daimon,[])} + ref=Some (Daimon,[])} | _ -> anomaly "Daimon: Wrong number of subtrees") - + let daimon _ pftree = set_daimon_flag (); {pftree with @@ -150,7 +151,7 @@ let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon ) let rec is_focussing_instr = function Pthus i | Pthen i | Phence i -> is_focussing_instr i - | Pescape | Pper _ | Pclaim _ | Pfocus _ + | Pescape | Pper _ | Pclaim _ | Pfocus _ | Psuppose _ | Pcase (_,_,_) -> true | _ -> false @@ -158,7 +159,7 @@ let mark_rule_as_done = function Decl_proof true -> Decl_proof false | Decl_proof false -> anomaly "already marked as done" - | Nested(Proof_instr (lock_focus,instr),spfl) -> + | Nested(Proof_instr (lock_focus,instr),spfl) -> if lock_focus then Nested(Proof_instr (false,instr),spfl) else @@ -168,34 +169,34 @@ let mark_rule_as_done = function let mark_proof_tree_as_done pt = match pt.ref with None -> anomaly "mark_proof_tree_as_done" - | Some (r,spfl) -> + | Some (r,spfl) -> {pt with ref= Some (mark_rule_as_done r,spfl)} -let mark_as_done pts = - map_pftreestate - (fun _ -> mark_proof_tree_as_done) - (up_to_matching_rule is_focussing_command pts) +let mark_as_done pts = + map_pftreestate + (fun _ -> mark_proof_tree_as_done) + (up_to_matching_rule is_focussing_command pts) (* post-instruction focus management *) let goto_current_focus pts = up_until_matching_rule is_focussing_command pts -let goto_current_focus_or_top pts = - try +let goto_current_focus_or_top pts = + try up_until_matching_rule is_focussing_command pts with Not_found -> top_of_tree pts (* return *) let close_tactic_mode pts = - let pts1= - try goto_current_focus pts - with Not_found -> + let pts1= + try goto_current_focus pts + with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." in let pts2 = daimon_subtree pts1 in - let pts3 = mark_as_done pts2 in - goto_current_focus pts3 - + let pts3 = mark_as_done pts2 in + goto_current_focus pts3 + let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode (* end proof/claim *) @@ -207,11 +208,11 @@ let close_block bt pts = else get_stack pts in match bt,stack with - B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> + B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> daimon_subtree (goto_current_focus pts) - | _, Claim::_ -> + | _, Claim::_ -> error "\"end claim\" expected." - | _, Focus_claim::_ -> + | _, Focus_claim::_ -> error "\"end focus\" expected." | _, [] -> error "\"end proof\" expected." @@ -225,18 +226,18 @@ let close_block bt pts = (* utility for suppose / suppose it is *) -let close_previous_case pts = - if - Proof_trees.is_complete_proof (proof_of_pftreestate pts) +let close_previous_case pts = + if + Proof_trees.is_complete_proof (proof_of_pftreestate pts) then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." - | Suppose_case :: Per (et,_,_,_) :: _ -> + Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus (mark_as_done pts) - | _ -> error "Not inside a proof per cases or induction." + | _ -> error "Not inside a proof per cases or induction." else match get_stack pts with - Per (et,_,_,_) :: _ -> pts + Per (et,_,_,_) :: _ -> pts | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus (mark_as_done (daimon_subtree pts)) | _ -> error "Not inside a proof per cases or induction." @@ -246,10 +247,10 @@ let close_previous_case pts = (* automation *) let filter_hyps f gls = - let filter_aux (id,_,_) = - if f id then + let filter_aux (id,_,_) = + if f id then tclIDTAC - else + else tclTRY (clear [id]) in tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls @@ -257,16 +258,16 @@ let local_hyp_prefix = id_of_string "___" let add_justification_hyps keep items gls = let add_aux c gls= - match kind_of_term c with - Var id -> + match kind_of_term c with + Var id -> keep:=Idset.add id !keep; - tclIDTAC gls - | _ -> - let id=pf_get_new_id local_hyp_prefix gls in - keep:=Idset.add id !keep; + tclIDTAC gls + | _ -> + let id=pf_get_new_id local_hyp_prefix gls in + keep:=Idset.add id !keep; tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) - (thin_body [id]) gls in - tclMAP add_aux items gls + (thin_body [id]) gls in + tclMAP add_aux items gls let prepare_goal items gls = let tokeep = ref Idset.empty in @@ -275,18 +276,18 @@ let prepare_goal items gls = [ (fun _ -> auxres); filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls -let my_automation_tac = ref +let my_automation_tac = ref (fun gls -> anomaly "No automation registered") let register_automation_tac tac = my_automation_tac:= tac let automation_tac gls = !my_automation_tac gls -let justification tac gls= - tclORELSE - (tclSOLVE [tclTHEN tac assumption]) - (fun gls -> - if get_strictness () then +let justification tac gls= + tclORELSE + (tclSOLVE [tclTHEN tac assumption]) + (fun gls -> + if get_strictness () then error "Insufficient justification." else begin @@ -326,7 +327,7 @@ type stackd_elt = se_type:types; se_last_meta:metavariable; se_meta_list:(metavariable*types) list; - se_evd: evar_defs} + se_evd: evar_map} let rec replace_in_list m l = function [] -> raise Not_found @@ -340,44 +341,44 @@ let enstack_subsubgoals env se stack gls= Inductive.lookup_mind_specif env ind in let gentypes= Inductive.arities_of_constructors ind (mib,oib) in - let process i gentyp = - let constructor = mkConstruct(ind,succ i) + let process i gentyp = + let constructor = mkConstruct(ind,succ i) (* constructors numbering*) in let appterm = applist (constructor,params) in let apptype = Term.prod_applist gentyp params in let rc,_ = Reduction.dest_prod env apptype in - let rec meta_aux last lenv = function + let rec meta_aux last lenv = function [] -> (last,lenv,[]) | (nam,_,typ)::q -> let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in - let (nlast,holes,nmetas) = + let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in - let evd = meta_assign se.se_meta + let evd = meta_assign se.se_meta (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in - let ncreated = replace_in_list + let ncreated = replace_in_list se.se_meta nmetas se.se_meta_list in - let evd0 = List.fold_left - (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in - List.iter (fun (m,typ) -> - Stack.push + let evd0 = List.fold_left + (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in + List.iter (fun (m,typ) -> + Stack.push {se_meta=m; se_type=typ; se_evd=evd0; se_meta_list=ncreated; - se_last_meta=nlast} stack) (List.rev nmetas) + se_last_meta=nlast} stack) (List.rev nmetas) in Array.iteri process gentypes | _ -> () -let rec nf_list evd = +let rec nf_list evd = function - [] -> [] - | (m,typ)::others -> - if meta_defined evd m then + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then nf_list evd others else (m,nf_meta evd typ)::nf_list evd others @@ -387,29 +388,29 @@ let find_subsubgoal c ctyp skip submetas gls = let concl = pf_concl gls in let evd = mk_evd ((0,concl)::submetas) gls in let stack = Stack.create () in - let max_meta = + let max_meta = List.fold_left (fun a (m,_) -> max a m) 0 submetas in - let _ = Stack.push + let _ = Stack.push {se_meta=0; se_type=concl; se_last_meta=max_meta; se_meta_list=[0,concl]; se_evd=evd} stack in - let rec dfs n = + let rec dfs n = let se = Stack.pop stack in - try - let unifier = - Unification.w_unify true env Reduction.CUMUL + try + let unifier = + Unification.w_unify true env Reduction.CUMUL ctyp se.se_type se.se_evd in - if n <= 0 then - {se with + if n <= 0 then + {se with se_evd=meta_assign se.se_meta (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier; - se_meta_list=replace_in_list + se_meta_list=replace_in_list se.se_meta submetas se.se_meta_list} else dfs (pred n) - with _ -> + with _ -> begin enstack_subsubgoals env se stack gls; dfs n @@ -421,20 +422,20 @@ let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.sort_of env evd concl) in + let sort = family_of_sort (Typing.sort_of env evd concl) in let rec aux env avoid subst = function [] -> anomaly "concl_refiner: cannot happen" | (n,typ)::rest -> - let _A = subst_meta subst typ in - let x = id_of_name_using_hdchar env _A Anonymous in + let _A = subst_meta subst typ in + let x = id_of_name_using_hdchar env _A Anonymous in let _x = fresh_id avoid x gls in let nenv = Environ.push_named (_x,None,_A) env in let asort = family_of_sort (Typing.sort_of nenv evd _A) in let nsubst = (n,mkVar _x)::subst in - if rest = [] then + if rest = [] then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) else - let bsort,_B,nbody = + let bsort,_B,nbody = aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in let body = mkNamedLambda _x _A nbody in if occur_term (mkVar _x) _B then @@ -450,7 +451,7 @@ let concl_refiner metas body gls = let _P0 = mkLambda(Anonymous,_AxB,concl) in InType,_AxB, mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|]) - | _,_ -> + | _,_ -> let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in let _P0 = mkLambda(Anonymous,_AxB,concl) in InType,_AxB, @@ -473,26 +474,23 @@ let concl_refiner metas body gls = let (_,_,prf) = aux env [] [] metas in mkApp(prf,[|mkMeta 1|]) -let thus_tac c ctyp submetas gls = - let list,proof = +let thus_tac c ctyp submetas gls = + let list,proof = try find_subsubgoal c ctyp 0 submetas gls - with Not_found -> + with Not_found -> error "I could not relate this statement to the thesis." in if list = [] then - exact_check proof gls + exact_check proof gls else let refiner = concl_refiner list proof gls in Tactics.refine refiner gls (* general forward step *) - -let anon_id_base = id_of_string "__" - -let mk_stat_or_thesis info gls = function +let mk_stat_or_thesis info gls = function This c -> c - | Thesis (For _ ) -> + | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> pf_concl gls @@ -500,34 +498,34 @@ let just_tac _then cut info gls0 = let items_tac gls = match cut.cut_by with None -> tclIDTAC gls - | Some items -> - let items_ = - if _then then + | Some items -> + let items_ = + if _then then let last_id = get_last (pf_env gls) in (mkVar last_id)::items - else items + else items in prepare_goal items_ gls in - let method_tac gls = + let method_tac gls = match cut.cut_using with - None -> + None -> automation_tac gls - | Some tac -> + | Some tac -> (Tacinterp.eval_tactic tac) gls in justification (tclTHEN items_tac method_tac) gls0 - -let instr_cut mkstat _thus _then cut gls0 = - let info = get_its_info gls0 in + +let instr_cut mkstat _thus _then cut gls0 = + let info = get_its_info gls0 in let stat = cut.cut_stat in - let (c_id,_) = match stat.st_label with - Anonymous -> - pf_get_new_id (id_of_string "_fact") gls0,false + let (c_id,_) = match stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_fact") gls0,false | Name id -> id,true in let c_stat = mkstat info gls0 stat.st_it in - let thus_tac gls= - if _thus then + let thus_tac gls= + if _thus then thus_tac (mkVar c_id) c_stat [] gls else tclIDTAC gls in - tclTHENS (assert_postpone c_id c_stat) + tclTHENS (assert_postpone c_id c_stat) [tclTHEN tcl_erase_info (just_tac _then cut info); thus_tac] gls0 @@ -541,162 +539,162 @@ let decompose_eq id gls = let whd = (special_whd gls typ) in match kind_of_term whd with App (f,args)-> - if eq_constr f _eq && (Array.length args)=3 + if eq_constr f _eq && (Array.length args)=3 then (args.(0), - args.(1), - args.(2)) + args.(1), + args.(2)) else error "Previous step is not an equality." | _ -> error "Previous step is not an equality." - -let instr_rew _thus rew_side cut gls0 = - let last_id = + +let instr_rew _thus rew_side cut gls0 = + let last_id = try get_last (pf_env gls0) with _ -> error "No previous equality." in - let typ,lhs,rhs = decompose_eq last_id gls0 in + let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with None -> tclIDTAC gls | Some items -> prepare_goal items gls in - let method_tac gls = + let method_tac gls = match cut.cut_using with - None -> + None -> automation_tac gls - | Some tac -> + | Some tac -> (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 - Anonymous -> - pf_get_new_id (id_of_string "_eq") gls0,false + let (c_id,_) = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_eq") gls0,false | Name id -> id,true in - let thus_tac new_eq gls= - if _thus then + let thus_tac new_eq gls= + if _thus then thus_tac (mkVar c_id) new_eq [] gls else tclIDTAC gls in - match rew_side with + match rew_side with Lhs -> let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in - tclTHENS (assert_postpone c_id new_eq) - [tclTHEN tcl_erase_info - (tclTHENS (transitivity lhs) + tclTHENS (assert_postpone c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity lhs) [just_tac;exact_check (mkVar last_id)]); thus_tac new_eq] gls0 | Rhs -> let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in - tclTHENS (assert_postpone c_id new_eq) - [tclTHEN tcl_erase_info - (tclTHENS (transitivity rhs) + tclTHENS (assert_postpone c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity rhs) [exact_check (mkVar last_id);just_tac]); thus_tac new_eq] gls0 - + (* tactics for claim/focus *) -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,false +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,false | Name id -> id,true in - let thus_tac gls= - if _thus then + let thus_tac gls= + if _thus then thus_tac (mkVar id) st.st_it [] gls else tclIDTAC gls in let ninfo1 = {pm_stack= (if _thus then Focus_claim else Claim)::info.pm_stack} in - tclTHENS (assert_postpone id st.st_it) + tclTHENS (assert_postpone id st.st_it) [tcl_change_info ninfo1; thus_tac] gls0 (* tactics for assume *) -let push_intro_tac coerce nam gls = +let push_intro_tac coerce nam gls = let (hid,_) = - match nam with - Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false + match nam with + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false | Name id -> id,true in - tclTHENLIST + tclTHENLIST [intro_mustbe_force hid; coerce hid] - gls - -let assume_tac hyps gls = - List.fold_right - (fun (Hvar st | Hprop st) -> - tclTHEN - (push_intro_tac - (fun id -> + gls + +let assume_tac hyps gls = + List.fold_right + (fun (Hvar st | Hprop st) -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) - hyps tclIDTAC gls - -let assume_hyps_or_theses hyps gls = - List.fold_right - (function - (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> - tclTHEN - (push_intro_tac - (fun id -> + hyps tclIDTAC gls + +let assume_hyps_or_theses hyps gls = + List.fold_right + (function + (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,c)) nam) - | Hprop {st_label=nam;st_it=Thesis (tk)} -> - tclTHEN - (push_intro_tac + | Hprop {st_label=nam;st_it=Thesis (tk)} -> + tclTHEN + (push_intro_tac (fun id -> tclIDTAC) nam)) - hyps tclIDTAC gls + hyps tclIDTAC gls -let assume_st hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac +let assume_st hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) - hyps tclIDTAC gls - -let assume_st_letin hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac - (fun id -> + hyps tclIDTAC gls + +let assume_st_letin hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) - hyps tclIDTAC gls + hyps tclIDTAC gls (* suffices *) -let rec metas_from n hyps = +let rec metas_from n hyps = match hyps with _ :: q -> n :: metas_from (succ n) q | [] -> [] - + let rec build_product args body = - match args with - (Hprop st| Hvar st )::rest -> + match args with + (Hprop st| Hvar st )::rest -> let pprod= lift 1 (build_product rest body) in let lbody = match st.st_label with Anonymous -> pprod | Name id -> subst_term (mkVar id) pprod in mkProd (st.st_label, st.st_it, lbody) - | [] -> body + | [] -> body let rec build_applist prod = function [] -> [],prod - | n::q -> + | n::q -> let (_,typ,_) = destProd prod in let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in (n,typ)::ctx,head -let instr_suffices _then cut gls0 = - let info = get_its_info gls0 in - let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in +let instr_suffices _then cut gls0 = + let info = get_its_info gls0 in + let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in let ctx,hd = cut.cut_stat in let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in let metas = metas_from 1 ctx in let c_ctx,c_head = build_applist c_stat metas in - let c_term = applist (mkVar c_id,List.map mkMeta metas) in - let thus_tac gls= + let c_term = applist (mkVar c_id,List.map mkMeta metas) in + let thus_tac gls= thus_tac c_term c_head c_ctx gls in - tclTHENS (assert_postpone c_id c_stat) - [tclTHENLIST - [ assume_tac ctx; + tclTHENS (assert_postpone c_id c_stat) + [tclTHENLIST + [ assume_tac ctx; tcl_erase_info; just_tac _then cut info]; thus_tac] gls0 @@ -706,7 +704,7 @@ let instr_suffices _then cut gls0 = let conjunction_arity id gls = let typ = pf_get_hyp_typ gls id in let hd,params = decompose_app (special_whd gls typ) in - let env =pf_env gls in + let env =pf_env gls in match kind_of_term hd with Ind ind when is_good_inductive env ind -> let mib,oib= @@ -719,70 +717,70 @@ let conjunction_arity id gls = List.length rc | _ -> raise Not_found -let rec intron_then n ids ltac gls = - if n<=0 then +let rec intron_then n ids ltac gls = + if n<=0 then ltac ids gls - else - let id = pf_get_new_id (id_of_string "_tmp") gls in - tclTHEN - (intro_mustbe_force id) - (intron_then (pred n) (id::ids) ltac) gls + else + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (intro_mustbe_force id) + (intron_then (pred n) (id::ids) ltac) gls let rec consider_match may_intro introduced available expected gls = - match available,expected with + match available,expected with [],[] -> tclIDTAC gls | _,[] -> error "Last statements do not match a complete hypothesis." (* should tell which ones *) - | [],hyps -> + | [],hyps -> if may_intro then begin let id = pf_get_new_id (id_of_string "_tmp") gls in - tclIFTHENELSE + tclIFTHENELSE (intro_mustbe_force id) - (consider_match true [] [id] hyps) - (fun _ -> + (consider_match true [] [id] hyps) + (fun _ -> error "Not enough sub-hypotheses to match statements.") - gls - end + gls + end else error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> tclIFTHENELSE (convert_hyp (id,None,st.st_it)) begin - match st.st_label with - Anonymous -> + match st.st_label with + Anonymous -> consider_match may_intro ((id,false)::introduced) rest_ids rest - | Name hid -> - tclTHENLIST + | Name hid -> + tclTHENLIST [rename_hyp [id,hid]; consider_match may_intro ((hid,true)::introduced) rest_ids rest] end begin - (fun gls -> + (fun gls -> let nhyps = - try conjunction_arity id gls with - Not_found -> error "Matching hypothesis not found." in - tclTHENLIST + try conjunction_arity id gls with + Not_found -> error "Matching hypothesis not found." in + tclTHENLIST [general_case_analysis false (mkVar id,NoBindings); intron_then nhyps [] - (fun l -> consider_match may_intro introduced + (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) end gls - + let consider_tac c hyps gls = match kind_of_term (strip_outer_cast c) with Var id -> - consider_match false [] [id] hyps gls - | _ -> + consider_match false [] [id] hyps gls + | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in - tclTHEN + tclTHEN (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) - (consider_match false [] [id] hyps) gls - + (consider_match false [] [id] hyps) gls + let given_tac hyps gls = consider_match true [] [] hyps gls @@ -792,22 +790,22 @@ let given_tac hyps gls = let rec take_tac wits gls = match wits with [] -> tclIDTAC gls - | wit::rest -> - let typ = pf_type_of gls wit in + | wit::rest -> + let typ = pf_type_of gls wit in tclTHEN (thus_tac wit typ []) (take_tac rest) gls (* tactics for define *) let rec build_function args body = - match args with - st::rest -> + match args with + st::rest -> let pfun= lift 1 (build_function rest body) in let id = match st.st_label with Anonymous -> assert false | Name id -> id in mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) - | [] -> body + | [] -> body let define_tac id args body gls = let t = build_function args body in @@ -815,43 +813,37 @@ let define_tac id args body gls = (* tactics for reconsider *) -let cast_tac id_or_thesis typ gls = +let cast_tac id_or_thesis typ gls = match id_or_thesis with This id -> let (_,body,_) = pf_get_hyp gls id in convert_hyp (id,body,typ) gls - | Thesis (For _ ) -> + | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> + | Thesis Plain -> convert_concl typ DEFAULTcast gls - + (* per cases *) let is_rec_pos (main_ind,wft) = match main_ind with None -> false - | Some index -> + | Some index -> match fst (Rtree.dest_node wft) with Mrec i when i = index -> true | _ -> false let rec constr_trees (main_ind,wft) ind = match Rtree.dest_node wft with - Norec,_ -> - let itree = - (snd (Global.lookup_inductive ind)).mind_recargs in + Norec,_ -> + let itree = + (snd (Global.lookup_inductive ind)).mind_recargs in constr_trees (None,itree) ind | _,constrs -> main_ind,constrs -let constr_args rp constr = - let main_ind,constrs = constr_trees rp (fst constr) in - let ctree = constrs.(pred (snd constr)) in - array_map_to_list (fun t -> main_ind,t) - (snd (Rtree.dest_node ctree)) - let ind_args rp ind = let main_ind,constrs = constr_trees rp ind in - let args ctree = + let args ctree = Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in Array.map args constrs @@ -862,7 +854,7 @@ let init_tree ids ind rp nexti = let map_tree_rp rp id_fun mapi = function Split_patt (ids,ind,branches) -> - let indargs = ind_args rp ind in + let indargs = ind_args rp ind in let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in Split_patt (id_fun ids,ind,Array.mapi do_i branches) | _ -> failwith "map_tree_rp: not a splitting node" @@ -874,19 +866,19 @@ let map_tree id_fun mapi = function | _ -> failwith "map_tree: not a splitting node" -let start_tree env ind rp = +let start_tree env ind rp = init_tree Idset.empty ind rp (fun _ _ -> None) -let build_per_info etype casee gls = +let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in let ctyp=pf_type_of gls casee in - let is_dep = dependent casee concl in + let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in - let ind = + let ind = try - destInd hd - with _ -> + destInd hd + with _ -> error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = @@ -894,10 +886,10 @@ let build_per_info etype casee gls = ET_Induction -> mind.mind_nparams_rec,Some (snd ind) | _ -> mind.mind_nparams,None in let params,real_args = list_chop nparams args in - let abstract_obj c body = - let typ=pf_type_of gls c in + let abstract_obj c body = + let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in - let pred= List.fold_right abstract_obj + let pred= List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in is_dep, {per_casee=casee; @@ -906,7 +898,7 @@ let build_per_info etype casee gls = per_pred=pred; per_args=real_args; per_params=params; - per_nparams=nparams; + per_nparams=nparams; per_wf=index,oind.mind_recargs} let per_tac etype casee gls= @@ -915,25 +907,25 @@ let per_tac etype casee gls= match casee with Real c -> let is_dep,per_info = build_per_info etype c gls in - let ek = + let ek = if is_dep then EK_dep (start_tree env per_info.per_ind per_info.per_wf) else EK_unknown in - tcl_change_info + tcl_change_info {pm_stack= Per(etype,per_info,ek,[])::info.pm_stack} gls | Virtual cut -> assert (cut.cut_stat.st_label=Anonymous); let id = pf_get_new_id (id_of_string "anonymous_matched") gls in let c = mkVar id in - let modified_cut = + let modified_cut = {cut with cut_stat={cut.cut_stat with st_label=Name id}} in - tclTHEN + tclTHEN (instr_cut (fun _ _ c -> c) false false modified_cut) (fun gls0 -> let is_dep,per_info = build_per_info etype c gls0 in assert (not is_dep); - tcl_change_info + tcl_change_info {pm_stack= Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) gls @@ -950,7 +942,7 @@ let register_nodep_subcase id= function end | _ -> anomaly "wrong stack state" -let suppose_tac hyps gls0 = +let suppose_tac hyps gls0 = let info = get_its_info gls0 in let thesis = pf_concl gls0 in let id = pf_get_new_id (id_of_string "subcase_") gls0 in @@ -958,13 +950,13 @@ let suppose_tac hyps gls0 = let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in let ninfo2 = {pm_stack=stack} in - tclTHENS (assert_postpone id clause) + tclTHENS (assert_postpone id clause) [tclTHENLIST [tcl_change_info ninfo1; assume_tac hyps; clear old_clauses]; tcl_change_info ninfo2] gls0 -(* suppose it is ... *) +(* suppose it is ... *) (* pattern matching compiling *) @@ -975,20 +967,20 @@ let rec skip_args rest ids n = Skip_patt (ids,skip_args rest ids (pred n)) let rec tree_of_pats ((id,_) as cpl) pats = - match pats with + match pats with [] -> End_patt cpl | args::stack -> match args with [] -> Close_patt (tree_of_pats cpl stack) | (patt,rp) :: rest_args -> match patt with - PatVar (_,v) -> + PatVar (_,v) -> Skip_patt (Idset.singleton id, tree_of_pats cpl (rest_args::stack)) | PatCstr (_,(ind,cnum),args,nam) -> let nexti i ati = - if i = pred cnum then - let nargs = + if i = pred cnum then + let nargs = list_map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.singleton id, tree_of_pats cpl (nargs::rest_args::stack)) @@ -996,49 +988,49 @@ let rec tree_of_pats ((id,_) as cpl) pats = in init_tree Idset.empty ind rp nexti let rec add_branch ((id,_) as cpl) pats tree= - match pats with - [] -> + match pats with + [] -> begin match tree with - End_patt cpl0 -> End_patt cpl0 - (* this ensures precedence for overlapping patterns *) + End_patt cpl0 -> End_patt cpl0 + (* this ensures precedence for overlapping patterns *) | _ -> anomaly "tree is expected to end here" end | args::stack -> - match args with + match args with [] -> begin match tree with - Close_patt t -> + Close_patt t -> Close_patt (add_branch cpl stack t) - | _ -> anomaly "we should pop here" + | _ -> anomaly "we should pop here" end | (patt,rp) :: rest_args -> match patt with PatVar (_,v) -> begin - match tree with - Skip_patt (ids,t) -> + match tree with + Skip_patt (ids,t) -> Skip_patt (Idset.add id ids, add_branch cpl (rest_args::stack) t) | Split_patt (_,_,_) -> map_tree (Idset.add id) - (fun i bri -> - append_branch cpl 1 (rest_args::stack) bri) + (fun i bri -> + append_branch cpl 1 (rest_args::stack) bri) tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly "No pop/stop expected here" end | PatCstr (_,(ind,cnum),args,nam) -> match tree with Skip_patt (ids,t) -> let nexti i ati = - if i = pred cnum then - let nargs = + if i = pred cnum then + let nargs = list_map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.add id ids, add_branch cpl (nargs::rest_args::stack) (skip_args t ids (Array.length ati))) - else + else Some (ids, skip_args t ids (Array.length ati)) in init_tree ids ind rp nexti @@ -1047,30 +1039,30 @@ let rec add_branch ((id,_) as cpl) pats tree= (* this can happen with coercions *) "Case pattern belongs to wrong inductive type."; let mapi i ati bri = - if i = pred cnum then - let nargs = + if i = pred cnum then + let nargs = list_map_i (fun j a -> (a,ati.(j))) 0 args in - append_branch cpl 0 + append_branch cpl 0 (nargs::rest_args::stack) bri else bri in map_tree_rp rp (fun ids -> ids) mapi tree | _ -> anomaly "No pop/stop expected here" and append_branch ((id,_) as cpl) depth pats = function - Some (ids,tree) -> + Some (ids,tree) -> Some (Idset.add id ids,append_tree cpl depth pats tree) | None -> Some (Idset.singleton id,tree_of_pats cpl pats) and append_tree ((id,_) as cpl) depth pats tree = if depth<=0 then add_branch cpl pats tree else match tree with - Close_patt t -> + Close_patt t -> Close_patt (append_tree cpl (pred depth) pats t) - | Skip_patt (ids,t) -> + | Skip_patt (ids,t) -> Skip_patt (Idset.add id ids,append_tree cpl depth pats t) | End_patt _ -> anomaly "Premature end of branch" - | Split_patt (_,_,_) -> - map_tree (Idset.add id) - (fun i bri -> append_branch cpl (succ depth) pats bri) tree + | Split_patt (_,_,_) -> + map_tree (Idset.add id) + (fun i bri -> append_branch cpl (succ depth) pats bri) tree (* suppose it is *) @@ -1084,22 +1076,22 @@ let thesis_for obj typ per_info env= let cind,all_args=decompose_app typ in let ind = destInd cind in let _ = if ind <> per_info.per_ind then - errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ - str"cannot give an induction hypothesis (wrong inductive type).") in + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = list_chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in compose_prod rc (whd_beta Evd.empty hd2) let rec build_product_dep pat_info per_info args body gls = - match args with - (Hprop {st_label=nam;st_it=This c} - | Hvar {st_label=nam;st_it=c})::rest -> - let pprod= + match args with + (Hprop {st_label=nam;st_it=This c} + | Hvar {st_label=nam;st_it=c})::rest -> + let pprod= lift 1 (build_product_dep pat_info per_info rest body gls) in let lbody = match nam with @@ -1107,7 +1099,7 @@ let rec build_product_dep pat_info per_info args body gls = | Name id -> subst_var id pprod in mkProd (nam,c,lbody) | Hprop ({st_it=Thesis tk} as st)::rest -> - let pprod= + let pprod= lift 1 (build_product_dep pat_info per_info rest body gls) in let lbody = match st.st_label with @@ -1117,14 +1109,14 @@ let rec build_product_dep pat_info per_info args body gls = match tk with For id -> let obj = mkVar id in - let typ = - try st_assoc (Name id) pat_info.pat_vars - with Not_found -> + let typ = + try st_assoc (Name id) pat_info.pat_vars + with Not_found -> snd (st_assoc (Name id) pat_info.pat_aliases) in thesis_for obj typ per_info (pf_env gls) | Plain -> pf_concl gls in mkProd (st.st_label,ptyp,lbody) - | [] -> body + | [] -> body let build_dep_clause params pat_info per_info hyps gls = let concl= @@ -1138,35 +1130,35 @@ let build_dep_clause params pat_info per_info hyps gls = let let_one_in st body = match st.st_label with Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) - | Name id -> + | Name id -> mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in - let aliased_clause = + let aliased_clause = List.fold_right let_one_in pat_info.pat_aliases open_clause in List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause let rec register_dep_subcase id env per_info pat = function EK_nodep -> error "Only \"suppose it is\" can be used here." - | EK_unknown -> + | EK_unknown -> register_dep_subcase id env per_info pat (EK_dep (start_tree env per_info.per_ind per_info.per_wf)) | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree) - + let case_tac params pat_info hyps gls0 = let info = get_its_info gls0 in let id = pf_get_new_id (id_of_string "subcase_") gls0 in let et,per_info,ek,old_clauses,rest = match info.pm_stack with - Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) + Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) | _ -> anomaly "wrong place for cases" in let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = - register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info - pat_info.pat_pat ek in + register_dep_subcase (id,(List.length params,List.length hyps)) + (pf_env gls0) per_info pat_info.pat_pat ek in let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in - tclTHENS (assert_postpone id clause) - [tclTHENLIST - [tcl_change_info ninfo1; + tclTHENS (assert_postpone id clause) + [tclTHENLIST + [tcl_change_info ninfo1; assume_st (params@pat_info.pat_vars); assume_st_letin pat_info.pat_aliases; assume_hyps_or_theses hyps; @@ -1181,23 +1173,23 @@ type instance_stack = let initial_instance_stack ids = List.map (fun id -> id,[None,[]]) ids -let push_one_arg arg = function +let push_one_arg arg = function [] -> anomaly "impossible" - | (head,args) :: ctx -> + | (head,args) :: ctx -> ((head,(arg::args)) :: ctx) let push_arg arg stacks = List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks - -let push_one_head c ids (id,stack) = + +let push_one_head c ids (id,stack) = let head = if Idset.mem id ids then Some c else None in id,(head,[]) :: stack let push_head c ids stacks = List.map (push_one_head c ids) stacks -let pop_one (id,stack) = +let pop_one (id,stack) = let nstack= match stack with [] -> anomaly "impossible" @@ -1212,28 +1204,26 @@ let pop_one (id,stack) = let pop_stacks stacks = List.map pop_one stacks -let patvar_base = id_of_string "__" - let hrec_for fix_id per_info gls obj_id = let obj=mkVar obj_id in let typ=pf_get_hyp_typ gls obj_id in let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in let ind = destInd cind in assert (ind=per_info.per_ind); - let params,args= list_chop per_info.per_nparams all_args in + let params,args= list_chop per_info.per_nparams all_args in assert begin - try List.for_all2 eq_constr params per_info.per_params with + try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; - let hd2 = applist (mkVar fix_id,args@[obj]) in + let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (whd_beta gls.sigma hd2) let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with - Close_patt t,_ -> - let args0 = pop_stacks args in + Close_patt t,_ -> + let args0 = pop_stacks args in execute_cases fix_name per_info tacnext args0 objs nhrec t gls - | Skip_patt (_,t),skipped::next_objs -> + | Skip_patt (_,t),skipped::next_objs -> let args0 = push_arg skipped args in execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls | End_patt (id,(nparams,nhyps)),[] -> @@ -1260,66 +1250,66 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let hd,all_args = decompose_app (special_whd gls ctyp) in let _ = assert (destInd hd = ind) in (* just in case *) let params,real_args = list_chop nparams all_args in - let abstract_obj c body = - let typ=pf_type_of gls c in + let abstract_obj c body = + let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in - let elim_pred = List.fold_right abstract_obj + let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in let case_info = Inductiveops.make_case_info env ind RegularStyle in let gen_arities = Inductive.arities_of_constructors ind spec in - let f_ids typ = - let sign = - fst (Sign.decompose_prod_assum (Term.prod_applist typ params)) in + let f_ids typ = + let sign = + (prod_assum (Term.prod_applist typ params)) in find_intro_names sign gls in let constr_args_ids = Array.map f_ids gen_arities in - let case_term = + let case_term = mkCase(case_info,elim_pred,casee, Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in let branch_tac i (recargs,bro) gls0 = let args_ids = constr_args_ids.(i) in let rec aux n = function - [] -> - assert (n=Array.length recargs); + [] -> + assert (n=Array.length recargs); next_objs,[],nhrec - | id :: q -> + | id :: q -> let objs,recs,nrec = aux (succ n) q in - if recargs.(n) - then (mkVar id::objs),(id::recs),succ nrec + if recargs.(n) + then (mkVar id::objs),(id::recs),succ nrec else (mkVar id::objs),recs,nrec in let objs,recs,nhrec = aux 0 args_ids in tclTHENLIST [tclMAP intro_mustbe_force args_ids; begin - fun gls1 -> - let hrecs = - List.map - (fun id -> - hrec_for (out_name fix_name) per_info gls1 id) + fun gls1 -> + let hrecs = + List.map + (fun id -> + hrec_for (out_name fix_name) per_info gls1 id) recs in generalize hrecs gls1 end; match bro with - None -> + None -> msg_warning (str "missing case"); tacnext (mkMeta 1) | Some (sub_ids,tree) -> let br_args = - List.filter - (fun (id,_) -> Idset.mem id sub_ids) args in - let construct = + List.filter + (fun (id,_) -> Idset.mem id sub_ids) args in + let construct = applist (mkConstruct(ind,succ i),params) in - let p_args = + let p_args = push_head construct ids br_args in - execute_cases fix_name per_info tacnext + execute_cases fix_name per_info tacnext p_args objs nhrec tree] gls0 in - tclTHENSV + tclTHENSV (refine case_term) (Array.mapi branch_tac br) gls - | Split_patt (_, _, _) , [] -> + | Split_patt (_, _, _) , [] -> anomaly "execute_cases : Nothing to split" - | Skip_patt _ , [] -> + | Skip_patt _ , [] -> anomaly "execute_cases : Nothing to skip" - | End_patt (_,_) , _ :: _ -> + | End_patt (_,_) , _ :: _ -> anomaly "execute_cases : End of branch with garbage left" let understand_my_constr c gls = @@ -1337,41 +1327,41 @@ let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in !refine oc gls)) (* end focus/claim *) - + let end_tac et2 gls = let info = get_its_info gls in - let et1,pi,ek,clauses = + let et1,pi,ek,clauses = match info.pm_stack with - Suppose_case::_ -> + Suppose_case::_ -> anomaly "This case should already be trapped" - | Claim::_ -> + | Claim::_ -> error "\"end claim\" expected." | Focus_claim::_ -> error "\"end focus\" expected." - | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) - | [] -> + | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) + | [] -> anomaly "This case should already be trapped" in - let et = + let et = if et1 <> et2 then - match et1 with - ET_Case_analysis -> + match et1 with + ET_Case_analysis -> error "\"end cases\" expected." | ET_Induction -> error "\"end induction\" expected." else et1 in - tclTHEN + tclTHEN tcl_erase_info begin match et,ek with - _,EK_unknown -> - tclSOLVE [simplest_elim pi.per_casee] + _,EK_unknown -> + tclSOLVE [simplest_elim pi.per_casee] | ET_Case_analysis,EK_nodep -> - tclTHEN + tclTHEN (general_case_analysis false (pi.per_casee,NoBindings)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); + [generalize (pi.per_args@[pi.per_casee]); simple_induct (AnonHyp (succ (List.length pi.per_args))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> @@ -1385,57 +1375,48 @@ let end_tac et2 gls = let nargs = (List.length pi.per_args) in tclTHEN (generalize (pi.per_args@[pi.per_casee])) begin - fun gls0 -> - let fix_id = + fun gls0 -> + let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in - let c_id = + let c_id = pf_get_new_id (id_of_string "_main_arg") gls0 in tclTHENLIST [fix (Some fix_id) (succ nargs); tclDO nargs introf; intro_mustbe_force c_id; - execute_cases (Name fix_id) pi + execute_cases (Name fix_id) pi (fun c -> - tclTHENLIST + tclTHENLIST [clear [fix_id]; my_refine c; clear clauses; justification assumption]) - (initial_instance_stack clauses) + (initial_instance_stack clauses) [mkVar c_id] 0 tree] gls0 - end + end end gls (* escape *) -let rec abstract_metas n avoid head = function - [] -> 1,head,[] - | (meta,typ)::rest -> - let id = next_ident_away (id_of_string "_sbgl") avoid in - let p,term,args = abstract_metas (succ n) (id::avoid) head rest in - succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term), - (mkMeta n)::args - - let escape_tac gls = tcl_erase_info gls (* General instruction engine *) -let rec do_proof_instr_gen _thus _then instr = - match instr with - Pthus i -> +let rec do_proof_instr_gen _thus _then instr = + match instr with + Pthus i -> assert (not _thus); do_proof_instr_gen true _then i - | Pthen i -> + | Pthen i -> assert (not _then); do_proof_instr_gen _thus true i - | Phence i -> + | Phence i -> assert (not (_then || _thus)); do_proof_instr_gen true true i | Pcut c -> instr_cut mk_stat_or_thesis _thus _then c | Psuffices c -> - instr_suffices _then c + instr_suffices _then c | Prew (s,c) -> assert (not _then); instr_rew _thus s c @@ -1443,75 +1424,75 @@ let rec do_proof_instr_gen _thus _then instr = | Pgiven hyps -> given_tac hyps | Passume hyps -> assume_tac hyps | Plet hyps -> assume_tac hyps - | Pclaim st -> instr_claim false st + | Pclaim st -> instr_claim false st | Pfocus st -> instr_claim true st | Ptake witl -> take_tac witl | Pdefine (id,args,body) -> define_tac id args body - | Pcast (id,typ) -> cast_tac id typ - | Pper (et,cs) -> per_tac et cs + | Pcast (id,typ) -> cast_tac id typ + | Pper (et,cs) -> per_tac et cs | Psuppose hyps -> suppose_tac hyps | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps | Pend (B_elim et) -> end_tac et | Pend _ -> anomaly "Not applicable" | Pescape -> escape_tac - + let eval_instr {instr=instr} = - do_proof_instr_gen false false instr + do_proof_instr_gen false false instr let rec preprocess pts instr = match instr with Phence i |Pthus i | Pthen i -> preprocess pts i - | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ - | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ + | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ + | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Pper _ | Prew _ -> check_not_per pts; true,pts - | Pescape -> + | Pescape -> check_not_per pts; true,pts - | Pcase _ | Psuppose _ | Pend (B_elim _) -> + | Pcase _ | Psuppose _ | Pend (B_elim _) -> true,close_previous_case pts - | Pend bt -> - false,close_block bt pts - -let rec postprocess pts instr = + | Pend bt -> + false,close_block bt pts + +let rec postprocess pts instr = match instr with Phence i | Pthus i | Pthen i -> postprocess pts i | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts - | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ | Pescape -> nth_unproven 1 pts | Pend (B_elim ET_Induction) -> begin let pf = proof_of_pftreestate pts in let (pfterm,_) = extract_open_pftreestate pts in let env = Evd.evar_env (goal_of_proof pf) in - try + try Inductiveops.control_only_guard env pfterm; goto_current_focus_or_top (mark_as_done pts) - with + with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly "\"end induction\" generated an ill-formed fixpoint" end - | Pend _ -> + | Pend _ -> goto_current_focus_or_top (mark_as_done pts) let do_instr raw_instr pts = let has_tactic,pts1 = preprocess pts raw_instr.instr in - let pts2 = + let pts2 = if has_tactic then let gl = nth_goal_of_pftreestate 1 pts1 in let env= pf_env gl in let sigma= project gl in - let ist = {ltacvars = ([],[]); ltacrecvars = []; + let ist = {ltacvars = ([],[]); ltacrecvars = []; gsigma = sigma; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in - let instr = + let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in let lock_focus = is_focussing_instr instr.instr in let marker= Proof_instr (lock_focus,instr) in - solve_nth_pftreestate 1 + solve_nth_pftreestate 1 (abstract_operation marker (tclTHEN (eval_instr instr) clean_tmp)) pts1 else pts1 in postprocess pts2 raw_instr.instr @@ -1522,8 +1503,8 @@ let proof_instr raw_instr = (* (* STUFF FOR ITERATED RELATIONS *) -let decompose_bin_app t= - let hd,args = destApp +let decompose_bin_app t= + let hd,args = destApp let identify_transitivity_lemma c = let varx,tx,c1 = destProd c in @@ -1534,4 +1515,4 @@ let identify_transitivity_lemma c = let p2=pop lp2 in let p3=pop lp3 in *) - + |