blob: ace11aee304d9fce92415bb80cb95ad09b0f76be (
plain)
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
|
(***********************************************************************)
(* 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 Util
open Names
open Coqast
open Tacexpr
open Extend
open Genarg
(* Toplevel control exceptions *)
exception ProtectedLoop
exception Drop
exception Quit
type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK
| FACT | LEMMA
| COERCION | LCOERCION | OBJECT | LOBJECT | OBJCOERCION | LOBJCOERCION
| SUBCLASS | LSUBCLASS
open Nametab
type class_rawexpr = FunClass | SortClass | RefClass of qualid located
type printable =
| PrintTables
| PrintLocalContext
| PrintFullContext
| PrintSectionContext of qualid located
| PrintInspect of int
| PrintGrammar of string * string
| PrintLoadPath
| PrintModules
| PrintMLLoadPath
| PrintMLModules
| PrintName of qualid located
| PrintOpaqueName of qualid located
| PrintGraph
| PrintClasses
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
| PrintUniverses of string option
| PrintHint of qualid located
| PrintHintGoal
| PrintHintDbName of string
| PrintHintDb
type searchable =
| SearchPattern of pattern_ast
| SearchRewrite of pattern_ast
| SearchHead of qualid located
type locatable =
| LocateTerm of qualid located
| LocateLibrary of qualid located
| LocateFile of string
type goable =
| GoTo of int
| GoTop
| GoNext
| GoPrev
type showable =
| ShowGoal of int option
| ShowGoalImplicitly of int option
| ShowProof
| ShowNode
| ShowScript
| ShowExistentials
| ShowTree
| ShowProofNames
| ShowIntros of bool
| ExplainProof of int list
| ExplainTree of int list
type theorem_kind =
| Theorem
| Lemma
| Decl
| Fact
| Remark
type definition_kind =
| Definition
| LocalDefinition
type goal_kind =
| StartTheoremProof of theorem_kind
| StartDefinitionBody of definition_kind
type assumption_kind =
| AssumptionHypothesis
| AssumptionVariable
| AssumptionAxiom
| AssumptionParameter
type comment =
| CommentConstr of constr_ast
| CommentString of string
| CommentInt of int
type raw_constr_ast = t
type hints =
| HintsResolve of (identifier option * constr_ast) list
| HintsImmediate of (identifier option * constr_ast) list
| HintsUnfold of (identifier option * qualid located) list
| HintsConstructors of identifier * qualid located
| HintsExtern of identifier * int * raw_constr_ast * raw_tactic_expr
type search_restriction =
| SearchInside of qualid located list
| SearchOutside of qualid located list
type option_value =
| StringValue of string
| IntValue of int
| BoolValue of bool
type option_ref_value =
| StringRefValue of string
| QualidRefValue of qualid located
type rec_flag = bool (* true = Rec; false = NoRec *)
type verbose_flag = bool (* true = Verbose; false = Silent *)
type opacity_flag = bool (* true = Opaque; false = Transparent *)
type locality_flag = bool (* true = Local; false = Global *)
type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *)
type export_flag = bool (* true = Export; false = Import *)
type specif_flag = bool (* true = Specification; false = Implementation *)
type inductive_flag = bool (* true = Inductive; false = CoInductive *)
type sort_expr = t
type simple_binder = identifier * constr_ast
type 'a with_coercion = coercion_flag * 'a
type constructor_expr = simple_binder with_coercion
type inductive_expr =
identifier * simple_binder list * constr_ast * constructor_expr list
type fixpoint_expr =
identifier * simple_binder list * constr_ast * constr_ast
type cofixpoint_expr =
identifier * constr_ast * constr_ast
type local_binder =
| LocalRawDef of identifier * constr_ast
| LocalRawAssum of identifier list * constr_ast
type definition_expr =
| ProveBody of local_binder list * constr_ast
| DefineBody of local_binder list * raw_red_expr option * constr_ast
* constr_ast option
type local_decl_expr =
| AssumExpr of identifier * constr_ast
| DefExpr of identifier * constr_ast * constr_ast option
type grammar_entry_ast =
(loc * string) * Ast.entry_type option *
grammar_associativity * raw_grammar_rule list
type vernac_expr =
(* Control *)
| VernacList of located_vernac_expr list
| VernacLoad of verbose_flag * string
| VernacTime of vernac_expr
| VernacVar of identifier
(* Syntax *)
| VernacGrammar of string * grammar_entry_ast list
| VernacTacticGrammar of
(string * (string * grammar_production list) * raw_tactic_expr) list
| VernacSyntax of string * syntax_entry_ast list
| VernacInfix of grammar_associativity * int * string * qualid located
| VernacDistfix of grammar_associativity * int * string * qualid located
(* Gallina *)
| VernacDefinition of definition_kind * identifier * definition_expr *
Proof_type.declaration_hook
| VernacStartTheoremProof of theorem_kind * identifier * Coqast.t * bool *
Proof_type.declaration_hook
| VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
| VernacExactProof of constr_ast
| VernacAssumption of assumption_kind * simple_binder with_coercion list
| VernacInductive of inductive_flag * inductive_expr list
| VernacFixpoint of fixpoint_expr list
| VernacCoFixpoint of cofixpoint_expr list
| VernacScheme of (identifier * bool * qualid located * sort_expr) list
(* Gallina extensions *)
| VernacRecord of identifier with_coercion * simple_binder list
* sort_expr * identifier option * local_decl_expr with_coercion list
| VernacBeginSection of identifier
| VernacEndSection of identifier
| VernacRequire of
export_flag option * specif_flag option * qualid located list
| VernacImport of export_flag * qualid located list
| VernacCanonical of qualid located
| VernacCoercion of strength * qualid located * class_rawexpr * class_rawexpr
| VernacIdentityCoercion of strength * identifier *
class_rawexpr * class_rawexpr
(* Solving *)
| VernacSolve of int * raw_tactic_expr
| VernacSolveExistential of int * constr_ast
(* Auxiliary file and library management *)
| VernacRequireFrom of export_flag * specif_flag option * identifier * string
| VernacAddLoadPath of rec_flag * string * dir_path option
| VernacRemoveLoadPath of string
| VernacAddMLPath of rec_flag * string
| VernacDeclareMLModule of string list
| VernacChdir of string option
(* State management *)
| VernacWriteState of string
| VernacRestoreState of string
(* Resetting *)
| VernacResetName of identifier
| VernacResetInitial
| VernacBack of int
(* Commands *)
| VernacDeclareTacticDefinition of
loc * (identifier located * raw_tactic_expr) list
| VernacHints of string list * hints
| VernacHintDestruct of
identifier * (bool,unit) location * constr_ast * int * raw_tactic_expr
| VernacSyntacticDefinition of identifier * constr_ast * int option
| VernacDeclareImplicits of qualid located * int list option
| VernacSetOpacity of opacity_flag * qualid located list
| VernacUnsetOption of Goptions.option_name
| VernacSetOption of Goptions.option_name * option_value
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
| VernacPrintOption of Goptions.option_name
| VernacCheckMayEval of raw_red_expr option * int option * constr_ast
| VernacGlobalCheck of constr_ast
| VernacPrint of printable
| VernacSearch of searchable * search_restriction
| VernacLocate of locatable
| VernacComments of comment list
| VernacNop
(* Proof management *)
| VernacGoal of constr_ast
| VernacAbort of identifier option
| VernacAbortAll
| VernacRestart
| VernacSuspend
| VernacResume of identifier option
| VernacUndo of int
| VernacFocus of int option
| VernacUnfocus
| VernacGo of goable
| VernacShow of showable
| VernacCheckGuard
| VernacDebug of bool
(* Toplevel control *)
| VernacToplevelControl of exn
(* For extension *)
| VernacExtend of string * raw_generic_argument list
and located_vernac_expr = loc * vernac_expr
|
