diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 995 |
1 files changed, 472 insertions, 523 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index a34446d8..895b97fe 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$ *) +(* $Id: decl_proof_instr.ml 11072 2008-06-08 16:13:37Z herbelin $ *) open Util open Pp @@ -22,6 +22,7 @@ open Decl_mode open Decl_interp open Rawterm open Names +open Nameops open Declarations open Tactics open Tacticals @@ -30,6 +31,7 @@ open Termops open Reductionops open Goptions + (* Strictness option *) let get_its_info gls = get_info gls.it @@ -81,42 +83,34 @@ let check_not_per pts = Please \"suppose\" something or \"end\" it now." | _ -> () -let get_thesis gls0 = - let info = get_its_info gls0 in - match info.pm_subgoals with - [m,thesis] -> thesis - | _ -> error "Thesis is split" - let mk_evd metalist gls = - let evd0= create_evar_defs (sig_sig gls) in + let evd0= create_goal_evar_defs (sig_sig gls) in 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) when - not (occur_id [] lid info.pm_partial_goal) -> - tclTRY (clear [lid]) - | _ -> tclIDTAC - end - begin - tcl_change_info - {info with - pm_last=Some cpl } - end gls - +let is_tmp id = (string_of_id id).[0] = '_' + +let tmp_ids gls = + let ctx = pf_hyps gls in + match ctx with + [] -> [] + | _::q -> List.filter is_tmp (ids_of_named_context q) + +let clean_tmp gls = + let clean_id id0 gls0 = + tclTRY (clear [id0]) gls0 in + let rec clean_all = function + [] -> tclIDTAC + | id :: rest -> tclTHEN (clean_id id) (clean_all rest) + in + clean_all (tmp_ids gls) gls + (* start a proof *) let start_proof_tac gls= let gl=sig_it gls in - let info={pm_last=None; - pm_partial_goal=mkMeta 1; - pm_subgoals= [1,gl.evar_concl]; - pm_stack=[]} in + let info={pm_stack=[]} in {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, function [pftree] -> @@ -267,7 +261,8 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere) + (thin_body [id]) gls in tclMAP add_aux items gls let prepare_goal items gls = @@ -292,14 +287,36 @@ let justification tac gls= error "insufficient justification" else begin - msgnl (str "Warning: insufficient justification"); + msg_warning (str "insufficient justification"); daimon_tac gls end) gls let default_justification elems gls= justification (tclTHEN (prepare_goal elems) automation_tac) gls -(* code for have/then/thus/hence *) +(* code for conclusion refining *) + +let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s) + +let _and = constant ["Init";"Logic"] "and" + +let _and_rect = constant ["Init";"Logic"] "and_rect" + +let _prod = constant ["Init";"Datatypes"] "prod" + +let _prod_rect = constant ["Init";"Datatypes"] "prod_rect" + +let _ex = constant ["Init";"Logic"] "ex" + +let _ex_ind = constant ["Init";"Logic"] "ex_ind" + +let _sig = constant ["Init";"Specif"] "sig" + +let _sig_rect = constant ["Init";"Specif"] "sig_rect" + +let _sigT = constant ["Init";"Specif"] "sigT" + +let _sigT_rect = constant ["Init";"Specif"] "sigT_rect" type stackd_elt = {se_meta:metavariable; @@ -336,7 +353,8 @@ let enstack_subsubgoals env se stack gls= 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 refiner se.se_evd in + let evd = meta_assign se.se_meta + (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in let ncreated = replace_in_list se.se_meta nmetas se.se_meta_list in let evd0 = List.fold_left @@ -352,19 +370,28 @@ let enstack_subsubgoals env se stack gls= Array.iteri process gentypes | _ -> () -let find_subsubgoal env c ctyp skip evd metas submetas gls = +let rec nf_list evd = + function + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then + nf_list evd others + else + (m,nf_meta evd typ)::nf_list evd others + +let find_subsubgoal c ctyp skip submetas gls = + let env= pf_env gls in + let concl = pf_concl gls in + let evd = mk_evd ((0,concl)::submetas) gls in let stack = Stack.create () in let max_meta = - let tmp = List.fold_left (fun a (m,_) -> max a m) 0 metas in - List.fold_left (fun a (m,_) -> max a m) tmp submetas in - let _ = - List.iter (fun (m,typ) -> - Stack.push - {se_meta=m; - se_type=typ; - se_last_meta=max_meta; - se_meta_list=metas; - se_evd=evd} stack) (List.rev metas) in + List.fold_left (fun a (m,_) -> max a m) 0 submetas in + 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 se = Stack.pop stack in try @@ -372,10 +399,11 @@ let find_subsubgoal env c ctyp skip evd metas submetas gls = Unification.w_unify true env Reduction.CUMUL ctyp se.se_type se.se_evd in if n <= 0 then - {se with - se_evd=meta_assign se.se_meta c unifier; - se_meta_list=replace_in_list - se.se_meta submetas se.se_meta_list} + {se with + se_evd=meta_assign se.se_meta + (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier; + se_meta_list=replace_in_list + se.se_meta submetas se.se_meta_list} else dfs (pred n) with _ -> @@ -384,85 +412,86 @@ let find_subsubgoal env c ctyp skip evd metas submetas gls = dfs n end in let nse= try dfs skip with Stack.Empty -> raise Not_found in - nse.se_meta_list,nse.se_evd - -let rec nf_list evd = - function - [] -> [] - | (m,typ)::others -> - if meta_defined evd m then - nf_list evd others - else - (m,nf_meta evd typ)::nf_list evd others - -let rec max_linear_context meta_one c = - if !meta_one = None then - if isMeta c then - begin - meta_one:= Some c; - mkMeta 1 - end - else - try - map_constr (max_linear_context meta_one) c - with Not_found -> - begin - meta_one:= Some c; - mkMeta 1 - end - else - if isMeta c then - raise Not_found - else - map_constr (max_linear_context meta_one) c + nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0) + +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 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 _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 + asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) + else + 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 + begin + let _P = mkNamedLambda _x _A _B in + match bsort,sort with + InProp,InProp -> + let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in + InProp,_AxB, + mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|]) + | InProp,_ -> + let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in + 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, + mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|]) + end + else + begin + match asort,bsort with + InProp,InProp -> + let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in + InProp,_AxB, + mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|]) + |_,_ -> + let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in + let _P0 = mkLambda(Anonymous,_AxB,concl) in + InType,_AxB, + mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|]) + end + in + let (_,_,prf) = aux env [] [] metas in + mkApp(prf,[|mkMeta 1|]) let thus_tac c ctyp submetas gls = - let info = get_its_info gls in - let evd0 = mk_evd (info.pm_subgoals@submetas) gls in - let list,evd = + let list,proof = try - find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals submetas gls + find_subsubgoal c ctyp 0 submetas gls with Not_found -> error "I could not relate this statement to the thesis" in - let nflist = nf_list evd list in - let nfgoal = nf_meta evd info.pm_partial_goal in -(* let _ = msgnl (str "Partial goal : " ++ - print_constr_env (pf_env gls) nfgoal) in *) - let rgl = ref None in - let refiner = max_linear_context rgl nfgoal in - match !rgl with - None -> exact_check refiner gls - | Some pgl when not (isMeta refiner) -> - let ninfo={info with - pm_partial_goal = pgl; - pm_subgoals = nflist} in - tclTHEN - (Tactics.refine refiner) - (tcl_change_info ninfo) - gls - | _ -> - let ninfo={info with - pm_partial_goal = nfgoal; - pm_subgoals = nflist} in - tcl_change_info ninfo gls + if list = [] then + exact_check proof gls + else + let refiner = concl_refiner list proof gls in + Tactics.refine refiner gls -let anon_id_base = id_of_string "__" +(* general forward step *) -let mk_stat_or_thesis info = function +let anon_id_base = id_of_string "__" + +let mk_stat_or_thesis info gls = function This c -> c | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here" - | Thesis (Sub n) -> - begin - try List.assoc n info.pm_subgoals - with Not_found -> error "No such part in thesis." - end - | Thesis Plain -> - match info.pm_subgoals with - [_,c] -> c - | _ -> error - "\"thesis\" is split, please specify which part you refer to." + | Thesis Plain -> pf_concl gls let just_tac _then cut info gls0 = let items_tac gls = @@ -470,11 +499,10 @@ let just_tac _then cut info gls0 = None -> tclIDTAC gls | Some items -> let items_ = - if _then then - match info.pm_last with - None -> error "no previous statement to use" - | Some (id,_) -> (mkVar id)::items - else items + if _then then + let last_id = get_last (pf_env gls) in + (mkVar last_id)::items + else items in prepare_goal items_ gls in let method_tac gls = match cut.cut_using with @@ -487,23 +515,23 @@ let just_tac _then cut info gls0 = let instr_cut mkstat _thus _then cut gls0 = let info = get_its_info gls0 in let stat = cut.cut_stat in - let (c_id,_) as cpl = match stat.st_label with + 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 stat.st_it in + let c_stat = mkstat info gls0 stat.st_it in let thus_tac gls= if _thus then thus_tac (mkVar c_id) c_stat [] gls else tclIDTAC gls in tclTHENS (internal_cut c_id c_stat) [tclTHEN tcl_erase_info (just_tac _then cut info); - tclTHEN (set_last cpl) thus_tac] gls0 + thus_tac] gls0 (* iterated equality *) -let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) +let _eq = Libnames.constr_of_global (Coqlib.glob_eq) let decompose_eq id gls = let typ = pf_get_hyp_typ gls id in @@ -518,11 +546,8 @@ let decompose_eq id gls = | _ -> error "previous step is not an equality" let instr_rew _thus rew_side cut gls0 = - let info = get_its_info gls0 in - let last_id = - match info.pm_last with - None -> error "no previous equality" - | Some (id,_) -> id in + 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 items_tac gls = match cut.cut_by with @@ -536,7 +561,7 @@ 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,_) as cpl = match cut.cut_stat.st_label with + 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 @@ -551,14 +576,14 @@ let instr_rew _thus rew_side cut gls0 = [tclTHEN tcl_erase_info (tclTHENS (transitivity lhs) [just_tac;exact_check (mkVar last_id)]); - tclTHEN (set_last cpl) (thus_tac new_eq)] gls0 + 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 (set_last cpl) (thus_tac new_eq)] gls0 + thus_tac new_eq] gls0 @@ -566,48 +591,29 @@ let instr_rew _thus rew_side cut gls0 = let instr_claim _thus st gls0 = let info = get_its_info gls0 in - let (id,_) as cpl = match st.st_label with + 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 thus_tac (mkVar id) st.st_it [] gls else tclIDTAC gls in - let ninfo1 = {info with - pm_stack= - (if _thus then Focus_claim else Claim)::info.pm_stack; - pm_partial_goal=mkMeta 1; - pm_subgoals = [1,st.st_it]} in + let ninfo1 = {pm_stack= + (if _thus then Focus_claim else Claim)::info.pm_stack} in tclTHENS (internal_cut id st.st_it) [tcl_change_info ninfo1; - tclTHEN (set_last cpl) thus_tac] gls0 + thus_tac] gls0 (* tactics for assume *) -let reset_concl gls = - let info = get_its_info gls in - tcl_change_info - {info with - pm_partial_goal=mkMeta 1; - pm_subgoals= [1,gls.it.evar_concl]} gls - - -let intro_pm id gls= - let info = get_its_info gls in - match info.pm_subgoals with - [(_,typ)] -> - tclTHEN (intro_mustbe_force id) reset_concl gls - | _ -> error "Goal is split" - let push_intro_tac coerce nam gls = - let (hid,_) as cpl = + let (hid,_) = match nam with Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false | Name id -> id,true in tclTHENLIST - [intro_pm hid; - coerce hid; - set_last cpl] + [intro_mustbe_force hid; + coerce hid] gls let assume_tac hyps gls = @@ -652,10 +658,6 @@ let assume_st_letin hyps gls = (* suffices *) -let free_meta info = - let max_next (i,_) j = if j <= i then succ i else j in - List.fold_right max_next info.pm_subgoals 1 - let rec metas_from n hyps = match hyps with _ :: q -> n :: metas_from (succ n) q @@ -683,31 +685,21 @@ 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 hd) in - let metas = metas_from (free_meta info) ctx 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= thus_tac c_term c_head c_ctx gls in tclTHENS (internal_cut c_id c_stat) [tclTHENLIST - [ tcl_change_info - {info with - pm_partial_goal=mkMeta 1; - pm_subgoals=[1,c_stat]}; - assume_tac ctx; + [ assume_tac ctx; tcl_erase_info; just_tac _then cut info]; - tclTHEN (set_last (c_id,false)) thus_tac] gls0 + thus_tac] gls0 (* tactics for consider/given *) -let update_goal_info gls = - let info = get_its_info gls in - match info.pm_subgoals with - [m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls - | _ -> error "thesis is split" - let conjunction_arity id gls = let typ = pf_get_hyp_typ gls id in let hd,params = decompose_app (special_whd gls typ) in @@ -726,30 +718,18 @@ let conjunction_arity id gls = let rec intron_then n ids ltac gls = if n<=0 then - tclTHEN - (fun gls -> - if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids then - update_goal_info gls - else - tclIDTAC gls) - (ltac ids) - gls + 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 -let pm_rename_hyp id hid gls = - if occur_id [] id (pf_concl gls) then - tclTHEN (rename_hyp id hid) update_goal_info gls - else - rename_hyp id hid gls let rec consider_match may_intro introduced available expected gls = match available,expected with [],[] -> - set_last (List.hd introduced) gls + tclIDTAC gls | _,[] -> error "last statements do not match a complete hypothesis" (* should tell which ones *) | [],hyps -> @@ -757,7 +737,7 @@ let rec consider_match may_intro introduced available expected gls = begin let id = pf_get_new_id (id_of_string "_tmp") gls in tclIFTHENELSE - (intro_pm id) + (intro_mustbe_force id) (consider_match true [] [id] hyps) (fun _ -> error "not enough sub-hypotheses to match statements") @@ -774,7 +754,7 @@ let rec consider_match may_intro introduced available expected gls = consider_match may_intro ((id,false)::introduced) rest_ids rest | Name hid -> tclTHENLIST - [pm_rename_hyp id hid; + [rename_hyp [id,hid]; consider_match may_intro ((hid,true)::introduced) rest_ids rest] end begin @@ -783,7 +763,7 @@ let rec consider_match may_intro introduced available expected gls = try conjunction_arity id gls with Not_found -> error "matching hypothesis not found" in tclTHENLIST - [general_case_analysis (mkVar id,NoBindings); + [general_case_analysis false (mkVar id,NoBindings); intron_then nhyps [] (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) @@ -828,49 +808,74 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac true (Name id) t Tacexpr.nowhere gls + letin_tac None (Name id) t Tacexpr.nowhere gls (* tactics for reconsider *) let cast_tac id_or_thesis typ gls = - let info = get_its_info gls in match id_or_thesis with This id -> let (_,body,_) = pf_get_hyp gls id in convert_hyp (id,body,typ) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here" - | Thesis (Sub n) -> - begin - let old_typ = - try List.assoc n info.pm_subgoals - with Not_found -> error "No such part in thesis." in - if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then - let new_sg = List.merge - (fun (n,_) (p,_) -> Pervasives.compare n p) - [n,typ] (List.remove_assoc n info.pm_subgoals) in - tcl_change_info {info with pm_subgoals=new_sg} gls - else - error "not convertible" - end - | Thesis Plain -> - match info.pm_subgoals with - [m,c] -> - tclTHEN - (convert_concl typ DEFAULTcast) - (tcl_change_info {info with pm_subgoals= [m,typ]}) gls - | _ -> error - "\"thesis\" is split, please specify which part you refer to." - + | Thesis Plain -> + convert_concl typ DEFAULTcast gls (* per cases *) -let start_tree env ind = - let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in - Split (Idset.empty,ind,Array.map (fun _ -> None) constrs) +let is_rec_pos (main_ind,wft) = + match main_ind with + None -> false + | 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 + 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 = + Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in + Array.map args constrs + +let init_tree ids ind rp nexti = + let indargs = ind_args rp ind in + let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in + Split_patt (ids,ind,Array.mapi do_i indargs) + +let map_tree_rp rp id_fun mapi = function + Split_patt (ids,ind,branches) -> + 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" + +let map_tree id_fun mapi = function + Split_patt (ids,ind,branches) -> + let do_i i (recargs,bri) = recargs,mapi i bri in + Split_patt (id_fun ids,ind,Array.mapi do_i branches) + | _ -> failwith "map_tree: not a splitting node" + + +let start_tree env ind rp = + init_tree Idset.empty ind rp (fun _ _ -> None) let build_per_info etype casee gls = - let concl=get_thesis gls in + 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 @@ -880,11 +885,11 @@ let build_per_info etype casee gls = destInd hd with _ -> error "Case analysis must be done on an inductive object" in - let nparams = - let mind = fst (Global.lookup_inductive ind) in - match etype with - ET_Induction -> mind.mind_nparams_rec - | _ -> mind.mind_nparams in + let mind,oind = Global.lookup_inductive ind in + let nparams,index = + match etype with + 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 @@ -898,7 +903,8 @@ 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= let env=pf_env gls in @@ -908,25 +914,24 @@ let per_tac etype casee gls= let is_dep,per_info = build_per_info etype c gls in let ek = if is_dep then - EK_dep (start_tree env per_info.per_ind) + EK_dep (start_tree env per_info.per_ind per_info.per_wf) else EK_unknown in tcl_change_info - {info with - pm_stack= + {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 "_matched") gls in + let id = pf_get_new_id (id_of_string "anonymous_matched") gls in let c = mkVar id in let modified_cut = {cut with cut_stat={cut.cut_stat with st_label=Name id}} in tclTHEN - (instr_cut (fun _ c -> c) false false modified_cut) + (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 - {info with pm_stack= + {pm_stack= Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) gls @@ -944,16 +949,12 @@ let register_nodep_subcase id= function let suppose_tac hyps gls0 = let info = get_its_info gls0 in - let thesis = get_thesis gls0 in - let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let thesis = pf_concl gls0 in + let id = pf_get_new_id (id_of_string "subcase_") gls0 in let clause = build_product hyps thesis in - let ninfo1 = {info with - pm_stack=Suppose_case::info.pm_stack; - pm_partial_goal=mkMeta 1; - pm_subgoals = [1,clause]} in + let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in - let ninfo2 = {info with - pm_stack=stack} in + let ninfo2 = {pm_stack=stack} in tclTHENS (internal_cut id clause) [tclTHENLIST [tcl_change_info ninfo1; assume_tac hyps; @@ -964,120 +965,109 @@ let suppose_tac hyps gls0 = (* pattern matching compiling *) -let rec nb_prod_after n c= - match kind_of_term c with - | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else - 1+(nb_prod_after 0 b) - | _ -> 0 - -let constructor_arities env ind = - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in - let constr_types = Inductiveops.arities_of_constructors env ind in - let hyp = nb_prod_after nparams in - Array.map hyp constr_types - -let rec n_push rest ids n = - if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) - -let explode_branches ids env ind rest= - Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind) +let rec skip_args rest ids n = + if n <= 0 then + Close_patt rest + else + Skip_patt (ids,skip_args rest ids (pred n)) -let rec tree_of_pats env ((id,_) as cpl) pats = +let rec tree_of_pats ((id,_) as cpl) pats = match pats with - [] -> End_of_branch cpl + [] -> End_patt cpl | args::stack -> match args with - [] -> Pop (tree_of_pats env cpl stack) - | patt :: rest_args -> + [] -> Close_patt (tree_of_pats cpl stack) + | (patt,rp) :: rest_args -> match patt with PatVar (_,v) -> - Push (Idset.singleton id, - tree_of_pats env cpl (rest_args::stack)) - | PatCstr (_,(ind,cnum),args,nam) -> - let _,mind = Inductive.lookup_mind_specif env ind in - let br= Array.map (fun _ -> None) mind.mind_consnames in - br.(pred cnum) <- - Some (Idset.singleton id, - tree_of_pats env cpl (args::rest_args::stack)); - Split(Idset.empty,ind,br) - -let rec add_branch env ((id,_) as cpl) pats tree= + 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 = + list_map_i (fun j a -> (a,ati.(j))) 0 args in + Some (Idset.singleton id, + tree_of_pats cpl (nargs::rest_args::stack)) + else None + in init_tree Idset.empty ind rp nexti + +let rec add_branch ((id,_) as cpl) pats tree= match pats with [] -> begin match tree with - End_of_branch cpl0 -> End_of_branch cpl0 - (* this ensures precedence *) + 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 [] -> begin - match tree with - Pop t -> Pop (add_branch env cpl stack t) + match tree with + Close_patt t -> + Close_patt (add_branch cpl stack t) | _ -> anomaly "we should pop here" end - | patt :: rest_args -> + | (patt,rp) :: rest_args -> match patt with PatVar (_,v) -> begin match tree with - Push (ids,t) -> - Push (Idset.add id ids, - add_branch env cpl (rest_args::stack) t) - | Split (ids,ind,br) -> - Split (Idset.add id ids, - ind,array_map2 - (append_branch env cpl 1 - (rest_args::stack)) - (constructor_arities env ind) br) + 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) + tree | _ -> anomaly "No pop/stop expected here" end | PatCstr (_,(ind,cnum),args,nam) -> - match tree with - Push (ids,t) -> - let br = explode_branches ids env ind t in - let _ = - br.(pred cnum)<- - option_map - (fun (ids,tree) -> - Idset.add id ids, - add_branch env cpl - (args::rest_args::stack) tree) - br.(pred cnum) in - Split (ids,ind,br) - | Split (ids,ind0,br0) -> + match tree with + Skip_patt (ids,t) -> + let nexti i ati = + 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 + Some (ids, + skip_args t ids (Array.length ati)) + in init_tree ids ind rp nexti + | Split_patt (_,ind0,_) -> if (ind <> ind0) then error (* this can happen with coercions *) - "Case pattern belongs to wrong inductive type"; - let br=Array.copy br0 in - let ca = constructor_arities env ind in - let _= br.(pred cnum)<- - append_branch env cpl 0 (args::rest_args::stack) - ca.(pred cnum) br.(pred cnum) in - Split (ids,ind,br) + "Case pattern belongs to wrong inductive type"; + let mapi i ati bri = + if i = pred cnum then + let nargs = + list_map_i (fun j a -> (a,ati.(j))) 0 args in + 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 env ((id,_) as cpl) depth pats nargs = function +and append_branch ((id,_) as cpl) depth pats = function Some (ids,tree) -> - Some (Idset.add id ids,append_tree env cpl depth pats tree) + Some (Idset.add id ids,append_tree cpl depth pats tree) | None -> - Some (* (n_push (tree_of_pats env cpl pats) - (Idset.singleton id) nargs) *) - (Idset.singleton id,tree_of_pats env cpl pats) -and append_tree env ((id,_) as cpl) depth pats tree = - if depth<=0 then add_branch env cpl pats tree + 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 - Pop t -> Pop (append_tree env cpl (pred depth) pats t) - | Push (ids,t) -> Push (Idset.add id ids, - append_tree env cpl depth pats t) - | End_of_branch _ -> anomaly "Premature end of branch" - | Split (ids,ind,branches) -> - Split (Idset.add id ids,ind, - array_map2 - (append_branch env cpl (succ depth) pats) - (constructor_arities env ind) - branches) + Close_patt t -> + Close_patt (append_tree cpl (pred depth) pats 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 (* suppose it is *) @@ -1129,8 +1119,7 @@ let rec build_product_dep pat_info per_info args body gls = with Not_found -> snd (st_assoc (Name id) pat_info.pat_aliases) in thesis_for obj typ per_info (pf_env gls) - | Plain -> get_thesis gls - | Sub n -> anomaly "Subthesis in cases" in + | Plain -> pf_concl gls in mkProd (st.st_label,ptyp,lbody) | [] -> body @@ -1156,26 +1145,22 @@ let rec register_dep_subcase id env per_info pat = function EK_nodep -> error "Only \"suppose it is\" can be used here." | EK_unknown -> register_dep_subcase id env per_info pat - (EK_dep (start_tree env per_info.per_ind)) - | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree) + (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 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) | _ -> anomaly "wrong place for cases" in let clause = build_dep_clause params pat_info per_info hyps gls0 in - let ninfo1 = {info with - pm_stack=Suppose_case::info.pm_stack; - pm_partial_goal=mkMeta 1; - pm_subgoals = [1,clause]} in + let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info pat_info.pat_pat ek in - let ninfo2 = {info with - pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in + let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in tclTHENS (internal_cut id clause) [tclTHENLIST [tcl_change_info ninfo1; @@ -1188,181 +1173,152 @@ let case_tac params pat_info hyps gls0 = (* end cases *) type instance_stack = - (constr option*bool*(constr list) list) list + (constr option*(constr list) list) list let initial_instance_stack ids = - List.map (fun id -> id,[None,false,[]]) ids + List.map (fun id -> id,[None,[]]) ids let push_one_arg arg = function [] -> anomaly "impossible" - | (head,is_rec,args) :: ctx -> - ((head,is_rec,(arg::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 is_rec 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,is_rec,[]) :: stack + id,(head,[]) :: stack -let push_head c is_rec ids stacks = - List.map (push_one_head c is_rec ids) stacks +let push_head c ids stacks = + List.map (push_one_head c ids) stacks -let pop_one rec_flag (id,stack) = +let pop_one (id,stack) = let nstack= match stack with [] -> anomaly "impossible" | [c] as l -> l - | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx -> + | (Some head,args)::(head0,args0)::ctx -> let arg = applist (head,(List.rev args)) in - rec_flag:= !rec_flag || is_rec; - (head0,is_rec0,(arg::args0))::ctx - | (None,is_rec,args)::(head0,is_rec0,args0)::ctx -> - rec_flag:= !rec_flag || is_rec; - (head0,is_rec0,(args@args0))::ctx + (head0,(arg::args0))::ctx + | (None,args)::(head0,args0)::ctx -> + (head0,(args@args0))::ctx in id,nstack let pop_stacks stacks = - let rec_flag= ref false in - let nstacks = List.map (pop_one rec_flag) stacks in - !rec_flag , nstacks + List.map pop_one stacks let patvar_base = id_of_string "__" -let test_fun (str:string) = () - -let hrec_for obj_id fix_id per_info gls= +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 - match kind_of_term cind with - Ind ind when ind=per_info.per_ind -> - let params,args= list_chop per_info.per_nparams all_args in - if try - (List.for_all2 eq_constr params per_info.per_params) - with Invalid_argument _ -> false then - let hd2 = applist (mkVar fix_id,args@[obj]) in - Some (compose_lam rc (whd_beta hd2)) - else None - | _ -> None - - -(* custom elim performs the case analysis of hypothesis id from the local -context, - -- generalizing hypotheses below id -- computing the elimination predicate (abstract inductive predicate) -- build case analysis term -- generalize rec_calls (use wf_paths) -- vector of introduced identifiers per branch - -match id in t return p with - C1 ... => ?1 -|C2 ... => ?2 -... -end*) - - - - - - - - - -let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = - match tree with - Pop t -> - let is_rec,nstacks = pop_stacks stacks in - if is_rec then - let _ = test_fun "is_rec=true" in - let c_id = pf_get_new_id (id_of_string "_hrec") gls in - tclTHEN - (intro_mustbe_force c_id) - (execute_cases false fix_name per_info kont0 nstacks t) gls - else - execute_cases false fix_name per_info kont0 nstacks t gls - | Push (_,t) -> - let id = pf_get_new_id patvar_base gls in - let nstacks = push_arg (mkVar id) stacks in - let kont = execute_cases false fix_name per_info kont0 nstacks t in - tclTHEN - (intro_mustbe_force id) - begin - match fix_name with - Anonymous -> kont - | Name fix_id -> - (fun gls -> - if at_top then - kont gls - else - match hrec_for id fix_id per_info gls with - None -> kont gls - | Some c_obj -> - let c_id = - pf_get_new_id (id_of_string "_hrec") gls in - tclTHENLIST - [generalize [c_obj]; - intro_mustbe_force c_id; - kont] gls) - end gls - | Split(ids,ind,br) -> - let (_,typ,_)= - try destProd (pf_concl gls) with Invalid_argument _ -> - anomaly "Sub-object not found." in - let hd,args=decompose_app (special_whd gls typ) in - if try ind <> destInd hd with Invalid_argument _ -> true then - (* argument of an inductive family : intro + discard *) - tclTHEN intro - (execute_cases at_top fix_name per_info kont0 stacks tree) gls - else - begin - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in - let params = list_firstn nparams args in - let constr i =applist (mkConstruct(ind,succ i),params) in - let next_tac is_rec i = function - Some (sub_ids,tree) -> - let br_stacks = - List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in - let p_stacks = - push_head (constr i) is_rec ids br_stacks in - execute_cases false fix_name per_info kont0 p_stacks tree - | None -> - msgnl (str "Warning : missing case"); - kont0 (mkMeta 1) - in - let id = pf_get_new_id patvar_base gls in - let kont is_rec = - tclTHENSV - (general_case_analysis (mkVar id,NoBindings)) - (Array.mapi (next_tac is_rec) br) in - tclTHEN - (intro_mustbe_force id) - begin - match fix_name with - Anonymous -> kont false - | Name fix_id -> - (fun gls -> - if at_top then - kont false gls - else - match hrec_for id fix_id per_info gls with - None -> kont false gls - | Some c_obj -> - tclTHENLIST - [generalize [c_obj]; - kont true] gls) - end gls - end - | End_of_branch (id,nhyps) -> - match List.assoc id stacks with - [None,_,args] -> - let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in - kont0 (applist (mkVar id,List.rev_append args metas)) gls - | _ -> anomaly "wrong stack size" - + let ind = destInd cind in assert (ind=per_info.per_ind); + 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 + Invalid_argument _ -> false end; + let hd2 = applist (mkVar fix_id,args@[obj]) in + compose_lam rc (whd_beta 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 + execute_cases fix_name per_info tacnext args0 objs nhrec t gls + | 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,nhyps),[] -> + begin + match List.assoc id args with + [None,br_args] -> + let metas = + list_tabulate (fun n -> mkMeta (succ n)) nhyps in + tclTHEN + (tclDO nhrec introf) + (tacnext + (applist (mkVar id,List.rev_append br_args metas))) gls + | _ -> anomaly "wrong stack size" + end + | Split_patt (ids,ind,br), casee::next_objs -> + let (mind,oind) as spec = Global.lookup_inductive ind in + let nparams = mind.mind_nparams in + let concl=pf_concl gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + 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 + lambda_create env (typ,subst_term c body) in + 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 + find_intro_names sign gls in + let constr_args_ids = Array.map f_ids gen_arities in + 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); + next_objs,[],nhrec + | id :: q -> + let objs,recs,nrec = aux (succ n) q in + 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) + recs in + generalize hrecs gls1 + end; + match bro with + 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 = + applist (mkConstruct(ind,succ i),params) in + let p_args = + push_head construct ids br_args in + execute_cases fix_name per_info tacnext + p_args objs nhrec tree] gls0 in + tclTHENSV + (refine case_term) + (Array.mapi branch_tac br) gls + | Split_patt (_, _, _) , [] -> + anomaly "execute_cases : Nothing to split" + | Skip_patt _ , [] -> + anomaly "execute_cases : Nothing to skip" + | End_patt (_,_) , _ :: _ -> + anomaly "execute_cases : End of branch with garbage left" + + + +(* end focus/claim *) + let end_tac et2 gls = let info = get_its_info gls in let et1,pi,ek,clauses = @@ -1392,7 +1348,7 @@ let end_tac et2 gls = tclSOLVE [simplest_elim pi.per_casee] | ET_Case_analysis,EK_nodep -> tclTHEN - (general_case_analysis (pi.per_casee,NoBindings)) + (general_case_analysis false (pi.per_casee,NoBindings)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST @@ -1400,31 +1356,35 @@ let end_tac et2 gls = simple_induct (AnonHyp (succ (List.length pi.per_args))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> - tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); - execute_cases true Anonymous pi + execute_cases Anonymous pi (fun c -> tclTHENLIST [refine c; clear clauses; justification assumption]) - (initial_instance_stack clauses) tree] + (initial_instance_stack clauses) [pi.per_casee] 0 tree | ET_Induction,EK_dep tree -> - tclTHEN (generalize (pi.per_args@[pi.per_casee])) - begin - fun gls0 -> - let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in - tclTHEN - (fix (Some fix_id) (succ (List.length pi.per_args))) - (execute_cases true (Name fix_id) pi - (fun c -> - tclTHENLIST - [clear [fix_id]; - refine c; - clear clauses; - justification assumption - (* justification automation_tac *)]) - (initial_instance_stack clauses) tree) gls0 - end + let nargs = (List.length pi.per_args) in + tclTHEN (generalize (pi.per_args@[pi.per_casee])) + begin + fun gls0 -> + let fix_id = + pf_get_new_id (id_of_string "_fix") gls0 in + 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 + (fun c -> + tclTHENLIST + [clear [fix_id]; + refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) + [mkVar c_id] 0 tree] gls0 + end end gls (* escape *) @@ -1432,25 +1392,13 @@ let end_tac et2 gls = let rec abstract_metas n avoid head = function [] -> 1,head,[] | (meta,typ)::rest -> - let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in + 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 build_refining_context gls = - let info = get_its_info gls in - let avoid=pf_ids_of_hyps gls in - let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in - applist (fn,args) -let escape_command pts = - let pts1 = nth_unproven 1 pts in - let gls = top_goal_of_pftreestate pts1 in - let term = build_refining_context gls in - let tac = tclTHEN - (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info) - (Tactics.refine term) in - traverse 1 (solve_pftreestate tac pts1) +let escape_tac gls = tcl_erase_info gls (* General instruction engine *) @@ -1485,7 +1433,8 @@ let rec do_proof_instr_gen _thus _then instr = | Psuppose hyps -> suppose_tac hyps | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps | Pend (B_elim et) -> end_tac et - | Pend _ | Pescape -> anomaly "Not applicable" + | Pend _ -> anomaly "Not applicable" + | Pescape -> escape_tac let eval_instr {instr=instr} = do_proof_instr_gen false false instr @@ -1500,7 +1449,7 @@ let rec preprocess pts instr = true,pts | Pescape -> check_not_per pts; - false,pts + true,pts | Pcase _ | Psuppose _ | Pend (B_elim _) -> true,close_previous_case pts | Pend bt -> @@ -1511,8 +1460,8 @@ let rec postprocess pts instr = 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 _ -> nth_unproven 1 pts - | Pescape -> escape_command pts + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ + | Pescape -> nth_unproven 1 pts | Pend (B_elim ET_Induction) -> begin let pf = proof_of_pftreestate pts in @@ -1523,7 +1472,7 @@ let rec postprocess pts instr = goto_current_focus_or_top (mark_as_done pts) with Type_errors.TypeError(env, - Type_errors.IllFormedRecBody(_,_,_)) -> + Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly "\"end induction\" generated an ill-formed fixpoint" end | Pend _ -> @@ -1544,7 +1493,7 @@ let do_instr raw_instr pts = let lock_focus = is_focussing_instr instr.instr in let marker= Proof_instr (lock_focus,instr) in solve_nth_pftreestate 1 - (abstract_operation marker (eval_instr instr)) pts1 + (abstract_operation marker (tclTHEN (eval_instr instr) clean_tmp)) pts1 else pts1 in postprocess pts2 raw_instr.instr |