diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 671 |
1 files changed, 466 insertions, 205 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dcc70edb..cf2126f8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,37 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names open Term open Termops -open Sign +open Context open Declarations -open Inductive -open Reduction -open Environ -open Libnames -open Refiner open Tacmach open Clenv -open Clenvtac -open Glob_term -open Pattern -open Matching -open Genarg -open Tacexpr +open Misctypes (************************************************************************) (* Tacticals re-exported from the Refiner module *) (************************************************************************) -let tclNORMEVAR = Refiner.tclNORMEVAR let tclIDTAC = Refiner.tclIDTAC let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE let tclORELSE0 = Refiner.tclORELSE0 @@ -58,9 +48,9 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO -let tclTIMEOUT = Refiner.tclTIMEOUT let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS let tclPROGRESS = Refiner.tclPROGRESS +let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL let tclTHENTRY = Refiner.tclTHENTRY let tclIFTHENELSE = Refiner.tclIFTHENELSE @@ -72,13 +62,6 @@ let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST let tclTHENSEQ = tclTHENLIST -(* Experimental *) - -let rec tclFIRST_PROGRESS_ON tac = function - | [] -> tclFAIL 0 (str "No applicable tactic") - | [a] -> tac a (* so that returned failure is the one from last item *) - | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl) - (************************************************************************) (* Tacticals applying on hypotheses *) (************************************************************************) @@ -95,7 +78,7 @@ let lastHypId gl = nthHypId 1 gl let lastHyp gl = nthHyp 1 gl let nLastDecls n gl = - try list_firstn n (pf_hyps gl) + try List.firstn n (pf_hyps gl) with Failure _ -> error "Not enough hypotheses in the goal." let nLastHypsId n gl = List.map pi1 (nLastDecls n gl) @@ -116,7 +99,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac let onNLastHyps n tac = onHyps (nLastHyps n) tac let afterHyp id gl = - fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl)) + fst (List.split_when (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl)) (***************************************) (* Clause Tacticals *) @@ -130,53 +113,17 @@ let afterHyp id gl = --Eduardo (8/8/97) *) -(* A [simple_clause] is a set of hypotheses, possibly extended with - the conclusion (conclusion is represented by None) *) - -type simple_clause = identifier option list - -(* An [clause] is the algebraic form of a - [concrete_clause]; it may refer to all hypotheses - independently of the effective contents of the current goal *) - -type clause = identifier gclause - -let allHypsAndConcl = { onhyps=None; concl_occs=all_occurrences_expr } -let allHyps = { onhyps=None; concl_occs=no_occurrences_expr } -let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr } -let onHyp id = - { onhyps=Some[((all_occurrences_expr,id),InHyp)]; - concl_occs=no_occurrences_expr } - -let simple_clause_of cl gls = - let error_occurrences () = - error "This tactic does not support occurrences selection" in - let error_body_selection () = - error "This tactic does not support body selection" in - let hyps = - match cl.onhyps with - | None -> - List.map Option.make (pf_ids_of_hyps gls) - | Some l -> - List.map (fun ((occs,id),w) -> - if occs <> all_occurrences_expr then error_occurrences (); - if w = InHypValueOnly then error_body_selection (); - Some id) l in - if cl.concl_occs = no_occurrences_expr then hyps - else - if cl.concl_occs <> all_occurrences_expr then error_occurrences () - else None :: hyps - let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl -let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl -let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl - -let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls -let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls +let onClause tac cl gls = + let hyps () = pf_ids_of_hyps gls in + tclMAP tac (Locusops.simple_clause_of hyps cl) gls +let onClauseLR tac cl gls = + let hyps () = pf_ids_of_hyps gls in + tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls let ifOnHyp pred tac1 tac2 id gl = if pred (id,pf_get_hyp_typ gl id) then @@ -184,52 +131,6 @@ let ifOnHyp pred tac1 tac2 id gl = else tac2 id gl - -(************************************************************************) -(* An intermediate form of occurrence clause that select components *) -(* of a definition, hypotheses and possibly the goal *) -(* (used for reduction tactics) *) -(************************************************************************) - -(* A [hyp_location] is an hypothesis together with a position, in - body if any, in type or in both *) - -type hyp_location = identifier * hyp_location_flag - -(* A [goal_location] is either an hypothesis (together with a position, in - body if any, in type or in both) or the goal *) - -type goal_location = hyp_location option - -(************************************************************************) -(* An intermediate structure for dealing with occurrence clauses *) -(************************************************************************) - -(* [clause_atom] refers either to an hypothesis location (i.e. an - hypothesis with occurrences and a position, in body if any, in type - or in both) or to some occurrences of the conclusion *) - -type clause_atom = - | OnHyp of identifier * occurrences_expr * hyp_location_flag - | OnConcl of occurrences_expr - -(* A [concrete_clause] is an effective collection of - occurrences in the hypotheses and the conclusion *) - -type concrete_clause = clause_atom list - -let concrete_clause_of cl gls = - let hyps = - match cl.onhyps with - | None -> - let f id = OnHyp (id,all_occurrences_expr,InHyp) in - List.map f (pf_ids_of_hyps gls) - | Some l -> - List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in - if cl.concl_occs = no_occurrences_expr then hyps - else - OnConcl cl.concl_occs :: hyps - (************************************************************************) (* Elimination Tacticals *) (************************************************************************) @@ -243,14 +144,14 @@ let concrete_clause_of cl gls = the elimination. *) type branch_args = { - ity : inductive; (* the type we were eliminating on *) + ity : pinductive; (* the type we were eliminating on *) largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) nassums : int; (* the number of assumptions to be introduced *) branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) - branchnames : intro_pattern_expr located list} + branchnames : Tacexpr.intro_patterns} type branch_assumptions = { ba : branch_args; (* the branch args *) @@ -261,11 +162,13 @@ let fix_empty_or_and_pattern nv l = names and "[ ]" for no clause at all *) (* 2- More generally, we admit "[ ]" for any disjunctive pattern of arbitrary length *) - if l = [[]] then list_make nv [] else l + match l with + | [[]] -> List.make nv [] + | _ -> l let check_or_and_pattern_size loc names n = - if List.length names <> n then - if n = 1 then + if not (Int.equal (List.length names) n) then + if Int.equal n 1 then user_err_loc (loc,"",str "Expects a conjunctive pattern.") else user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n @@ -274,31 +177,29 @@ let check_or_and_pattern_size loc names n = let compute_induction_names n = function | None -> Array.make n [] - | Some (loc,IntroOrAndPattern names) -> + | Some (loc,names) -> let names = fix_empty_or_and_pattern n names in check_or_and_pattern_size loc names n; Array.of_list names - | Some (loc,_) -> - user_err_loc (loc,"",str "Disjunctive/conjunctive introduction pattern expected.") -let compute_construtor_signatures isrec (_,k as ity) = +let compute_construtor_signatures isrec ((_,k as ity),u) = let rec analrec c recargs = match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> - let b = match dest_recarg recarg with + let b = match Declareops.dest_recarg recarg with | Norec | Imbr _ -> false - | Mrec (_,j) -> isrec & j=k + | Mrec (_,j) -> isrec && Int.equal j k in b :: (analrec c rest) | LetIn (_,_,_,c), rest -> false :: (analrec c rest) | _, [] -> [] - | _ -> anomaly "compute_construtor_signatures" + | _ -> anomaly (Pp.str "compute_construtor_signatures") in let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in let lc = Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in - let lrecargs = dest_subterms mip.mind_recargs in - array_map2 analrec lc lrecargs + let lrecargs = Declareops.dest_subterms mip.mind_recargs in + Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = pf_apply Retyping.get_sort_family_of gl (pf_concl gl) @@ -310,67 +211,19 @@ let elimination_sort_of_clause = function | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id -(* Find the right elimination suffix corresponding to the sort of the goal *) -(* c should be of type A1->.. An->B with B an inductive definition *) - -let general_elim_then_using mk_elim - isrec allnames tac predicate (indbindings,elimbindings) - ind indclause gl = - let elim = mk_elim ind gl in - (* applying elimination_scheme just a little modified *) - let indclause' = clenv_match_args indbindings indclause in - let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in - let indmv = - match kind_of_term (last_arg elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> anomaly "elimination" - in - let pmv = - let p, _ = decompose_app elimclause.templtyp.Evd.rebus in - match kind_of_term p with - | Meta p -> p - | _ -> - let name_elim = - match kind_of_term elim with - | Const kn -> string_of_con kn - | Var id -> string_of_id id - | _ -> "\b" - in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") - in - let elimclause' = clenv_fchain indmv elimclause indclause' in - let elimclause' = clenv_match_args elimbindings elimclause' in - let branchsigns = compute_construtor_signatures isrec ind in - let brnames = compute_induction_names (Array.length branchsigns) allnames in - let after_tac ce i gl = - let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = - List.fold_left - (fun acc b -> if b then acc+2 else acc+1) - 0 branchsigns.(i); - branchnum = i+1; - ity = ind; - largs = List.map (clenv_nf_meta ce) largs; - pred = clenv_nf_meta ce hd } - in - tac ba gl - in - let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> - clenv_unify ~flags:Unification.elim_flags - Reduction.CONV (mkMeta pmv) p elimclause' - in - elim_res_pf_THEN_i elimclause' branchtacs gl + +let pf_with_evars glsev k gls = + let evd, a = glsev gls in + tclTHEN (Refiner.tclEVARS evd) (k a) gls + +let pf_constr_of_global gr k = + pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k (* computing the case/elim combinators *) let gl_make_elim ind gl = - Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) + let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in + pf_apply Evd.fresh_global gl gr let gl_make_case_dep ind gl = pf_apply Indrec.build_case_analysis_scheme gl ind true @@ -380,22 +233,6 @@ let gl_make_case_nodep ind gl = pf_apply Indrec.build_case_analysis_scheme gl ind false (elimination_sort_of_goal gl) -let elimination_then_using tac predicate bindings c gl = - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - let indclause = mk_clenv_from gl (c,t) in - general_elim_then_using gl_make_elim - true None tac predicate bindings ind indclause gl - -let case_then_using = - general_elim_then_using gl_make_case_dep false - -let case_nodep_then_using = - general_elim_then_using gl_make_case_nodep false - -let elimination_then tac = elimination_then_using tac None -let simple_elimination_then tac = elimination_then tac ([],[]) - - let make_elim_branch_assumptions ba gl = let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc = match lb,lc with @@ -414,11 +251,11 @@ let make_elim_branch_assumptions ba gl = id::constargs, recargs, indargs) tl idtl - | (_, _) -> anomaly "make_elim_branch_assumptions" + | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions") in makerec ([],[],[],[],[]) ba.branchsign - (try list_firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly "make_elim_branch_assumptions") + (try List.firstn ba.nassums (pf_hyps gl) + with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions")) let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl @@ -438,11 +275,435 @@ let make_case_branch_assumptions ba gl = id::cargs, recargs, id::constargs) tl idtl - | (_, _) -> anomaly "make_case_branch_assumptions" + | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions") in makerec ([],[],[],[]) ba.branchsign - (try list_firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly "make_case_branch_assumptions") + (try List.firstn ba.nassums (pf_hyps gl) + with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions")) let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl + +(** Tacticals of Ltac defined directly in term of Proofview *) +module New = struct + open Proofview + open Proofview.Notations + open Tacmach.New + + let tclIDTAC = tclUNIT () + + let tclTHEN t1 t2 = + t1 <*> t2 + + let tclFAIL lvl msg = + tclZERO (Refiner.FailError (lvl,lazy msg)) + + let tclZEROMSG ?loc msg = + let err = UserError ("", msg) in + let info = match loc with + | None -> Exninfo.null + | Some loc -> Loc.add_loc Exninfo.null loc + in + tclZERO ~info err + + let catch_failerror e = + try + Refiner.catch_failerror e; + tclUNIT () + with e -> tclZERO e + + (* spiwack: I chose to give the Ltac + the same semantics as + [Proofview.tclOR], however, for consistency with the or-else + tactical, we may consider wrapping the first argument with + [tclPROGRESS]. It strikes me as a bad idea, but consistency can be + considered valuable. *) + let tclOR t1 t2 = + tclINDEPENDENT begin + Proofview.tclOR + t1 + begin fun e -> + catch_failerror e <*> t2 + end + end + + let tclORD t1 t2 = + tclINDEPENDENT begin + Proofview.tclOR + t1 + begin fun e -> + catch_failerror e <*> t2 () + end + end + + let tclONCE = Proofview.tclONCE + + let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t + + let tclIFCATCH t tt te = + tclINDEPENDENT begin + Proofview.tclIFCATCH t + tt + (fun e -> catch_failerror e <*> te ()) + end + + let tclORELSE0 t1 t2 = + tclINDEPENDENT begin + tclORELSE + t1 + begin fun e -> + catch_failerror e <*> t2 + end + end + let tclORELSE t1 t2 = + tclORELSE0 (tclPROGRESS t1) t2 + + let tclTHENS3PARTS t1 l1 repeat l2 = + tclINDEPENDENT begin + t1 <*> + Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) + begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end + begin function (e, info) -> match e with + | SizeMismatch (i,_)-> + let errmsg = + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str")" + in + tclFAIL 0 errmsg + | reraise -> tclZERO ~info reraise + end + end + let tclTHENSFIRSTn t1 l repeat = + tclTHENS3PARTS t1 l repeat [||] + let tclTHENFIRSTn t1 l = + tclTHENSFIRSTn t1 l (tclUNIT()) + let tclTHENFIRST t1 t2 = + tclTHENFIRSTn t1 [|t2|] + let tclTHENLASTn t1 l = + tclTHENS3PARTS t1 [||] (tclUNIT()) l + let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] + let tclTHENS t l = + tclINDEPENDENT begin + t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) + begin tclDISPATCH l end + begin function (e, info) -> match e with + | SizeMismatch (i,_)-> + let errmsg = + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str")" + in + tclFAIL 0 errmsg + | reraise -> tclZERO ~info reraise + end + end + let tclTHENLIST l = + List.fold_left tclTHEN (tclUNIT()) l + + + (* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) + let tclMAP tacfun l = + List.fold_right (fun x -> (tclTHEN (tacfun x))) l (tclUNIT()) + + let tclTRY t = + tclORELSE0 t (tclUNIT ()) + + let tclIFTHENELSE t1 t2 t3 = + tclINDEPENDENT begin + Proofview.tclIFCATCH t1 + (fun () -> t2) + (fun (e, info) -> Proofview.tclORELSE t3 (fun e' -> tclZERO ~info e)) + end + let tclIFTHENSVELSE t1 a t3 = + Proofview.tclIFCATCH t1 + (fun () -> tclDISPATCH (Array.to_list a)) + (fun _ -> t3) + let tclIFTHENTRYELSEMUST t1 t2 = + tclIFTHENELSE t1 (tclTRY t2) t2 + + (* Try the first tactic that does not fail in a list of tactics *) + let rec tclFIRST = function + | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic.")) + | t::rest -> tclORELSE0 t (tclFIRST rest) + + let rec tclFIRST_PROGRESS_ON tac = function + | [] -> tclFAIL 0 (str "No applicable tactic") + | [a] -> tac a (* so that returned failure is the one from last item *) + | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl) + + let rec tclDO n t = + if n < 0 then + tclZERO (Errors.UserError ( + "Refiner.tclDO", + str"Wrong argument : Do needs a positive integer.") + ) + else if n = 0 then tclUNIT () + else if n = 1 then t + else tclTHEN t (tclDO (n-1) t) + + let rec tclREPEAT0 t = + tclINDEPENDENT begin + Proofview.tclIFCATCH t + (fun () -> tclCHECKINTERRUPT <*> tclREPEAT0 t) + (fun e -> catch_failerror e <*> tclUNIT ()) + end + let tclREPEAT t = + tclREPEAT0 (tclPROGRESS t) + let rec tclREPEAT_MAIN0 t = + Proofview.tclIFCATCH t + (fun () -> tclTRYFOCUS 1 1 (tclREPEAT_MAIN0 t)) + (fun e -> catch_failerror e <*> tclUNIT ()) + let tclREPEAT_MAIN t = + tclREPEAT_MAIN0 (tclPROGRESS t) + + let tclCOMPLETE t = + t >>= fun res -> + (tclINDEPENDENT + (tclZERO (Errors.UserError ("",str"Proof is not complete."))) + ) <*> + tclUNIT res + + (* Try the first thats solves the current goal *) + let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) + + let tclPROGRESS t = + Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) + + (* Check that holes in arguments have been resolved *) + + let check_evars env sigma extsigma origsigma = + let rec is_undefined_up_to_restriction sigma evk = + let evi = Evd.find sigma evk in + match Evd.evar_body evi with + | Evd.Evar_empty -> Some (evk,evi) + | Evd.Evar_defined c -> match Term.kind_of_term c with + | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | _ -> + (* We make the assumption that there is no way to refine an + evar remaining after typing from the initial term given to + apply/elim and co tactics, is it correct? *) + None in + let rest = + Evd.fold_undefined (fun evk evi acc -> + match is_undefined_up_to_restriction sigma evk with + | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc + | _ -> acc) + extsigma [] + in + match rest with + | [] -> () + | (evk,evi) :: _ -> + let (loc,_) = evi.Evd.evar_source in + Pretype_errors.error_unsolvable_implicit loc env sigma evk None + + let tclWITHHOLES accept_unresolved_holes tac sigma x = + tclEVARMAP >>= fun sigma_initial -> + if sigma == sigma_initial then tac x + else + let check_evars env new_sigma sigma initial_sigma = + try + check_evars env new_sigma sigma initial_sigma; + tclUNIT () + with e when Errors.noncritical e -> + tclZERO e + in + let check_evars_if = + if not accept_unresolved_holes then + tclEVARMAP >>= fun sigma_final -> + tclENV >>= fun env -> + check_evars env sigma_final sigma sigma_initial + else + tclUNIT () + in + Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if + + let tclTIMEOUT n t = + Proofview.tclOR + (Proofview.tclTIMEOUT n t) + begin function (e, info) -> match e with + | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e))) + | e -> Proofview.tclZERO ~info e + end + + let tclTIME s t = + Proofview.tclTIME s t + + let nthDecl m gl = + let hyps = Proofview.Goal.hyps gl in + try + List.nth hyps (m-1) + with Failure _ -> Errors.error "No such assumption." + + let nLastDecls gl n = + try List.firstn n (Proofview.Goal.hyps gl) + with Failure _ -> error "Not enough hypotheses in the goal." + + let nthHypId m gl = + (** We only use [id] *) + let gl = Proofview.Goal.assume gl in + let (id,_,_) = nthDecl m gl in + id + let nthHyp m gl = + mkVar (nthHypId m gl) + + let onNthHypId m tac = + Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end + let onNthHyp m tac = + Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end + + let onLastHypId = onNthHypId 1 + let onLastHyp = onNthHyp 1 + + let onNthDecl m tac = + Proofview.Goal.nf_enter begin fun gl -> + Proofview.tclUNIT (nthDecl m gl) >>= tac + end + let onLastDecl = onNthDecl 1 + + let ifOnHyp pred tac1 tac2 id = + Proofview.Goal.nf_enter begin fun gl -> + let typ = Tacmach.New.pf_get_hyp_typ id gl in + if pred (id,typ) then + tac1 id + else + tac2 id + end + + let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl)) + + let afterHyp id tac = + Proofview.Goal.nf_enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in + tac rem + end + + let fullGoal gl = + let hyps = Tacmach.New.pf_ids_of_hyps gl in + None :: List.map Option.make hyps + + let tryAllHyps tac = + Proofview.Goal.enter begin fun gl -> + let hyps = Tacmach.New.pf_ids_of_hyps gl in + tclFIRST_PROGRESS_ON tac hyps + end + let tryAllHypsAndConcl tac = + Proofview.Goal.enter begin fun gl -> + tclFIRST_PROGRESS_ON tac (fullGoal gl) + end + + let onClause tac cl = + Proofview.Goal.enter begin fun gl -> + let hyps = Tacmach.New.pf_ids_of_hyps gl in + tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) + end + + (* Find the right elimination suffix corresponding to the sort of the goal *) + (* c should be of type A1->.. An->B with B an inductive definition *) + let general_elim_then_using mk_elim + isrec allnames tac predicate ind (c, t) = + Proofview.Goal.nf_enter begin fun gl -> + let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in + (** FIXME: evar leak. *) + let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in + (* applying elimination_scheme just a little modified *) + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in + let indmv = + match kind_of_term (last_arg elimclause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> anomaly (str"elimination") + in + let pmv = + let p, _ = decompose_app elimclause.templtyp.Evd.rebus in + match kind_of_term p with + | Meta p -> p + | _ -> + let name_elim = + match kind_of_term elim with + | Const (kn, _) -> string_of_con kn + | Var id -> string_of_id id + | _ -> "\b" + in + error ("The elimination combinator " ^ name_elim ^ " is unknown.") + in + let elimclause' = clenv_fchain indmv elimclause indclause in + let branchsigns = compute_construtor_signatures isrec ind in + let brnames = compute_induction_names (Array.length branchsigns) allnames in + let flags = Unification.elim_flags () in + let elimclause' = + match predicate with + | None -> elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' + in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in + let after_tac i = + let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in + let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); + nassums = + List.fold_left + (fun acc b -> if b then acc+2 else acc+1) + 0 branchsigns.(i); + branchnum = i+1; + ity = ind; + largs = List.map (clenv_nf_meta clenv') largs; + pred = clenv_nf_meta clenv' hd } + in + tac ba + in + let branchtacs = List.init (Array.length branchsigns) after_tac in + Proofview.tclTHEN + (Clenvtac.clenv_refine false clenv') + (Proofview.tclEXTEND [] tclIDTAC branchtacs) + end + + let elimination_then tac c = + Proofview.Goal.nf_enter begin fun gl -> + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let isrec,mkelim = + match (Global.lookup_mind (fst (fst ind))).mind_record with + | None -> true,gl_make_elim + | Some _ -> false,gl_make_case_dep + in + general_elim_then_using mkelim isrec None tac None ind (c, t) + end + + let case_then_using = + general_elim_then_using gl_make_case_dep false + + let case_nodep_then_using = + general_elim_then_using gl_make_case_nodep false + + let elim_on_ba tac ba = + Proofview.Goal.nf_enter begin fun gl -> + let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in + tac branches + end + + let case_on_ba tac ba = + Proofview.Goal.nf_enter begin fun gl -> + let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in + tac branches + end + + let elimination_sort_of_goal gl = + (** Retyping will expand evars anyway. *) + let c = Proofview.Goal.concl (Goal.assume gl) in + pf_apply Retyping.get_sort_family_of gl c + + let elimination_sort_of_hyp id gl = + (** Retyping will expand evars anyway. *) + let c = pf_get_hyp_typ id (Goal.assume gl) in + pf_apply Retyping.get_sort_family_of gl c + + let elimination_sort_of_clause id gl = match id with + | None -> elimination_sort_of_goal gl + | Some id -> elimination_sort_of_hyp id gl + + let pf_constr_of_global ref tac = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let (sigma, c) = Evd.fresh_global env sigma ref in + Proofview.Unsafe.tclEVARS sigma <*> (tac c) + end + +end |