From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tactics/auto.mli | 225 ++++++------------------------------------------------- 1 file changed, 22 insertions(+), 203 deletions(-) (limited to 'tactics/auto.mli') diff --git a/tactics/auto.mli b/tactics/auto.mli index 5ac2de87..ea3f0ac0 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,268 +1,87 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* hints_path -val path_matches : hints_path -> hints_path_atom list -> bool -val path_derivate : hints_path -> hints_path_atom -> hints_path -val pp_hints_path : hints_path -> Pp.std_ppcmds - -module Hint_db : - sig - type t - val empty : transparent_state -> bool -> t - val find : global_reference -> t -> search_entry - val map_none : t -> pri_auto_tactic list - val map_all : global_reference -> t -> pri_auto_tactic list - val map_auto : global_reference * constr -> t -> pri_auto_tactic list - val add_one : hint_entry -> t -> t - val add_list : (hint_entry) list -> t -> t - val remove_one : global_reference -> t -> t - val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> pri_auto_tactic list -> unit) -> t -> unit - - val use_dn : t -> bool - val transparent_state : t -> transparent_state - val set_transparent_state : t -> transparent_state -> t - - val add_cut : hints_path -> t -> t - val cut : t -> hints_path - - val unfolds : t -> Idset.t * Cset.t - end - -type hint_db_name = string - -type hint_db = Hint_db.t - -type hints_entry = - | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list - | HintsImmediateEntry of (hints_path_atom * constr) list - | HintsCutEntry of hints_path - | HintsUnfoldEntry of evaluable_global_reference list - | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsExternEntry of - int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr - -val searchtable_map : hint_db_name -> hint_db - -val searchtable_add : (hint_db_name * hint_db) -> unit - -(** [create_hint_db local name st use_dn]. - [st] is a transparency state for unification using this db - [use_dn] switches the use of the discrimination net for all hints - and patterns. *) - -val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit - -val remove_hints : bool -> hint_db_name list -> global_reference list -> unit - -val current_db_names : unit -> hint_db_name list - -val interp_hints : hints_expr -> hints_entry +val extern_interp : + (patvar_map -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic) Hook.t -val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit - -val prepare_hint : env -> open_constr -> constr - -val print_searchtable : unit -> unit - -val print_applicable_hint : unit -> unit - -val print_hint_ref : global_reference -> unit - -val print_hint_db_by_name : hint_db_name -> unit - -val print_hint_db : Hint_db.t -> unit - -(** [make_exact_entry pri (c, ctyp)]. - [c] is the term given as an exact proof to solve the goal; - [ctyp] is the type of [c]. *) - -val make_exact_entry : evar_map -> int option -> ?name:hints_path_atom -> constr * constr -> hint_entry - -(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)]. - [eapply] is true if this hint will be used only with EApply; - [hnf] should be true if we should expand the head of cty before searching for - products; - [c] is the term given as an exact proof to solve the goal; - [cty] is the type of [c]. *) - -val make_apply_entry : - env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> - constr * constr -> hint_entry - -(** A constr which is Hint'ed will be: - - (1) used as an Exact, if it does not start with a product - - (2) used as an Apply, if its HNF starts with a product, and - has no missing arguments. - - (3) used as an EApply, if its HNF starts with a product, and - has missing arguments. *) - -val make_resolves : - env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> - constr -> hint_entry list - -(** [make_resolve_hyp hname htyp]. - used to add an hypothesis to the local hint database; - Never raises a user exception; - If the hyp cannot be used as a Hint, the empty list is returned. *) - -val make_resolve_hyp : - env -> evar_map -> named_declaration -> hint_entry list - -(** [make_extern pri pattern tactic_expr] *) - -val make_extern : - int -> constr_pattern option -> Tacexpr.glob_tactic_expr - -> hint_entry - -val set_extern_interp : - (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit - -val set_extern_intern_tac : - (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) - -> unit - -val set_extern_subst_tactic : - (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) - -> unit - -(** Create a Hint database from the pairs (name, constr). - Useful to take the current goal hypotheses as hints; - Boolean tells if lemmas with evars are allowed *) - -val make_local_hint_db : ?ts:transparent_state -> bool -> open_constr list -> goal sigma -> hint_db +(** Auto and related automation tactics *) val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list val default_search_depth : int ref -val auto_unif_flags : Unification.unify_flags +val auto_flags_of_state : transparent_state -> Unification.unify_flags (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve_nodelta : (constr * clausenv) -> tactic +val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic -val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic +val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic +val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic (** The Auto tactic *) (** The use of the "core" database can be de-activated by passing "nocore" amongst the databases. *) -val make_db_list : hint_db_name list -> hint_db list - val auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> hint_db_name list -> tactic + int -> open_constr list -> hint_db_name list -> unit Proofview.tactic (** Auto with more delta. *) val new_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> hint_db_name list -> tactic + int -> open_constr list -> hint_db_name list -> unit Proofview.tactic (** auto with default search depth and with the hint database "core" *) -val default_auto : tactic +val default_auto : unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database *) val full_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> tactic + int -> open_constr list -> unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database and doing delta *) val new_full_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> tactic + int -> open_constr list -> unit Proofview.tactic (** auto with default search depth and with all hint databases except the "v62" compatibility database *) -val default_full_auto : tactic +val default_full_auto : unit Proofview.tactic (** The generic form of auto (second arg [None] means all bases) *) val gen_auto : ?debug:Tacexpr.debug -> - int option -> open_constr list -> hint_db_name list option -> tactic + int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic (** The hidden version of auto *) val h_auto : ?debug:Tacexpr.debug -> - int option -> open_constr list -> hint_db_name list option -> tactic + int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic (** Trivial *) val trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list -> tactic + open_constr list -> hint_db_name list -> unit Proofview.tactic val gen_trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list option -> tactic + open_constr list -> hint_db_name list option -> unit Proofview.tactic val full_trivial : ?debug:Tacexpr.debug -> - open_constr list -> tactic + open_constr list -> unit Proofview.tactic val h_trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list option -> tactic - -val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds - -(** Hook for changing the initialization of auto *) - -val add_auto_init : (unit -> unit) -> unit + open_constr list -> hint_db_name list option -> unit Proofview.tactic -- cgit v1.2.3