source: extracted/globalenvs.mli @ 2731

Last change on this file since 2731 was 2730, checked in by sacerdot, 8 years ago

Exported again.

File size: 9.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 symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident
218
219val symbol_of_function_val' : 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident
220
221val find_funct_id :
222  'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option
223
224val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
225
226val alloc_pair :
227  GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
228  GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1
229
230val prod_jmdiscr0 : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
231
232val related_globals_rect_Type4 :
233  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
234  -> 'a3
235
236val related_globals_rect_Type5 :
237  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
238  -> 'a3
239
240val related_globals_rect_Type3 :
241  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
242  -> 'a3
243
244val related_globals_rect_Type2 :
245  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
246  -> 'a3
247
248val related_globals_rect_Type1 :
249  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
250  -> 'a3
251
252val related_globals_rect_Type0 :
253  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
254  -> 'a3
255
256val related_globals_inv_rect_Type4 :
257  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
258  'a3) -> 'a3
259
260val related_globals_inv_rect_Type3 :
261  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
262  'a3) -> 'a3
263
264val related_globals_inv_rect_Type2 :
265  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
266  'a3) -> 'a3
267
268val related_globals_inv_rect_Type1 :
269  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
270  'a3) -> 'a3
271
272val related_globals_inv_rect_Type0 :
273  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
274  'a3) -> 'a3
275
276val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
277
278val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
279
280val related_globals_gen_rect_Type4 :
281  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
282  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
283  -> __ -> __ -> 'a3) -> 'a3
284
285val related_globals_gen_rect_Type5 :
286  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
287  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
288  -> __ -> __ -> 'a3) -> 'a3
289
290val related_globals_gen_rect_Type3 :
291  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
292  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
293  -> __ -> __ -> 'a3) -> 'a3
294
295val related_globals_gen_rect_Type2 :
296  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
297  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
298  -> __ -> __ -> 'a3) -> 'a3
299
300val related_globals_gen_rect_Type1 :
301  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
302  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
303  -> __ -> __ -> 'a3) -> 'a3
304
305val related_globals_gen_rect_Type0 :
306  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
307  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
308  -> __ -> __ -> 'a3) -> 'a3
309
310val related_globals_gen_inv_rect_Type4 :
311  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
312  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
313  -> __ -> __ -> __ -> 'a3) -> 'a3
314
315val related_globals_gen_inv_rect_Type3 :
316  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
317  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
318  -> __ -> __ -> __ -> 'a3) -> 'a3
319
320val related_globals_gen_inv_rect_Type2 :
321  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
322  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
323  -> __ -> __ -> __ -> 'a3) -> 'a3
324
325val related_globals_gen_inv_rect_Type1 :
326  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
327  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
328  -> __ -> __ -> __ -> 'a3) -> 'a3
329
330val related_globals_gen_inv_rect_Type0 :
331  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
332  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
333  -> __ -> __ -> __ -> 'a3) -> 'a3
334
335val related_globals_gen_discr :
336  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
337  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
338
339val related_globals_gen_jmdiscr :
340  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
341  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
342
343open Extra_bool
344
Note: See TracBrowser for help on using the repository browser.