source: extracted/globalenvs.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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