source: extracted/pointers.ml @ 2716

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

...

File size: 11.0 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
79(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
80let rec block_rect_Type4 h_mk_block x_2388 =
81  let block_id = x_2388 in h_mk_block block_id
82
83(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
84let rec block_rect_Type5 h_mk_block x_2390 =
85  let block_id = x_2390 in h_mk_block block_id
86
87(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
88let rec block_rect_Type3 h_mk_block x_2392 =
89  let block_id = x_2392 in h_mk_block block_id
90
91(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
92let rec block_rect_Type2 h_mk_block x_2394 =
93  let block_id = x_2394 in h_mk_block block_id
94
95(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
96let rec block_rect_Type1 h_mk_block x_2396 =
97  let block_id = x_2396 in h_mk_block block_id
98
99(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
100let rec block_rect_Type0 h_mk_block x_2398 =
101  let block_id = x_2398 in h_mk_block block_id
102
103(** val block_id : block -> Z.z **)
104let rec block_id xxx =
105  let yyy = xxx in yyy
106
107(** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
108let block_inv_rect_Type4 hterm h1 =
109  let hcut = block_rect_Type4 h1 hterm in hcut __
110
111(** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
112let block_inv_rect_Type3 hterm h1 =
113  let hcut = block_rect_Type3 h1 hterm in hcut __
114
115(** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
116let block_inv_rect_Type2 hterm h1 =
117  let hcut = block_rect_Type2 h1 hterm in hcut __
118
119(** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
120let block_inv_rect_Type1 hterm h1 =
121  let hcut = block_rect_Type1 h1 hterm in hcut __
122
123(** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
124let block_inv_rect_Type0 hterm h1 =
125  let hcut = block_rect_Type0 h1 hterm in hcut __
126
127(** val block_discr : block -> block -> __ **)
128let block_discr x y =
129  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
130
131(** val block_jmdiscr : block -> block -> __ **)
132let block_jmdiscr x y =
133  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
134
135(** val block_region : block -> AST.region **)
136let block_region b =
137  match Z.zleb (block_id b) Z.OZ with
138  | Bool.True -> AST.Code
139  | Bool.False -> AST.XData
140
141(** val dummy_block_code : block **)
142let dummy_block_code =
143  Z.OZ
144
145(** val eq_block : block -> block -> Bool.bool **)
146let eq_block b1 b2 =
147  Z.eqZb (block_id b1) (block_id b2)
148
149(** val block_eq : Deqsets.deqSet **)
150let block_eq =
151  Obj.magic eq_block
152
153(** val offset_size : Nat.nat **)
154let offset_size =
155  Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
156    Nat.O)))))))) AST.size_pointer
157
158type offset =
159  BitVector.bitVector
160  (* singleton inductive, whose constructor was mk_offset *)
161
162(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
163let rec offset_rect_Type4 h_mk_offset x_2414 =
164  let offv = x_2414 in h_mk_offset offv
165
166(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
167let rec offset_rect_Type5 h_mk_offset x_2416 =
168  let offv = x_2416 in h_mk_offset offv
169
170(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
171let rec offset_rect_Type3 h_mk_offset x_2418 =
172  let offv = x_2418 in h_mk_offset offv
173
174(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
175let rec offset_rect_Type2 h_mk_offset x_2420 =
176  let offv = x_2420 in h_mk_offset offv
177
178(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
179let rec offset_rect_Type1 h_mk_offset x_2422 =
180  let offv = x_2422 in h_mk_offset offv
181
182(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
183let rec offset_rect_Type0 h_mk_offset x_2424 =
184  let offv = x_2424 in h_mk_offset offv
185
186(** val offv : offset -> BitVector.bitVector **)
187let rec offv xxx =
188  let yyy = xxx in yyy
189
190(** val offset_inv_rect_Type4 :
191    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
192let offset_inv_rect_Type4 hterm h1 =
193  let hcut = offset_rect_Type4 h1 hterm in hcut __
194
195(** val offset_inv_rect_Type3 :
196    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
197let offset_inv_rect_Type3 hterm h1 =
198  let hcut = offset_rect_Type3 h1 hterm in hcut __
199
200(** val offset_inv_rect_Type2 :
201    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
202let offset_inv_rect_Type2 hterm h1 =
203  let hcut = offset_rect_Type2 h1 hterm in hcut __
204
205(** val offset_inv_rect_Type1 :
206    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
207let offset_inv_rect_Type1 hterm h1 =
208  let hcut = offset_rect_Type1 h1 hterm in hcut __
209
210(** val offset_inv_rect_Type0 :
211    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
212let offset_inv_rect_Type0 hterm h1 =
213  let hcut = offset_rect_Type0 h1 hterm in hcut __
214
215(** val offset_discr : offset -> offset -> __ **)
216let offset_discr x y =
217  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
218
219(** val offset_jmdiscr : offset -> offset -> __ **)
220let offset_jmdiscr x y =
221  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
222
223(** val eq_offset : offset -> offset -> Bool.bool **)
224let eq_offset x y =
225  BitVector.eq_bv offset_size (offv x) (offv y)
226
227(** val offset_of_Z : Z.z -> offset **)
228let offset_of_Z z0 =
229  BitVectorZ.bitvector_of_Z offset_size z0
230
231(** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
232let shift_offset n o i =
233  Arithmetic.addition_n offset_size (offv o)
234    (Arithmetic.sign_ext n offset_size i)
235
236(** val shift_offset_n :
237    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
238    offset **)
239let shift_offset_n n o i sg j =
240  Arithmetic.addition_n offset_size (offv o)
241    (Arithmetic.short_multiplication offset_size
242      (Arithmetic.bitvector_of_nat offset_size i)
243      (match sg with
244       | AST.Signed -> Arithmetic.sign_ext n offset_size j
245       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
246
247(** val neg_shift_offset :
248    Nat.nat -> offset -> BitVector.bitVector -> offset **)
249let neg_shift_offset n o i =
250  Arithmetic.subtraction offset_size (offv o)
251    (Arithmetic.sign_ext n offset_size i)
252
253(** val neg_shift_offset_n :
254    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
255    offset **)
256let neg_shift_offset_n n o i sg j =
257  Arithmetic.subtraction offset_size (offv o)
258    (Arithmetic.short_multiplication offset_size
259      (Arithmetic.bitvector_of_nat offset_size i)
260      (match sg with
261       | AST.Signed -> Arithmetic.sign_ext n offset_size j
262       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
263
264(** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
265let sub_offset n x y =
266  Arithmetic.sign_ext offset_size n
267    (Arithmetic.subtraction offset_size (offv x) (offv y))
268
269(** val zero_offset : offset **)
270let zero_offset =
271  BitVector.zero offset_size
272
273(** val lt_offset : offset -> offset -> Bool.bool **)
274let lt_offset x y =
275  Arithmetic.lt_u offset_size (offv x) (offv y)
276
277type pointer = { pblock : block; poff : offset }
278
279(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
280let rec pointer_rect_Type4 h_mk_pointer x_2440 =
281  let { pblock = pblock0; poff = poff0 } = x_2440 in
282  h_mk_pointer pblock0 poff0
283
284(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
285let rec pointer_rect_Type5 h_mk_pointer x_2442 =
286  let { pblock = pblock0; poff = poff0 } = x_2442 in
287  h_mk_pointer pblock0 poff0
288
289(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
290let rec pointer_rect_Type3 h_mk_pointer x_2444 =
291  let { pblock = pblock0; poff = poff0 } = x_2444 in
292  h_mk_pointer pblock0 poff0
293
294(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
295let rec pointer_rect_Type2 h_mk_pointer x_2446 =
296  let { pblock = pblock0; poff = poff0 } = x_2446 in
297  h_mk_pointer pblock0 poff0
298
299(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
300let rec pointer_rect_Type1 h_mk_pointer x_2448 =
301  let { pblock = pblock0; poff = poff0 } = x_2448 in
302  h_mk_pointer pblock0 poff0
303
304(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
305let rec pointer_rect_Type0 h_mk_pointer x_2450 =
306  let { pblock = pblock0; poff = poff0 } = x_2450 in
307  h_mk_pointer pblock0 poff0
308
309(** val pblock : pointer -> block **)
310let rec pblock xxx =
311  xxx.pblock
312
313(** val poff : pointer -> offset **)
314let rec poff xxx =
315  xxx.poff
316
317(** val pointer_inv_rect_Type4 :
318    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
319let pointer_inv_rect_Type4 hterm h1 =
320  let hcut = pointer_rect_Type4 h1 hterm in hcut __
321
322(** val pointer_inv_rect_Type3 :
323    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
324let pointer_inv_rect_Type3 hterm h1 =
325  let hcut = pointer_rect_Type3 h1 hterm in hcut __
326
327(** val pointer_inv_rect_Type2 :
328    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
329let pointer_inv_rect_Type2 hterm h1 =
330  let hcut = pointer_rect_Type2 h1 hterm in hcut __
331
332(** val pointer_inv_rect_Type1 :
333    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
334let pointer_inv_rect_Type1 hterm h1 =
335  let hcut = pointer_rect_Type1 h1 hterm in hcut __
336
337(** val pointer_inv_rect_Type0 :
338    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
339let pointer_inv_rect_Type0 hterm h1 =
340  let hcut = pointer_rect_Type0 h1 hterm in hcut __
341
342(** val pointer_discr : pointer -> pointer -> __ **)
343let pointer_discr x y =
344  Logic.eq_rect_Type2 x
345    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
346    y
347
348(** val pointer_jmdiscr : pointer -> pointer -> __ **)
349let pointer_jmdiscr x y =
350  Logic.eq_rect_Type2 x
351    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
352    y
353
354(** val ptype : pointer -> AST.region **)
355let ptype p =
356  block_region p.pblock
357
358(** val shift_pointer :
359    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
360let shift_pointer n p i =
361  { pblock = p.pblock; poff = (shift_offset n p.poff i) }
362
363(** val shift_pointer_n :
364    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
365    pointer **)
366let shift_pointer_n n p i sg j =
367  { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }
368
369(** val neg_shift_pointer :
370    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
371let neg_shift_pointer n p i =
372  { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }
373
374(** val neg_shift_pointer_n :
375    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
376    pointer **)
377let neg_shift_pointer_n n p i sg j =
378  { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }
379
380(** val eq_pointer : pointer -> pointer -> Bool.bool **)
381let eq_pointer p3 p4 =
382  Bool.andb (eq_block p3.pblock p4.pblock) (eq_offset p3.poff p4.poff)
383
Note: See TracBrowser for help on using the repository browser.