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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
open Names
open Coqast
open Nametab
open Rawterm
open Util
open Genarg
type 'a or_metaid = AI of 'a | MetaId of loc * string
type reference_expr =
| RQualid of qualid located
| RIdent of identifier located
type direction_flag = bool (* true = Left-to-right false = right-to-right *)
type raw_red_flag =
| FBeta
| FIota
| FZeta
| FConst of qualid or_metanum list
| FDeltaBut of qualid or_metanum list
type raw_red_expr = (constr_ast, qualid or_metanum) red_expr_gen
let make_red_flag =
let rec add_flag red = function
| [] -> red
| FBeta :: lf -> add_flag { red with rBeta = true } lf
| FIota :: lf -> add_flag { red with rIota = true } lf
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
error
"Cannot set both constants to unfold and constants not to unfold";
add_flag { red with rConst = list_union red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] & not red.rDelta then
error
"Cannot set both constants to unfold and constants not to unfold";
add_flag
{ red with rConst = list_union red.rConst l; rDelta = true }
lf
in
add_flag
{rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
type 'a raw_hyp_location = (* To distinguish body and type of local defs *)
| InHyp of 'a
| InHypType of 'a
type extend_tactic_arg =
| TacticArgMeta of loc * string
| TacticArgAst of Coqast.t
type 'a induction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of identifier located
| ElimOnAnonHyp of int
type intro_pattern_expr =
| IntroOrAndPattern of intro_pattern_expr list list
| IntroWildcard
| IntroIdentifier of identifier
type 'id clause_pattern = int list option * ('id * int list) list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
type pattern_ast = Coqast.t
(* Type of patterns *)
type 'a match_pattern =
| Term of 'a
| Subterm of identifier option * 'a
(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
| NoHypId of 'a match_pattern
| Hyp of identifier located * '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 ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of intro_pattern_expr list
| TacIntrosUntil of quantified_hypothesis
| TacIntroMove of identifier option * identifier located option
| TacAssumption
| TacExact of 'constr
| TacApply of 'constr with_bindings
| TacElim of 'constr with_bindings * 'constr with_bindings option
| TacElimType of 'constr
| TacCase of 'constr with_bindings
| TacCaseType of 'constr
| TacFix of identifier option * int
| TacMutualFix of identifier * int * (identifier * int * 'constr) list
| TacCofix of identifier option
| TacMutualCofix of identifier * (identifier * 'constr) list
| TacCut of 'constr
| TacTrueCut of identifier option * 'constr
| TacForward of bool * name * 'constr
| TacGeneralize of 'constr list
| TacGeneralizeDep of 'constr
| TacLetTac of identifier * 'constr * 'id clause_pattern
| TacInstantiate of int * 'constr
(* Derived basic tactics *)
| TacOldInduction of quantified_hypothesis
| TacNewInduction of 'constr induction_arg
| TacOldDestruct of quantified_hypothesis
| TacNewDestruct of 'constr induction_arg
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
| TacDecomposeAnd of 'constr
| TacDecomposeOr of 'constr
| TacDecompose of 'ind list * 'constr
(*
| TacOldElim of 'constr
*)
| TacSpecialize of int option * 'constr with_bindings
| TacLApply of 'constr
(* Automation tactics *)
| TacTrivial of string list option
| TacAuto of int option * string list option
| TacAutoTDB of int option
| TacDestructHyp of (bool * identifier located)
| TacDestructConcl
| TacSuperAuto of (int option * qualid located list * bool * bool)
| TacDAuto of int option * int option
(* Context management *)
| TacClear of identifier or_metanum list
| TacClearBody of identifier or_metanum list
| TacMove of bool * identifier located * identifier located
| TacRename of identifier located * identifier located
(* Constructors *)
| TacLeft of 'constr substitution
| TacRight of 'constr substitution
| TacSplit of 'constr substitution
| TacAnyConstructor of raw_tactic_expr option
| TacConstructor of int or_metaid * 'constr substitution
(* Conversion *)
| TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list
| TacChange of 'constr * 'id raw_hyp_location list
(* Equivalence relations *)
| TacReflexivity
| TacSymmetry
| TacTransitivity of 'constr
(* For ML extensions *)
| TacExtend of string * ('constr,raw_tactic_expr) generic_argument list
(* For syntax extensions *)
| TacAlias of string *
(string * ('constr,raw_tactic_expr) generic_argument) list
* raw_tactic_expr
and raw_tactic_expr =
(constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_tactic_expr
and ('constr,'cst,'ind,'id) gen_tactic_expr =
| TacAtom of loc * ('constr,'cst,'ind,'id) gen_atomic_tactic_expr
| TacThen of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr
| TacThens of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr list
| TacFirst of ('constr,'cst,'ind,'id) gen_tactic_expr list
| TacSolve of ('constr,'cst,'ind,'id) gen_tactic_expr list
| TacTry of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacOrelse of ('constr,'cst,'ind,'id) gen_tactic_expr * ('constr,'cst,'ind,'id) gen_tactic_expr
| TacDo of int * ('constr,'cst,'ind,'id) gen_tactic_expr
| TacRepeat of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacProgress of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacAbstract of ('constr,'cst,'ind,'id) gen_tactic_expr * identifier option
| TacId
| TacFail of int
| TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr
| TacLetIn of (identifier located * constr_ast may_eval option * ('constr,'cst,'ind,'id) gen_tactic_arg) list * ('constr,'cst,'ind,'id) gen_tactic_expr
| TacLetCut of (identifier * constr_ast may_eval * ('constr,'cst,'ind,'id) gen_tactic_arg) list
| TacMatch of constr_ast may_eval * (pattern_ast,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
| TacMatchContext of direction_flag * (pattern_ast,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
| TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast
| TacFunRec of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast)
| TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg
and ('constr,'cst,'ind,'id) gen_tactic_fun_ast =
identifier option list * ('constr,'cst,'ind,'id) gen_tactic_expr
(* These are possible arguments of a tactic definition *)
and ('constr,'cst,'ind,'id) gen_tactic_arg =
| TacDynamic of loc * Dyn.t
| TacVoid
| MetaNumArg of loc * int
| MetaIdArg of loc * string
| ConstrMayEval of 'constr may_eval
| Reference of reference_expr
| Integer of int
| TacCall of loc * ('constr,'cst,'ind,'id) gen_tactic_arg * ('constr,'cst,'ind,'id) gen_tactic_arg list
| Tacexp of raw_tactic_expr
type raw_atomic_tactic_expr =
(constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_atomic_tactic_expr
type raw_tactic_arg =
(constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_tactic_arg
type raw_generic_argument =
(constr_ast,raw_tactic_expr) generic_argument
type closed_raw_generic_argument =
(constr_ast,raw_tactic_expr) generic_argument
type 'a raw_abstract_argument_type =
('a, constr_ast,raw_tactic_expr) abstract_argument_type
|
