1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Names
open Term
open Sign
open Proof_type
open Tacmach
open Clenv
open Pattern
open Environ
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 *)
| 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 = {
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 search_entry = stored_data list * stored_data list * stored_data Btermdn.t
(* The head may not be bound. *)
type hint_entry = global_reference option * pri_auto_tactic
module Hint_db :
sig
type t
val empty : transparent_state -> bool -> t
val find : global_reference -> t -> search_entry
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 iter : (global_reference option -> stored_data list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> transparent_state
val set_transparent_state : t -> transparent_state -> t
end
type hint_db_name = string
type hint_db = Hint_db.t
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 current_db_names : unit -> hint_db_name list
val add_hints : locality_flag -> hint_db_name list -> hints -> unit
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
(* [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
(* [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
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
(* 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
(* [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 : bool -> constr list -> goal sigma -> hint_db
val priority : (int * 'a) list -> 'a list
val default_search_depth : int ref
val auto_unif_flags : Unification.unify_flags
(* 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]:
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 *)
val auto : int -> constr list -> hint_db_name list -> tactic
(* Auto with more delta. *)
val new_auto : int -> 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
and doing delta *)
val new_full_auto : int -> constr list -> tactic
(* 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 hidden version of auto *)
val h_auto : int option -> 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
val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
(*s The following is not yet up to date -- Papageno. *)
(* DAuto *)
val dauto : int option * int option -> constr list -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
val h_dauto : int option * int option -> constr list -> tactic
(* SuperAuto *)
type autoArguments =
| UsingTDB
| Destructing
(*
val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
*)
val h_superauto : int option -> reference list -> bool -> bool -> tactic
val auto_init : (unit -> unit) ref
|
