source: extracted/genMem.mli @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 8 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
RevLine 
[2601]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
[2649]37open ErrorMessages
38
[2601]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
[2717]59open Exp
60
[2601]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
[2649]189val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod
[2601]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.