source: extracted/identifiers.mli @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 9.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open Util
34
35open List
36
37open Lists
38
39open Extralib
40
41open ErrorMessages
42
43open PreIdentifiers
44
45open Errors
46
47type universe =
48  Positive.pos
49  (* singleton inductive, whose constructor was mk_universe *)
50
51val universe_rect_Type4 :
52  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
53
54val universe_rect_Type5 :
55  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
56
57val universe_rect_Type3 :
58  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
59
60val universe_rect_Type2 :
61  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
62
63val universe_rect_Type1 :
64  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
65
66val universe_rect_Type0 :
67  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1
68
69val next_identifier :
70  PreIdentifiers.identifierTag -> universe -> Positive.pos
71
72val universe_inv_rect_Type4 :
73  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
74  'a1
75
76val universe_inv_rect_Type3 :
77  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
78  'a1
79
80val universe_inv_rect_Type2 :
81  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
82  'a1
83
84val universe_inv_rect_Type1 :
85  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
86  'a1
87
88val universe_inv_rect_Type0 :
89  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
90  'a1
91
92val universe_discr :
93  PreIdentifiers.identifierTag -> universe -> universe -> __
94
95val universe_jmdiscr :
96  PreIdentifiers.identifierTag -> universe -> universe -> __
97
98val new_universe : PreIdentifiers.identifierTag -> universe
99
100val fresh :
101  PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
102  universe) Types.prod
103
104type fresh_for_univ = __
105
106type 'a env_fresh_for_univ = __
107
108val eq_identifier :
109  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
110  PreIdentifiers.identifier -> Bool.bool
111
112val eq_identifier_elim :
113  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
114  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
115
116open Deqsets
117
118val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet
119
120val word_of_identifier :
121  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos
122
123val identifier_eq :
124  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
125  PreIdentifiers.identifier -> (__, __) Types.sum
126
127val identifier_of_nat :
128  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier
129
130type 'a distinct_env = __
131
132val check_member_env :
133  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
134  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res
135
136val check_distinct_env :
137  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
138  List.list -> __ Errors.res
139
140open PositiveMap
141
142type 'a identifier_map =
143  'a PositiveMap.positive_map
144  (* singleton inductive, whose constructor was an_id_map *)
145
146val identifier_map_rect_Type4 :
147  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
148  'a1 identifier_map -> 'a2
149
150val identifier_map_rect_Type5 :
151  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
152  'a1 identifier_map -> 'a2
153
154val identifier_map_rect_Type3 :
155  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
156  'a1 identifier_map -> 'a2
157
158val identifier_map_rect_Type2 :
159  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
160  'a1 identifier_map -> 'a2
161
162val identifier_map_rect_Type1 :
163  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
164  'a1 identifier_map -> 'a2
165
166val identifier_map_rect_Type0 :
167  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
168  'a1 identifier_map -> 'a2
169
170val identifier_map_inv_rect_Type4 :
171  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
172  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
173
174val identifier_map_inv_rect_Type3 :
175  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
176  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
177
178val identifier_map_inv_rect_Type2 :
179  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
180  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
181
182val identifier_map_inv_rect_Type1 :
183  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
184  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
185
186val identifier_map_inv_rect_Type0 :
187  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
188  PositiveMap.positive_map -> __ -> 'a2) -> 'a2
189
190val identifier_map_discr :
191  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
192  __
193
194val identifier_map_jmdiscr :
195  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
196  __
197
198val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map
199
200val lookup0 :
201  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
202  PreIdentifiers.identifier -> 'a1 Types.option
203
204val lookup_def :
205  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
206  PreIdentifiers.identifier -> 'a1 -> 'a1
207
208val member0 :
209  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
210  PreIdentifiers.identifier -> Bool.bool
211
212val lookup_safe :
213  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
214  PreIdentifiers.identifier -> 'a1
215
216val add :
217  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
218  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
219
220val elements :
221  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
222  (PreIdentifiers.identifier, 'a1) Types.prod List.list
223
224val idmap_all :
225  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
226  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool
227
228val update0 :
229  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
230  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res
231
232val remove :
233  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
234  PreIdentifiers.identifier -> 'a1 identifier_map
235
236val foldi0 :
237  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
238  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2
239
240val fold_inf :
241  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
242  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
243
244val find0 :
245  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
246  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
247  (PreIdentifiers.identifier, 'a1) Types.prod Types.option
248
249val lookup_present :
250  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
251  PreIdentifiers.identifier -> 'a1
252
253val update_present :
254  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
255  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map
256
257type 'a fresh_for_map = __
258
259type identifier_set = Types.unit0 identifier_map
260
261val empty_set : PreIdentifiers.identifierTag -> identifier_set
262
263val add_set :
264  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
265  -> identifier_set
266
267val singleton_set :
268  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set
269
270val union_set :
271  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
272  identifier_set
273
274val minus_set :
275  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
276  'a1 identifier_map
277
278val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid
279
280val id_map_size :
281  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat
282
283open Proper
284
285val set_from_list :
286  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
287  Types.unit0 identifier_map
288
289val dpi1__o__id_set_from_list__o__inject :
290  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
291  Types.dPair -> Types.unit0 identifier_map Types.sig0
292
293val eject__o__id_set_from_list__o__inject :
294  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
295  Types.sig0 -> Types.unit0 identifier_map Types.sig0
296
297val id_set_from_list__o__inject :
298  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
299  Types.unit0 identifier_map Types.sig0
300
301val dpi1__o__id_set_from_list :
302  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
303  Types.dPair -> Types.unit0 identifier_map
304
305val eject__o__id_set_from_list :
306  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
307  Types.sig0 -> Types.unit0 identifier_map
308
309val choose :
310  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
311  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
312  Types.prod Types.option
313
314val try_remove :
315  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
316  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
317  Types.option
318
319val id_set_of_map :
320  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
321
322val set_of_list :
323  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
324  identifier_set
325
326val domain_of_map :
327  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set
328
Note: See TracBrowser for help on using the repository browser.