-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathcoqlib.mli
300 lines (240 loc) · 10.4 KB
/
coqlib.mli
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
300
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
open Names
(** Indirection between logical names and global references.
This module provides a mechanism to bind “names” to constants and to look up
these constants using their names.
The two main functions are [register_ref n r] which binds the name [n] to
the reference [r] and [lib_ref n] which returns the previously registered
reference under name [n].
The first function is meant to be available through the vernacular command
[Register r as n], so that plug-ins can refer to a constant without knowing
its user-facing name, the precise module path in which it is defined, etc.
For instance, [lib_ref "core.eq.type"] returns the proper [GlobRef.t] for
the type of the core equality type.
*)
(** Registers a global reference under the given name. *)
val register_ref : string -> GlobRef.t -> unit
(** Retrieves the reference bound to the given name (by a previous call to {!register_ref}).
Raises an error if no reference is bound to this name. *)
val lib_ref : string -> GlobRef.t
(** Checks whether a name refers to a registered constant.
For any name [n], if [has_ref n] returns [true], [lib_ref n] will succeed. *)
val has_ref : string -> bool
(** Checks whether a name is bound to a known inductive. *)
val check_ind_ref : string -> inductive -> bool
(** List of all currently bound names. *)
val get_lib_refs : unit -> (string * GlobRef.t) list
(* Exceptions to deprecation *)
(** {2 For Equality tactics} *)
type coq_sigma_data = {
proj1 : GlobRef.t;
proj2 : GlobRef.t;
elim : GlobRef.t;
intro : GlobRef.t;
typ : GlobRef.t }
val build_sigma_set : coq_sigma_data delayed
val build_sigma_type : coq_sigma_data delayed
val build_sigma : coq_sigma_data delayed
type coq_eq_data = {
eq : GlobRef.t;
ind : GlobRef.t;
refl : GlobRef.t;
sym : GlobRef.t;
trans: GlobRef.t;
congr: GlobRef.t }
val build_coq_eq_data : coq_eq_data delayed
val build_coq_identity_data : coq_eq_data delayed
val build_coq_jmeq_data : coq_eq_data delayed
(* XXX: Some tactics special case JMeq, they should instead check for
the constant, not the module *)
(** For tactics/commands requiring vernacular libraries *)
val check_required_library : string list -> unit
(* Used by obligations *)
val datatypes_module_name : string list
(* Used by ind_schemes *)
val logic_module_name : string list
(* Used by tactics *)
val jmeq_module_name : string list
(*************************************************************************)
(** {2 DEPRECATED} *)
(*************************************************************************)
(** All the functions below are deprecated and should go away in the
next coq version ... *)
(** [find_reference caller_message [dir;subdir;...] s] returns a global
reference to the name dir.subdir.(...).s; the corresponding module
must have been required or in the process of being compiled so that
it must be used lazily; it raises an anomaly with the given message
if not found *)
val find_reference : string -> string list -> string -> GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** This just prefixes find_reference with Coq... *)
val coq_reference : string -> string list -> string -> GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Search in several modules (not prefixed by "Coq") *)
val gen_reference_in_modules : string->string list list-> string -> GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val arith_modules : string list list
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val zarith_base_modules : string list list
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val init_modules : string list list
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** {6 Global references } *)
(** Modules *)
val logic_module : ModPath.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val logic_type_module : DirPath.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Identity *)
val id : Constant.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val type_of_id : Constant.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Natural numbers *)
val nat_path : Libnames.full_path
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_nat : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val path_of_O : constructor
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val path_of_S : constructor
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_O : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_S : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Booleans *)
val glob_bool : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val path_of_true : constructor
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val path_of_false : constructor
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_true : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_false : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Equality *)
val glob_eq : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_identity : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val glob_jmeq : GlobRef.t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** {6 ... } *)
(** Constructions and patterns related to Coq initial state are unknown
at compile time. Therefore, we can only provide methods to build
them at runtime. This is the purpose of the [constr delayed] and
[constr_pattern delayed] types. Objects of this time needs to be
forced with [delayed_force] to get the actual constr or pattern
at runtime. *)
type coq_bool_data = {
andb : GlobRef.t;
andb_prop : GlobRef.t;
andb_true_intro : GlobRef.t
}
val build_bool_type : coq_bool_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Non-dependent pairs in Set from Datatypes *)
val build_prod : coq_sigma_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_eq : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** = [(build_coq_eq_data()).eq] *)
val build_coq_eq_refl : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** = [(build_coq_eq_data()).refl] *)
val build_coq_eq_sym : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** = [(build_coq_eq_data()).sym] *)
val build_coq_f_equal2 : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Data needed for discriminate and injection *)
type coq_inversion_data = {
inv_eq : GlobRef.t; (** : forall params, args -> Prop *)
inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args
-> P args *)
inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args ->
f params = f args *)
}
val build_coq_inversion_eq_data : coq_inversion_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_inversion_identity_data : coq_inversion_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_inversion_jmeq_data : coq_inversion_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_inversion_eq_true_data : coq_inversion_data delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Specif *)
val build_coq_sumbool : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** {6 ... }
Connectives
The False proposition *)
val build_coq_False : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** The True proposition and its unique proof *)
val build_coq_True : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_I : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Negation *)
val build_coq_not : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Conjunction *)
val build_coq_and : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_conj : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_iff : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_iff_left_proj : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_iff_right_proj : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Pairs *)
val build_coq_prod : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val build_coq_pair : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Disjunction *)
val build_coq_or : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
(** Existential quantifier *)
val build_coq_ex : GlobRef.t delayed
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_eq_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_identity_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_jmeq_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_eq_true_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_existS_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_existT_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_exist_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_not_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_False_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_sumbool_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_sig_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_or_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]
val coq_iff_ref : GlobRef.t lazy_t
[@@ocaml.deprecated "Please use Coqlib.lib_ref"]