diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 163 |
1 files changed, 82 insertions, 81 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c28cb521..fb033363 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -9,7 +9,6 @@ open Loc open Names open Term -open Context open Environ open Proof_type open Evd @@ -22,26 +21,27 @@ open Unification open Misctypes open Locus -(** Main tactics. *) +(** Main tactics defined in ML. This file is huge and should probably be split + in more reasonable units at some point. Because of its size and age, the + implementation features various styles and stages of the proof engine. + This has to be uniformized someday. *) (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> goal sigma -> bool +val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : ?check:bool -> Id.t -> unit Proofview.tactic -val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic +val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -val convert_hyp_no_check : named_declaration -> unit Proofview.tactic -val thin : Id.t list -> tactic +val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic val mutual_fix : - Id.t -> int -> (Id.t * int * constr) list -> int -> tactic -val fix : Id.t option -> int -> tactic -val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic -val cofix : Id.t option -> tactic + Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic +val fix : Id.t option -> int -> unit Proofview.tactic +val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic +val cofix : Id.t option -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic @@ -50,7 +50,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t -val find_intro_names : rel_context -> goal sigma -> Id.t list +val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic @@ -74,7 +74,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> goal sigma -> int + bool -> quantified_hypothesis -> ([`NF],'b) Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic @@ -94,7 +94,11 @@ val try_intros_until : val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> - constr with_bindings induction_arg -> unit Proofview.tactic + constr with_bindings destruction_arg -> unit Proofview.tactic + +val force_destruction_arg : evars_flag -> env -> evar_map -> + delayed_open_constr_with_bindings destruction_arg -> + evar_map * constr with_bindings destruction_arg (** Tell if a used hypothesis should be cleared by default or not *) @@ -102,85 +106,85 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) -val intro_patterns : intro_patterns -> unit Proofview.tactic -val intro_patterns_to : Id.t move_location -> intro_patterns -> +val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic +val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) -val intros_patterns : intro_patterns -> unit Proofview.tactic +val intros_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic (** {6 Exact tactics. } *) val assumption : unit Proofview.tactic -val exact_no_check : constr -> tactic -val vm_cast_no_check : constr -> tactic -val native_cast_no_check : constr -> tactic +val exact_no_check : constr -> unit Proofview.tactic +val vm_cast_no_check : constr -> unit Proofview.tactic +val native_cast_no_check : constr -> unit Proofview.tactic val exact_check : constr -> unit Proofview.tactic -val exact_proof : Constrexpr.constr_expr -> tactic +val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic (** {6 Reduction tactics. } *) type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> constr Sigma.run val make_change_arg : constr -> change_arg -val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic -val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic -val reduct_in_concl : tactic_reduction * cast_kind -> tactic +val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic +val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic +val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> hyp_location -> unit Proofview.tactic -val red_in_concl : tactic -val red_in_hyp : hyp_location -> tactic -val red_option : goal_location -> tactic -val hnf_in_concl : tactic -val hnf_in_hyp : hyp_location -> tactic -val hnf_option : goal_location -> tactic -val simpl_in_concl : tactic -val simpl_in_hyp : hyp_location -> tactic -val simpl_option : goal_location -> tactic -val normalise_in_concl : tactic -val normalise_in_hyp : hyp_location -> tactic -val normalise_option : goal_location -> tactic -val normalise_vm_in_concl : tactic +val red_in_concl : unit Proofview.tactic +val red_in_hyp : hyp_location -> unit Proofview.tactic +val red_option : goal_location -> unit Proofview.tactic +val hnf_in_concl : unit Proofview.tactic +val hnf_in_hyp : hyp_location -> unit Proofview.tactic +val hnf_option : goal_location -> unit Proofview.tactic +val simpl_in_concl : unit Proofview.tactic +val simpl_in_hyp : hyp_location -> unit Proofview.tactic +val simpl_option : goal_location -> unit Proofview.tactic +val normalise_in_concl : unit Proofview.tactic +val normalise_in_hyp : hyp_location -> unit Proofview.tactic +val normalise_option : goal_location -> unit Proofview.tactic +val normalise_vm_in_concl : unit Proofview.tactic val unfold_in_concl : - (occurrences * evaluable_global_reference) list -> tactic + (occurrences * evaluable_global_reference) list -> unit Proofview.tactic val unfold_in_hyp : - (occurrences * evaluable_global_reference) list -> hyp_location -> tactic + (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic val unfold_option : - (occurrences * evaluable_global_reference) list -> goal_location -> tactic + (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : - constr_pattern option -> change_arg -> clause -> tactic + constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : - (occurrences * constr) list -> goal_location -> tactic -val reduce : red_expr -> clause -> tactic -val unfold_constr : global_reference -> tactic + (occurrences * constr) list -> goal_location -> unit Proofview.tactic +val reduce : red_expr -> clause -> unit Proofview.tactic +val unfold_constr : global_reference -> unit Proofview.tactic (** {6 Modification of the local context. } *) -val clear : Id.t list -> tactic +val clear : Id.t list -> unit Proofview.tactic val clear_body : Id.t list -> unit Proofview.tactic -val unfold_body : Id.t -> tactic +val unfold_body : Id.t -> unit Proofview.tactic val keep : Id.t list -> unit Proofview.tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic -val specialize : constr with_bindings -> tactic +val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> tactic +val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> tactic -val bring_hyps : named_context -> unit Proofview.tactic +val apply_type : constr -> constr list -> unit Proofview.tactic +val bring_hyps : Context.Named.t -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic @@ -206,6 +210,8 @@ val apply_delayed_in : (clear_flag * delayed_open_constr_with_bindings located) list -> intro_pattern option -> unit Proofview.tactic +val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map + (** {6 Elimination tactics. } *) (* @@ -237,20 +243,20 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) - nparams: int; (** number of parameters *) - predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) - npredicates: int; (** Number of predicates *) - branches: rel_context; (** branchr,...,branch1 *) - nbranches: int; (** Number of branches *) - args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) - nargs: int; (** number of arguments *) - indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) - concl: types; (** Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) - indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) - farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) + params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (** number of parameters *) + predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (** Number of predicates *) + branches: Context.Rel.t; (** branchr,...,branch1 *) + nbranches: int; (** Number of branches *) + args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (** number of arguments *) + indarg: Context.Rel.Declaration.t option; (** Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (** Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) + farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme @@ -293,7 +299,7 @@ val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option (** Implements user-level "destruct" and "induction" *) val induction_destruct : rec_flag -> evars_flag -> - (delayed_open_constr_with_bindings induction_arg + (delayed_open_constr_with_bindings destruction_arg * (intro_pattern_naming option * or_and_intro_pattern option) * clause option) list * constr with_bindings option -> unit Proofview.tactic @@ -364,7 +370,7 @@ val pose_proof : Name.t -> constr -> (** Common entry point for user-level "assert", "enough" and "pose proof" *) -val forward : bool -> unit Proofview.tactic option -> +val forward : bool -> unit Proofview.tactic option option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactic cut, actually a modus ponens rule *) @@ -383,12 +389,12 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) -val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic -val new_generalize : constr list -> unit Proofview.tactic +val generalize : constr list -> unit Proofview.tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic + val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic -val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic +val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> unit Proofview.tactic (** {6 Other tactics. } *) @@ -397,7 +403,7 @@ val unify : ?state:Names.transparent_state -> constr -> constr -> unit val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic -val specialize_eqs : Id.t -> tactic +val specialize_eqs : Id.t -> unit Proofview.tactic val general_rewrite_clause : (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t @@ -416,9 +422,6 @@ module Simple : sig (** Simplified version of some of the above tactics *) val intro : Id.t -> unit Proofview.tactic - val generalize : constr list -> tactic - val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic - val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic @@ -431,13 +434,11 @@ end module New : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic - (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c] + val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic + (** [refine ?unsafe c] is [Refine.refine ?unsafe c] followed by beta-iota-reduction of the conclusion. *) val reduce_after_refine : unit Proofview.tactic (** The reducing tactic called after {!refine}. *) - open Proofview - val exact_proof : Constrexpr.constr_expr -> unit tactic end |