source: extracted/globalenvs.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: 11.6 KB
Line 
1open Preamble
2
3open ErrorMessages
4
5open Option
6
7open Setoids
8
9open Monad
10
11open Jmeq
12
13open Russell
14
15open Positive
16
17open PreIdentifiers
18
19open Bool
20
21open Relations
22
23open Nat
24
25open List
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open Errors
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open Extralib
46
47open Lists
48
49open Identifiers
50
51open Exp
52
53open Arithmetic
54
55open Vector
56
57open Div_and_mod
58
59open Util
60
61open FoldStuff
62
63open BitVector
64
65open Extranat
66
67open Integers
68
69open AST
70
71open Coqlib
72
73open Values
74
75open FrontEndVal
76
77open Hide
78
79open ByteValues
80
81open Division
82
83open Z
84
85open BitVectorZ
86
87open Pointers
88
89open GenMem
90
91open FrontEndMem
92
93type 'f genv_t = { functions : 'f PositiveMap.positive_map;
94                   nextfunction : Positive.pos;
95                   symbols : Pointers.block Identifiers.identifier_map }
96
97val genv_t_rect_Type4 :
98  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
99  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
100
101val genv_t_rect_Type5 :
102  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
103  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
104
105val genv_t_rect_Type3 :
106  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
107  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
108
109val genv_t_rect_Type2 :
110  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
111  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
112
113val genv_t_rect_Type1 :
114  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
115  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
116
117val genv_t_rect_Type0 :
118  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
119  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
120
121val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map
122
123val nextfunction : 'a1 genv_t -> Positive.pos
124
125val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map
126
127val genv_t_inv_rect_Type4 :
128  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
129  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
130
131val genv_t_inv_rect_Type3 :
132  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
133  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
134
135val genv_t_inv_rect_Type2 :
136  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
137  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
138
139val genv_t_inv_rect_Type1 :
140  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
141  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
142
143val genv_t_inv_rect_Type0 :
144  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
145  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
146
147val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __
148
149val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __
150
151val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t
152
153val add_funct : (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t
154
155val add_symbol : AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t
156
157val empty_mem : GenMem.mem1
158
159val empty0 : 'a1 genv_t
160
161val add_functs :
162  'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t
163
164val find_symbol : 'a1 genv_t -> AST.ident -> Pointers.block Types.option
165
166val store_init_data :
167  'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data ->
168  GenMem.mem1 Types.option
169
170val size_init_data : AST.init_data -> Nat.nat
171
172val store_init_data_list :
173  'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data
174  List.list -> GenMem.mem1 Types.option
175
176val size_init_data_list : AST.init_data List.list -> Nat.nat
177
178val add_globals :
179  ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem1) Types.prod ->
180  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
181  genv_t, GenMem.mem1) Types.prod
182
183val init_globals :
184  ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem1 ->
185  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
186  GenMem.mem1 Errors.res
187
188val globalenv_allocmem :
189  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1 genv_t,
190  GenMem.mem1) Types.prod
191
192val globalenv :
193  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t
194
195val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t
196
197val init_mem :
198  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem1
199  Errors.res
200
201val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem1
202
203val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option
204
205val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option
206
207val symbol_for_block : 'a1 genv_t -> Pointers.block -> AST.ident Types.option
208
209val symbol_of_function_block : 'a1 genv_t -> Pointers.block -> AST.ident
210
211val symbol_of_function_block' :
212  'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident
213
214val find_funct_ptr_id :
215  'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option
216
217val opt_eq_from_res__o__ffpi_drop__o__inject :
218  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
219  Types.sig0
220
221val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
222  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
223  'a2) Types.dPair -> __ Types.sig0
224
225val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
226  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
227  Types.sig0 -> __ Types.sig0
228
229val jmeq_to_eq__o__ffpi_drop__o__inject :
230  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
231
232val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
233  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
234  Types.sig0
235
236val dpi1__o__ffpi_drop__o__inject :
237  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
238  -> __ Types.sig0
239
240val eject__o__ffpi_drop__o__inject :
241  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
242  Types.sig0
243
244val ffpi_drop__o__inject :
245  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
246
247val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident
248
249val symbol_of_function_val' : 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident
250
251val find_funct_id :
252  'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option
253
254val opt_eq_from_res__o__ffi_drop__o__inject :
255  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
256  Types.sig0
257
258val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
259  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2)
260  Types.dPair -> __ Types.sig0
261
262val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
263  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
264  Types.sig0 -> __ Types.sig0
265
266val jmeq_to_eq__o__ffi_drop__o__inject :
267  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
268
269val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
270  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
271  Types.sig0
272
273val dpi1__o__ffi_drop__o__inject :
274  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
275  __ Types.sig0
276
277val eject__o__ffi_drop__o__inject :
278  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
279  Types.sig0
280
281val ffi_drop__o__inject :
282  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0
283
284val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
285
286val alloc_pair :
287  GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
288  GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1
289
290val prod_jmdiscr0 : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
291
292val related_globals_rect_Type4 :
293  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
294  -> 'a3
295
296val related_globals_rect_Type5 :
297  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
298  -> 'a3
299
300val related_globals_rect_Type3 :
301  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
302  -> 'a3
303
304val related_globals_rect_Type2 :
305  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
306  -> 'a3
307
308val related_globals_rect_Type1 :
309  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
310  -> 'a3
311
312val related_globals_rect_Type0 :
313  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
314  -> 'a3
315
316val related_globals_inv_rect_Type4 :
317  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
318  'a3) -> 'a3
319
320val related_globals_inv_rect_Type3 :
321  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
322  'a3) -> 'a3
323
324val related_globals_inv_rect_Type2 :
325  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
326  'a3) -> 'a3
327
328val related_globals_inv_rect_Type1 :
329  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
330  'a3) -> 'a3
331
332val related_globals_inv_rect_Type0 :
333  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
334  'a3) -> 'a3
335
336val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
337
338val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
339
340val related_globals_gen_rect_Type4 :
341  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
342  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
343  -> __ -> __ -> 'a3) -> 'a3
344
345val related_globals_gen_rect_Type5 :
346  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
347  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
348  -> __ -> __ -> 'a3) -> 'a3
349
350val related_globals_gen_rect_Type3 :
351  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
352  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
353  -> __ -> __ -> 'a3) -> 'a3
354
355val related_globals_gen_rect_Type2 :
356  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
357  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
358  -> __ -> __ -> 'a3) -> 'a3
359
360val related_globals_gen_rect_Type1 :
361  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
362  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
363  -> __ -> __ -> 'a3) -> 'a3
364
365val related_globals_gen_rect_Type0 :
366  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
367  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
368  -> __ -> __ -> 'a3) -> 'a3
369
370val related_globals_gen_inv_rect_Type4 :
371  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
372  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
373  -> __ -> __ -> __ -> 'a3) -> 'a3
374
375val related_globals_gen_inv_rect_Type3 :
376  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
377  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
378  -> __ -> __ -> __ -> 'a3) -> 'a3
379
380val related_globals_gen_inv_rect_Type2 :
381  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
382  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
383  -> __ -> __ -> __ -> 'a3) -> 'a3
384
385val related_globals_gen_inv_rect_Type1 :
386  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
387  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
388  -> __ -> __ -> __ -> 'a3) -> 'a3
389
390val related_globals_gen_inv_rect_Type0 :
391  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
392  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
393  -> __ -> __ -> __ -> 'a3) -> 'a3
394
395val related_globals_gen_discr :
396  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
397  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
398
399val related_globals_gen_jmdiscr :
400  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
401  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
402
403open Extra_bool
404
Note: See TracBrowser for help on using the repository browser.