source: extracted/byteValues.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: 31.4 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open PreIdentifiers
10
11open Errors
12
13open Extralib
14
15open Setoids
16
17open Monad
18
19open Option
20
21open Lists
22
23open Identifiers
24
25open Coqlib
26
27open Floats
28
29open Integers
30
31open AST
32
33open Division
34
35open Arithmetic
36
37open Char
38
39open String
40
41open Extranat
42
43open Vector
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open List
52
53open Util
54
55open FoldStuff
56
57open BitVector
58
59open Types
60
61open Bool
62
63open Relations
64
65open Nat
66
67open Hints_declaration
68
69open Core_notation
70
71open Pts
72
73open Logic
74
75open Positive
76
77open Z
78
79open BitVectorZ
80
81open Pointers
82
83open Hide
84
85type cpointer = Pointers.pointer Types.sig0
86
87type xpointer = Pointers.pointer Types.sig0
88
89type program_counter = { pc_block : Pointers.block Types.sig0;
90                         pc_offset : Positive.pos }
91
92(** val program_counter_rect_Type4 :
93    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
94    'a1 **)
95let rec program_counter_rect_Type4 h_mk_program_counter x_5073 =
96  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5073 in
97  h_mk_program_counter pc_block0 pc_offset0
98
99(** val program_counter_rect_Type5 :
100    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
101    'a1 **)
102let rec program_counter_rect_Type5 h_mk_program_counter x_5075 =
103  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5075 in
104  h_mk_program_counter pc_block0 pc_offset0
105
106(** val program_counter_rect_Type3 :
107    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
108    'a1 **)
109let rec program_counter_rect_Type3 h_mk_program_counter x_5077 =
110  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5077 in
111  h_mk_program_counter pc_block0 pc_offset0
112
113(** val program_counter_rect_Type2 :
114    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
115    'a1 **)
116let rec program_counter_rect_Type2 h_mk_program_counter x_5079 =
117  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5079 in
118  h_mk_program_counter pc_block0 pc_offset0
119
120(** val program_counter_rect_Type1 :
121    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
122    'a1 **)
123let rec program_counter_rect_Type1 h_mk_program_counter x_5081 =
124  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5081 in
125  h_mk_program_counter pc_block0 pc_offset0
126
127(** val program_counter_rect_Type0 :
128    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
129    'a1 **)
130let rec program_counter_rect_Type0 h_mk_program_counter x_5083 =
131  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5083 in
132  h_mk_program_counter pc_block0 pc_offset0
133
134(** val pc_block : program_counter -> Pointers.block Types.sig0 **)
135let rec pc_block xxx =
136  xxx.pc_block
137
138(** val pc_offset : program_counter -> Positive.pos **)
139let rec pc_offset xxx =
140  xxx.pc_offset
141
142(** val program_counter_inv_rect_Type4 :
143    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
144    'a1) -> 'a1 **)
145let program_counter_inv_rect_Type4 hterm h1 =
146  let hcut = program_counter_rect_Type4 h1 hterm in hcut __
147
148(** val program_counter_inv_rect_Type3 :
149    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
150    'a1) -> 'a1 **)
151let program_counter_inv_rect_Type3 hterm h1 =
152  let hcut = program_counter_rect_Type3 h1 hterm in hcut __
153
154(** val program_counter_inv_rect_Type2 :
155    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
156    'a1) -> 'a1 **)
157let program_counter_inv_rect_Type2 hterm h1 =
158  let hcut = program_counter_rect_Type2 h1 hterm in hcut __
159
160(** val program_counter_inv_rect_Type1 :
161    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
162    'a1) -> 'a1 **)
163let program_counter_inv_rect_Type1 hterm h1 =
164  let hcut = program_counter_rect_Type1 h1 hterm in hcut __
165
166(** val program_counter_inv_rect_Type0 :
167    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
168    'a1) -> 'a1 **)
169let program_counter_inv_rect_Type0 hterm h1 =
170  let hcut = program_counter_rect_Type0 h1 hterm in hcut __
171
172(** val program_counter_discr : program_counter -> program_counter -> __ **)
173let program_counter_discr x y =
174  Logic.eq_rect_Type2 x
175    (let { pc_block = a0; pc_offset = a1 } = x in
176    Obj.magic (fun _ dH -> dH __ __)) y
177
178(** val program_counter_jmdiscr :
179    program_counter -> program_counter -> __ **)
180let program_counter_jmdiscr x y =
181  Logic.eq_rect_Type2 x
182    (let { pc_block = a0; pc_offset = a1 } = x in
183    Obj.magic (fun _ dH -> dH __ __)) y
184
185(** val eq_program_counter :
186    program_counter -> program_counter -> Bool.bool **)
187let eq_program_counter pc1 pc2 =
188  Bool.andb
189    (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
190    (Positive.eqb0 pc1.pc_offset pc2.pc_offset)
191
192(** val bitvector_from_pos :
193    Nat.nat -> Positive.pos -> BitVector.bitVector **)
194let bitvector_from_pos n p =
195  BitVectorZ.bitvector_of_Z n (Z.zpred (Z.Pos p))
196
197(** val pos_from_bitvector :
198    Nat.nat -> BitVector.bitVector -> Positive.pos **)
199let pos_from_bitvector n v =
200  (match Z.zsucc (BitVectorZ.z_of_unsigned_bitvector n v) with
201   | Z.OZ -> (fun _ -> assert false (* absurd case *))
202   | Z.Pos x -> (fun _ -> x)
203   | Z.Neg x -> (fun _ -> assert false (* absurd case *))) __
204
205(** val cpointer_of_pc : program_counter -> cpointer Types.option **)
206let cpointer_of_pc pc =
207  let pc_off = pc.pc_offset in
208  (match Positive.leb0 pc_off (Positive.two_power_nat Pointers.offset_size) with
209   | Bool.True ->
210     Obj.magic
211       (Monad.m_return0 (Monad.max_def Option.option0) { Pointers.pblock =
212         (Types.pi1 pc.pc_block); Pointers.poff =
213         (bitvector_from_pos Pointers.offset_size pc_off) })
214   | Bool.False -> Types.None)
215
216type part =
217  Nat.nat
218  (* singleton inductive, whose constructor was mk_part *)
219
220(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
221let rec part_rect_Type4 h_mk_part x_5099 =
222  let part_no = x_5099 in h_mk_part part_no __
223
224(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
225let rec part_rect_Type5 h_mk_part x_5101 =
226  let part_no = x_5101 in h_mk_part part_no __
227
228(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
229let rec part_rect_Type3 h_mk_part x_5103 =
230  let part_no = x_5103 in h_mk_part part_no __
231
232(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
233let rec part_rect_Type2 h_mk_part x_5105 =
234  let part_no = x_5105 in h_mk_part part_no __
235
236(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
237let rec part_rect_Type1 h_mk_part x_5107 =
238  let part_no = x_5107 in h_mk_part part_no __
239
240(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
241let rec part_rect_Type0 h_mk_part x_5109 =
242  let part_no = x_5109 in h_mk_part part_no __
243
244(** val part_no : part -> Nat.nat **)
245let rec part_no xxx =
246  let yyy = xxx in yyy
247
248(** val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
249let part_inv_rect_Type4 hterm h1 =
250  let hcut = part_rect_Type4 h1 hterm in hcut __
251
252(** val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
253let part_inv_rect_Type3 hterm h1 =
254  let hcut = part_rect_Type3 h1 hterm in hcut __
255
256(** val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
257let part_inv_rect_Type2 hterm h1 =
258  let hcut = part_rect_Type2 h1 hterm in hcut __
259
260(** val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
261let part_inv_rect_Type1 hterm h1 =
262  let hcut = part_rect_Type1 h1 hterm in hcut __
263
264(** val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
265let part_inv_rect_Type0 hterm h1 =
266  let hcut = part_rect_Type0 h1 hterm in hcut __
267
268(** val part_discr : part -> part -> __ **)
269let part_discr x y =
270  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
271
272(** val part_jmdiscr : part -> part -> __ **)
273let part_jmdiscr x y =
274  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
275
276(** val dpi1__o__part_no__o__inject :
277    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
278let dpi1__o__part_no__o__inject x2 =
279  part_no x2.Types.dpi1
280
281(** val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z **)
282let dpi1__o__part_no__o__Z_of_nat x1 =
283  Z.z_of_nat (part_no x1.Types.dpi1)
284
285(** val eject__o__part_no__o__inject :
286    part Types.sig0 -> Nat.nat Types.sig0 **)
287let eject__o__part_no__o__inject x2 =
288  part_no (Types.pi1 x2)
289
290(** val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z **)
291let eject__o__part_no__o__Z_of_nat x1 =
292  Z.z_of_nat (part_no (Types.pi1 x1))
293
294(** val part_no__o__Z_of_nat : part -> Z.z **)
295let part_no__o__Z_of_nat x0 =
296  Z.z_of_nat (part_no x0)
297
298(** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
299let part_no__o__inject x1 =
300  part_no x1
301
302(** val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat **)
303let dpi1__o__part_no x1 =
304  part_no x1.Types.dpi1
305
306(** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
307let eject__o__part_no x1 =
308  part_no (Types.pi1 x1)
309
310(** val part_from_sig : Nat.nat Types.sig0 -> part **)
311let part_from_sig n_sig =
312  Types.pi1 n_sig
313
314type beval =
315| BVundef
316| BVnonzero
317| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
318   * part
319| BVByte of BitVector.byte
320| BVnull of part
321| BVptr of Pointers.pointer * part
322| BVpc of program_counter * part
323
324(** val beval_rect_Type4 :
325    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
326    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
327    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
328    -> beval -> 'a1 **)
329let rec beval_rect_Type4 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
330| BVundef -> h_BVundef
331| BVnonzero -> h_BVnonzero
332| BVXor (x_5143, x_5142, x_5141) -> h_BVXor x_5143 x_5142 x_5141
333| BVByte x_5144 -> h_BVByte x_5144
334| BVnull x_5145 -> h_BVnull x_5145
335| BVptr (x_5147, x_5146) -> h_BVptr x_5147 x_5146
336| BVpc (x_5149, x_5148) -> h_BVpc x_5149 x_5148
337
338(** val beval_rect_Type5 :
339    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
340    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
341    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
342    -> beval -> 'a1 **)
343let rec beval_rect_Type5 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
344| BVundef -> h_BVundef
345| BVnonzero -> h_BVnonzero
346| BVXor (x_5160, x_5159, x_5158) -> h_BVXor x_5160 x_5159 x_5158
347| BVByte x_5161 -> h_BVByte x_5161
348| BVnull x_5162 -> h_BVnull x_5162
349| BVptr (x_5164, x_5163) -> h_BVptr x_5164 x_5163
350| BVpc (x_5166, x_5165) -> h_BVpc x_5166 x_5165
351
352(** val beval_rect_Type3 :
353    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
354    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
355    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
356    -> beval -> 'a1 **)
357let rec beval_rect_Type3 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
358| BVundef -> h_BVundef
359| BVnonzero -> h_BVnonzero
360| BVXor (x_5177, x_5176, x_5175) -> h_BVXor x_5177 x_5176 x_5175
361| BVByte x_5178 -> h_BVByte x_5178
362| BVnull x_5179 -> h_BVnull x_5179
363| BVptr (x_5181, x_5180) -> h_BVptr x_5181 x_5180
364| BVpc (x_5183, x_5182) -> h_BVpc x_5183 x_5182
365
366(** val beval_rect_Type2 :
367    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
368    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
369    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
370    -> beval -> 'a1 **)
371let rec beval_rect_Type2 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
372| BVundef -> h_BVundef
373| BVnonzero -> h_BVnonzero
374| BVXor (x_5194, x_5193, x_5192) -> h_BVXor x_5194 x_5193 x_5192
375| BVByte x_5195 -> h_BVByte x_5195
376| BVnull x_5196 -> h_BVnull x_5196
377| BVptr (x_5198, x_5197) -> h_BVptr x_5198 x_5197
378| BVpc (x_5200, x_5199) -> h_BVpc x_5200 x_5199
379
380(** val beval_rect_Type1 :
381    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
382    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
383    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
384    -> beval -> 'a1 **)
385let rec beval_rect_Type1 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
386| BVundef -> h_BVundef
387| BVnonzero -> h_BVnonzero
388| BVXor (x_5211, x_5210, x_5209) -> h_BVXor x_5211 x_5210 x_5209
389| BVByte x_5212 -> h_BVByte x_5212
390| BVnull x_5213 -> h_BVnull x_5213
391| BVptr (x_5215, x_5214) -> h_BVptr x_5215 x_5214
392| BVpc (x_5217, x_5216) -> h_BVpc x_5217 x_5216
393
394(** val beval_rect_Type0 :
395    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
396    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
397    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
398    -> beval -> 'a1 **)
399let rec beval_rect_Type0 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
400| BVundef -> h_BVundef
401| BVnonzero -> h_BVnonzero
402| BVXor (x_5228, x_5227, x_5226) -> h_BVXor x_5228 x_5227 x_5226
403| BVByte x_5229 -> h_BVByte x_5229
404| BVnull x_5230 -> h_BVnull x_5230
405| BVptr (x_5232, x_5231) -> h_BVptr x_5232 x_5231
406| BVpc (x_5234, x_5233) -> h_BVpc x_5234 x_5233
407
408(** val beval_inv_rect_Type4 :
409    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
410    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
411    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
412    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
413let beval_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
414  let hcut = beval_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
415
416(** val beval_inv_rect_Type3 :
417    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
418    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
419    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
420    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
421let beval_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
422  let hcut = beval_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
423
424(** val beval_inv_rect_Type2 :
425    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
426    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
427    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
428    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
429let beval_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
430  let hcut = beval_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
431
432(** val beval_inv_rect_Type1 :
433    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
434    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
435    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
436    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
437let beval_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
438  let hcut = beval_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
439
440(** val beval_inv_rect_Type0 :
441    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
442    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
443    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
444    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
445let beval_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
446  let hcut = beval_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
447
448(** val beval_discr : beval -> beval -> __ **)
449let beval_discr x y =
450  Logic.eq_rect_Type2 x
451    (match x with
452     | BVundef -> Obj.magic (fun _ dH -> dH)
453     | BVnonzero -> Obj.magic (fun _ dH -> dH)
454     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
455     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
456     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
457     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
458     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
459
460(** val beval_jmdiscr : beval -> beval -> __ **)
461let beval_jmdiscr x y =
462  Logic.eq_rect_Type2 x
463    (match x with
464     | BVundef -> Obj.magic (fun _ dH -> dH)
465     | BVnonzero -> Obj.magic (fun _ dH -> dH)
466     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
467     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
468     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
469     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
470     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
471
472(** val eq_bv_suffix :
473    Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector ->
474    BitVector.bitVector -> Bool.bool **)
475let eq_bv_suffix n m p v1 v2 =
476  let b1 = (Vector.vsplit n p v1).Types.snd in
477  let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2
478
479(** val corruptedPointer : String.string **)
480let corruptedPointer = "corrupted pointer"
481  (* failwith "AXIOM TO BE REALIZED" *)
482
483(** val pointer_of_bevals :
484    beval List.list -> Pointers.pointer Errors.res **)
485let pointer_of_bevals = function
486| List.Nil ->
487  Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
488| List.Cons (bv1, tl) ->
489  (match tl with
490   | List.Nil ->
491     Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
492   | List.Cons (bv2, tl') ->
493     (match tl' with
494      | List.Nil ->
495        (match bv1 with
496         | BVundef ->
497           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
498         | BVnonzero ->
499           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
500         | BVXor (x, x0, x1) ->
501           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
502         | BVByte x ->
503           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
504         | BVnull x ->
505           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
506         | BVptr (ptr1, p3) ->
507           (match bv2 with
508            | BVundef ->
509              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
510                List.Nil))
511            | BVnonzero ->
512              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
513                List.Nil))
514            | BVXor (x, x0, x1) ->
515              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
516                List.Nil))
517            | BVByte x ->
518              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
519                List.Nil))
520            | BVnull x ->
521              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
522                List.Nil))
523            | BVptr (ptr2, p4) ->
524              (match Bool.andb
525                       (Bool.andb
526                         (Bool.andb (Nat.eqb (part_no p3) Nat.O)
527                           (Nat.eqb (part_no p4) (Nat.S Nat.O)))
528                         (Pointers.eq_block ptr1.Pointers.pblock
529                           ptr2.Pointers.pblock))
530                       (eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531                         (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S
532                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
534                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
535                         (Pointers.offv ptr1.Pointers.poff)
536                         (Pointers.offv ptr2.Pointers.poff)) with
537               | Bool.True ->
538                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
539               | Bool.False ->
540                 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
541                   List.Nil)))
542            | BVpc (x, x0) ->
543              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
544                List.Nil)))
545         | BVpc (x, x0) ->
546           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil)))
547      | List.Cons (x, x0) ->
548        Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))))
549
550(** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
551let pc_of_bevals = function
552| List.Nil ->
553  Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
554| List.Cons (bv1, tl) ->
555  (match tl with
556   | List.Nil ->
557     Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
558   | List.Cons (bv2, tl') ->
559     (match tl' with
560      | List.Nil ->
561        (match bv1 with
562         | BVundef ->
563           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
564         | BVnonzero ->
565           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
566         | BVXor (x, x0, x1) ->
567           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
568         | BVByte x ->
569           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
570         | BVnull x ->
571           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
572         | BVptr (x, x0) ->
573           Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))
574         | BVpc (ptr1, p3) ->
575           (match bv2 with
576            | BVundef ->
577              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
578                List.Nil))
579            | BVnonzero ->
580              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
581                List.Nil))
582            | BVXor (x, x0, x1) ->
583              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
584                List.Nil))
585            | BVByte x ->
586              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
587                List.Nil))
588            | BVnull x ->
589              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
590                List.Nil))
591            | BVptr (x, x0) ->
592              Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
593                List.Nil))
594            | BVpc (ptr2, p4) ->
595              (match Bool.andb
596                       (Bool.andb (Nat.eqb (part_no p3) Nat.O)
597                         (Nat.eqb (part_no p4) (Nat.S Nat.O)))
598                       (eq_program_counter ptr1 ptr2) with
599               | Bool.True ->
600                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
601               | Bool.False ->
602                 Errors.Error (List.Cons ((Errors.MSG corruptedPointer),
603                   List.Nil)))))
604      | List.Cons (x, x0) ->
605        Errors.Error (List.Cons ((Errors.MSG corruptedPointer), List.Nil))))
606
607(** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
608let bevals_of_pointer p =
609  List.map (fun n_sig -> BVptr (p, (part_from_sig n_sig)))
610    (Lists.range_strong AST.size_pointer)
611
612(** val bevals_of_pc : program_counter -> beval List.list **)
613let bevals_of_pc p =
614  List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
615    (Lists.range_strong AST.size_pointer)
616
617(** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
618let list_to_pair l =
619  (match l with
620   | List.Nil ->
621     (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
622   | List.Cons (a, tl) ->
623     (match tl with
624      | List.Nil ->
625        (fun _ ->
626          Obj.magic Nat.nat_discr (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) __
627            (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S Nat.O) __))
628      | List.Cons (b, tl') ->
629        (match tl' with
630         | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
631         | List.Cons (c, tl'') ->
632           (fun _ ->
633             Obj.magic Nat.nat_discr (Nat.S (Nat.S (Nat.S
634               (List.length tl'')))) (Nat.S (Nat.S Nat.O)) __ (fun _ ->
635               Obj.magic Nat.nat_discr (Nat.S (Nat.S (List.length tl'')))
636                 (Nat.S Nat.O) __ (fun _ ->
637                 Obj.magic Nat.nat_discr (Nat.S (List.length tl'')) Nat.O __))))))
638    __
639
640(** val notATwoBytesPointer : String.string **)
641let notATwoBytesPointer = "not a two bytes pointer"
642  (* failwith "AXIOM TO BE REALIZED" *)
643
644(** val beval_pair_of_pointer :
645    Pointers.pointer -> (beval, beval) Types.prod **)
646let beval_pair_of_pointer p =
647  list_to_pair (bevals_of_pointer p)
648
649(** val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod **)
650let beval_pair_of_pc p =
651  list_to_pair (bevals_of_pc p)
652
653(** val valueNotABoolean : String.string **)
654let valueNotABoolean = "value not a boolean"
655  (* failwith "AXIOM TO BE REALIZED" *)
656
657(** val bool_of_beval : beval -> Bool.bool Errors.res **)
658let bool_of_beval = function
659| BVundef ->
660  Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
661| BVnonzero -> Errors.OK Bool.True
662| BVXor (x, x0, x1) ->
663  Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
664| BVByte b ->
665  Errors.OK
666    (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
667      Nat.O))))))))
668      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
669        Nat.O))))))))) b)
670| BVnull x -> Errors.OK Bool.False
671| BVptr (x, x0) -> Errors.OK Bool.True
672| BVpc (x, x0) ->
673  Errors.Error (List.Cons ((Errors.MSG valueNotABoolean), List.Nil))
674
675(** val byte_of_val : String.string -> beval -> BitVector.byte Errors.res **)
676let byte_of_val err = function
677| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
678| BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
679| BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
680| BVByte b0 -> Errors.OK b0
681| BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
682| BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
683| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
684
685(** val notAnInt32Val : String.string **)
686let notAnInt32Val = "not an int32 val"
687  (* failwith "AXIOM TO BE REALIZED" *)
688
689(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
690let word_of_list_beval l =
691  let first_byte = fun l0 ->
692    match l0 with
693    | List.Nil ->
694      Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),
695        List.Nil)))
696    | List.Cons (hd0, tl) ->
697      Monad.m_bind0 (Monad.max_def Errors.res0)
698        (Obj.magic (byte_of_val notAnInt32Val hd0)) (fun b ->
699        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
700  in
701  Obj.magic
702    (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
703      Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
704        Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
705          (fun b3 l2 ->
706          Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
707            (fun b4 l3 ->
708            match l3 with
709            | List.Nil ->
710              Obj.magic (Errors.OK
711                (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
712                  (Nat.S (Nat.S Nat.O))))))))
713                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
714                    (Nat.S Nat.O))))))))
715                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
716                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
717                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
718                  (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
719                    (Nat.S (Nat.S Nat.O))))))))
720                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
721                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
722                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
723                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
724                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
725                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
726            | List.Cons (x, x0) ->
727              Obj.magic (Errors.Error (List.Cons ((Errors.MSG notAnInt32Val),
728                List.Nil))))))))
729
730type bebit =
731| BBbit of Bool.bool
732| BBundef
733| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
734
735(** val bebit_rect_Type4 :
736    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
737    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
738let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
739| BBbit x_5353 -> h_BBbit x_5353
740| BBundef -> h_BBundef
741| BBptrcarry (x_5356, x_5355, p, x_5354) ->
742  h_BBptrcarry x_5356 x_5355 p x_5354
743
744(** val bebit_rect_Type5 :
745    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
746    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
747let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
748| BBbit x_5361 -> h_BBbit x_5361
749| BBundef -> h_BBundef
750| BBptrcarry (x_5364, x_5363, p, x_5362) ->
751  h_BBptrcarry x_5364 x_5363 p x_5362
752
753(** val bebit_rect_Type3 :
754    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
755    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
756let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
757| BBbit x_5369 -> h_BBbit x_5369
758| BBundef -> h_BBundef
759| BBptrcarry (x_5372, x_5371, p, x_5370) ->
760  h_BBptrcarry x_5372 x_5371 p x_5370
761
762(** val bebit_rect_Type2 :
763    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
764    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
765let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
766| BBbit x_5377 -> h_BBbit x_5377
767| BBundef -> h_BBundef
768| BBptrcarry (x_5380, x_5379, p, x_5378) ->
769  h_BBptrcarry x_5380 x_5379 p x_5378
770
771(** val bebit_rect_Type1 :
772    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
773    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
774let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
775| BBbit x_5385 -> h_BBbit x_5385
776| BBundef -> h_BBundef
777| BBptrcarry (x_5388, x_5387, p, x_5386) ->
778  h_BBptrcarry x_5388 x_5387 p x_5386
779
780(** val bebit_rect_Type0 :
781    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
782    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
783let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
784| BBbit x_5393 -> h_BBbit x_5393
785| BBundef -> h_BBundef
786| BBptrcarry (x_5396, x_5395, p, x_5394) ->
787  h_BBptrcarry x_5396 x_5395 p x_5394
788
789(** val bebit_inv_rect_Type4 :
790    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
791    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
792let bebit_inv_rect_Type4 hterm h1 h2 h3 =
793  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
794
795(** val bebit_inv_rect_Type3 :
796    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
797    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
798let bebit_inv_rect_Type3 hterm h1 h2 h3 =
799  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
800
801(** val bebit_inv_rect_Type2 :
802    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
803    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
804let bebit_inv_rect_Type2 hterm h1 h2 h3 =
805  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
806
807(** val bebit_inv_rect_Type1 :
808    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
809    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
810let bebit_inv_rect_Type1 hterm h1 h2 h3 =
811  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
812
813(** val bebit_inv_rect_Type0 :
814    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
815    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
816let bebit_inv_rect_Type0 hterm h1 h2 h3 =
817  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
818
819(** val bebit_discr : bebit -> bebit -> __ **)
820let bebit_discr x y =
821  Logic.eq_rect_Type2 x
822    (match x with
823     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
824     | BBundef -> Obj.magic (fun _ dH -> dH)
825     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
826    y
827
828(** val bebit_jmdiscr : bebit -> bebit -> __ **)
829let bebit_jmdiscr x y =
830  Logic.eq_rect_Type2 x
831    (match x with
832     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
833     | BBundef -> Obj.magic (fun _ dH -> dH)
834     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
835    y
836
837(** val bit_of_val : String.string -> bebit -> BitVector.bit Errors.res **)
838let bit_of_val err = function
839| BBbit b0 -> Errors.OK b0
840| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
841| BBptrcarry (x, x0, x1, x2) ->
842  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
843
Note: See TracBrowser for help on using the repository browser.