source: extracted/byteValues.ml @ 3001

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

New extraction.

File size: 40.8 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_2980 =
92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2980 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_2982 =
99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2982 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_2984 =
106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2984 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_2986 =
113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2986 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_2988 =
120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2988 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_2990 =
127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2990 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_3006 =
218  let part_no = x_3006 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_3008 =
222  let part_no = x_3008 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_3010 =
226  let part_no = x_3010 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_3012 =
230  let part_no = x_3012 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_3014 =
234  let part_no = x_3014 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_3016 =
238  let part_no = x_3016 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_3050, x_3049, x_3048) -> h_BVXor x_3050 x_3049 x_3048
489| BVByte x_3051 -> h_BVByte x_3051
490| BVnull x_3052 -> h_BVnull x_3052
491| BVptr (x_3054, x_3053) -> h_BVptr x_3054 x_3053
492| BVpc (x_3056, x_3055) -> h_BVpc x_3056 x_3055
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_3067, x_3066, x_3065) -> h_BVXor x_3067 x_3066 x_3065
503| BVByte x_3068 -> h_BVByte x_3068
504| BVnull x_3069 -> h_BVnull x_3069
505| BVptr (x_3071, x_3070) -> h_BVptr x_3071 x_3070
506| BVpc (x_3073, x_3072) -> h_BVpc x_3073 x_3072
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_3084, x_3083, x_3082) -> h_BVXor x_3084 x_3083 x_3082
517| BVByte x_3085 -> h_BVByte x_3085
518| BVnull x_3086 -> h_BVnull x_3086
519| BVptr (x_3088, x_3087) -> h_BVptr x_3088 x_3087
520| BVpc (x_3090, x_3089) -> h_BVpc x_3090 x_3089
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_3101, x_3100, x_3099) -> h_BVXor x_3101 x_3100 x_3099
531| BVByte x_3102 -> h_BVByte x_3102
532| BVnull x_3103 -> h_BVnull x_3103
533| BVptr (x_3105, x_3104) -> h_BVptr x_3105 x_3104
534| BVpc (x_3107, x_3106) -> h_BVpc x_3107 x_3106
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_3118, x_3117, x_3116) -> h_BVXor x_3118 x_3117 x_3116
545| BVByte x_3119 -> h_BVByte x_3119
546| BVnull x_3120 -> h_BVnull x_3120
547| BVptr (x_3122, x_3121) -> h_BVptr x_3122 x_3121
548| BVpc (x_3124, x_3123) -> h_BVpc x_3124 x_3123
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_3135, x_3134, x_3133) -> h_BVXor x_3135 x_3134 x_3133
559| BVByte x_3136 -> h_BVByte x_3136
560| BVnull x_3137 -> h_BVnull x_3137
561| BVptr (x_3139, x_3138) -> h_BVptr x_3139 x_3138
562| BVpc (x_3141, x_3140) -> h_BVpc x_3141 x_3140
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 (Pointers.pblock ptr1)
688                           (Pointers.pblock ptr2)))
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 (Pointers.poff ptr1))
695                         (Pointers.offv (Pointers.poff ptr2))) 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    (Bool.notb
831      (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
832        (Nat.S Nat.O))))))))
833        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
834          (Nat.S Nat.O))))))))) b))
835| BVnull x -> Errors.OK Bool.False
836| BVptr (x, x0) -> Errors.OK Bool.True
837| BVpc (x, x0) ->
838  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
839    List.Nil))
840
841(** val byte_of_val :
842    ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
843let byte_of_val err = function
844| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
845| BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
846| BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
847| BVByte b0 -> Errors.OK b0
848| BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
849| BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
850| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
851
852(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
853let word_of_list_beval l =
854  let first_byte = fun l0 ->
855    match l0 with
856    | List.Nil ->
857      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
858        ErrorMessages.NotAnInt32Val), List.Nil)))
859    | List.Cons (hd, tl) ->
860      Monad.m_bind0 (Monad.max_def Errors.res0)
861        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b ->
862        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
863  in
864  Obj.magic
865    (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
866      Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
867        Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
868          (fun b3 l2 ->
869          Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
870            (fun b4 l3 ->
871            match l3 with
872            | List.Nil ->
873              Obj.magic (Errors.OK
874                (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
875                  (Nat.S (Nat.S Nat.O))))))))
876                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
877                    (Nat.S Nat.O))))))))
878                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
879                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
880                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
881                  (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
882                    (Nat.S (Nat.S Nat.O))))))))
883                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
884                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
885                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
886                    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
887                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
888                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
889            | List.Cons (x, x0) ->
890              Obj.magic (Errors.Error (List.Cons ((Errors.MSG
891                ErrorMessages.NotAnInt32Val), List.Nil))))))))
892
893type add_or_sub =
894| Do_add
895| Do_sub
896
897(** val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
898let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function
899| Do_add -> h_do_add
900| Do_sub -> h_do_sub
901
902(** val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
903let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function
904| Do_add -> h_do_add
905| Do_sub -> h_do_sub
906
907(** val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
908let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function
909| Do_add -> h_do_add
910| Do_sub -> h_do_sub
911
912(** val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
913let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function
914| Do_add -> h_do_add
915| Do_sub -> h_do_sub
916
917(** val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
918let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function
919| Do_add -> h_do_add
920| Do_sub -> h_do_sub
921
922(** val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
923let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function
924| Do_add -> h_do_add
925| Do_sub -> h_do_sub
926
927(** val add_or_sub_inv_rect_Type4 :
928    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
929let add_or_sub_inv_rect_Type4 hterm h1 h2 =
930  let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __
931
932(** val add_or_sub_inv_rect_Type3 :
933    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
934let add_or_sub_inv_rect_Type3 hterm h1 h2 =
935  let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __
936
937(** val add_or_sub_inv_rect_Type2 :
938    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
939let add_or_sub_inv_rect_Type2 hterm h1 h2 =
940  let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __
941
942(** val add_or_sub_inv_rect_Type1 :
943    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
944let add_or_sub_inv_rect_Type1 hterm h1 h2 =
945  let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __
946
947(** val add_or_sub_inv_rect_Type0 :
948    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
949let add_or_sub_inv_rect_Type0 hterm h1 h2 =
950  let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __
951
952(** val add_or_sub_discr : add_or_sub -> add_or_sub -> __ **)
953let add_or_sub_discr x y =
954  Logic.eq_rect_Type2 x
955    (match x with
956     | Do_add -> Obj.magic (fun _ dH -> dH)
957     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
958
959(** val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __ **)
960let add_or_sub_jmdiscr x y =
961  Logic.eq_rect_Type2 x
962    (match x with
963     | Do_add -> Obj.magic (fun _ dH -> dH)
964     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
965
966(** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
967let eq_add_or_sub x y =
968  match x with
969  | Do_add ->
970    (match y with
971     | Do_add -> Bool.True
972     | Do_sub -> Bool.False)
973  | Do_sub ->
974    (match y with
975     | Do_add -> Bool.False
976     | Do_sub -> Bool.True)
977
978type bebit =
979| BBbit of Bool.bool
980| BBundef
981| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
982
983(** val bebit_rect_Type4 :
984    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
985    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
986let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
987| BBbit x_3299 -> h_BBbit x_3299
988| BBundef -> h_BBundef
989| BBptrcarry (x_3302, x_3301, p, x_3300) ->
990  h_BBptrcarry x_3302 x_3301 p x_3300
991
992(** val bebit_rect_Type5 :
993    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
994    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
995let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
996| BBbit x_3307 -> h_BBbit x_3307
997| BBundef -> h_BBundef
998| BBptrcarry (x_3310, x_3309, p, x_3308) ->
999  h_BBptrcarry x_3310 x_3309 p x_3308
1000
1001(** val bebit_rect_Type3 :
1002    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1003    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1004let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
1005| BBbit x_3315 -> h_BBbit x_3315
1006| BBundef -> h_BBundef
1007| BBptrcarry (x_3318, x_3317, p, x_3316) ->
1008  h_BBptrcarry x_3318 x_3317 p x_3316
1009
1010(** val bebit_rect_Type2 :
1011    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1012    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1013let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
1014| BBbit x_3323 -> h_BBbit x_3323
1015| BBundef -> h_BBundef
1016| BBptrcarry (x_3326, x_3325, p, x_3324) ->
1017  h_BBptrcarry x_3326 x_3325 p x_3324
1018
1019(** val bebit_rect_Type1 :
1020    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1021    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1022let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
1023| BBbit x_3331 -> h_BBbit x_3331
1024| BBundef -> h_BBundef
1025| BBptrcarry (x_3334, x_3333, p, x_3332) ->
1026  h_BBptrcarry x_3334 x_3333 p x_3332
1027
1028(** val bebit_rect_Type0 :
1029    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1030    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1031let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
1032| BBbit x_3339 -> h_BBbit x_3339
1033| BBundef -> h_BBundef
1034| BBptrcarry (x_3342, x_3341, p, x_3340) ->
1035  h_BBptrcarry x_3342 x_3341 p x_3340
1036
1037(** val bebit_inv_rect_Type4 :
1038    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1039    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1040let bebit_inv_rect_Type4 hterm h1 h2 h3 =
1041  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
1042
1043(** val bebit_inv_rect_Type3 :
1044    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1045    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1046let bebit_inv_rect_Type3 hterm h1 h2 h3 =
1047  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
1048
1049(** val bebit_inv_rect_Type2 :
1050    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1051    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1052let bebit_inv_rect_Type2 hterm h1 h2 h3 =
1053  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
1054
1055(** val bebit_inv_rect_Type1 :
1056    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1057    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1058let bebit_inv_rect_Type1 hterm h1 h2 h3 =
1059  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
1060
1061(** val bebit_inv_rect_Type0 :
1062    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1063    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1064let bebit_inv_rect_Type0 hterm h1 h2 h3 =
1065  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
1066
1067(** val bebit_discr : bebit -> bebit -> __ **)
1068let bebit_discr x y =
1069  Logic.eq_rect_Type2 x
1070    (match x with
1071     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1072     | BBundef -> Obj.magic (fun _ dH -> dH)
1073     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1074    y
1075
1076(** val bebit_jmdiscr : bebit -> bebit -> __ **)
1077let bebit_jmdiscr x y =
1078  Logic.eq_rect_Type2 x
1079    (match x with
1080     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1081     | BBundef -> Obj.magic (fun _ dH -> dH)
1082     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1083    y
1084
1085(** val bit_of_val :
1086    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
1087let bit_of_val err = function
1088| BBbit b0 -> Errors.OK b0
1089| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1090| BBptrcarry (x, x0, x1, x2) ->
1091  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1092
Note: See TracBrowser for help on using the repository browser.