summaryrefslogtreecommitdiff
path: root/proofs/tacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacexpr.ml')
-rw-r--r--proofs/tacexpr.ml314
1 files changed, 314 insertions, 0 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
new file mode 100644
index 00000000..d8d7319d
--- /dev/null
+++ b/proofs/tacexpr.ml
@@ -0,0 +1,314 @@
+(************************************************************************)
+(* 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: tacexpr.ml,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Names
+open Topconstr
+open Libnames
+open Nametab
+open Rawterm
+open Util
+open Genarg
+open Pattern
+
+type 'a or_metaid = AI of 'a | MetaId of loc * string
+
+type direction_flag = bool (* true = Left-to-right false = right-to-right *)
+
+type raw_red_flag =
+ | FBeta
+ | FIota
+ | FZeta
+ | FConst of reference list
+ | FDeltaBut of reference 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 hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
+type 'a raw_hyp_location =
+ 'a * int list * (hyp_location_flag * hyp_location_flag option ref)
+
+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 option
+ | DepInversion of inversion_kind * 'c option * intro_pattern_expr option
+ | InversionUsing of 'c * 'id list
+
+type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
+
+type 'id gsimple_clause = ('id raw_hyp_location) option
+(* onhyps:
+ [None] means *on every hypothesis*
+ [Some l] means on hypothesis belonging to l *)
+type 'id gclause =
+ { onhyps : 'id raw_hyp_location list option;
+ onconcl : bool;
+ concl_occs :int list }
+
+let simple_clause_of = function
+ { onhyps = Some[scl]; onconcl = false } -> Some scl
+ | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
+ | _ -> error "not a simple clause (one hypothesis or conclusion)"
+
+type pattern_expr = constr_expr
+
+(* Type of patterns *)
+type 'a match_pattern =
+ | Term of 'a
+ | Subterm of identifier option * 'a
+
+(* Type of hypotheses for a Match Context rule *)
+type 'a match_context_hyps =
+ | Hyp of name located * '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) gen_atomic_tactic_expr =
+ (* Basic tactics *)
+ | TacIntroPattern of intro_pattern_expr list
+ | TacIntrosUntil of quantified_hypothesis
+ | TacIntroMove of identifier option * identifier located option
+ | TacAssumption
+ | TacExact of 'constr
+ | TacApply of 'constr with_bindings
+ | TacElim of 'constr with_bindings * 'constr with_bindings option
+ | TacElimType of 'constr
+ | TacCase of 'constr with_bindings
+ | TacCaseType of 'constr
+ | TacFix of identifier option * int
+ | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+ | TacCofix of identifier option
+ | TacMutualCofix of identifier * (identifier * 'constr) list
+ | TacCut of 'constr
+ | TacTrueCut of name * 'constr
+ | TacForward of bool * name * 'constr
+ | TacGeneralize of 'constr list
+ | TacGeneralizeDep of 'constr
+ | TacLetTac of name * 'constr * 'id gclause
+ | TacInstantiate of int * 'constr * 'id gclause
+
+ (* Derived basic tactics *)
+ | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)
+ | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
+ * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
+ | TacSimpleDestruct of quantified_hypothesis
+ | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
+ * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
+
+ | 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 string list option
+ | TacAuto of int option * string list option
+ | TacAutoTDB of int option
+ | TacDestructHyp of (bool * identifier located)
+ | TacDestructConcl
+ | TacSuperAuto of (int option * reference list * bool * bool)
+ | TacDAuto of int option * int option
+
+ (* Context management *)
+ | TacClear of 'id list
+ | TacClearBody of 'id list
+ | TacMove of bool * 'id * 'id
+ | TacRename of 'id * 'id
+
+ (* Constructors *)
+ | TacLeft of 'constr bindings
+ | TacRight of 'constr bindings
+ | TacSplit of bool * 'constr bindings
+ | TacAnyConstructor of 'tac option
+ | TacConstructor of int or_metaid * 'constr bindings
+
+ (* Conversion *)
+ | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
+ | TacChange of
+ 'constr occurrences option * 'constr * 'id gclause
+
+ (* Equivalence relations *)
+ | TacReflexivity
+ | TacSymmetry of 'id gclause
+ | TacTransitivity of 'constr
+
+ (* Equality and inversion *)
+ | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
+
+ (* For ML extensions *)
+ | TacExtend of loc * string * ('constr,'tac) generic_argument list
+
+ (* For syntax extensions *)
+ | TacAlias of loc * string *
+ (identifier * ('constr,'tac) generic_argument) list
+ * (dir_path * 'tac)
+
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
+ | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
+ | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+ | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+ | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+ | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option
+ | TacId of string
+ | TacFail of int or_var * string
+ | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+
+ | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+ | TacMatch of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+ | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+ | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
+ | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
+
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
+ identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+
+ (* These are possible arguments of a tactic definition *)
+and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
+ | TacDynamic of loc * Dyn.t
+ | TacVoid
+ | MetaIdArg of loc * string
+ | ConstrMayEval of ('constr,'cst) may_eval
+ | IntroPattern of intro_pattern_expr
+ | Reference of 'ref
+ | Integer of int
+ | TacCall of loc *
+ 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
+ | TacFreshId of string option
+ | Tacexp of 'tac
+
+type raw_tactic_expr =
+ (constr_expr,
+ pattern_expr,
+ reference,
+ reference,
+ reference,
+ identifier located or_metaid,
+ raw_tactic_expr) gen_tactic_expr
+
+type raw_atomic_tactic_expr =
+ (constr_expr, (* constr *)
+ pattern_expr, (* pattern *)
+ reference, (* evaluable reference *)
+ reference, (* inductive *)
+ reference, (* ltac reference *)
+ identifier located or_metaid, (* identifier *)
+ raw_tactic_expr) gen_atomic_tactic_expr
+
+type raw_tactic_arg =
+ (constr_expr,
+ pattern_expr,
+ reference,
+ reference,
+ reference,
+ identifier located or_metaid,
+ raw_tactic_expr) gen_tactic_arg
+
+type raw_generic_argument =
+ (constr_expr,raw_tactic_expr) generic_argument
+
+type raw_red_expr = (constr_expr, reference) red_expr_gen
+
+(* Globalized tactics *)
+type glob_tactic_expr =
+ (rawconstr_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) gen_tactic_expr
+
+type glob_atomic_tactic_expr =
+ (rawconstr_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) gen_atomic_tactic_expr
+
+type glob_tactic_arg =
+ (rawconstr_and_expr,
+ constr_pattern,
+ evaluable_global_reference and_short_name or_var,
+ inductive or_var,
+ ltac_constant located,
+ identifier located or_var,
+ glob_tactic_expr) gen_tactic_arg
+
+type glob_generic_argument =
+ (rawconstr_and_expr,glob_tactic_expr) generic_argument
+
+type glob_red_expr =
+ (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
+
+type closed_raw_generic_argument =
+ (constr_expr,raw_tactic_expr) generic_argument
+
+type 'a raw_abstract_argument_type =
+ ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+
+type 'a glob_abstract_argument_type =
+ ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+
+type open_generic_argument =
+ (Term.constr,glob_tactic_expr) generic_argument
+
+type closed_generic_argument =
+ (Term.constr,glob_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+ ('a,Term.constr,glob_tactic_expr) abstract_argument_type
+
+type declaration_hook = Decl_kinds.strength -> global_reference -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:40:41 +0000