blob: 24b16f283ceaa96c71c7a131da2a775ff979c8ed (
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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(** {6 Identifiers } *)
type identifier
(** Parsing and printing of identifiers *)
val string_of_id : identifier -> string
val id_of_string : string -> identifier
val id_ord : identifier -> identifier -> int
(** Identifiers sets and maps *)
module Idset : Set.S with type elt = identifier
module Idpred : Predicate.S with type elt = identifier
module Idmap : sig
include Map.S with type key = identifier
val exists : (identifier -> 'a -> bool) -> 'a t -> bool
val singleton : key -> 'a -> 'a t
end
(** {6 Various types based on identifiers } *)
type name = Name of identifier | Anonymous
type variable = identifier
(** {6 Directory paths = section names paths } *)
type module_ident = identifier
module ModIdmap : Map.S with type key = module_ident
type dir_path
(** Inner modules idents on top of list (to improve sharing).
For instance: A.B.C is ["C";"B";"A"] *)
val make_dirpath : module_ident list -> dir_path
val repr_dirpath : dir_path -> module_ident list
val empty_dirpath : dir_path
(** Printing of directory paths as ["coq_root.module.submodule"] *)
val string_of_dirpath : dir_path -> string
(** {6 Names of structure elements } *)
type label
val mk_label : string -> label
val string_of_label : label -> string
val pr_label : label -> Pp.std_ppcmds
val label_of_id : identifier -> label
val id_of_label : label -> identifier
module Labset : Set.S with type elt = label
module Labmap : Map.S with type key = label
(** {6 Unique names for bound modules } *)
type mod_bound_id
(** The first argument is a file name - to prevent conflict between
different files *)
val make_mbid : dir_path -> identifier -> mod_bound_id
val repr_mbid : mod_bound_id -> int * identifier * dir_path
val id_of_mbid : mod_bound_id -> identifier
val debug_string_of_mbid : mod_bound_id -> string
val string_of_mbid : mod_bound_id -> string
(** {6 The module part of the kernel name } *)
type module_path =
| MPfile of dir_path
| MPbound of mod_bound_id
| MPdot of module_path * label
val check_bound_mp : module_path -> bool
val string_of_mp : module_path -> string
module MPset : Set.S with type elt = module_path
module MPmap : Map.S with type key = module_path
(** Initial "seed" of the unique identifier generator *)
val initial_dir : dir_path
(** Name of the toplevel structure *)
val initial_path : module_path (** [= MPfile initial_dir] *)
(** {6 The absolute names of objects seen by kernel } *)
type kernel_name
(** Constructor and destructor *)
val make_kn : module_path -> dir_path -> label -> kernel_name
val repr_kn : kernel_name -> module_path * dir_path * label
val modpath : kernel_name -> module_path
val label : kernel_name -> label
val string_of_kn : kernel_name -> string
val pr_kn : kernel_name -> Pp.std_ppcmds
val kn_ord : kernel_name -> kernel_name -> int
module KNset : Set.S with type elt = kernel_name
module KNpred : Predicate.S with type elt = kernel_name
module KNmap : Map.S with type key = kernel_name
(** {6 Specific paths for declarations } *)
type constant
type mutual_inductive
(** Beware: first inductive has index 0 *)
type inductive = mutual_inductive * int
(** Beware: first constructor has index 1 *)
type constructor = inductive * int
(** *_env modules consider an order on user part of names
the others consider an order on canonical part of names*)
module Cmap : Map.S with type key = constant
module Cmap_env : Map.S with type key = constant
module Cpred : Predicate.S with type elt = constant
module Cset : Set.S with type elt = constant
module Cset_env : Set.S with type elt = constant
module Mindmap : Map.S with type key = mutual_inductive
module Mindmap_env : Map.S with type key = mutual_inductive
module Mindset : Set.S with type elt = mutual_inductive
module Indmap : Map.S with type key = inductive
module Constrmap : Map.S with type key = constructor
module Indmap_env : Map.S with type key = inductive
module Constrmap_env : Map.S with type key = constructor
val constant_of_kn : kernel_name -> constant
val constant_of_kn_equiv : kernel_name -> kernel_name -> constant
val make_con : module_path -> dir_path -> label -> constant
val make_con_equiv : module_path -> module_path -> dir_path
-> label -> constant
val user_con : constant -> kernel_name
val canonical_con : constant -> kernel_name
val repr_con : constant -> module_path * dir_path * label
val eq_constant : constant -> constant -> bool
val con_with_label : constant -> label -> constant
val string_of_con : constant -> string
val con_label : constant -> label
val con_modpath : constant -> module_path
val pr_con : constant -> Pp.std_ppcmds
val debug_pr_con : constant -> Pp.std_ppcmds
val debug_string_of_con : constant -> string
val mind_of_kn : kernel_name -> mutual_inductive
val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive
val make_mind : module_path -> dir_path -> label -> mutual_inductive
val make_mind_equiv : module_path -> module_path -> dir_path
-> label -> mutual_inductive
val user_mind : mutual_inductive -> kernel_name
val canonical_mind : mutual_inductive -> kernel_name
val repr_mind : mutual_inductive -> module_path * dir_path * label
val eq_mind : mutual_inductive -> mutual_inductive -> bool
val string_of_mind : mutual_inductive -> string
val mind_label : mutual_inductive -> label
val mind_modpath : mutual_inductive -> module_path
val pr_mind : mutual_inductive -> Pp.std_ppcmds
val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds
val debug_string_of_mind : mutual_inductive -> string
val ind_modpath : inductive -> module_path
val constr_modpath : constructor -> module_path
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
val eq_constructor : constructor -> constructor -> bool
(** Better to have it here that in Closure, since required in grammar.cma *)
type evaluable_global_reference =
| EvalVarRef of identifier
| EvalConstRef of constant
val eq_egr : evaluable_global_reference -> evaluable_global_reference
-> bool
(** {6 Hash-consing } *)
val hcons_string : string -> string
val hcons_ident : identifier -> identifier
val hcons_name : name -> name
val hcons_dirpath : dir_path -> dir_path
val hcons_con : constant -> constant
val hcons_mind : mutual_inductive -> mutual_inductive
val hcons_ind : inductive -> inductive
val hcons_construct : constructor -> constructor
(******)
type 'a tableKey =
| ConstKey of constant
| VarKey of identifier
| RelKey of 'a
type transparent_state = Idpred.t * Cpred.t
val empty_transparent_state : transparent_state
val full_transparent_state : transparent_state
val var_full_transparent_state : transparent_state
val cst_full_transparent_state : transparent_state
type inv_rel_key = int (** index in the [rel_context] part of environment
starting by the end, {e inverse}
of de Bruijn indice *)
type id_key = inv_rel_key tableKey
val eq_id_key : id_key -> id_key -> bool
(*equalities on constant and inductive
names for the checker*)
val eq_con_chk : constant -> constant -> bool
val eq_ind_chk : inductive -> inductive -> bool
|
