source: extracted/globalenvs.mli @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 9.0 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 Arithmetic
52
53open Vector
54
55open Div_and_mod
56
57open Util
58
59open FoldStuff
60
61open BitVector
62
63open Extranat
64
65open Integers
66
67open AST
68
69open Coqlib
70
71open Values
72
73open FrontEndVal
74
75open Hide
76
77open ByteValues
78
79open Division
80
81open Z
82
83open BitVectorZ
84
85open Pointers
86
87open GenMem
88
89open FrontEndMem
90
91type 'f genv_t = { functions : 'f PositiveMap.positive_map;
92                   nextfunction : Positive.pos;
93                   symbols : Pointers.block Identifiers.identifier_map }
94
95val genv_t_rect_Type4 :
96  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
97  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
98
99val genv_t_rect_Type5 :
100  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
101  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
102
103val genv_t_rect_Type3 :
104  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
105  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
106
107val genv_t_rect_Type2 :
108  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
109  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
110
111val genv_t_rect_Type1 :
112  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
113  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
114
115val genv_t_rect_Type0 :
116  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
117  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2
118
119val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map
120
121val nextfunction : 'a1 genv_t -> Positive.pos
122
123val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map
124
125val genv_t_inv_rect_Type4 :
126  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
127  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
128
129val genv_t_inv_rect_Type3 :
130  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
131  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
132
133val genv_t_inv_rect_Type2 :
134  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
135  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
136
137val genv_t_inv_rect_Type1 :
138  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
139  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
140
141val genv_t_inv_rect_Type0 :
142  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
143  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2
144
145val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __
146
147val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __
148
149val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t
150
151val add_funct : (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t
152
153val add_symbol : AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t
154
155val empty_mem : GenMem.mem1
156
157val empty0 : 'a1 genv_t
158
159val add_functs :
160  'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t
161
162val find_symbol : 'a1 genv_t -> AST.ident -> Pointers.block Types.option
163
164val store_init_data :
165  'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data ->
166  GenMem.mem1 Types.option
167
168val size_init_data : AST.init_data -> Nat.nat
169
170val store_init_data_list :
171  'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data
172  List.list -> GenMem.mem1 Types.option
173
174val size_init_data_list : AST.init_data List.list -> Nat.nat
175
176val add_globals :
177  ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem1) Types.prod ->
178  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
179  genv_t, GenMem.mem1) Types.prod
180
181val init_globals :
182  ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem1 ->
183  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
184  GenMem.mem1 Errors.res
185
186val globalenv_allocmem :
187  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1 genv_t,
188  GenMem.mem1) Types.prod
189
190val globalenv :
191  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t
192
193val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t
194
195val init_mem :
196  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem1
197  Errors.res
198
199val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem1
200
201val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option
202
203val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option
204
205val symbol_for_block : 'a1 genv_t -> Pointers.block -> AST.ident Types.option
206
207val symbol_of_function_block : 'a1 genv_t -> Pointers.block -> AST.ident
208
209val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos
210
211val alloc_pair :
212  GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
213  GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1
214
215val prod_jmdiscr0 : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
216
217val related_globals_rect_Type4 :
218  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
219
220val related_globals_rect_Type5 :
221  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
222
223val related_globals_rect_Type3 :
224  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
225
226val related_globals_rect_Type2 :
227  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
228
229val related_globals_rect_Type1 :
230  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
231
232val related_globals_rect_Type0 :
233  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) -> 'a3
234
235val related_globals_inv_rect_Type4 :
236  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
237  -> 'a3
238
239val related_globals_inv_rect_Type3 :
240  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
241  -> 'a3
242
243val related_globals_inv_rect_Type2 :
244  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
245  -> 'a3
246
247val related_globals_inv_rect_Type1 :
248  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
249  -> 'a3
250
251val related_globals_inv_rect_Type0 :
252  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
253  -> 'a3
254
255val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
256
257val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __
258
259val related_globals_gen_rect_Type4 :
260  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
261  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
262  -> __ -> 'a3) -> 'a3
263
264val related_globals_gen_rect_Type5 :
265  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
266  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
267  -> __ -> 'a3) -> 'a3
268
269val related_globals_gen_rect_Type3 :
270  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
271  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
272  -> __ -> 'a3) -> 'a3
273
274val related_globals_gen_rect_Type2 :
275  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
276  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
277  -> __ -> 'a3) -> 'a3
278
279val related_globals_gen_rect_Type1 :
280  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
281  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
282  -> __ -> 'a3) -> 'a3
283
284val related_globals_gen_rect_Type0 :
285  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
286  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
287  -> __ -> 'a3) -> 'a3
288
289val related_globals_gen_inv_rect_Type4 :
290  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
291  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
292  -> __ -> __ -> 'a3) -> 'a3
293
294val related_globals_gen_inv_rect_Type3 :
295  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
296  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
297  -> __ -> __ -> 'a3) -> 'a3
298
299val related_globals_gen_inv_rect_Type2 :
300  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
301  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
302  -> __ -> __ -> 'a3) -> 'a3
303
304val related_globals_gen_inv_rect_Type1 :
305  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
306  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
307  -> __ -> __ -> 'a3) -> 'a3
308
309val related_globals_gen_inv_rect_Type0 :
310  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
311  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
312  -> __ -> __ -> 'a3) -> 'a3
313
314val related_globals_gen_discr :
315  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
316  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
317
318val related_globals_gen_jmdiscr :
319  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
320  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
321
322open Extra_bool
323
Note: See TracBrowser for help on using the repository browser.