source: extracted/genMem.mli @ 2746

Last change on this file since 2746 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: 4.1 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
37open ErrorMessages
38
39open PreIdentifiers
40
41open Errors
42
43open Setoids
44
45open Monad
46
47open Option
48
49open Lists
50
51open Identifiers
52
53open Integers
54
55open AST
56
57open Division
58
59open Exp
60
61open Arithmetic
62
63open Extranat
64
65open Vector
66
67open FoldStuff
68
69open BitVector
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open Hide
80
81open ByteValues
82
83val update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
84
85val update_block :
86  Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1
87
88type contentmap = Z.z -> ByteValues.beval
89
90type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
91
92val block_contents_rect_Type4 :
93  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
94
95val block_contents_rect_Type5 :
96  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
97
98val block_contents_rect_Type3 :
99  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
100
101val block_contents_rect_Type2 :
102  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
103
104val block_contents_rect_Type1 :
105  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
106
107val block_contents_rect_Type0 :
108  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
109
110val low : block_contents -> Z.z
111
112val high : block_contents -> Z.z
113
114val contents : block_contents -> contentmap
115
116val block_contents_inv_rect_Type4 :
117  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
118
119val block_contents_inv_rect_Type3 :
120  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
121
122val block_contents_inv_rect_Type2 :
123  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
124
125val block_contents_inv_rect_Type1 :
126  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
127
128val block_contents_inv_rect_Type0 :
129  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
130
131val block_contents_discr : block_contents -> block_contents -> __
132
133val block_contents_jmdiscr : block_contents -> block_contents -> __
134
135type mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
136
137val mem_rect_Type4 :
138  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
139
140val mem_rect_Type5 :
141  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
142
143val mem_rect_Type3 :
144  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
145
146val mem_rect_Type2 :
147  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
148
149val mem_rect_Type1 :
150  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
151
152val mem_rect_Type0 :
153  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
154
155val blocks : mem1 -> Pointers.block -> block_contents
156
157val nextblock : mem1 -> Z.z
158
159val mem_inv_rect_Type4 :
160  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
161  'a1
162
163val mem_inv_rect_Type3 :
164  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
165  'a1
166
167val mem_inv_rect_Type2 :
168  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
169  'a1
170
171val mem_inv_rect_Type1 :
172  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
173  'a1
174
175val mem_inv_rect_Type0 :
176  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
177  'a1
178
179val mem_discr : mem1 -> mem1 -> __
180
181val mem_jmdiscr : mem1 -> mem1 -> __
182
183val oneZ : Z.z
184
185val empty_block : Z.z -> Z.z -> block_contents
186
187val empty : mem1
188
189val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod
190
191val free : mem1 -> Pointers.block -> mem1
192
193val free_list : mem1 -> Pointers.block List.list -> mem1
194
195val low_bound : mem1 -> Pointers.block -> Z.z
196
197val high_bound : mem1 -> Pointers.block -> Z.z
198
199val block_region0 : mem1 -> Pointers.block -> AST.region
200
201val do_if_in_bounds :
202  mem1 -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
203  'a1) -> 'a1 Types.option
204
205val beloadv : mem1 -> Pointers.pointer -> ByteValues.beval Types.option
206
207val bestorev :
208  mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option
209
Note: See TracBrowser for help on using the repository browser.