source: extracted/pointers.ml @ 2960

Last change on this file since 2960 was 2827, checked in by sacerdot, 7 years ago

Everything extracted again.

File size: 11.0 KB
RevLine 
[2601]1open Preamble
2
3open Division
4
[2717]5open Exp
6
[2601]7open Arithmetic
8
[2773]9open Setoids
10
11open Monad
12
13open Option
14
[2601]15open Extranat
16
17open Vector
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open List
26
27open Util
28
29open FoldStuff
30
31open BitVector
32
33open Types
34
35open Bool
36
37open Relations
38
39open Nat
40
41open Hints_declaration
42
43open Core_notation
44
45open Pts
46
47open Logic
48
49open Positive
50
51open Z
52
53open BitVectorZ
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
[2649]61open ErrorMessages
62
[2601]63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Lists
70
71open Identifiers
72
73open Integers
74
75open AST
76
[2649]77type block =
78  Z.z
79  (* singleton inductive, whose constructor was mk_block *)
[2601]80
[2649]81(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]82let rec block_rect_Type4 h_mk_block x_5015 =
83  let block_id = x_5015 in h_mk_block block_id
[2601]84
[2649]85(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]86let rec block_rect_Type5 h_mk_block x_5017 =
87  let block_id = x_5017 in h_mk_block block_id
[2601]88
[2649]89(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]90let rec block_rect_Type3 h_mk_block x_5019 =
91  let block_id = x_5019 in h_mk_block block_id
[2601]92
[2649]93(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]94let rec block_rect_Type2 h_mk_block x_5021 =
95  let block_id = x_5021 in h_mk_block block_id
[2601]96
[2649]97(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]98let rec block_rect_Type1 h_mk_block x_5023 =
99  let block_id = x_5023 in h_mk_block block_id
[2601]100
[2649]101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
[2827]102let rec block_rect_Type0 h_mk_block x_5025 =
103  let block_id = x_5025 in h_mk_block block_id
[2601]104
105(** val block_id : block -> Z.z **)
106let rec block_id xxx =
[2649]107  let yyy = xxx in yyy
[2601]108
[2649]109(** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
[2601]110let block_inv_rect_Type4 hterm h1 =
111  let hcut = block_rect_Type4 h1 hterm in hcut __
112
[2649]113(** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
[2601]114let block_inv_rect_Type3 hterm h1 =
115  let hcut = block_rect_Type3 h1 hterm in hcut __
116
[2649]117(** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
[2601]118let block_inv_rect_Type2 hterm h1 =
119  let hcut = block_rect_Type2 h1 hterm in hcut __
120
[2649]121(** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
[2601]122let block_inv_rect_Type1 hterm h1 =
123  let hcut = block_rect_Type1 h1 hterm in hcut __
124
[2649]125(** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
[2601]126let block_inv_rect_Type0 hterm h1 =
127  let hcut = block_rect_Type0 h1 hterm in hcut __
128
129(** val block_discr : block -> block -> __ **)
130let block_discr x y =
[2649]131  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
[2601]132
133(** val block_jmdiscr : block -> block -> __ **)
134let block_jmdiscr x y =
[2649]135  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
[2601]136
[2649]137(** val block_region : block -> AST.region **)
138let block_region b =
139  match Z.zleb (block_id b) Z.OZ with
140  | Bool.True -> AST.Code
141  | Bool.False -> AST.XData
142
143(** val dummy_block_code : block **)
144let dummy_block_code =
145  Z.OZ
146
[2601]147(** val eq_block : block -> block -> Bool.bool **)
148let eq_block b1 b2 =
[2649]149  Z.eqZb (block_id b1) (block_id b2)
[2601]150
151(** val block_eq : Deqsets.deqSet **)
152let block_eq =
153  Obj.magic eq_block
154
155(** val offset_size : Nat.nat **)
156let offset_size =
157  Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
158    Nat.O)))))))) AST.size_pointer
159
160type offset =
161  BitVector.bitVector
162  (* singleton inductive, whose constructor was mk_offset *)
163
164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]165let rec offset_rect_Type4 h_mk_offset x_5041 =
166  let offv = x_5041 in h_mk_offset offv
[2601]167
168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]169let rec offset_rect_Type5 h_mk_offset x_5043 =
170  let offv = x_5043 in h_mk_offset offv
[2601]171
172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]173let rec offset_rect_Type3 h_mk_offset x_5045 =
174  let offv = x_5045 in h_mk_offset offv
[2601]175
176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]177let rec offset_rect_Type2 h_mk_offset x_5047 =
178  let offv = x_5047 in h_mk_offset offv
[2601]179
180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]181let rec offset_rect_Type1 h_mk_offset x_5049 =
182  let offv = x_5049 in h_mk_offset offv
[2601]183
184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
[2827]185let rec offset_rect_Type0 h_mk_offset x_5051 =
186  let offv = x_5051 in h_mk_offset offv
[2601]187
188(** val offv : offset -> BitVector.bitVector **)
189let rec offv xxx =
190  let yyy = xxx in yyy
191
192(** val offset_inv_rect_Type4 :
193    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
194let offset_inv_rect_Type4 hterm h1 =
195  let hcut = offset_rect_Type4 h1 hterm in hcut __
196
197(** val offset_inv_rect_Type3 :
198    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
199let offset_inv_rect_Type3 hterm h1 =
200  let hcut = offset_rect_Type3 h1 hterm in hcut __
201
202(** val offset_inv_rect_Type2 :
203    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
204let offset_inv_rect_Type2 hterm h1 =
205  let hcut = offset_rect_Type2 h1 hterm in hcut __
206
207(** val offset_inv_rect_Type1 :
208    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
209let offset_inv_rect_Type1 hterm h1 =
210  let hcut = offset_rect_Type1 h1 hterm in hcut __
211
212(** val offset_inv_rect_Type0 :
213    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
214let offset_inv_rect_Type0 hterm h1 =
215  let hcut = offset_rect_Type0 h1 hterm in hcut __
216
217(** val offset_discr : offset -> offset -> __ **)
218let offset_discr x y =
219  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
220
221(** val offset_jmdiscr : offset -> offset -> __ **)
222let offset_jmdiscr x y =
223  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
224
225(** val eq_offset : offset -> offset -> Bool.bool **)
226let eq_offset x y =
227  BitVector.eq_bv offset_size (offv x) (offv y)
228
229(** val offset_of_Z : Z.z -> offset **)
[2773]230let offset_of_Z z =
231  BitVectorZ.bitvector_of_Z offset_size z
[2601]232
233(** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
234let shift_offset n o i =
235  Arithmetic.addition_n offset_size (offv o)
236    (Arithmetic.sign_ext n offset_size i)
237
238(** val shift_offset_n :
239    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
240    offset **)
241let shift_offset_n n o i sg j =
242  Arithmetic.addition_n offset_size (offv o)
243    (Arithmetic.short_multiplication offset_size
244      (Arithmetic.bitvector_of_nat offset_size i)
245      (match sg with
246       | AST.Signed -> Arithmetic.sign_ext n offset_size j
247       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
248
249(** val neg_shift_offset :
250    Nat.nat -> offset -> BitVector.bitVector -> offset **)
251let neg_shift_offset n o i =
252  Arithmetic.subtraction offset_size (offv o)
253    (Arithmetic.sign_ext n offset_size i)
254
255(** val neg_shift_offset_n :
256    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
257    offset **)
258let neg_shift_offset_n n o i sg j =
259  Arithmetic.subtraction offset_size (offv o)
260    (Arithmetic.short_multiplication offset_size
261      (Arithmetic.bitvector_of_nat offset_size i)
262      (match sg with
263       | AST.Signed -> Arithmetic.sign_ext n offset_size j
264       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
265
266(** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
267let sub_offset n x y =
268  Arithmetic.sign_ext offset_size n
269    (Arithmetic.subtraction offset_size (offv x) (offv y))
270
271(** val zero_offset : offset **)
272let zero_offset =
273  BitVector.zero offset_size
274
275(** val lt_offset : offset -> offset -> Bool.bool **)
276let lt_offset x y =
277  Arithmetic.lt_u offset_size (offv x) (offv y)
278
279type pointer = { pblock : block; poff : offset }
280
281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]282let rec pointer_rect_Type4 h_mk_pointer x_5067 =
283  let { pblock = pblock0; poff = poff0 } = x_5067 in
[2601]284  h_mk_pointer pblock0 poff0
285
286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]287let rec pointer_rect_Type5 h_mk_pointer x_5069 =
288  let { pblock = pblock0; poff = poff0 } = x_5069 in
[2601]289  h_mk_pointer pblock0 poff0
290
291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]292let rec pointer_rect_Type3 h_mk_pointer x_5071 =
293  let { pblock = pblock0; poff = poff0 } = x_5071 in
[2601]294  h_mk_pointer pblock0 poff0
295
296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]297let rec pointer_rect_Type2 h_mk_pointer x_5073 =
298  let { pblock = pblock0; poff = poff0 } = x_5073 in
[2601]299  h_mk_pointer pblock0 poff0
300
301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]302let rec pointer_rect_Type1 h_mk_pointer x_5075 =
303  let { pblock = pblock0; poff = poff0 } = x_5075 in
[2601]304  h_mk_pointer pblock0 poff0
305
306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
[2827]307let rec pointer_rect_Type0 h_mk_pointer x_5077 =
308  let { pblock = pblock0; poff = poff0 } = x_5077 in
[2601]309  h_mk_pointer pblock0 poff0
310
311(** val pblock : pointer -> block **)
312let rec pblock xxx =
313  xxx.pblock
314
315(** val poff : pointer -> offset **)
316let rec poff xxx =
317  xxx.poff
318
319(** val pointer_inv_rect_Type4 :
320    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
321let pointer_inv_rect_Type4 hterm h1 =
322  let hcut = pointer_rect_Type4 h1 hterm in hcut __
323
324(** val pointer_inv_rect_Type3 :
325    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
326let pointer_inv_rect_Type3 hterm h1 =
327  let hcut = pointer_rect_Type3 h1 hterm in hcut __
328
329(** val pointer_inv_rect_Type2 :
330    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
331let pointer_inv_rect_Type2 hterm h1 =
332  let hcut = pointer_rect_Type2 h1 hterm in hcut __
333
334(** val pointer_inv_rect_Type1 :
335    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
336let pointer_inv_rect_Type1 hterm h1 =
337  let hcut = pointer_rect_Type1 h1 hterm in hcut __
338
339(** val pointer_inv_rect_Type0 :
340    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
341let pointer_inv_rect_Type0 hterm h1 =
342  let hcut = pointer_rect_Type0 h1 hterm in hcut __
343
344(** val pointer_discr : pointer -> pointer -> __ **)
345let pointer_discr x y =
346  Logic.eq_rect_Type2 x
347    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
348    y
349
350(** val pointer_jmdiscr : pointer -> pointer -> __ **)
351let pointer_jmdiscr x y =
352  Logic.eq_rect_Type2 x
353    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
354    y
355
356(** val ptype : pointer -> AST.region **)
357let ptype p =
[2649]358  block_region p.pblock
[2601]359
360(** val shift_pointer :
361    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
362let shift_pointer n p i =
363  { pblock = p.pblock; poff = (shift_offset n p.poff i) }
364
365(** val shift_pointer_n :
366    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
367    pointer **)
368let shift_pointer_n n p i sg j =
369  { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }
370
371(** val neg_shift_pointer :
372    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
373let neg_shift_pointer n p i =
374  { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }
375
376(** val neg_shift_pointer_n :
377    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
378    pointer **)
379let neg_shift_pointer_n n p i sg j =
380  { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }
381
382(** val eq_pointer : pointer -> pointer -> Bool.bool **)
[2773]383let eq_pointer p1 p2 =
384  Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)
[2601]385
Note: See TracBrowser for help on using the repository browser.