source: extracted/pointers.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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