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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \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
(*i*)
type auto_tactic =
| Res_pf of constr * unit clausenv (* Hint Apply *)
| ERes_pf of constr * unit clausenv (* Hint EApply *)
| Give_exact of constr
| Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
| Unfold_nth of global_reference (* Hint Unfold *)
| Extern of Coqast.t (* Hint Extern *)
open Rawterm
type pri_auto_tactic = {
hname : identifier; (* name of the hint *)
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
module Hint_db :
sig
type t
val empty : t
val find : constr_label -> t -> search_entry
val map_all : constr_label -> t -> pri_auto_tactic list
val map_auto : constr_label * constr -> t -> pri_auto_tactic list
val add_one : constr_label * pri_auto_tactic -> t -> t
val add_list : (constr_label * pri_auto_tactic) list -> t -> t
val iter : (constr_label -> stored_data list -> unit) -> t -> unit
end
type frozen_hint_db_table = Hint_db.t Stringmap.t
type hint_db_table = Hint_db.t Stringmap.t ref
val searchtable : hint_db_table
(* [make_exact_entry hint_name (c, ctyp)].
[hint_name] is the name of then hint;
[c] is the term given as an exact proof to solve the goal;
[ctyp] is the type of [hc]. *)
val make_exact_entry :
identifier -> constr * constr -> constr_label * pri_auto_tactic
(* [make_apply_entry (eapply,verbose) name (c,cty)].
[eapply] is true if this hint will be used only with EApply;
[name] is the name of then hint;
[c] is the term given as an exact proof to solve the goal;
[cty] is the type of [hc]. *)
val make_apply_entry :
env -> 'a evar_map -> bool * bool -> identifier -> constr * constr
-> constr_label * pri_auto_tactic
(* 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 -> 'a evar_map -> identifier -> bool * bool -> constr * constr ->
(constr_label * pri_auto_tactic) list
(* [make_resolve_hyp hname htyp].
used to add an hypothesis to the local hint database;
Never raises an User_exception;
If the hyp cannot be used as a Hint, the empty list is returned. *)
val make_resolve_hyp :
env -> 'a evar_map -> named_declaration ->
(constr_label * pri_auto_tactic) list
(* [make_extern name pri pattern tactic_ast] *)
val make_extern :
identifier -> int -> constr_pattern -> Coqast.t
-> constr_label * pri_auto_tactic
(* Create a Hint database from the pairs (name, constr).
Useful to take the current goal hypotheses as hints *)
val make_local_hint_db : goal sigma -> Hint_db.t
val priority : (int * 'a) list -> 'a list
val default_search_depth : int ref
(* Try unification with the precompiled clause, then use registered Apply *)
val unify_resolve : (constr * unit clausenv) -> tactic
(* The Auto tactic *)
val auto : int -> string 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 -> tactic
(* auto with default search depth and with all hint databases
except the "v62" compatibility database *)
val default_full_auto : tactic
(* The hidden version of auto *)
val h_auto : tactic_arg list -> tactic
(* Trivial *)
val trivial : string list -> tactic
val full_trivial : tactic
val h_trivial : tactic_arg list -> tactic
(*s The following is not yet up to date -- Papageno. *)
(* DAuto *)
val dauto : int option * int option -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
(* SuperAuto *)
type autoArguments =
| UsingTDB
| Destructing
val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
|
