diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:08:29 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:08:29 +0100 |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /tactics/auto.mli | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'tactics/auto.mli')
-rw-r--r-- | tactics/auto.mli | 170 |
1 files changed, 102 insertions, 68 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index eef6a0ee..521c5ed2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(*i $Id: auto.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term @@ -22,31 +19,52 @@ open Evd open Libnames open Vernacexpr open Mod_subst -(*i*) -type auto_tactic = - | Res_pf of constr * clausenv (* Hint Apply *) - | ERes_pf of constr * clausenv (* Hint EApply *) +(** Auto and related automation tactics *) + +type 'a auto_tactic = + | Res_pf of constr * 'a (** Hint Apply *) + | ERes_pf of constr * 'a (** Hint EApply *) | Give_exact of constr - | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *) - | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) + | Res_pf_THEN_trivial_fail of constr * 'a (** Hint Immediate *) + | Unfold_nth of evaluable_global_reference (** Hint Unfold *) + | Extern of Tacexpr.glob_tactic_expr (** Hint Extern *) -open Rawterm +open Glob_term -type pri_auto_tactic = { - pri : int; (* A number between 0 and 4, 4 = lower priority *) - pat : constr_pattern option; (* A pattern for the concl of the Goal *) - code : auto_tactic; (* the tactic to apply when the concl matches pat *) +type hints_path_atom = + | PathHints of global_reference list + | PathAny + +type 'a gen_auto_tactic = { + pri : int; (** A number between 0 and 4, 4 = lower priority *) + pat : constr_pattern option; (** A pattern for the concl of the Goal *) + name : hints_path_atom; (** A potential name to refer to the hint *) + code : 'a auto_tactic; (** the tactic to apply when the concl matches pat *) } -type stored_data = pri_auto_tactic +type pri_auto_tactic = clausenv gen_auto_tactic + +type stored_data = int * clausenv gen_auto_tactic type search_entry -(* The head may not be bound. *) +(** The head may not be bound. *) -type hint_entry = global_reference option * pri_auto_tactic +type hint_entry = global_reference option * types gen_auto_tactic + +type hints_path = + | PathAtom of hints_path_atom + | PathStar of hints_path + | PathSeq of hints_path * hints_path + | PathOr of hints_path * hints_path + | PathEmpty + | PathEpsilon + +val normalize_path : hints_path -> 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 @@ -58,12 +76,17 @@ module Hint_db : 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 iter : (global_reference option -> stored_data list -> unit) -> t -> unit + 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 @@ -72,8 +95,9 @@ type hint_db_name = string type hint_db = Hint_db.t type hints_entry = - | HintsResolveEntry of (int option * bool * constr) list - | HintsImmediateEntry of constr list + | 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 @@ -85,19 +109,23 @@ 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]. +(** [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 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 @@ -108,13 +136,13 @@ val print_hint_db_by_name : hint_db_name -> unit val print_hint_db : Hint_db.t -> unit -(* [make_exact_entry pri (c, ctyp)]. +(** [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 -> constr * constr -> hint_entry +val make_exact_entry : evar_map -> int option -> ?name:hints_path_atom -> constr * constr -> hint_entry -(* [make_apply_entry (eapply,verbose) pri (c,cty)]. +(** [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; @@ -122,21 +150,21 @@ val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry [cty] is the type of [c]. *) val make_apply_entry : - env -> evar_map -> bool * bool * bool -> int option -> constr * constr - -> hint_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. *) +(** 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 -> constr -> - hint_entry list + env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> + constr -> hint_entry list -(* [make_resolve_hyp hname htyp]. +(** [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. *) @@ -144,7 +172,7 @@ val make_resolves : val make_resolve_hyp : env -> evar_map -> named_declaration -> hint_entry list -(* [make_extern pri pattern tactic_expr] *) +(** [make_extern pri pattern tactic_expr] *) val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr @@ -161,11 +189,11 @@ val set_extern_subst_tactic : (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit -(* Create a Hint database from the pairs (name, constr). +(** 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 : bool -> constr list -> goal sigma -> hint_db +val make_local_hint_db : ?ts:transparent_state -> bool -> open_constr list -> goal sigma -> hint_db val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list @@ -173,63 +201,69 @@ val default_search_depth : int ref val auto_unif_flags : Unification.unify_flags -(* Try unification with the precompiled clause, then use registered Apply *) +(** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve_nodelta : (constr * clausenv) -> tactic val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic -(* [ConclPattern concl pat tacast]: +(** [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 -(* The Auto tactic *) +(** The Auto tactic *) -val auto : int -> constr list -> hint_db_name list -> tactic +(** The use of the "core" database can be de-activated by passing + "nocore" amongst the databases. *) -(* Auto with more delta. *) +val make_db_list : hint_db_name list -> hint_db list -val new_auto : int -> constr list -> hint_db_name list -> tactic +val auto : int -> open_constr list -> hint_db_name list -> tactic -(* auto with default search depth and with the hint database "core" *) +(** Auto with more delta. *) + +val new_auto : int -> open_constr list -> hint_db_name list -> tactic + +(** auto with default search depth and with the hint database "core" *) val default_auto : tactic -(* auto with all hint databases except the "v62" compatibility database *) -val full_auto : int -> constr list -> tactic +(** auto with all hint databases except the "v62" compatibility database *) +val full_auto : int -> open_constr list -> tactic -(* auto with all hint databases except the "v62" compatibility database +(** auto with all hint databases except the "v62" compatibility database and doing delta *) -val new_full_auto : int -> constr list -> tactic +val new_full_auto : int -> open_constr list -> tactic -(* auto with default search depth and with all hint databases +(** auto with default search depth and with all hint databases except the "v62" compatibility database *) val default_full_auto : tactic -(* The generic form of auto (second arg [None] means all bases) *) -val gen_auto : int option -> constr list -> hint_db_name list option -> tactic +(** The generic form of auto (second arg [None] means all bases) *) +val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic -(* The hidden version of auto *) -val h_auto : int option -> constr list -> hint_db_name list option -> tactic +(** The hidden version of auto *) +val h_auto : int option -> open_constr list -> hint_db_name list option -> tactic -(* Trivial *) -val trivial : constr list -> hint_db_name list -> tactic -val gen_trivial : constr list -> hint_db_name list option -> tactic -val full_trivial : constr list -> tactic -val h_trivial : constr list -> hint_db_name list option -> tactic +(** Trivial *) +val trivial : open_constr list -> hint_db_name list -> tactic +val gen_trivial : open_constr list -> hint_db_name list option -> tactic +val full_trivial : open_constr list -> tactic +val h_trivial : open_constr list -> hint_db_name list option -> tactic -val pr_autotactic : auto_tactic -> Pp.std_ppcmds +val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds -(*s The following is not yet up to date -- Papageno. *) +(** {6 The following is not yet up to date -- Papageno. } *) -(* DAuto *) -val dauto : int option * int option -> constr list -> tactic +(** DAuto *) +val dauto : int option * int option -> open_constr list -> tactic val default_search_decomp : int ref val default_dauto : tactic -val h_dauto : int option * int option -> constr list -> tactic -(* SuperAuto *) +val h_dauto : int option * int option -> open_constr list -> tactic + +(** SuperAuto *) type autoArguments = | UsingTDB @@ -241,4 +275,4 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti val h_superauto : int option -> reference list -> bool -> bool -> tactic -val auto_init : (unit -> unit) ref +val add_auto_init : (unit -> unit) -> unit |