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
|
(************************************************************************)
(* 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: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Util
open Names
open Rawterm
open Extend
open Genarg
open Topconstr
open Tacexpr
open Vernacexpr
open Libnames
(* The lexer and parser of Coq. *)
val lexer : Compat.lexer
module Gram : Grammar.S with type te = Compat.token
(* The superclass of all grammar entries *)
type grammar_object
(* The type of typed grammar objects *)
type typed_entry
type entry_type = argument_type
val type_of_typed_entry : typed_entry -> entry_type
val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
val get_constr_entry :
bool -> constr_entry -> grammar_object Gram.Entry.e * int option
val grammar_extend :
grammar_object Gram.Entry.e -> Gramext.position option ->
(* for reinitialization if ever: *) Gramext.g_assoc option ->
(string option * Gramext.g_assoc option *
(Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
-> unit
val remove_grammars : int -> unit
val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
(* Parse a string *)
val parse_string : 'a Gram.Entry.e -> string -> 'a
val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
(* Entry types *)
(* Table of Coq's grammar entries *)
type gram_universe
val create_univ_if_new : string -> string * gram_universe
val get_univ : string -> string * gram_universe
val get_entry : string * gram_universe -> string -> typed_entry
val entry_type : string * gram_universe -> string -> entry_type option
val get_entry_type : string * string -> entry_type
val create_entry_if_new :
string * gram_universe -> string -> entry_type -> unit
val create_entry :
string * gram_universe -> string -> entry_type -> typed_entry
val force_entry_type :
string * gram_universe -> string -> entry_type -> typed_entry
val create_constr_entry :
string * gram_universe -> string -> constr_expr Gram.Entry.e
val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.Entry.e
val get_generic_entry : string -> grammar_object Gram.Entry.e
val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
(* Tactics as arguments *)
val tactic_main_level : int
val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type
val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type
val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type
val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type
val is_tactic_genarg : argument_type -> bool
val tactic_genarg_level : string -> int option
(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e
(* Initial state of the grammar *)
module Prim :
sig
open Util
open Names
open Libnames
val preident : string Gram.Entry.e
val ident : identifier Gram.Entry.e
val name : name located Gram.Entry.e
val identref : identifier located Gram.Entry.e
val pattern_ident : identifier Gram.Entry.e
val pattern_identref : identifier located Gram.Entry.e
val base_ident : identifier Gram.Entry.e
val natural : int Gram.Entry.e
val bigint : Bigint.bigint Gram.Entry.e
val integer : int Gram.Entry.e
val string : string Gram.Entry.e
val qualid : qualid located Gram.Entry.e
val fullyqualid : identifier list located Gram.Entry.e
val reference : reference Gram.Entry.e
val dirpath : dir_path Gram.Entry.e
val ne_string : string Gram.Entry.e
val var : identifier located Gram.Entry.e
end
module Constr :
sig
val constr : constr_expr Gram.Entry.e
val constr_eoi : constr_expr Gram.Entry.e
val lconstr : constr_expr Gram.Entry.e
val binder_constr : constr_expr Gram.Entry.e
val operconstr : constr_expr Gram.Entry.e
val ident : identifier Gram.Entry.e
val global : reference Gram.Entry.e
val sort : rawsort Gram.Entry.e
val pattern : cases_pattern_expr Gram.Entry.e
val annot : constr_expr Gram.Entry.e
val constr_pattern : constr_expr Gram.Entry.e
val lconstr_pattern : constr_expr Gram.Entry.e
val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
val binder_let : local_binder list Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
end
module Module :
sig
val module_expr : module_ast Gram.Entry.e
val module_type : module_type_ast Gram.Entry.e
end
module Tactic :
sig
open Rawterm
val open_constr : open_constr_expr Gram.Entry.e
val casted_open_constr : open_constr_expr Gram.Entry.e
val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
val bindings : constr_expr bindings Gram.Entry.e
val constr_may_eval : (constr_expr,reference or_by_notation) may_eval Gram.Entry.e
val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
val int_or_var : int or_var Gram.Entry.e
val red_expr : raw_red_expr Gram.Entry.e
val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic_expr : raw_tactic_expr Gram.Entry.e
val binder_tactic : raw_tactic_expr Gram.Entry.e
val tactic : raw_tactic_expr Gram.Entry.e
val tactic_eoi : raw_tactic_expr Gram.Entry.e
end
module Vernac_ :
sig
open Decl_kinds
val gallina : vernac_expr Gram.Entry.e
val gallina_ext : vernac_expr Gram.Entry.e
val command : vernac_expr Gram.Entry.e
val syntax : vernac_expr Gram.Entry.e
val vernac : vernac_expr Gram.Entry.e
(* MMode *)
val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e
(*/ MMode *)
val vernac_eoi : vernac_expr Gram.Entry.e
end
(* Binding entry names to campl4 entries *)
val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
bool -> constr_production_entry -> Compat.token Gramext.g_symbol
(* Registering/resetting the level of an entry *)
val find_position :
bool (* true if for creation in pattern entry; false if in constr entry *) ->
Gramext.g_assoc option -> int option ->
Gramext.position option * Gramext.g_assoc option * string option *
(* for reinitialization: *) Gramext.g_assoc option
val synchronize_level_positions : unit -> unit
val register_empty_levels : bool -> int list ->
(Gramext.position option * Gramext.g_assoc option *
string option * Gramext.g_assoc option) list
val remove_levels : int -> unit
val coerce_global_to_id : reference -> identifier
|
