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
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Loc
open Names
open Constrexpr
open Libnames
open Globnames
open Nametab
open Genredexpr
open Genarg
open Pattern
open Decl_kinds
open Misctypes
open Locus
type direction_flag = bool (* true = Left-to-right false = right-to-right *)
type lazy_flag = bool (* true = lazy false = eager *)
type evars_flag = bool (* true = pose evars false = fail on evars *)
type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
type 'a core_induction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Id.t located
| ElimOnAnonHyp of int
type 'a induction_arg =
clear_flag * 'a core_induction_arg
type inversion_kind =
| SimpleInversion
| FullInversion
| FullInversionClear
type ('c,'id) inversion_strength =
| NonDepInversion of
inversion_kind * 'id list * 'c or_and_intro_pattern_expr located option
| DepInversion of
inversion_kind * 'c option * 'c or_and_intro_pattern_expr located option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
type 'id message_token =
| MsgString of string
| MsgInt of int
| MsgIdent of 'id
type 'constr induction_clause =
'constr with_bindings induction_arg *
(intro_pattern_naming_expr located option (* eqn:... *)
* 'constr or_and_intro_pattern_expr located option) (* as ... *)
type ('constr,'id) induction_clause_list =
'constr induction_clause list
* 'constr with_bindings option (* using ... *)
* 'id clause_expr option (* in ... *)
type 'a with_bindings_arg = clear_flag * 'a with_bindings
type multi =
| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus
(* Type of patterns *)
type 'a match_pattern =
| Term of 'a
| Subterm of bool * Id.t option * 'a
(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
| Hyp of Name.t located * 'a match_pattern
| Def of Name.t located * 'a match_pattern * 'a match_pattern
(* Type of a Match rule for Match Context and Match *)
type ('a,'t) match_rule =
| Pat of 'a match_context_hyps list * 'a match_pattern * 't
| All of 't
type ml_tactic_name = {
mltac_plugin : string;
mltac_tactic : string;
}
(** Composite types *)
(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
in the environment by the effective calls to Intro, Inversion, etc
The [constr_expr] field is [None] in TacDef though *)
type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
type open_glob_constr = unit * glob_constr_and_expr
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
type delayed_open_constr_with_bindings =
Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings
type delayed_open_constr =
Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
type intro_pattern = delayed_open_constr intro_pattern_expr located
type intro_patterns = delayed_open_constr intro_pattern_expr located list
type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
type intro_pattern_naming = intro_pattern_naming_expr located
(** Generic expressions for atomic tactics *)
type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of 'trm intro_pattern_expr located list
| TacIntroMove of Id.t option * 'nam move_location
| TacExact of 'trm
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
(clear_flag * 'nam * 'trm intro_pattern_expr located option) option
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacFix of Id.t option * int
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
| TacCofix of Id.t option
| TacMutualCofix of Id.t * (Id.t * 'trm) list
| TacAssert of
bool * ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option *
'trm intro_pattern_expr located option * 'trm
| TacGeneralize of ('trm with_occurrences * Name.t) list
| TacGeneralizeDep of 'trm
| TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
intro_pattern_naming_expr located option
(* Derived basic tactics *)
| TacInductionDestruct of
rec_flag * evars_flag * ('trm,'nam) induction_clause_list
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
(* Automation tactics *)
| TacTrivial of debug * 'trm list * string list option
| TacAuto of debug * int or_var option * 'trm list * string list option
(* Context management *)
| TacClear of bool * 'nam list
| TacClearBody of 'nam list
| TacMove of bool * 'nam * 'nam move_location
| TacRename of ('nam *'nam) list
(* Trmuctors *)
| TacSplit of evars_flag * 'trm bindings list
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
| TacChange of 'pat option * 'trm * 'nam clause_expr
(* Equivalence relations *)
| TacSymmetry of 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
(bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr *
('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option
| TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
(** Possible arguments of a tactic definition *)
and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg =
| TacDynamic of Loc.t * Dyn.t
| TacGeneric of 'lev generic_argument
| MetaIdArg of Loc.t * bool * string
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| UConstr of 'trm (* We can reuse ['trm] because terms and untyped terms
only differ at interpretation time (and not at
internalisation), and the output of interpration
is not a variant of [tactic_expr]. *)
| Reference of 'ref
| TacCall of Loc.t * 'ref *
('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list
| TacExternal of Loc.t * string * string *
('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list
| TacFreshId of string or_var list
| Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr
| TacPretype of 'trm
| TacNumgoals
(** Generic ltac expressions.
't : terms, 'p : patterns, 'c : constants, 'i : inductive,
'r : ltac refs, 'n : idents, 'l : levels *)
and ('t,'p,'c,'r,'n,'l) gen_tactic_expr =
| TacAtom of Loc.t * ('t,'p,'c,'r,'n,'l) gen_atomic_tactic_expr
| TacThen of
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacDispatch of
('t,'p,'c,'r,'n,'l) gen_tactic_expr list
| TacExtendTac of
('t,'p,'c,'r,'n,'l) gen_tactic_expr array *
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr array
| TacThens of
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr list
| TacThens3parts of
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr array *
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr array
| TacFirst of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
| TacComplete of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacSolve of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
| TacTry of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacOr of
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacOnce of
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacExactlyOnce of
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacOrelse of
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacDo of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacTimeout of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacTime of string option * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacRepeat of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacProgress of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacShowHyps of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacAbstract of
('t,'p,'c,'r,'n,'l) gen_tactic_expr * Id.t option
| TacId of 'n message_token list
| TacFail of int or_var * 'n message_token list
| TacInfo of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacLetIn of rec_flag *
(Id.t located * ('t,'p,'c,'r,'n,'l) gen_tactic_arg) list *
('t,'p,'c,'r,'n,'l) gen_tactic_expr
| TacMatch of lazy_flag *
('t,'p,'c,'r,'n,'l) gen_tactic_expr *
('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list
| TacMatchGoal of lazy_flag * direction_flag *
('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list
| TacFun of ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast
| TacArg of ('t,'p,'c,'r,'n,'l) gen_tactic_arg located
(* For ML extensions *)
| TacML of Loc.t * ml_tactic_name * 'l generic_argument list
(* For syntax extensions *)
| TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
and ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast =
Id.t option list * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
(** Globalized tactics *)
type g_trm = glob_constr_and_expr
type g_pat = glob_constr_and_expr * constr_pattern
type g_cst = evaluable_global_reference and_short_name or_var
type g_ref = ltac_constant located or_var
type g_nam = Id.t located
type glob_tactic_expr =
(g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_expr
type glob_atomic_tactic_expr =
(g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_atomic_tactic_expr
type glob_tactic_arg =
(g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_arg
(** Raw tactics *)
type r_trm = constr_expr
type r_pat = constr_pattern_expr
type r_cst = reference or_by_notation
type r_ref = reference
type r_nam = Id.t located
type r_lev = rlevel
type raw_atomic_tactic_expr =
(r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_atomic_tactic_expr
type raw_tactic_expr =
(r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_expr
type raw_tactic_arg =
(r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_arg
(** Misc *)
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
|
