source: extracted/pointers.mli @ 2716

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

...

File size: 4.5 KB
Line 
1open Preamble
2
3open Division
4
5open Arithmetic
6
7open Extranat
8
9open Vector
10
11open Div_and_mod
12
13open Jmeq
14
15open Russell
16
17open List
18
19open Util
20
21open FoldStuff
22
23open BitVector
24
25open Types
26
27open Bool
28
29open Relations
30
31open Nat
32
33open Hints_declaration
34
35open Core_notation
36
37open Pts
38
39open Logic
40
41open Positive
42
43open Z
44
45open BitVectorZ
46
47open Proper
48
49open PositiveMap
50
51open Deqsets
52
53open ErrorMessages
54
55open PreIdentifiers
56
57open Errors
58
59open Extralib
60
61open Setoids
62
63open Monad
64
65open Option
66
67open Lists
68
69open Identifiers
70
71open Integers
72
73open AST
74
75type block =
76  Z.z
77  (* singleton inductive, whose constructor was mk_block *)
78
79val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1
80
81val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1
82
83val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1
84
85val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1
86
87val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1
88
89val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1
90
91val block_id : block -> Z.z
92
93val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1
94
95val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1
96
97val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1
98
99val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1
100
101val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1
102
103val block_discr : block -> block -> __
104
105val block_jmdiscr : block -> block -> __
106
107val block_region : block -> AST.region
108
109val dummy_block_code : block
110
111val eq_block : block -> block -> Bool.bool
112
113val block_eq : Deqsets.deqSet
114
115val offset_size : Nat.nat
116
117type offset =
118  BitVector.bitVector
119  (* singleton inductive, whose constructor was mk_offset *)
120
121val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
122
123val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
124
125val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
126
127val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
128
129val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
130
131val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
132
133val offv : offset -> BitVector.bitVector
134
135val offset_inv_rect_Type4 :
136  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
137
138val offset_inv_rect_Type3 :
139  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
140
141val offset_inv_rect_Type2 :
142  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
143
144val offset_inv_rect_Type1 :
145  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
146
147val offset_inv_rect_Type0 :
148  offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
149
150val offset_discr : offset -> offset -> __
151
152val offset_jmdiscr : offset -> offset -> __
153
154val eq_offset : offset -> offset -> Bool.bool
155
156val offset_of_Z : Z.z -> offset
157
158val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
159
160val shift_offset_n :
161  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
162  offset
163
164val neg_shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
165
166val neg_shift_offset_n :
167  Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
168  offset
169
170val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector
171
172val zero_offset : offset
173
174val lt_offset : offset -> offset -> Bool.bool
175
176type pointer = { pblock : block; poff : offset }
177
178val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1
179
180val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1
181
182val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1
183
184val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1
185
186val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1
187
188val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1
189
190val pblock : pointer -> block
191
192val poff : pointer -> offset
193
194val pointer_inv_rect_Type4 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
195
196val pointer_inv_rect_Type3 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
197
198val pointer_inv_rect_Type2 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
199
200val pointer_inv_rect_Type1 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
201
202val pointer_inv_rect_Type0 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
203
204val pointer_discr : pointer -> pointer -> __
205
206val pointer_jmdiscr : pointer -> pointer -> __
207
208val ptype : pointer -> AST.region
209
210val shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
211
212val shift_pointer_n :
213  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
214  pointer
215
216val neg_shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
217
218val neg_shift_pointer_n :
219  Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
220  pointer
221
222val eq_pointer : pointer -> pointer -> Bool.bool
223
Note: See TracBrowser for help on using the repository browser.