source: extracted/genMem.mli @ 2649

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

...

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 Arithmetic
60
61open Extranat
62
63open Vector
64
65open FoldStuff
66
67open BitVector
68
69open Positive
70
71open Z
72
73open BitVectorZ
74
75open Pointers
76
77open Hide
78
79open ByteValues
80
81val update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
82
83val update_block :
84  Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1
85
86type contentmap = Z.z -> ByteValues.beval
87
88type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
89
90val block_contents_rect_Type4 :
91  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
92
93val block_contents_rect_Type5 :
94  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
95
96val block_contents_rect_Type3 :
97  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
98
99val block_contents_rect_Type2 :
100  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
101
102val block_contents_rect_Type1 :
103  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
104
105val block_contents_rect_Type0 :
106  (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1
107
108val low : block_contents -> Z.z
109
110val high : block_contents -> Z.z
111
112val contents : block_contents -> contentmap
113
114val block_contents_inv_rect_Type4 :
115  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
116
117val block_contents_inv_rect_Type3 :
118  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
119
120val block_contents_inv_rect_Type2 :
121  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
122
123val block_contents_inv_rect_Type1 :
124  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
125
126val block_contents_inv_rect_Type0 :
127  block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1
128
129val block_contents_discr : block_contents -> block_contents -> __
130
131val block_contents_jmdiscr : block_contents -> block_contents -> __
132
133type mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
134
135val mem_rect_Type4 :
136  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
137
138val mem_rect_Type5 :
139  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
140
141val mem_rect_Type3 :
142  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
143
144val mem_rect_Type2 :
145  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
146
147val mem_rect_Type1 :
148  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
149
150val mem_rect_Type0 :
151  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
152
153val blocks : mem1 -> Pointers.block -> block_contents
154
155val nextblock : mem1 -> Z.z
156
157val mem_inv_rect_Type4 :
158  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
159  'a1
160
161val mem_inv_rect_Type3 :
162  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
163  'a1
164
165val mem_inv_rect_Type2 :
166  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
167  'a1
168
169val mem_inv_rect_Type1 :
170  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
171  'a1
172
173val mem_inv_rect_Type0 :
174  mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
175  'a1
176
177val mem_discr : mem1 -> mem1 -> __
178
179val mem_jmdiscr : mem1 -> mem1 -> __
180
181val oneZ : Z.z
182
183val empty_block : Z.z -> Z.z -> block_contents
184
185val empty : mem1
186
187val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod
188
189val free : mem1 -> Pointers.block -> mem1
190
191val free_list : mem1 -> Pointers.block List.list -> mem1
192
193val low_bound : mem1 -> Pointers.block -> Z.z
194
195val high_bound : mem1 -> Pointers.block -> Z.z
196
197val block_region0 : mem1 -> Pointers.block -> AST.region
198
199val do_if_in_bounds :
200  mem1 -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
201  'a1) -> 'a1 Types.option
202
203val beloadv : mem1 -> Pointers.pointer -> ByteValues.beval Types.option
204
205val bestorev :
206  mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option
207
Note: See TracBrowser for help on using the repository browser.