source: extracted/byteValues.ml @ 2827

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

Everything extracted again.

File size: 38.1 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Lists
18
19open Identifiers
20
21open Integers
22
23open AST
24
25open Division
26
27open Exp
28
29open Arithmetic
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Extranat
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Types
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open Hide
80
81type cpointer = Pointers.pointer Types.sig0
82
83type xpointer = Pointers.pointer Types.sig0
84
85type program_counter = { pc_block : Pointers.block Types.sig0;
86                         pc_offset : Positive.pos }
87
88(** val program_counter_rect_Type4 :
89    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
90    'a1 **)
91let rec program_counter_rect_Type4 h_mk_program_counter x_6139 =
92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6139 in
93  h_mk_program_counter pc_block0 pc_offset0
94
95(** val program_counter_rect_Type5 :
96    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
97    'a1 **)
98let rec program_counter_rect_Type5 h_mk_program_counter x_6141 =
99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6141 in
100  h_mk_program_counter pc_block0 pc_offset0
101
102(** val program_counter_rect_Type3 :
103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
104    'a1 **)
105let rec program_counter_rect_Type3 h_mk_program_counter x_6143 =
106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6143 in
107  h_mk_program_counter pc_block0 pc_offset0
108
109(** val program_counter_rect_Type2 :
110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
111    'a1 **)
112let rec program_counter_rect_Type2 h_mk_program_counter x_6145 =
113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6145 in
114  h_mk_program_counter pc_block0 pc_offset0
115
116(** val program_counter_rect_Type1 :
117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
118    'a1 **)
119let rec program_counter_rect_Type1 h_mk_program_counter x_6147 =
120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6147 in
121  h_mk_program_counter pc_block0 pc_offset0
122
123(** val program_counter_rect_Type0 :
124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
125    'a1 **)
126let rec program_counter_rect_Type0 h_mk_program_counter x_6149 =
127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6149 in
128  h_mk_program_counter pc_block0 pc_offset0
129
130(** val pc_block : program_counter -> Pointers.block Types.sig0 **)
131let rec pc_block xxx =
132  xxx.pc_block
133
134(** val pc_offset : program_counter -> Positive.pos **)
135let rec pc_offset xxx =
136  xxx.pc_offset
137
138(** val program_counter_inv_rect_Type4 :
139    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
140    'a1) -> 'a1 **)
141let program_counter_inv_rect_Type4 hterm h1 =
142  let hcut = program_counter_rect_Type4 h1 hterm in hcut __
143
144(** val program_counter_inv_rect_Type3 :
145    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
146    'a1) -> 'a1 **)
147let program_counter_inv_rect_Type3 hterm h1 =
148  let hcut = program_counter_rect_Type3 h1 hterm in hcut __
149
150(** val program_counter_inv_rect_Type2 :
151    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
152    'a1) -> 'a1 **)
153let program_counter_inv_rect_Type2 hterm h1 =
154  let hcut = program_counter_rect_Type2 h1 hterm in hcut __
155
156(** val program_counter_inv_rect_Type1 :
157    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
158    'a1) -> 'a1 **)
159let program_counter_inv_rect_Type1 hterm h1 =
160  let hcut = program_counter_rect_Type1 h1 hterm in hcut __
161
162(** val program_counter_inv_rect_Type0 :
163    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
164    'a1) -> 'a1 **)
165let program_counter_inv_rect_Type0 hterm h1 =
166  let hcut = program_counter_rect_Type0 h1 hterm in hcut __
167
168(** val program_counter_discr : program_counter -> program_counter -> __ **)
169let program_counter_discr x y =
170  Logic.eq_rect_Type2 x
171    (let { pc_block = a0; pc_offset = a1 } = x in
172    Obj.magic (fun _ dH -> dH __ __)) y
173
174(** val program_counter_jmdiscr :
175    program_counter -> program_counter -> __ **)
176let program_counter_jmdiscr x y =
177  Logic.eq_rect_Type2 x
178    (let { pc_block = a0; pc_offset = a1 } = x in
179    Obj.magic (fun _ dH -> dH __ __)) y
180
181(** val eq_program_counter :
182    program_counter -> program_counter -> Bool.bool **)
183let eq_program_counter pc1 pc2 =
184  Bool.andb
185    (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
186    (Positive.eqb pc1.pc_offset pc2.pc_offset)
187
188(** val bitvector_from_pos :
189    Nat.nat -> Positive.pos -> BitVector.bitVector **)
190let bitvector_from_pos n p =
191  BitVectorZ.bitvector_of_Z n (Z.zpred (Z.Pos p))
192
193(** val pos_from_bitvector :
194    Nat.nat -> BitVector.bitVector -> Positive.pos **)
195let pos_from_bitvector n v =
196  (match Z.zsucc (BitVectorZ.z_of_unsigned_bitvector n v) with
197   | Z.OZ -> (fun _ -> assert false (* absurd case *))
198   | Z.Pos x -> (fun _ -> x)
199   | Z.Neg x -> (fun _ -> assert false (* absurd case *))) __
200
201(** val cpointer_of_pc : program_counter -> cpointer Types.option **)
202let cpointer_of_pc pc =
203  let pc_off = pc.pc_offset in
204  (match Positive.leb pc_off (Positive.two_power_nat Pointers.offset_size) with
205   | Bool.True ->
206     Obj.magic
207       (Monad.m_return0 (Monad.max_def Option.option) { Pointers.pblock =
208         (Types.pi1 pc.pc_block); Pointers.poff =
209         (bitvector_from_pos Pointers.offset_size pc_off) })
210   | Bool.False -> Types.None)
211
212type part =
213  Nat.nat
214  (* singleton inductive, whose constructor was mk_part *)
215
216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
217let rec part_rect_Type4 h_mk_part x_6165 =
218  let part_no = x_6165 in h_mk_part part_no __
219
220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
221let rec part_rect_Type5 h_mk_part x_6167 =
222  let part_no = x_6167 in h_mk_part part_no __
223
224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
225let rec part_rect_Type3 h_mk_part x_6169 =
226  let part_no = x_6169 in h_mk_part part_no __
227
228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
229let rec part_rect_Type2 h_mk_part x_6171 =
230  let part_no = x_6171 in h_mk_part part_no __
231
232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
233let rec part_rect_Type1 h_mk_part x_6173 =
234  let part_no = x_6173 in h_mk_part part_no __
235
236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
237let rec part_rect_Type0 h_mk_part x_6175 =
238  let part_no = x_6175 in h_mk_part part_no __
239
240(** val part_no : part -> Nat.nat **)
241let rec part_no xxx =
242  let yyy = xxx in yyy
243
244(** val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
245let part_inv_rect_Type4 hterm h1 =
246  let hcut = part_rect_Type4 h1 hterm in hcut __
247
248(** val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
249let part_inv_rect_Type3 hterm h1 =
250  let hcut = part_rect_Type3 h1 hterm in hcut __
251
252(** val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
253let part_inv_rect_Type2 hterm h1 =
254  let hcut = part_rect_Type2 h1 hterm in hcut __
255
256(** val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
257let part_inv_rect_Type1 hterm h1 =
258  let hcut = part_rect_Type1 h1 hterm in hcut __
259
260(** val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
261let part_inv_rect_Type0 hterm h1 =
262  let hcut = part_rect_Type0 h1 hterm in hcut __
263
264(** val part_discr : part -> part -> __ **)
265let part_discr x y =
266  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
267
268(** val part_jmdiscr : part -> part -> __ **)
269let part_jmdiscr x y =
270  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
271
272(** val dpi1__o__part_no__o__inject :
273    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
274let dpi1__o__part_no__o__inject x2 =
275  part_no x2.Types.dpi1
276
277(** val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z **)
278let dpi1__o__part_no__o__Z_of_nat x1 =
279  Z.z_of_nat (part_no x1.Types.dpi1)
280
281(** val eject__o__part_no__o__inject :
282    part Types.sig0 -> Nat.nat Types.sig0 **)
283let eject__o__part_no__o__inject x2 =
284  part_no (Types.pi1 x2)
285
286(** val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z **)
287let eject__o__part_no__o__Z_of_nat x1 =
288  Z.z_of_nat (part_no (Types.pi1 x1))
289
290(** val part_no__o__Z_of_nat : part -> Z.z **)
291let part_no__o__Z_of_nat x0 =
292  Z.z_of_nat (part_no x0)
293
294(** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
295let part_no__o__inject x1 =
296  part_no x1
297
298(** val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat **)
299let dpi1__o__part_no x1 =
300  part_no x1.Types.dpi1
301
302(** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
303let eject__o__part_no x1 =
304  part_no (Types.pi1 x1)
305
306(** val part_from_sig : Nat.nat Types.sig0 -> part **)
307let part_from_sig n_sig =
308  Types.pi1 n_sig
309
310(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
311    (part, 'a1) Types.dPair -> part Types.sig0 **)
312let dpi1__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
313  part_from_sig (dpi1__o__part_no__o__inject x2)
314
315(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
316    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
317let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
318  part_no__o__inject (part_from_sig (dpi1__o__part_no__o__inject x2))
319
320(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
321    (part, 'a1) Types.dPair -> Z.z **)
322let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
323  part_no__o__Z_of_nat (part_from_sig (dpi1__o__part_no__o__inject x1))
324
325(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
326    (part, 'a1) Types.dPair -> Nat.nat **)
327let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
328  part_no (part_from_sig (dpi1__o__part_no__o__inject x1))
329
330(** val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
331    part Types.sig0 -> part Types.sig0 **)
332let eject__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
333  part_from_sig (eject__o__part_no__o__inject x2)
334
335(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
336    part Types.sig0 -> Nat.nat Types.sig0 **)
337let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
338  part_no__o__inject (part_from_sig (eject__o__part_no__o__inject x2))
339
340(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
341    part Types.sig0 -> Z.z **)
342let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
343  part_no__o__Z_of_nat (part_from_sig (eject__o__part_no__o__inject x1))
344
345(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
346    part Types.sig0 -> Nat.nat **)
347let eject__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
348  part_no (part_from_sig (eject__o__part_no__o__inject x1))
349
350(** val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0 **)
351let inject__o__sig_to_part__o__inject x0 =
352  part_from_sig x0
353
354(** val inject__o__sig_to_part__o__part_no__o__inject :
355    Nat.nat -> Nat.nat Types.sig0 **)
356let inject__o__sig_to_part__o__part_no__o__inject x0 =
357  part_no__o__inject (part_from_sig x0)
358
359(** val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z **)
360let inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
361  part_no__o__Z_of_nat (part_from_sig x0)
362
363(** val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat **)
364let inject__o__sig_to_part__o__part_no x0 =
365  part_no (part_from_sig x0)
366
367(** val part_no__o__inject__o__sig_to_part__o__inject :
368    part -> part Types.sig0 **)
369let part_no__o__inject__o__sig_to_part__o__inject x0 =
370  part_from_sig (part_no__o__inject x0)
371
372(** val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
373    part -> Nat.nat Types.sig0 **)
374let part_no__o__inject__o__sig_to_part__o__part_no__o__inject x0 =
375  part_no__o__inject (part_from_sig (part_no__o__inject x0))
376
377(** val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
378    part -> Z.z **)
379let part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
380  part_no__o__Z_of_nat (part_from_sig (part_no__o__inject x0))
381
382(** val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat **)
383let part_no__o__inject__o__sig_to_part__o__part_no x0 =
384  part_no (part_from_sig (part_no__o__inject x0))
385
386(** val dpi1__o__sig_to_part__o__inject :
387    (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0 **)
388let dpi1__o__sig_to_part__o__inject x2 =
389  part_from_sig x2.Types.dpi1
390
391(** val dpi1__o__sig_to_part__o__part_no__o__inject :
392    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
393let dpi1__o__sig_to_part__o__part_no__o__inject x2 =
394  part_no__o__inject (part_from_sig x2.Types.dpi1)
395
396(** val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
397    (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z **)
398let dpi1__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
399  part_no__o__Z_of_nat (part_from_sig x1.Types.dpi1)
400
401(** val dpi1__o__sig_to_part__o__part_no :
402    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat **)
403let dpi1__o__sig_to_part__o__part_no x1 =
404  part_no (part_from_sig x1.Types.dpi1)
405
406(** val eject__o__sig_to_part__o__inject :
407    Nat.nat Types.sig0 Types.sig0 -> part Types.sig0 **)
408let eject__o__sig_to_part__o__inject x2 =
409  part_from_sig (Types.pi1 x2)
410
411(** val eject__o__sig_to_part__o__part_no__o__inject :
412    Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0 **)
413let eject__o__sig_to_part__o__part_no__o__inject x2 =
414  part_no__o__inject (part_from_sig (Types.pi1 x2))
415
416(** val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
417    Nat.nat Types.sig0 Types.sig0 -> Z.z **)
418let eject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
419  part_no__o__Z_of_nat (part_from_sig (Types.pi1 x1))
420
421(** val eject__o__sig_to_part__o__part_no :
422    Nat.nat Types.sig0 Types.sig0 -> Nat.nat **)
423let eject__o__sig_to_part__o__part_no x1 =
424  part_no (part_from_sig (Types.pi1 x1))
425
426(** val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat **)
427let sig_to_part__o__part_no x0 =
428  part_no (part_from_sig x0)
429
430(** val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z **)
431let sig_to_part__o__part_no__o__Z_of_nat x0 =
432  part_no__o__Z_of_nat (part_from_sig x0)
433
434(** val sig_to_part__o__part_no__o__inject :
435    Nat.nat Types.sig0 -> Nat.nat Types.sig0 **)
436let sig_to_part__o__part_no__o__inject x1 =
437  part_no__o__inject (part_from_sig x1)
438
439(** val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0 **)
440let sig_to_part__o__inject x1 =
441  part_from_sig x1
442
443(** val dpi1__o__part_no__o__inject__o__sig_to_part :
444    (part, 'a1) Types.dPair -> part **)
445let dpi1__o__part_no__o__inject__o__sig_to_part x1 =
446  part_from_sig (dpi1__o__part_no__o__inject x1)
447
448(** val eject__o__part_no__o__inject__o__sig_to_part :
449    part Types.sig0 -> part **)
450let eject__o__part_no__o__inject__o__sig_to_part x1 =
451  part_from_sig (eject__o__part_no__o__inject x1)
452
453(** val inject__o__sig_to_part : Nat.nat -> part **)
454let inject__o__sig_to_part x0 =
455  part_from_sig x0
456
457(** val part_no__o__inject__o__sig_to_part : part -> part **)
458let part_no__o__inject__o__sig_to_part x0 =
459  part_from_sig (part_no__o__inject x0)
460
461(** val dpi1__o__sig_to_part :
462    (Nat.nat Types.sig0, 'a1) Types.dPair -> part **)
463let dpi1__o__sig_to_part x1 =
464  part_from_sig x1.Types.dpi1
465
466(** val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part **)
467let eject__o__sig_to_part x1 =
468  part_from_sig (Types.pi1 x1)
469
470type beval =
471| BVundef
472| BVnonzero
473| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
474   * part
475| BVByte of BitVector.byte
476| BVnull of part
477| BVptr of Pointers.pointer * part
478| BVpc of program_counter * part
479
480(** val beval_rect_Type4 :
481    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
482    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
483    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
484    -> beval -> 'a1 **)
485let rec beval_rect_Type4 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
486| BVundef -> h_BVundef
487| BVnonzero -> h_BVnonzero
488| BVXor (x_6209, x_6208, x_6207) -> h_BVXor x_6209 x_6208 x_6207
489| BVByte x_6210 -> h_BVByte x_6210
490| BVnull x_6211 -> h_BVnull x_6211
491| BVptr (x_6213, x_6212) -> h_BVptr x_6213 x_6212
492| BVpc (x_6215, x_6214) -> h_BVpc x_6215 x_6214
493
494(** val beval_rect_Type5 :
495    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
496    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
497    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
498    -> beval -> 'a1 **)
499let rec beval_rect_Type5 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
500| BVundef -> h_BVundef
501| BVnonzero -> h_BVnonzero
502| BVXor (x_6226, x_6225, x_6224) -> h_BVXor x_6226 x_6225 x_6224
503| BVByte x_6227 -> h_BVByte x_6227
504| BVnull x_6228 -> h_BVnull x_6228
505| BVptr (x_6230, x_6229) -> h_BVptr x_6230 x_6229
506| BVpc (x_6232, x_6231) -> h_BVpc x_6232 x_6231
507
508(** val beval_rect_Type3 :
509    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
510    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
511    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
512    -> beval -> 'a1 **)
513let rec beval_rect_Type3 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
514| BVundef -> h_BVundef
515| BVnonzero -> h_BVnonzero
516| BVXor (x_6243, x_6242, x_6241) -> h_BVXor x_6243 x_6242 x_6241
517| BVByte x_6244 -> h_BVByte x_6244
518| BVnull x_6245 -> h_BVnull x_6245
519| BVptr (x_6247, x_6246) -> h_BVptr x_6247 x_6246
520| BVpc (x_6249, x_6248) -> h_BVpc x_6249 x_6248
521
522(** val beval_rect_Type2 :
523    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
524    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
525    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
526    -> beval -> 'a1 **)
527let rec beval_rect_Type2 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
528| BVundef -> h_BVundef
529| BVnonzero -> h_BVnonzero
530| BVXor (x_6260, x_6259, x_6258) -> h_BVXor x_6260 x_6259 x_6258
531| BVByte x_6261 -> h_BVByte x_6261
532| BVnull x_6262 -> h_BVnull x_6262
533| BVptr (x_6264, x_6263) -> h_BVptr x_6264 x_6263
534| BVpc (x_6266, x_6265) -> h_BVpc x_6266 x_6265
535
536(** val beval_rect_Type1 :
537    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
538    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
539    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
540    -> beval -> 'a1 **)
541let rec beval_rect_Type1 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
542| BVundef -> h_BVundef
543| BVnonzero -> h_BVnonzero
544| BVXor (x_6277, x_6276, x_6275) -> h_BVXor x_6277 x_6276 x_6275
545| BVByte x_6278 -> h_BVByte x_6278
546| BVnull x_6279 -> h_BVnull x_6279
547| BVptr (x_6281, x_6280) -> h_BVptr x_6281 x_6280
548| BVpc (x_6283, x_6282) -> h_BVpc x_6283 x_6282
549
550(** val beval_rect_Type0 :
551    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
552    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
553    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
554    -> beval -> 'a1 **)
555let rec beval_rect_Type0 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
556| BVundef -> h_BVundef
557| BVnonzero -> h_BVnonzero
558| BVXor (x_6294, x_6293, x_6292) -> h_BVXor x_6294 x_6293 x_6292
559| BVByte x_6295 -> h_BVByte x_6295
560| BVnull x_6296 -> h_BVnull x_6296
561| BVptr (x_6298, x_6297) -> h_BVptr x_6298 x_6297
562| BVpc (x_6300, x_6299) -> h_BVpc x_6300 x_6299
563
564(** val beval_inv_rect_Type4 :
565    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
566    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
567    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
568    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
569let beval_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
570  let hcut = beval_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
571
572(** val beval_inv_rect_Type3 :
573    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
574    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
575    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
576    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
577let beval_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
578  let hcut = beval_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
579
580(** val beval_inv_rect_Type2 :
581    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
582    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
583    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
584    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
585let beval_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
586  let hcut = beval_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
587
588(** val beval_inv_rect_Type1 :
589    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
590    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
591    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
592    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
593let beval_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
594  let hcut = beval_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
595
596(** val beval_inv_rect_Type0 :
597    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
598    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
599    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
600    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
601let beval_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
602  let hcut = beval_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
603
604(** val beval_discr : beval -> beval -> __ **)
605let beval_discr x y =
606  Logic.eq_rect_Type2 x
607    (match x with
608     | BVundef -> Obj.magic (fun _ dH -> dH)
609     | BVnonzero -> Obj.magic (fun _ dH -> dH)
610     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
611     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
612     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
613     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
614     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
615
616(** val beval_jmdiscr : beval -> beval -> __ **)
617let beval_jmdiscr x y =
618  Logic.eq_rect_Type2 x
619    (match x with
620     | BVundef -> Obj.magic (fun _ dH -> dH)
621     | BVnonzero -> Obj.magic (fun _ dH -> dH)
622     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
623     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
624     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
625     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
626     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
627
628(** val eq_bv_suffix :
629    Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector ->
630    BitVector.bitVector -> Bool.bool **)
631let eq_bv_suffix n m p v1 v2 =
632  let b1 = (Vector.vsplit n p v1).Types.snd in
633  let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2
634
635(** val pointer_of_bevals :
636    beval List.list -> Pointers.pointer Errors.res **)
637let pointer_of_bevals = function
638| List.Nil ->
639  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
640    List.Nil))
641| List.Cons (bv1, tl) ->
642  (match tl with
643   | List.Nil ->
644     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
645       List.Nil))
646   | List.Cons (bv2, tl') ->
647     (match tl' with
648      | List.Nil ->
649        (match bv1 with
650         | BVundef ->
651           Errors.Error (List.Cons ((Errors.MSG
652             ErrorMessages.CorruptedPointer), List.Nil))
653         | BVnonzero ->
654           Errors.Error (List.Cons ((Errors.MSG
655             ErrorMessages.CorruptedPointer), List.Nil))
656         | BVXor (x, x0, x1) ->
657           Errors.Error (List.Cons ((Errors.MSG
658             ErrorMessages.CorruptedPointer), List.Nil))
659         | BVByte x ->
660           Errors.Error (List.Cons ((Errors.MSG
661             ErrorMessages.CorruptedPointer), List.Nil))
662         | BVnull x ->
663           Errors.Error (List.Cons ((Errors.MSG
664             ErrorMessages.CorruptedPointer), List.Nil))
665         | BVptr (ptr1, p1) ->
666           (match bv2 with
667            | BVundef ->
668              Errors.Error (List.Cons ((Errors.MSG
669                ErrorMessages.CorruptedPointer), List.Nil))
670            | BVnonzero ->
671              Errors.Error (List.Cons ((Errors.MSG
672                ErrorMessages.CorruptedPointer), List.Nil))
673            | BVXor (x, x0, x1) ->
674              Errors.Error (List.Cons ((Errors.MSG
675                ErrorMessages.CorruptedPointer), List.Nil))
676            | BVByte x ->
677              Errors.Error (List.Cons ((Errors.MSG
678                ErrorMessages.CorruptedPointer), List.Nil))
679            | BVnull x ->
680              Errors.Error (List.Cons ((Errors.MSG
681                ErrorMessages.CorruptedPointer), List.Nil))
682            | BVptr (ptr2, p2) ->
683              (match Bool.andb
684                       (Bool.andb
685                         (Bool.andb (Nat.eqb (part_no p1) Nat.O)
686                           (Nat.eqb (part_no p2) (Nat.S Nat.O)))
687                         (Pointers.eq_block ptr1.Pointers.pblock
688                           ptr2.Pointers.pblock))
689                       (eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
690                         (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S
691                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
692                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
693                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
694                         (Pointers.offv ptr1.Pointers.poff)
695                         (Pointers.offv ptr2.Pointers.poff)) with
696               | Bool.True ->
697                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
698               | Bool.False ->
699                 Errors.Error (List.Cons ((Errors.MSG
700                   ErrorMessages.CorruptedPointer), List.Nil)))
701            | BVpc (x, x0) ->
702              Errors.Error (List.Cons ((Errors.MSG
703                ErrorMessages.CorruptedPointer), List.Nil)))
704         | BVpc (x, x0) ->
705           Errors.Error (List.Cons ((Errors.MSG
706             ErrorMessages.CorruptedPointer), List.Nil)))
707      | List.Cons (x, x0) ->
708        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
709          List.Nil))))
710
711(** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
712let pc_of_bevals = function
713| List.Nil ->
714  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
715    List.Nil))
716| List.Cons (bv1, tl) ->
717  (match tl with
718   | List.Nil ->
719     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
720       List.Nil))
721   | List.Cons (bv2, tl') ->
722     (match tl' with
723      | List.Nil ->
724        (match bv1 with
725         | BVundef ->
726           Errors.Error (List.Cons ((Errors.MSG
727             ErrorMessages.CorruptedPointer), List.Nil))
728         | BVnonzero ->
729           Errors.Error (List.Cons ((Errors.MSG
730             ErrorMessages.CorruptedPointer), List.Nil))
731         | BVXor (x, x0, x1) ->
732           Errors.Error (List.Cons ((Errors.MSG
733             ErrorMessages.CorruptedPointer), List.Nil))
734         | BVByte x ->
735           Errors.Error (List.Cons ((Errors.MSG
736             ErrorMessages.CorruptedPointer), List.Nil))
737         | BVnull x ->
738           Errors.Error (List.Cons ((Errors.MSG
739             ErrorMessages.CorruptedPointer), List.Nil))
740         | BVptr (x, x0) ->
741           Errors.Error (List.Cons ((Errors.MSG
742             ErrorMessages.CorruptedPointer), List.Nil))
743         | BVpc (ptr1, p1) ->
744           (match bv2 with
745            | BVundef ->
746              Errors.Error (List.Cons ((Errors.MSG
747                ErrorMessages.CorruptedPointer), List.Nil))
748            | BVnonzero ->
749              Errors.Error (List.Cons ((Errors.MSG
750                ErrorMessages.CorruptedPointer), List.Nil))
751            | BVXor (x, x0, x1) ->
752              Errors.Error (List.Cons ((Errors.MSG
753                ErrorMessages.CorruptedPointer), List.Nil))
754            | BVByte x ->
755              Errors.Error (List.Cons ((Errors.MSG
756                ErrorMessages.CorruptedPointer), List.Nil))
757            | BVnull x ->
758              Errors.Error (List.Cons ((Errors.MSG
759                ErrorMessages.CorruptedPointer), List.Nil))
760            | BVptr (x, x0) ->
761              Errors.Error (List.Cons ((Errors.MSG
762                ErrorMessages.CorruptedPointer), List.Nil))
763            | BVpc (ptr2, p2) ->
764              (match Bool.andb
765                       (Bool.andb (Nat.eqb (part_no p1) Nat.O)
766                         (Nat.eqb (part_no p2) (Nat.S Nat.O)))
767                       (eq_program_counter ptr1 ptr2) with
768               | Bool.True ->
769                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
770               | Bool.False ->
771                 Errors.Error (List.Cons ((Errors.MSG
772                   ErrorMessages.CorruptedPointer), List.Nil)))))
773      | List.Cons (x, x0) ->
774        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
775          List.Nil))))
776
777(** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
778let bevals_of_pointer p =
779  List.map (fun n_sig -> BVptr (p, (part_from_sig n_sig)))
780    (Lists.range_strong AST.size_pointer)
781
782(** val bevals_of_pc : program_counter -> beval List.list **)
783let bevals_of_pc p =
784  List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
785    (Lists.range_strong AST.size_pointer)
786
787(** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
788let list_to_pair l =
789  (match l with
790   | List.Nil ->
791     (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
792   | List.Cons (a, tl) ->
793     (match tl with
794      | List.Nil ->
795        (fun _ ->
796          Obj.magic Nat.nat_discr (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) __
797            (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S Nat.O) __))
798      | List.Cons (b, tl') ->
799        (match tl' with
800         | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
801         | List.Cons (c, tl'') ->
802           (fun _ ->
803             Obj.magic Nat.nat_discr (Nat.S (Nat.S (Nat.S
804               (List.length tl'')))) (Nat.S (Nat.S Nat.O)) __ (fun _ ->
805               Obj.magic Nat.nat_discr (Nat.S (Nat.S (List.length tl'')))
806                 (Nat.S Nat.O) __ (fun _ ->
807                 Obj.magic Nat.nat_discr (Nat.S (List.length tl'')) Nat.O __))))))
808    __
809
810(** val beval_pair_of_pointer :
811    Pointers.pointer -> (beval, beval) Types.prod **)
812let beval_pair_of_pointer p =
813  list_to_pair (bevals_of_pointer p)
814
815(** val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod **)
816let beval_pair_of_pc p =
817  list_to_pair (bevals_of_pc p)
818
819(** val bool_of_beval : beval -> Bool.bool Errors.res **)
820let bool_of_beval = function
821| BVundef ->
822  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
823    List.Nil))
824| BVnonzero -> Errors.OK Bool.True
825| BVXor (x, x0, x1) ->
826  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
827    List.Nil))
828| BVByte b ->
829  Errors.OK
830    (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
831      Nat.O))))))))
832      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
833        Nat.O))))))))) b)
834| BVnull x -> Errors.OK Bool.False
835| BVptr (x, x0) -> Errors.OK Bool.True
836| BVpc (x, x0) ->
837  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
838    List.Nil))
839
840(** val byte_of_val :
841    ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
842let byte_of_val err = function
843| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
844| BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
845| BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
846| BVByte b0 -> Errors.OK b0
847| BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
848| BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
849| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
850
851(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
852let word_of_list_beval l =
853  let first_byte = fun l0 ->
854    match l0 with
855    | List.Nil ->
856      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
857        ErrorMessages.NotAnInt32Val), List.Nil)))
858    | List.Cons (hd, tl) ->
859      Monad.m_bind0 (Monad.max_def Errors.res0)
860        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b ->
861        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
862  in
863  Obj.magic
864    (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
865      Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
866        Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
867          (fun b3 l2 ->
868          Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
869            (fun b4 l3 ->
870            match l3 with
871            | List.Nil ->
872              Obj.magic (Errors.OK
873                (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
874                  (Nat.S (Nat.S Nat.O))))))))
875                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
876                    (Nat.S Nat.O))))))))
877                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
878                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
879                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
880                  (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
881                    (Nat.S (Nat.S Nat.O))))))))
882                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
883                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
884                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
885                    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
886                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
887                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
888            | List.Cons (x, x0) ->
889              Obj.magic (Errors.Error (List.Cons ((Errors.MSG
890                ErrorMessages.NotAnInt32Val), List.Nil))))))))
891
892type bebit =
893| BBbit of Bool.bool
894| BBundef
895| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
896
897(** val bebit_rect_Type4 :
898    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
899    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
900let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
901| BBbit x_6419 -> h_BBbit x_6419
902| BBundef -> h_BBundef
903| BBptrcarry (x_6422, x_6421, p, x_6420) ->
904  h_BBptrcarry x_6422 x_6421 p x_6420
905
906(** val bebit_rect_Type5 :
907    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
908    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
909let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
910| BBbit x_6427 -> h_BBbit x_6427
911| BBundef -> h_BBundef
912| BBptrcarry (x_6430, x_6429, p, x_6428) ->
913  h_BBptrcarry x_6430 x_6429 p x_6428
914
915(** val bebit_rect_Type3 :
916    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
917    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
918let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
919| BBbit x_6435 -> h_BBbit x_6435
920| BBundef -> h_BBundef
921| BBptrcarry (x_6438, x_6437, p, x_6436) ->
922  h_BBptrcarry x_6438 x_6437 p x_6436
923
924(** val bebit_rect_Type2 :
925    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
926    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
927let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
928| BBbit x_6443 -> h_BBbit x_6443
929| BBundef -> h_BBundef
930| BBptrcarry (x_6446, x_6445, p, x_6444) ->
931  h_BBptrcarry x_6446 x_6445 p x_6444
932
933(** val bebit_rect_Type1 :
934    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
935    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
936let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
937| BBbit x_6451 -> h_BBbit x_6451
938| BBundef -> h_BBundef
939| BBptrcarry (x_6454, x_6453, p, x_6452) ->
940  h_BBptrcarry x_6454 x_6453 p x_6452
941
942(** val bebit_rect_Type0 :
943    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
944    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
945let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
946| BBbit x_6459 -> h_BBbit x_6459
947| BBundef -> h_BBundef
948| BBptrcarry (x_6462, x_6461, p, x_6460) ->
949  h_BBptrcarry x_6462 x_6461 p x_6460
950
951(** val bebit_inv_rect_Type4 :
952    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
953    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
954let bebit_inv_rect_Type4 hterm h1 h2 h3 =
955  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
956
957(** val bebit_inv_rect_Type3 :
958    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
959    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
960let bebit_inv_rect_Type3 hterm h1 h2 h3 =
961  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
962
963(** val bebit_inv_rect_Type2 :
964    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
965    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
966let bebit_inv_rect_Type2 hterm h1 h2 h3 =
967  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
968
969(** val bebit_inv_rect_Type1 :
970    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
971    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
972let bebit_inv_rect_Type1 hterm h1 h2 h3 =
973  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
974
975(** val bebit_inv_rect_Type0 :
976    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
977    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
978let bebit_inv_rect_Type0 hterm h1 h2 h3 =
979  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
980
981(** val bebit_discr : bebit -> bebit -> __ **)
982let bebit_discr x y =
983  Logic.eq_rect_Type2 x
984    (match x with
985     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
986     | BBundef -> Obj.magic (fun _ dH -> dH)
987     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
988    y
989
990(** val bebit_jmdiscr : bebit -> bebit -> __ **)
991let bebit_jmdiscr x y =
992  Logic.eq_rect_Type2 x
993    (match x with
994     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
995     | BBundef -> Obj.magic (fun _ dH -> dH)
996     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
997    y
998
999(** val bit_of_val :
1000    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
1001let bit_of_val err = function
1002| BBbit b0 -> Errors.OK b0
1003| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1004| BBptrcarry (x, x0, x1, x2) ->
1005  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1006
Note: See TracBrowser for help on using the repository browser.