summaryrefslogtreecommitdiff
path: root/tactics/decl_proof_instr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/decl_proof_instr.ml')
-rw-r--r--tactics/decl_proof_instr.ml1476
1 files changed, 1476 insertions, 0 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
new file mode 100644
index 00000000..e7acd6d6
--- /dev/null
+++ b/tactics/decl_proof_instr.ml
@@ -0,0 +1,1476 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Pp
+open Evd
+
+open Refiner
+open Proof_type
+open Proof_trees
+open Tacmach
+open Tacinterp
+open Decl_expr
+open Decl_mode
+open Decl_interp
+open Rawterm
+open Names
+open Declarations
+open Tactics
+open Tacticals
+open Term
+open Termops
+open Reductionops
+open Goptions
+
+(* Strictness option *)
+
+let get_its_info gls = get_info gls.it
+
+let get_strictness,set_strictness =
+ let strictness = ref false in
+ (fun () -> (!strictness)),(fun b -> strictness:=b)
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "strict mode";
+ optkey = (SecondaryTable ("Strict","Proofs"));
+ optread = get_strictness;
+ optwrite = set_strictness }
+
+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
+ [pftree] ->
+ {pftree with
+ goal=gl;
+ ref=Some (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
+
+let tcl_erase_info gls = tcl_change_info_gen None gls
+
+let special_whd gl=
+ let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+ (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let special_nf gl=
+ let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
+ (fun t -> Closure.norm_val infos (Closure.inject t))
+
+let is_good_inductive env ind =
+ let mib,oib = Inductive.lookup_mind_specif env ind in
+ oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
+
+let check_not_per pts =
+ if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then
+ match get_stack pts with
+ Per (_,_,_,_)::_ ->
+ error "You are inside a proof per cases/induction.\n\
+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
+
+(* start a proof *)
+
+let start_proof_tac gls=
+ let gl=sig_it gls in
+ let info={pm_last=Anonymous;
+ pm_partial_goal=mkMeta 1;
+ pm_hyps=
+ begin
+ let hyps = pf_ids_of_hyps gls in
+ List.fold_right Idset.add hyps Idset.empty
+ end;
+ pm_subgoals= [1,gl.evar_concl];
+ pm_stack=[]} in
+ {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls},
+ function
+ [pftree] ->
+ {pftree with
+ goal=gl;
+ ref=Some (Decl_proof true,[pftree])}
+ | _ -> anomaly "Dem : Wrong number of subtrees"
+
+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
+ [] ->
+ {open_subgoals=0;
+ goal=sig_it gls;
+ ref=Some (Daimon,[])}
+ | _ -> anomaly "Daimon: Wrong number of subtrees")
+
+let daimon _ pftree =
+ set_daimon_flag ();
+ {pftree with
+ open_subgoals=0;
+ ref=Some (Daimon,[])}
+
+let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon )
+
+(* marking closed blocks *)
+
+let rec is_focussing_instr = function
+ Pthus i | Pthen i | Phence i -> is_focussing_instr i
+ | Pescape | Pper _ | Pclaim _ | Pfocus _
+ | Psuppose _ | Pcase (_,_,_) -> true
+ | _ -> false
+
+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) ->
+ if lock_focus then
+ Nested(Proof_instr (false,instr),spfl)
+ else
+ anomaly "already marked as done"
+ | _ -> anomaly "mark_rule_as_done"
+
+let mark_proof_tree_as_done pt =
+ match pt.ref with
+ None -> anomaly "mark_proof_tree_as_done"
+ | 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)
+ (traverse 0 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
+ 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 ->
+ 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 return_from_tactic_mode () = Pfedit.mutate close_tactic_mode
+
+(* end proof/claim *)
+
+let close_block bt pts =
+ let stack =
+ if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then
+ get_top_stack pts
+ else
+ get_stack pts in
+ match bt,stack with
+ B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
+ daimon_subtree (goto_current_focus pts)
+ | _, Claim::_ ->
+ error "\"end claim\" expected"
+ | _, Focus_claim::_ ->
+ error "\"end focus\" expected"
+ | _, [] ->
+ error "\"end proof\" expected"
+ | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
+ begin
+ match et with
+ ET_Case_analysis -> error "\"end cases\" expected"
+ | ET_Induction -> error "\"end induction\" expected"
+ end
+ | _,_ -> anomaly "lonely suppose on stack"
+
+(* utility for suppose / suppose it is *)
+
+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,_,_,_) :: _ ->
+ goto_current_focus (mark_as_done pts)
+ | _ -> error "Not inside a proof per cases or induction."
+ else
+ match get_stack pts with
+ 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."
+
+(* Proof instructions *)
+
+(* automation *)
+
+let filter_hyps f gls =
+ let filter_aux (id,_,_) =
+ if f id then
+ tclIDTAC
+ else
+ tclTRY (clear [id]) in
+ tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls
+
+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 ->
+ keep:=Idset.add id !keep;
+ tclIDTAC 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
+ tclMAP add_aux items gls
+
+let apply_to_prepared_goal items kont gls =
+ let tokeep = ref Idset.empty in
+ let auxres = add_justification_hyps tokeep items gls in
+ tclTHENLIST
+ [ (fun _ -> auxres);
+ filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep);
+ kont ] gls
+
+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 [tac])
+ (fun gls ->
+ if get_strictness () then
+ error "insufficient justification"
+ else
+ begin
+ msgnl (str "Warning: insufficient justification");
+ daimon_tac gls
+ end) gls
+
+let default_justification items gls=
+ justification (apply_to_prepared_goal items automation_tac) gls
+
+(* code for have/then/thus/hence *)
+
+type stackd_elt =
+{se_meta:metavariable;
+ se_type:types;
+ se_last_meta:metavariable;
+ se_meta_list:(metavariable*types) list;
+ se_evd: evar_defs}
+
+let rec replace_in_list m l = function
+ [] -> raise Not_found
+ | c::q -> if m=fst c then l@q else c::replace_in_list m l q
+
+let enstack_subsubgoals env se stack gls=
+ let hd,params = decompose_app (special_whd gls se.se_type) in
+ match kind_of_term hd with
+ Ind ind when is_good_inductive env ind ->
+ let mib,oib=
+ 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)
+ (* 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
+ [] -> (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) =
+ 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 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
+ {se_meta=m;
+ se_type=typ;
+ se_evd=evd0;
+ se_meta_list=ncreated;
+ se_last_meta=nlast} stack) (List.rev nmetas)
+ in
+ Array.iteri process gentypes
+ | _ -> ()
+
+let find_subsubgoal env c ctyp skip evd metas gls =
+ let stack = Stack.create () in
+ let max_meta =
+ List.fold_left (fun a (m,_) -> max a m) 0 metas 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
+ let rec dfs n =
+ let se = Stack.pop stack in
+ try
+ let unifier =
+ 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}
+ else
+ dfs (pred n)
+ with _ ->
+ begin
+ enstack_subsubgoals env se stack 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
+
+let thus_tac c ctyp gls =
+ let info = get_its_info gls in
+ let evd0 = mk_evd info.pm_subgoals gls in
+ let list,evd =
+ try
+ find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals 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
+
+let anon_id_base = id_of_string "__"
+
+
+let mk_stat_or_thesis info = 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."
+
+let instr_cut mkstat _thus _then cut gls0 =
+ let info = get_its_info gls0 in
+ let just_tac gls =
+ match cut.cut_by with
+ Automated l ->
+ let elems =
+ if _then then
+ match info.pm_last with
+ Anonymous -> l
+ | Name id -> (mkVar id) ::l
+ else l in
+ default_justification elems gls
+ | By_tactic t ->
+ justification (Tacinterp.eval_tactic t) gls in
+ let c_id = match cut.cut_stat.st_label with
+ Anonymous ->
+ pf_get_new_id (id_of_string "_fact") gls0
+ | Name id -> id in
+ let c_stat = mkstat info cut.cut_stat.st_it in
+ let thus_tac gls=
+ if _thus then
+ thus_tac (mkVar c_id) c_stat gls
+ else tclIDTAC gls in
+ let ninfo = {info with pm_last=Name c_id} in
+ tclTHENS (internal_cut c_id c_stat)
+ [tclTHEN tcl_erase_info just_tac;
+ tclTHEN (tcl_change_info ninfo) thus_tac] gls0
+
+(* iterated equality *)
+let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+
+let decompose_eq id gls =
+ let typ = pf_get_hyp_typ gls id in
+ 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
+ then (args.(0),
+ 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 info = get_its_info gls0 in
+ let last_id =
+ match info.pm_last with
+ Anonymous -> error "no previous equality"
+ | Name id -> id in
+ let typ,lhs,rhs = decompose_eq last_id gls0 in
+ let just_tac gls =
+ match cut.cut_by with
+ Automated l ->
+ let elems = (mkVar last_id) :: l in
+ default_justification elems gls
+ | By_tactic t ->
+ justification (Tacinterp.eval_tactic t) gls in
+ let c_id = match cut.cut_stat.st_label with
+ Anonymous ->
+ pf_get_new_id (id_of_string "_eq") gls0
+ | Name id -> id in
+ let ninfo = {info with pm_last=Name c_id} in
+ 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
+ Lhs ->
+ let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
+ tclTHENS (internal_cut c_id new_eq)
+ [tclTHEN tcl_erase_info
+ (tclTHENS (transitivity lhs)
+ [just_tac;exact_check (mkVar last_id)]);
+ tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+ | Rhs ->
+ let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
+ tclTHENS (internal_cut c_id new_eq)
+ [tclTHEN tcl_erase_info
+ (tclTHENS (transitivity rhs)
+ [exact_check (mkVar last_id);just_tac]);
+ tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+
+
+
+(* 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
+ | Name id -> id 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 ninfo2 = {info with pm_last=Name id} in
+ tclTHENS (internal_cut id st.st_it)
+ [tcl_change_info ninfo1;
+ tclTHEN (tcl_change_info ninfo2) thus_tac] gls0
+
+(* 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 set_last id gls =
+ let info = get_its_info gls in
+ tcl_change_info
+ {info with
+ pm_last=Name id} gls
+
+let intro_pm id gls=
+ let info = get_its_info gls in
+ 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 =
+ match nam with
+ Anonymous -> pf_get_new_id (id_of_string "_hyp") gls
+ | Name id -> id in
+ let mark_id gls0 =
+ let info = get_its_info gls0 in
+ let ninfo = {info with
+ pm_last = Name hid;
+ pm_hyps = Idset.add hid info.pm_hyps } in
+ tcl_change_info ninfo gls0 in
+ tclTHENLIST
+ [intro_pm hid;
+ coerce hid;
+ mark_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 ->
+ convert_hyp (id,None,c)) nam)
+ | Hprop {st_label=nam;st_it=Thesis (tk)} ->
+ tclTHEN
+ (push_intro_tac
+ (fun id -> tclIDTAC) nam))
+ hyps tclIDTAC gls
+
+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 ->
+ convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
+ hyps tclIDTAC gls
+
+(* 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
+ let env =pf_env gls in
+ match kind_of_term hd with
+ Ind ind when is_good_inductive env ind ->
+ let mib,oib=
+ Inductive.lookup_mind_specif env ind in
+ let gentypes=
+ Inductive.arities_of_constructors ind (mib,oib) in
+ let _ = if Array.length gentypes <> 1 then raise Not_found in
+ let apptype = Term.prod_applist gentypes.(0) params in
+ let rc,_ = Reduction.dest_prod env apptype in
+ List.length rc
+ | _ -> raise Not_found
+
+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
+ 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
+ [],[] ->
+ if not may_intro then
+ set_last (List.hd introduced) gls
+ else
+ let info = get_its_info gls in
+ let nameset=List.fold_right Idset.add introduced info.pm_hyps in
+ tcl_change_info {info with
+ pm_last = Name (List.hd introduced);
+ pm_hyps = nameset} gls
+ | _,[] -> error "last statements do not match a complete hypothesis"
+ (* should tell which ones *)
+ | [],hyps ->
+ if may_intro then
+ begin
+ let id = pf_get_new_id (id_of_string "_tmp") gls in
+ tclIFTHENELSE
+ (intro_pm id)
+ (consider_match true [] [id] hyps)
+ (fun _ ->
+ error "not enough sub-hypotheses to match statements")
+ 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 ->
+ consider_match may_intro (id::introduced) rest_ids rest
+ | Name hid ->
+ tclTHENLIST
+ [pm_rename_hyp id hid;
+ consider_match may_intro (hid::introduced) rest_ids rest]
+ end
+ begin
+ (fun gls ->
+ let nhyps =
+ try conjunction_arity id gls with
+ Not_found -> error "matching hypothesis not found" in
+ tclTHENLIST
+ [general_case_analysis (mkVar id,NoBindings);
+ intron_then nhyps []
+ (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
+ | _ ->
+ let id = pf_get_new_id (id_of_string "_tmp") gls in
+ tclTHEN
+ (forward None (Genarg.IntroIdentifier id) c)
+ (consider_match false [] [id] hyps) gls
+
+
+let given_tac hyps gls =
+ consider_match true [] [] hyps gls
+
+(* tactics for take *)
+
+let rec take_tac wits gls =
+ match wits with
+ [] -> tclIDTAC gls
+ | 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 ->
+ 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
+
+let define_tac id args body gls =
+ let t = build_function args body in
+ letin_tac true (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."
+
+
+(* 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 build_per_info etype casee gls =
+ let concl=get_thesis gls in
+ let env=pf_env gls in
+ let ctyp=pf_type_of gls casee in
+ let is_dep = dependent casee concl in
+ let hd,args = decompose_app (special_whd gls ctyp) in
+ let ind =
+ try
+ 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 params,real_args = list_chop nparams args in
+ let abstract_obj body c =
+ let typ=pf_type_of gls c in
+ lambda_create env (typ,subst_term c body) in
+ let pred= List.fold_left abstract_obj
+ (lambda_create env (ctyp,subst_term casee concl)) real_args in
+ is_dep,
+ {per_casee=casee;
+ per_ctype=ctyp;
+ per_ind=ind;
+ per_pred=pred;
+ per_args=real_args;
+ per_params=params;
+ per_nparams=nparams}
+
+let per_tac etype casee gls=
+ let env=pf_env gls in
+ let info = get_its_info gls in
+ match casee with
+ Real c ->
+ 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)
+ else EK_unknown in
+ tcl_change_info
+ {info with
+ 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 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)
+ (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=
+ Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
+ gls
+
+(* suppose *)
+
+let rec build_product args body =
+ 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 -> body
+ | Name id -> subst_term (mkVar id) pprod in
+ mkProd (st.st_label, st.st_it, lbody)
+ | [] -> body
+
+let register_nodep_subcase id= function
+ Per(et,pi,ek,clauses)::s ->
+ begin
+ match ek with
+ EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+ | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+ | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
+ end
+ | _ -> anomaly "wrong stack state"
+
+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 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 old_clauses,stack = register_nodep_subcase id info.pm_stack in
+ let ninfo2 = {info with
+ pm_stack=stack} in
+ tclTHENS (internal_cut id clause)
+ [tclTHENLIST [tcl_change_info ninfo1;
+ assume_tac hyps;
+ clear old_clauses];
+ tcl_change_info ninfo2] gls0
+
+(* suppose it is ... *)
+
+(* 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 tree_of_pats env ((id,_) as cpl) pats =
+ match pats with
+ [] -> End_of_branch cpl
+ | args::stack ->
+ match args with
+ [] -> Pop (tree_of_pats env cpl stack)
+ | patt :: 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=
+ match pats with
+ [] ->
+ begin
+ match tree with
+ End_of_branch cpl0 -> End_of_branch cpl0
+ (* this ensures precedence *)
+ | _ -> 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)
+ | _ -> anomaly "we should pop here"
+ end
+ | patt :: 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)
+ | _ -> 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) ->
+ 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)
+ | _ -> anomaly "No pop/stop expected here"
+and append_branch env ((id,_) as cpl) depth pats nargs = function
+ Some (ids,tree) ->
+ Some (Idset.add id ids,append_tree env 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
+ 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)
+
+(* suppose it is *)
+
+let rec st_assoc id = function
+ [] -> raise Not_found
+ | st::_ when st.st_label = id -> st.st_it
+ | _ :: rest -> st_assoc id rest
+
+let thesis_for obj typ per_info env=
+ let rc,hd1=decompose_prod typ in
+ 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
+ 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 () ++
+ 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 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=
+ lift 1 (build_product_dep pat_info per_info rest body gls) in
+ let lbody =
+ match nam with
+ Anonymous -> body
+ | Name id -> subst_var id pprod in
+ mkProd (nam,c,lbody)
+ | Hprop ({st_it=Thesis tk} as st)::rest ->
+ let pprod=
+ lift 1 (build_product_dep pat_info per_info rest body gls) in
+ let lbody =
+ match st.st_label with
+ Anonymous -> body
+ | Name id -> subst_var id pprod in
+ let ptyp =
+ match tk with
+ For id ->
+ let obj = mkVar id in
+ 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 -> get_thesis gls
+ | Sub n -> anomaly "Subthesis in cases" in
+ mkProd (st.st_label,ptyp,lbody)
+ | [] -> body
+
+let build_dep_clause params pat_info per_info hyps gls =
+ let concl=
+ thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in
+ let open_clause =
+ build_product_dep pat_info per_info hyps concl gls in
+ let prod_one st body =
+ match st.st_label with
+ Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body)
+ | Name id -> mkNamedProd id st.st_it (lift 1 body) in
+ 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 ->
+ mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
+ 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 ->
+ 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)
+
+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)
+ | _ -> 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 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
+ tclTHENS (internal_cut 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;
+ clear old_clauses];
+ tcl_change_info ninfo2] gls0
+
+(* end cases *)
+
+type instance_stack =
+ (constr option*bool*(constr list) list) list
+
+let initial_instance_stack ids =
+ List.map (fun id -> id,[None,false,[]]) ids
+
+let push_one_arg arg = function
+ [] -> anomaly "impossible"
+ | (head,is_rec,args) :: ctx ->
+ ((head,is_rec,(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 head = if Idset.mem id ids then Some c else None in
+ id,(head,is_rec,[]) :: stack
+
+let push_head c is_rec ids stacks =
+ List.map (push_one_head c is_rec ids) stacks
+
+let pop_one rec_flag (id,stack) =
+ let nstack=
+ match stack with
+ [] -> anomaly "impossible"
+ | [c] as l -> l
+ | (Some head,is_rec,args)::(head0,is_rec0,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
+ 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
+
+let patvar_base = id_of_string "__"
+
+let test_fun (str:string) = ()
+
+let hrec_for obj_id fix_id per_info gls=
+ 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
+
+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,_)=destProd (pf_concl gls) in
+ let hd,args=decompose_app (special_whd gls typ) in
+ let _ = assert (ind = destInd hd) in
+ 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_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 end_tac et2 gls =
+ let info = get_its_info gls in
+ let et1,pi,ek,clauses =
+ match info.pm_stack with
+ Suppose_case::_ ->
+ anomaly "This case should already be trapped"
+ | Claim::_ ->
+ error "\"end claim\" expected."
+ | Focus_claim::_ ->
+ error "\"end focus\" expected."
+ | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
+ | [] ->
+ anomaly "This case should already be trapped" in
+ let et =
+ if et1 <> et2 then
+ match et1 with
+ ET_Case_analysis ->
+ error "\"end cases\" expected."
+ | ET_Induction ->
+ error "\"end induction\" expected."
+ else et1 in
+ tclTHEN
+ tcl_erase_info
+ begin
+ match et,ek with
+ _,EK_unknown ->
+ tclSOLVE [simplest_elim pi.per_casee]
+ | ET_Case_analysis,EK_nodep ->
+ tclTHEN
+ (general_case_analysis (pi.per_casee,NoBindings))
+ (default_justification (List.map mkVar clauses))
+ | ET_Induction,EK_nodep ->
+ tclTHENLIST
+ [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 ->
+ tclTHENLIST
+ [generalize (pi.per_args@[pi.per_casee]);
+ execute_cases true Anonymous pi
+ (fun c -> tclTHENLIST
+ [refine c;
+ clear clauses;
+ justification assumption])
+ (initial_instance_stack clauses) 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
+ end gls
+
+(* escape *)
+
+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 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)
+
+(* General instruction engine *)
+
+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 ->
+ assert (not _then);
+ do_proof_instr_gen _thus true 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
+ | Prew (s,c) ->
+ assert (not _then);
+ instr_rew _thus s c
+ | Pconsider (c,hyps) -> consider_tac c hyps
+ | Pgiven hyps -> given_tac hyps
+ | Passume hyps -> assume_tac hyps
+ | Plet hyps -> assume_tac hyps
+ | 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
+ | 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"
+
+let eval_instr {instr=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
+ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _
+ | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _
+ | Pdefine (_,_,_) | Pper _ | Prew _ ->
+ check_not_per pts;
+ true,pts
+ | Pescape ->
+ check_not_per pts;
+ false,pts
+ | Pcase _ | Psuppose _ | Pend (B_elim _) ->
+ true,close_previous_case pts
+ | 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 _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
+ | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
+ | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
+ | Pescape ->
+ escape_command pts
+ | 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 =
+ 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 = [];
+ gsigma = sigma; genv = env} in
+ let glob_instr = intern_proof_instr ist raw_instr in
+ 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
+ (abstract_operation marker (eval_instr instr)) pts1
+ else pts1 in
+ postprocess pts2 raw_instr.instr
+
+let proof_instr raw_instr =
+ Pfedit.mutate (do_instr raw_instr)
+
+(*
+
+(* STUFF FOR ITERATED RELATIONS *)
+let decompose_bin_app t=
+ let hd,args = destApp
+
+let identify_transitivity_lemma c =
+ let varx,tx,c1 = destProd c in
+ let vary,ty,c2 = destProd (pop c1) in
+ let varz,tz,c3 = destProd (pop c2) in
+ let _,p1,c4 = destProd (pop c3) in
+ let _,lp2,lp3 = destProd (pop c4) in
+ let p2=pop lp2 in
+ let p3=pop lp3 in
+*)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 00:17:03 +0000