diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 56 |
1 files changed, 36 insertions, 20 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 132b9063..072e0298 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Util @@ -23,26 +23,26 @@ open Libnames open Vernacexpr open Mod_subst (*i*) - -type auto_tactic = + +type auto_tactic = | Res_pf of constr * clausenv (* Hint Apply *) | ERes_pf of constr * clausenv (* Hint EApply *) - | Give_exact of constr + | 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 *) open Rawterm -type pri_auto_tactic = { +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 stored_data = pri_auto_tactic +type stored_data = pri_auto_tactic -type search_entry = stored_data list * stored_data list * stored_data Btermdn.t +type search_entry (* The head may not be bound. *) @@ -63,26 +63,40 @@ module Hint_db : val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t + + 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 * constr) list + | HintsImmediateEntry of constr list + | 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 + | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location * + (patvar list * constr_pattern) * 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]. +(* [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 + [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 current_db_names : unit -> hint_db_name list -val add_hints : locality_flag -> hint_db_name list -> hints -> unit +val interp_hints : hints_expr -> hints_entry + +val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit val print_searchtable : unit -> unit @@ -92,19 +106,21 @@ val print_hint_ref : global_reference -> unit val print_hint_db_by_name : hint_db_name -> unit -(* [make_exact_entry pri (c, ctyp)]. +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 : int option -> constr * constr -> hint_entry +val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry (* [make_apply_entry (eapply,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 + [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 -> constr * constr -> hint_entry @@ -117,7 +133,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> int option -> constr -> + env -> evar_map -> bool * bool * bool -> int option -> constr -> hint_entry list (* [make_resolve_hyp hname htyp]. @@ -125,7 +141,7 @@ val make_resolves : Never raises a user exception; If the hyp cannot be used as a Hint, the empty list is returned. *) -val make_resolve_hyp : +val make_resolve_hyp : env -> evar_map -> named_declaration -> hint_entry list (* [make_extern pri pattern tactic_expr] *) @@ -163,7 +179,7 @@ val unify_resolve_nodelta : (constr * clausenv) -> tactic val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic (* [ConclPattern concl pat tacast]: - if the term concl matches the pattern pat, (in sense of + 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 *) @@ -187,7 +203,7 @@ val full_auto : int -> constr list -> tactic and doing delta *) val new_full_auto : int -> 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 @@ -216,8 +232,8 @@ val h_dauto : int option * int option -> constr list -> tactic (* SuperAuto *) type autoArguments = - | UsingTDB - | Destructing + | UsingTDB + | Destructing (* val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic |