summaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml457
1 files changed, 457 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
new file mode 100644
index 00000000..77898afb
--- /dev/null
+++ b/tactics/tacticals.ml
@@ -0,0 +1,457 @@
+(************************************************************************)
+(* 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: tacticals.ml,v 1.60.2.1 2004/07/16 19:30:55 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Termops
+open Sign
+open Declarations
+open Inductive
+open Reduction
+open Environ
+open Libnames
+open Refiner
+open Tacmach
+open Clenv
+open Pattern
+open Matching
+open Evar_refiner
+open Genarg
+open Tacexpr
+
+(******************************************)
+(* Basic Tacticals *)
+(******************************************)
+
+(*************************************************)
+(* Tacticals re-exported from the Refiner module.*)
+(*************************************************)
+
+let tclIDTAC = tclIDTAC
+let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
+let tclORELSE = tclORELSE
+let tclTHEN = tclTHEN
+let tclTHENLIST = tclTHENLIST
+let tclTHEN_i = tclTHEN_i
+let tclTHENFIRST = tclTHENFIRST
+let tclTHENLAST = tclTHENLAST
+let tclTHENS = tclTHENS
+let tclTHENSV = Refiner.tclTHENSV
+let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn
+let tclTHENSLASTn = Refiner.tclTHENSLASTn
+let tclTHENFIRSTn = Refiner.tclTHENFIRSTn
+let tclTHENLASTn = Refiner.tclTHENLASTn
+let tclREPEAT = Refiner.tclREPEAT
+let tclREPEAT_MAIN = tclREPEAT_MAIN
+let tclFIRST = Refiner.tclFIRST
+let tclSOLVE = Refiner.tclSOLVE
+let tclTRY = Refiner.tclTRY
+let tclINFO = Refiner.tclINFO
+let tclCOMPLETE = Refiner.tclCOMPLETE
+let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
+let tclFAIL = Refiner.tclFAIL
+let tclDO = Refiner.tclDO
+let tclPROGRESS = Refiner.tclPROGRESS
+let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
+let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL
+let tclTHENTRY = tclTHENTRY
+let tclIFTHENELSE = tclIFTHENELSE
+let tclIFTHENSELSE = tclIFTHENSELSE
+let tclIFTHENSVELSE = tclIFTHENSVELSE
+
+let unTAC = unTAC
+
+(* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
+let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
+
+(* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
+(* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
+let tclMAP tacfun l =
+ List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
+
+(* apply a tactic to the nth element of the signature *)
+
+let tclNTH_HYP m (tac : constr->tactic) gl =
+ tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id)
+ with Failure _ -> error "No such assumption") gl
+
+(* apply a tactic to the last element of the signature *)
+
+let tclLAST_HYP = tclNTH_HYP 1
+
+let tclTRY_sign (tac : constr->tactic) sign gl =
+ let rec arec = function
+ | [] -> tclFAIL 0 "no applicable hypothesis"
+ | [s] -> tac (mkVar s) (*added in order to get useful error messages *)
+ | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl)
+ in
+ arec (ids_of_named_context sign) gl
+
+let tclTRY_HYPS (tac : constr->tactic) gl =
+ tclTRY_sign tac (pf_hyps gl) gl
+
+(***************************************)
+(* Clause Tacticals *)
+(***************************************)
+
+(* The following functions introduce several tactic combinators and
+ functions useful for working with clauses. A clause is either None
+ or (Some id), where id is an identifier. This type is useful for
+ defining tactics that may be used either to transform the
+ conclusion (None) or to transform a hypothesis id (Some id). --
+ --Eduardo (8/8/97)
+*)
+
+(* The type of clauses *)
+
+type simple_clause = identifier gsimple_clause
+type clause = identifier gclause
+
+let allClauses = { onhyps=None; onconcl=true; concl_occs=[] }
+let allHyps = { onhyps=None; onconcl=false; concl_occs=[] }
+let onHyp id =
+ { onhyps=Some[(id,[],(InHyp, ref None))]; onconcl=false; concl_occs=[] }
+let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] }
+
+let simple_clause_list_of cl gls =
+ let hyps =
+ match cl.onhyps with
+ None ->
+ List.map (fun id -> Some(id,[],(InHyp,ref None))) (pf_ids_of_hyps gls)
+ | Some l -> List.map (fun h -> Some h) l in
+ if cl.onconcl then None::hyps else hyps
+
+
+(* OR-branch *)
+let tryClauses tac cl gls =
+ let rec firstrec = function
+ | [] -> tclFAIL 0 "no applicable hypothesis"
+ | [cls] -> tac cls (* added in order to get a useful error message *)
+ | cls::tl -> (tclORELSE (tac cls) (firstrec tl))
+ in
+ let hyps = simple_clause_list_of cl gls in
+ firstrec hyps gls
+
+(* AND-branch *)
+let onClauses tac cl gls =
+ let hyps = simple_clause_list_of cl gls in
+ tclMAP tac hyps gls
+
+(* AND-branch reverse order*)
+let onClausesLR tac cl gls =
+ let hyps = simple_clause_list_of cl gls in
+ tclMAP tac (List.rev hyps) gls
+
+(* A clause corresponding to the |n|-th hypothesis or None *)
+
+let nth_clause n gl =
+ if n = 0 then
+ onConcl
+ else if n < 0 then
+ let id = List.nth (List.rev (pf_ids_of_hyps gl)) (-n-1) in
+ onHyp id
+ else
+ let id = List.nth (pf_ids_of_hyps gl) (n-1) in
+ onHyp id
+
+(* Gets the conclusion or the type of a given hypothesis *)
+
+let clause_type cls gl =
+ match simple_clause_of cls with
+ | None -> pf_concl gl
+ | Some (id,_,_) -> pf_get_hyp_typ gl id
+
+(* Functions concerning matching of clausal environments *)
+
+let pf_is_matching gls pat n =
+ let (wc,_) = startWalk gls in
+ is_matching_conv (w_env wc) (w_Underlying wc) pat n
+
+let pf_matches gls pat n =
+ matches_conv (pf_env gls) (project gls) pat n
+
+(* [OnCL clausefinder clausetac]
+ * executes the clausefinder to find the clauses, and then executes the
+ * clausetac on the clause so obtained. *)
+
+let onCL cfind cltac gl = cltac (cfind gl) gl
+
+
+(* [OnHyps hypsfinder hypstac]
+ * idem [OnCL] but only for hypotheses, not for conclusion *)
+
+let onHyps find tac gl = tac (find gl) gl
+
+
+
+(* Create a clause list with all the hypotheses from the context, occuring
+ after id *)
+
+let afterHyp id gl =
+ fst (list_splitby (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+
+
+(* Create a singleton clause list with the last hypothesis from then context *)
+
+let lastHyp gl = List.hd (pf_ids_of_hyps gl)
+
+
+(* Create a clause list with the n last hypothesis from then context *)
+
+let nLastHyps n gl =
+ try list_firstn n (pf_hyps gl)
+ with Failure "firstn" -> error "Not enough hypotheses in the goal"
+
+
+let onClause t cls gl = t cls gl
+let tryAllClauses tac = tryClauses tac allClauses
+let onAllClauses tac = onClauses tac allClauses
+let onAllClausesLR tac = onClausesLR tac allClauses
+let onNthLastHyp n tac gls = tac (nth_clause n gls) gls
+
+let tryAllHyps tac =
+ tryClauses (function Some(id,_,_) -> tac id | _ -> assert false) allHyps
+let onNLastHyps n tac = onHyps (nLastHyps n) (tclMAP tac)
+let onLastHyp tac gls = tac (lastHyp gls) gls
+
+let clauseTacThen tac continuation =
+ (fun cls -> (tclTHEN (tac cls) continuation))
+
+let if_tac pred tac1 tac2 gl =
+ if pred gl then tac1 gl else tac2 gl
+
+let ifOnClause pred tac1 tac2 cls gl =
+ if pred (cls,clause_type cls gl) then
+ tac1 cls gl
+ else
+ tac2 cls gl
+
+let ifOnHyp pred tac1 tac2 id gl =
+ if pred (id,pf_get_hyp_typ gl id) then
+ tac1 id gl
+ else
+ tac2 id gl
+
+(***************************************)
+(* Elimination Tacticals *)
+(***************************************)
+
+(* The following tacticals allow to apply a tactic to the
+ branches generated by the application of an elimination
+ tactic.
+
+ Two auxiliary types --branch_args and branch_assumptions-- are
+ used to keep track of some information about the ``branches'' of
+ the elimination. *)
+
+type branch_args = {
+ ity : inductive; (* 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 list}
+
+type branch_assumptions = {
+ ba : branch_args; (* the branch args *)
+ assums : named_context} (* the list of assumptions introduced *)
+
+let compute_induction_names n = function
+ | None ->
+ Array.make n []
+ | Some (IntroOrAndPattern names) when List.length names = n ->
+ Array.of_list names
+ | _ ->
+ errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
+
+let compute_construtor_signatures isrec (_,k as ity) =
+ let rec analrec c recargs =
+ match kind_of_term c, recargs with
+ | Prod (_,_,c), recarg::rest ->
+ let b = match dest_recarg recarg with
+ | Norec | Imbr _ -> false
+ | Mrec j -> isrec & j=k
+ in b :: (analrec c rest)
+ | LetIn (_,_,_,c), rest -> false :: (analrec c rest)
+ | _, [] -> []
+ | _ -> anomaly "compute_construtor_signatures"
+ in
+ let (mib,mip) = Global.lookup_inductive ity in
+ let n = mip.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 elimination_sort_of_goal gl =
+ match kind_of_term (hnf_type_of gl (pf_concl gl)) with
+ | Sort s ->
+ (match s with
+ | Prop Null -> InProp
+ | Prop Pos -> InSet
+ | Type _ -> InType)
+ | _ -> anomaly "goal should be a type"
+
+let elimination_sort_of_hyp id gl =
+ match kind_of_term (hnf_type_of gl (pf_get_hyp_typ gl id)) with
+ | Sort s ->
+ (match s with
+ | Prop Null -> InProp
+ | Prop Pos -> InSet
+ | Type _ -> InType)
+ | _ -> anomaly "goal should be a type"
+
+
+(* 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 last_arg c = match kind_of_term c with
+ | App (f,cl) -> array_last cl
+ | _ -> anomaly "last_arg"
+
+let general_elim_then_using
+ elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
+ let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ (* applying elimination_scheme just a little modified *)
+ let (wc,kONT) = startWalk gl in
+ let indclause = mk_clenv_from wc (c,t) in
+ let indclause' = clenv_constrain_with_bindings indbindings indclause in
+ let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
+ let indmv =
+ match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+ | Meta mv -> mv
+ | _ -> error "elimination"
+ in
+ let pmv =
+ let p, _ = decompose_app (clenv_template_type elimclause).rebus in
+ match kind_of_term p with
+ | Meta p -> p
+ | _ ->
+ let name_elim =
+ match kind_of_term elim with
+ | Const kn -> string_of_kn kn
+ | Var id -> string_of_id id
+ | _ -> "\b"
+ in
+ error ("The elimination combinator " ^ name_elim ^ " is not known")
+ in
+ let elimclause' = clenv_fchain indmv elimclause indclause' in
+ let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
+ let branchsigns = compute_construtor_signatures isrec ity in
+ let brnames = compute_induction_names (Array.length branchsigns) allnames in
+ let after_tac ce i gl =
+ let (hd,largs) = decompose_app (clenv_template_type ce).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 = ity;
+ largs = List.map (clenv_instance_term ce) largs;
+ pred = clenv_instance_term 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_assign pmv p elimclause'
+ in
+ elim_res_pf_THEN_i kONT elimclause' branchtacs gl
+
+
+let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
+ let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let elim =
+ Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
+ general_elim_then_using
+ elim true None tac predicate (indbindings,elimbindings) c gl
+
+
+let elimination_then tac = elimination_then_using tac None
+let simple_elimination_then tac = elimination_then tac ([],[])
+
+let case_then_using allnames tac predicate (indbindings,elimbindings) c gl =
+ (* finding the case combinator *)
+ let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let sigma = project gl in
+ let sort = elimination_sort_of_goal gl in
+ let elim = Indrec.make_case_dep (pf_env gl) sigma ity sort in
+ general_elim_then_using
+ elim false allnames tac predicate (indbindings,elimbindings) c gl
+
+let case_nodep_then_using allnames tac predicate (indbindings,elimbindings)
+ c gl =
+ (* finding the case combinator *)
+ let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let sigma = project gl in
+ let sort = elimination_sort_of_goal gl in
+ let elim = Indrec.make_case_nodep (pf_env gl) sigma ity sort in
+ general_elim_then_using
+ elim false allnames tac predicate (indbindings,elimbindings) c gl
+
+
+let make_elim_branch_assumptions ba gl =
+ let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
+ match lb,lc with
+ | ([], _) ->
+ { ba = ba;
+ assums = assums}
+ | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) ->
+ makerec (recarg::indarg::assums,
+ idrec::cargs,
+ idrec::recargs,
+ constargs,
+ idind::indargs) tl idtl
+ | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
+ makerec (constarg::assums,
+ id::cargs,
+ id::constargs,
+ recargs,
+ indargs) tl idtl
+ | (_, _) -> error "make_elim_branch_assumptions"
+ in
+ makerec ([],[],[],[],[]) ba.branchsign
+ (try list_firstn ba.nassums (pf_hyps gl)
+ with Failure _ -> anomaly "make_elim_branch_assumptions")
+
+let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
+
+let make_case_branch_assumptions ba gl =
+ let rec makerec (assums,cargs,constargs,recargs) p_0 p_1 =
+ match p_0,p_1 with
+ | ([], _) ->
+ { ba = ba;
+ assums = assums}
+ | ((true::tl), ((idrec,_,_ as recarg)::idtl)) ->
+ makerec (recarg::assums,
+ idrec::cargs,
+ idrec::recargs,
+ constargs) tl idtl
+ | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
+ makerec (constarg::assums,
+ id::cargs,
+ recargs,
+ id::constargs) tl idtl
+ | (_, _) -> error "make_case_branch_assumptions"
+ in
+ makerec ([],[],[],[]) ba.branchsign
+ (try list_firstn ba.nassums (pf_hyps gl)
+ with Failure _ -> anomaly "make_case_branch_assumptions")
+
+let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
+
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 09:53:39 +0000