diff options
Diffstat (limited to 'proofs/tacexpr.ml')
| -rw-r--r-- | proofs/tacexpr.ml | 345 |
1 files changed, 0 insertions, 345 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml deleted file mode 100644 index 536c966c..00000000 --- a/proofs/tacexpr.ml +++ /dev/null @@ -1,345 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \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 Util -open Genarg -open Pattern -open Decl_kinds - -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 - -let make_red_flag = - let rec add_flag red = function - | [] -> red - | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FIota :: lf -> add_flag { red with rIota = true } lf - | FZeta :: lf -> add_flag { red with rZeta = true } lf - | FConst l :: lf -> - if red.rDelta then - error - "Cannot set both constants to unfold and constants not to unfold"; - add_flag { red with rConst = list_union red.rConst l } lf - | FDeltaBut l :: lf -> - if red.rConst <> [] & not red.rDelta then - error - "Cannot set both constants to unfold and constants not to unfold"; - add_flag - { red with rConst = list_union red.rConst l; rDelta = true } - lf - in - add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} - -type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag - -type 'id move_location = - | MoveAfter of 'id - | MoveBefore of 'id - | MoveToEnd of bool - -let no_move = MoveToEnd true - -open Pp - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top") - -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 - -(* onhyps: - [None] means *on every hypothesis* - [Some l] means on hypothesis belonging to l *) -type 'id gclause = - { onhyps : 'id raw_hyp_location list option; - concl_occs : occurrences_expr } - -let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} - -type 'constr induction_clause = - 'constr with_bindings induction_arg * - (intro_pattern_expr located option (* eqn:... *) - * intro_pattern_expr located option) (* as ... *) - -type ('constr,'id) induction_clause_list = - 'constr induction_clause list - * 'constr with_bindings option (* using ... *) - * 'id gclause option (* in ... *) - -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 gclause * letin_flag * - intro_pattern_expr located option - - (* 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 gclause - | TacChange of 'pat option * 'constr * 'id gclause - - (* Equivalence relations *) - | TacReflexivity - | TacSymmetry of 'id gclause - | TacTransitivity of 'constr option - - (* Equality and inversion *) - | TacRewrite of - evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * '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 declaration_hook = locality -> global_reference -> unit |