diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 306 |
1 files changed, 306 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli new file mode 100644 index 000000000..16ba9f95e --- /dev/null +++ b/intf/tacexpr.mli @@ -0,0 +1,306 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Topconstr +open Libnames +open Nametab +open Glob_term +open Errors +open Pp +open Util +open Genarg +open Pattern +open Decl_kinds +open Misctypes +open Locus + +type 'a or_metaid = AI of 'a | MetaId of loc * string + +type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type lazy_flag = bool (* true = lazy false = eager *) +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type split_flag = bool (* true = exists false = split *) +type hidden_flag = bool (* true = internal use false = user-level *) +type letin_flag = bool (* true = use local def false = use Leibniz *) + +type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) + +type glob_red_flag = + | FBeta + | FIota + | FZeta + | FConst of reference or_by_notation list + | FDeltaBut of reference or_by_notation list + +type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (* can be seen as "no move" when doing intro *) + +type 'a induction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of identifier located + | ElimOnAnonHyp of int + +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + +type ('c,'id) inversion_strength = + | NonDepInversion of + inversion_kind * 'id list * intro_pattern_expr located option + | DepInversion of + inversion_kind * 'c option * intro_pattern_expr located option + | InversionUsing of 'c * 'id list + +type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b + +type 'id message_token = + | MsgString of string + | MsgInt of int + | MsgIdent of 'id + +type 'constr induction_clause = + ('constr with_bindings induction_arg list * 'constr with_bindings option * + (intro_pattern_expr located option * intro_pattern_expr located option)) + +type ('constr,'id) induction_clause_list = + 'constr induction_clause list * 'id clause_expr option + +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + +(* Type of patterns *) +type 'a match_pattern = + | Term of 'a + | Subterm of bool * identifier option * 'a + +(* Type of hypotheses for a Match Context rule *) +type 'a match_context_hyps = + | Hyp of name located * 'a match_pattern + | Def of name located * 'a match_pattern * 'a match_pattern + +(* Type of a Match rule for Match Context and Match *) +type ('a,'t) match_rule = + | Pat of 'a match_context_hyps list * 'a match_pattern * 't + | All of 't + +type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = + (* Basic tactics *) + | TacIntroPattern of intro_pattern_expr located list + | TacIntrosUntil of quantified_hypothesis + | TacIntroMove of identifier option * 'id move_location + | TacAssumption + | TacExact of 'constr + | TacExactNoCheck of 'constr + | TacVmCastNoCheck of 'constr + | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * + ('id * intro_pattern_expr located option) option + | TacElim of evars_flag * 'constr with_bindings * + 'constr with_bindings option + | TacElimType of 'constr + | TacCase of evars_flag * 'constr with_bindings + | TacCaseType of 'constr + | TacFix of identifier option * int + | TacMutualFix of hidden_flag * identifier * int * (identifier * int * + 'constr) list + | TacCofix of identifier option + | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list + | TacCut of 'constr + | TacAssert of 'tac option * intro_pattern_expr located option * 'constr + | TacGeneralize of ('constr with_occurrences * name) list + | TacGeneralizeDep of 'constr + | TacLetTac of name * 'constr * 'id clause_expr * letin_flag + + (* Derived basic tactics *) + | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis + | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause_list + | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis + | TacDecomposeAnd of 'constr + | TacDecomposeOr of 'constr + | TacDecompose of 'ind list * 'constr + | TacSpecialize of int option * 'constr with_bindings + | TacLApply of 'constr + + (* Automation tactics *) + | TacTrivial of debug * 'constr list * string list option + | TacAuto of debug * int or_var option * 'constr list * string list option + + (* Context management *) + | TacClear of bool * 'id list + | TacClearBody of 'id list + | TacMove of bool * 'id * 'id move_location + | TacRename of ('id *'id) list + | TacRevert of 'id list + + (* Constructors *) + | TacLeft of evars_flag * 'constr bindings + | TacRight of evars_flag * 'constr bindings + | TacSplit of evars_flag * split_flag * 'constr bindings list + | TacAnyConstructor of evars_flag * 'tac option + | TacConstructor of evars_flag * int or_var * 'constr bindings + + (* Conversion *) + | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id clause_expr + | TacChange of 'pat option * 'constr * 'id clause_expr + + (* Equivalence relations *) + | TacReflexivity + | TacSymmetry of 'id clause_expr + | TacTransitivity of 'constr option + + (* Equality and inversion *) + | TacRewrite of + evars_flag * (bool * multi * 'constr with_bindings) list * 'id clause_expr * 'tac option + | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis + + (* For ML extensions *) + | TacExtend of loc * string * 'lev generic_argument list + + (* For syntax extensions *) + | TacAlias of loc * string * + (identifier * 'lev generic_argument) list + * (dir_path * glob_tactic_expr) + +and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = + | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr + | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array * + ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array + | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * + ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list + | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list + | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr list + | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option + | TacId of 'id message_token list + | TacFail of int or_var * 'id message_token list + | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list + | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list + | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast + | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located + +and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast = + identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr + + (* These are the possible arguments of a tactic definition *) +and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg = + | TacDynamic of loc * Dyn.t + | TacVoid + | MetaIdArg of loc * bool * string + | ConstrMayEval of ('constr,'cst,'pat) may_eval + | IntroPattern of intro_pattern_expr located + | Reference of 'ref + | Integer of int + | TacCall of loc * + 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list + | TacExternal of loc * string * string * + ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list + | TacFreshId of string or_var list + | Tacexp of 'tac + +(* Globalized tactics *) +and glob_tactic_expr = + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr, + glevel) gen_tactic_expr + +type raw_tactic_expr = + (constr_expr, + constr_pattern_expr, + reference or_by_notation, + reference or_by_notation, + reference, + identifier located or_metaid, + raw_tactic_expr, + rlevel) gen_tactic_expr + +type raw_atomic_tactic_expr = + (constr_expr, (* constr *) + constr_pattern_expr, (* pattern *) + reference or_by_notation, (* evaluable reference *) + reference or_by_notation, (* inductive *) + reference, (* ltac reference *) + identifier located or_metaid, (* identifier *) + raw_tactic_expr, + rlevel) gen_atomic_tactic_expr + +type raw_tactic_arg = + (constr_expr, + constr_pattern_expr, + reference or_by_notation, + reference or_by_notation, + reference, + identifier located or_metaid, + raw_tactic_expr, + rlevel) gen_tactic_arg + +type raw_generic_argument = rlevel generic_argument + +type raw_red_expr = + (constr_expr, reference or_by_notation, constr_expr) red_expr_gen + +type glob_atomic_tactic_expr = + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr, + glevel) gen_atomic_tactic_expr + +type glob_tactic_arg = + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr, + glevel) gen_tactic_arg + +type glob_generic_argument = glevel generic_argument + +type glob_red_expr = + (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern) + red_expr_gen + +type typed_generic_argument = tlevel generic_argument + +type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type + +type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type + +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type + +type 'a declaration_hook = locality -> global_reference -> 'a |