diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 174 |
1 files changed, 106 insertions, 68 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 25a0d897..b9c8ab92 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Pp @@ -21,6 +21,8 @@ open Reduction open Pattern open Genarg open Tacexpr +open Termops +open Rawterm (*i*) (* Tacticals i.e. functions from tactics to tactics. *) @@ -51,76 +53,112 @@ val tclINFO : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic +val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic - -val tclNTH_HYP : int -> (constr -> tactic) -> tactic -val tclNTH_DECL : int -> (named_declaration -> tactic) -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic -val tclLAST_HYP : (constr -> tactic) -> tactic -val tclLAST_DECL : (named_declaration -> tactic) -> tactic -val tclLAST_NHYPS : int -> (identifier list -> tactic) -> tactic -val tclTRY_sign : (constr -> tactic) -> named_context -> tactic -val tclTRY_HYPS : (constr -> tactic) -> tactic - -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic +val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic +val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic +val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic -val unTAC : tactic -> goal sigma -> proof_tree sigma +val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic + +(*s Tacticals applying to hypotheses *) + +val onNthHypId : int -> (identifier -> tactic) -> tactic +val onNthHyp : int -> (constr -> tactic) -> tactic +val onNthDecl : int -> (named_declaration -> tactic) -> tactic +val onLastHypId : (identifier -> tactic) -> tactic +val onLastHyp : (constr -> tactic) -> tactic +val onLastDecl : (named_declaration -> tactic) -> tactic +val onNLastHypsId : int -> (identifier list -> tactic) -> tactic +val onNLastHyps : int -> (constr list -> tactic) -> tactic +val onNLastDecls : int -> (named_context -> tactic) -> tactic + +val lastHypId : goal sigma -> identifier +val lastHyp : goal sigma -> constr +val lastDecl : goal sigma -> named_declaration +val nLastHypsId : int -> goal sigma -> identifier list +val nLastHyps : int -> goal sigma -> constr list +val nLastDecls : int -> goal sigma -> named_context + +val afterHyp : identifier -> goal sigma -> named_context + +val ifOnHyp : (identifier * types -> bool) -> + (identifier -> tactic) -> (identifier -> tactic) -> + identifier -> tactic -(*s Clause tacticals. *) +val onHyps : (goal sigma -> named_context) -> + (named_context -> tactic) -> tactic + +(*s Tacticals applying to goal components *) + +(* A [simple_clause] is a set of hypotheses, possibly extended with + the conclusion (conclusion is represented by None) *) + +type simple_clause = identifier option list + +(* A [clause] denotes occurrences and hypotheses in a + goal; in particular, it can abstractly refer to the set of + hypotheses independently of the effective contents of the current goal *) -type simple_clause = identifier gsimple_clause type clause = identifier gclause -val allClauses : 'a gclause -val allHyps : clause -val onHyp : identifier -> clause -val onConcl : 'a gclause - -val nth_clause : int -> goal sigma -> clause -val clause_type : clause -> goal sigma -> constr -val simple_clause_list_of : clause -> goal sigma -> simple_clause list - -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - -val afterHyp : identifier -> goal sigma -> named_context -val lastHyp : goal sigma -> identifier -val nLastHyps : int -> goal sigma -> named_context - -val onCL : (goal sigma -> clause) -> - (clause -> tactic) -> tactic -val tryAllClauses : (simple_clause -> tactic) -> tactic -val onAllClauses : (simple_clause -> tactic) -> tactic -val onClause : (clause -> tactic) -> clause -> tactic -val onClauses : (simple_clause -> tactic) -> clause -> tactic -val onAllClausesLR : (simple_clause -> tactic) -> tactic -val onNthLastHyp : int -> (clause -> tactic) -> tactic -val clauseTacThen : (clause -> tactic) -> tactic -> clause -> tactic -val if_tac : (goal sigma -> bool) -> tactic -> (tactic) -> tactic -val ifOnClause : - (clause * types -> bool) -> - (clause -> tactic) -> (clause -> tactic) -> clause -> tactic -val ifOnHyp : - (identifier * types -> bool) -> - (identifier -> tactic) -> (identifier -> tactic) -> identifier -> tactic - -val onHyps : (goal sigma -> named_context) -> - (named_context -> tactic) -> tactic -val tryAllHyps : (identifier -> tactic) -> tactic -val onNLastHyps : int -> (named_declaration -> tactic) -> tactic -val onLastHyp : (identifier -> tactic) -> tactic +val simple_clause_of : clause -> goal sigma -> simple_clause + +val allHypsAndConcl : clause +val allHyps : clause +val onHyp : identifier -> clause +val onConcl : clause + +val tryAllHyps : (identifier -> tactic) -> tactic +val tryAllHypsAndConcl : (identifier option -> tactic) -> tactic + +val onAllHyps : (identifier -> tactic) -> tactic +val onAllHypsAndConcl : (identifier option -> tactic) -> tactic +val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic + +val onClause : (identifier option -> tactic) -> clause -> tactic +val onClauseLR : (identifier option -> tactic) -> clause -> tactic + +(*s An intermediate form of occurrence clause with no mention of occurrences *) + +(* 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 + +(*s A concrete view of 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 + +(* This interprets an [clause] in a given [goal] context *) +val concrete_clause_of : clause -> goal sigma -> concrete_clause (*s Elimination tacticals. *) -type branch_args = { +type branch_args = { ity : inductive; (* the type we were eliminating on *) largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) @@ -137,15 +175,15 @@ type branch_assumptions = { (* [check_disjunctive_pattern_size loc pats n] returns an appropriate *) (* error message if |pats| <> n *) val check_or_and_pattern_size : - Util.loc -> or_and_intro_pattern_expr -> int -> unit + Util.loc -> or_and_intro_pattern_expr -> int -> unit (* Tolerate "[]" to mean a disjunctive pattern of any length *) -val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> +val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> or_and_intro_pattern_expr (* Useful for [as intro_pattern] modifier *) -val compute_induction_names : - int -> intro_pattern_expr located option -> +val compute_induction_names : + int -> intro_pattern_expr located option -> intro_pattern_expr located list array val elimination_sort_of_goal : goal sigma -> sorts_family @@ -154,30 +192,30 @@ val elimination_sort_of_clause : identifier option -> goal sigma -> sorts_family val general_elim_then_using : (inductive -> goal sigma -> constr) -> rec_flag -> - intro_pattern_expr located option -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic - + val elimination_then_using : - (branch_args -> tactic) -> constr option -> + (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic val elimination_then : - (branch_args -> tactic) -> + (branch_args -> tactic) -> (arg_bindings * arg_bindings) -> constr -> tactic val case_then_using : - intro_pattern_expr located option -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val case_nodep_then_using : - intro_pattern_expr located option -> (branch_args -> tactic) -> - constr option -> (arg_bindings * arg_bindings) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> + constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val simple_elimination_then : (branch_args -> tactic) -> constr -> tactic -val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic -val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic +val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic +val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic |