From ea1eaa9b152b73652f417e02bd469e5b289cec47 Mon Sep 17 00:00:00 2001 From: corbinea Date: Thu, 26 Apr 2007 08:54:28 +0000 Subject: fin des conclusions multiples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 17 +- ide/coq.mli | 2 +- ide/coqide.ml | 8 +- parsing/g_decl_mode.ml4 | 1 - parsing/ppdecl_proof.ml | 1 - parsing/printer.ml | 7 +- proofs/decl_expr.mli | 1 - proofs/decl_mode.ml | 10 +- proofs/decl_mode.mli | 7 +- tactics/decl_interp.ml | 10 +- tactics/decl_proof_instr.ml | 418 ++++++++++++++++++------------------------- tactics/decl_proof_instr.mli | 2 + 12 files changed, 201 insertions(+), 283 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 16b2460ad..930c50a77 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -269,24 +269,13 @@ let prepare_goal sigma g = (prepare_hyps sigma env, (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) -let prepare_meta sigma env (m,typ) = - env, sigma, - (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ)) - -let prepare_metas info sigma env = - List.fold_right - (fun cpl acc -> - let meta = prepare_meta sigma env cpl in meta :: acc) - info.pm_subgoals [] - let get_current_pm_goal () = let pfts = get_pftreestate () in let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in - let info = Decl_mode.get_info gls.it in - let env = pf_env gls in let sigma= sig_sig gls in - (prepare_hyps sigma env, - prepare_metas info sigma env) + let gl = sig_it gls in + prepare_goal sigma gl + let get_current_goals () = let pfts = get_pftreestate () in diff --git a/ide/coq.mli b/ide/coq.mli index 7b43a0c95..991f104db 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -33,7 +33,7 @@ type goal = hyp list * concl val get_current_goals : unit -> goal list -val get_current_pm_goal : unit -> hyp list * meta list +val get_current_pm_goal : unit -> goal val get_current_goals_nb : unit -> int diff --git a/ide/coqide.ml b/ide/coqide.ml index 25af11363..90130da37 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -804,17 +804,15 @@ object(self) proof_buffer#insert (Printf.sprintf " *** Declarative Mode ***\n"); try - let (hyps,metas) = get_current_pm_goal () in + let (hyps,concl) = get_current_pm_goal () in List.iter (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "\n"); - List.iter - (fun (_,_,m) -> - proof_buffer#insert (m^"\n")) - metas; + let (_,_,_,s) = concl in + proof_buffer#insert ("thesis := \n "^s^"\n"); let my_mark = `NAME "end_of_conclusion" in proof_buffer#move_mark ~where:((proof_buffer#get_iter_at_mark `INSERT)) diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 5c7b40afb..8942b6541 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -28,7 +28,6 @@ GLOBAL: proof_instr; thesis : [[ "thesis" -> Plain | "thesis"; "for"; i=ident -> (For i) - | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n)) ]]; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index ec8523d4d..9e3de9838 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -41,7 +41,6 @@ let pr_or_thesis pr_this env = function Thesis Plain -> str "thesis" | Thesis (For id) -> str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]" | This c -> pr_this env c let pr_cut pr_it env c = diff --git a/parsing/printer.ml b/parsing/printer.ml index c1a4415e3..7272ee697 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -262,16 +262,15 @@ let default_pr_goal g = pr_context_of env, pr_ltype_env_at_top env g.evar_concl else - let {pm_subgoals=metas} = get_info g in - (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), pr_context_of env, - pr_subgoal_metas metas env + pr_ltype_env_at_top env g.evar_concl in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () + str"thesis := " ++ fnl () ++ str " " ++ pc) ++ fnl () (* display the conclusion of a goal *) let pr_concl n g = diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli index 1c5cc0e74..d02060fc0 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.mli @@ -18,7 +18,6 @@ type 'it statement = type thesis_kind = Plain - | Sub of int | For of identifier type 'this or_thesis = diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index 5428166a9..cb148f4e5 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -67,10 +67,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list} + { pm_stack : stack_info list} let pm_in,pm_out = Dyn.create "pm_info" @@ -118,3 +115,8 @@ let get_end_command pts = end | Mode_none -> error "no proof in progress" + +let get_last env = + try + let (id,_,_) = List.hd (Environ.named_context env) in id + with Invalid_argument _ -> error "no previous statement to use" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli index 4a8aa85f1..412624b4d 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.mli @@ -56,10 +56,7 @@ type stack_info = | Focus_claim type pm_info = - { pm_last: (Names.identifier * bool) option (* anonymous if none *); - pm_partial_goal : constr ; (* partial goal construction *) - pm_subgoals : (metavariable*constr) list; - pm_stack : stack_info list } + {pm_stack : stack_info list } val pm_in : pm_info -> Dyn.t @@ -70,3 +67,5 @@ val get_end_command : pftreestate -> string option val get_stack : pftreestate -> stack_info list val get_top_stack : pftreestate -> stack_info list + +val get_last: Environ.env -> identifier diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 87a472003..02c688e25 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -166,11 +166,7 @@ let decompose_eq env id = | _ -> error "previous step is not an equality" let get_eq_typ info env = - let last_id = - match info.pm_last with - None -> error "no previous equality" - | Some (id,_) -> id in - let typ = decompose_eq env last_id in + let typ = decompose_eq env (get_last env) in typ let interp_constr_in_type typ sigma env c = @@ -352,8 +348,6 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let pat_vars,aliases,patt = interp_pattern env pat in let inject = function Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) - | Thesis (Sub n) -> - error "thesis[_] is not allowed here" | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" @@ -405,7 +399,7 @@ let interp_suffices_clause sigma env (hyps,cot)= This (c,_) -> let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc - | Thesis (Plain| Sub _) as th -> interp_hyps sigma env hyps,th + | Thesis Plain as th -> interp_hyps sigma env hyps,th | Thesis (For n) -> error "\"thesis for\" is not applicable here" in let push_one hyp env0 = match hyp with diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 4c526ecee..6ac4caad4 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -30,6 +30,7 @@ open Termops open Reductionops open Goptions + (* Strictness option *) let get_its_info gls = get_info gls.it @@ -81,40 +82,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 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] -> @@ -297,7 +292,29 @@ let justification tac 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; @@ -350,19 +367,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 @@ -382,83 +408,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 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 = @@ -466,11 +495,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 @@ -483,18 +511,18 @@ 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 @@ -514,11 +542,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 @@ -532,7 +557,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 @@ -547,14 +572,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 @@ -562,48 +587,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 = @@ -648,10 +654,6 @@ let assume_st_letin hyps gls = (* suffices *) -let free_meta info = - let max_next (i,_) j = if i >= j 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 @@ -679,31 +681,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 @@ -722,30 +714,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 -> @@ -753,7 +733,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") @@ -770,7 +750,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 @@ -829,35 +809,14 @@ let define_tac id args body 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 *) @@ -866,7 +825,7 @@ let start_tree env ind = Split (Idset.empty,ind,Array.map (fun _ -> None) constrs) 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 @@ -907,8 +866,7 @@ let per_tac etype casee gls= EK_dep (start_tree env per_info.per_ind) 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); @@ -917,12 +875,12 @@ let per_tac etype casee gls= 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 @@ -940,16 +898,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; @@ -1125,8 +1079,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 @@ -1157,21 +1110,17 @@ let rec register_dep_subcase id env per_info pat = function 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; @@ -1428,20 +1377,8 @@ let rec abstract_metas n avoid head = function 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 *) @@ -1476,7 +1413,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 @@ -1491,7 +1429,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 -> @@ -1503,7 +1441,7 @@ let rec postprocess pts instr = | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts - | Pescape -> escape_command pts + | Pescape -> pts | Pend (B_elim ET_Induction) -> begin let pf = proof_of_pftreestate pts in @@ -1535,7 +1473,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 diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 0d51cf979..0ad33455a 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -22,6 +22,8 @@ val automation_tac : tactic val daimon_subtree: pftreestate -> pftreestate +val concl_refiner: Termops.metamap -> constr -> Proof_type.goal sigma -> constr + val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate val proof_instr: Decl_expr.raw_proof_instr -> unit -- cgit v1.2.3