source: extracted/byteValues.ml @ 2933

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

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 40.5 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_3 =
92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_3 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_5 =
99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5 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_7 =
106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_7 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_9 =
113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_9 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_11 =
120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_11 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_13 =
127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_13 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_29 =
218  let part_no = x_29 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_31 =
222  let part_no = x_31 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_33 =
226  let part_no = x_33 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_35 =
230  let part_no = x_35 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_37 =
234  let part_no = x_37 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_39 =
238  let part_no = x_39 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_73, x_72, x_71) -> h_BVXor x_73 x_72 x_71
489| BVByte x_74 -> h_BVByte x_74
490| BVnull x_75 -> h_BVnull x_75
491| BVptr (x_77, x_76) -> h_BVptr x_77 x_76
492| BVpc (x_79, x_78) -> h_BVpc x_79 x_78
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_90, x_89, x_88) -> h_BVXor x_90 x_89 x_88
503| BVByte x_91 -> h_BVByte x_91
504| BVnull x_92 -> h_BVnull x_92
505| BVptr (x_94, x_93) -> h_BVptr x_94 x_93
506| BVpc (x_96, x_95) -> h_BVpc x_96 x_95
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_107, x_106, x_105) -> h_BVXor x_107 x_106 x_105
517| BVByte x_108 -> h_BVByte x_108
518| BVnull x_109 -> h_BVnull x_109
519| BVptr (x_111, x_110) -> h_BVptr x_111 x_110
520| BVpc (x_113, x_112) -> h_BVpc x_113 x_112
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_124, x_123, x_122) -> h_BVXor x_124 x_123 x_122
531| BVByte x_125 -> h_BVByte x_125
532| BVnull x_126 -> h_BVnull x_126
533| BVptr (x_128, x_127) -> h_BVptr x_128 x_127
534| BVpc (x_130, x_129) -> h_BVpc x_130 x_129
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_141, x_140, x_139) -> h_BVXor x_141 x_140 x_139
545| BVByte x_142 -> h_BVByte x_142
546| BVnull x_143 -> h_BVnull x_143
547| BVptr (x_145, x_144) -> h_BVptr x_145 x_144
548| BVpc (x_147, x_146) -> h_BVpc x_147 x_146
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_158, x_157, x_156) -> h_BVXor x_158 x_157 x_156
559| BVByte x_159 -> h_BVByte x_159
560| BVnull x_160 -> h_BVnull x_160
561| BVptr (x_162, x_161) -> h_BVptr x_162 x_161
562| BVpc (x_164, x_163) -> h_BVpc x_164 x_163
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    (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_322 -> h_BBbit x_322
988| BBundef -> h_BBundef
989| BBptrcarry (x_325, x_324, p, x_323) -> h_BBptrcarry x_325 x_324 p x_323
990
991(** val bebit_rect_Type5 :
992    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
993    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
994let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
995| BBbit x_330 -> h_BBbit x_330
996| BBundef -> h_BBundef
997| BBptrcarry (x_333, x_332, p, x_331) -> h_BBptrcarry x_333 x_332 p x_331
998
999(** val bebit_rect_Type3 :
1000    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1001    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1002let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
1003| BBbit x_338 -> h_BBbit x_338
1004| BBundef -> h_BBundef
1005| BBptrcarry (x_341, x_340, p, x_339) -> h_BBptrcarry x_341 x_340 p x_339
1006
1007(** val bebit_rect_Type2 :
1008    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1009    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1010let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
1011| BBbit x_346 -> h_BBbit x_346
1012| BBundef -> h_BBundef
1013| BBptrcarry (x_349, x_348, p, x_347) -> h_BBptrcarry x_349 x_348 p x_347
1014
1015(** val bebit_rect_Type1 :
1016    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1017    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1018let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
1019| BBbit x_354 -> h_BBbit x_354
1020| BBundef -> h_BBundef
1021| BBptrcarry (x_357, x_356, p, x_355) -> h_BBptrcarry x_357 x_356 p x_355
1022
1023(** val bebit_rect_Type0 :
1024    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
1025    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
1026let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
1027| BBbit x_362 -> h_BBbit x_362
1028| BBundef -> h_BBundef
1029| BBptrcarry (x_365, x_364, p, x_363) -> h_BBptrcarry x_365 x_364 p x_363
1030
1031(** val bebit_inv_rect_Type4 :
1032    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1033    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1034let bebit_inv_rect_Type4 hterm h1 h2 h3 =
1035  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
1036
1037(** val bebit_inv_rect_Type3 :
1038    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1039    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1040let bebit_inv_rect_Type3 hterm h1 h2 h3 =
1041  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
1042
1043(** val bebit_inv_rect_Type2 :
1044    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1045    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1046let bebit_inv_rect_Type2 hterm h1 h2 h3 =
1047  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
1048
1049(** val bebit_inv_rect_Type1 :
1050    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1051    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1052let bebit_inv_rect_Type1 hterm h1 h2 h3 =
1053  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
1054
1055(** val bebit_inv_rect_Type0 :
1056    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
1057    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
1058let bebit_inv_rect_Type0 hterm h1 h2 h3 =
1059  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
1060
1061(** val bebit_discr : bebit -> bebit -> __ **)
1062let bebit_discr x y =
1063  Logic.eq_rect_Type2 x
1064    (match x with
1065     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1066     | BBundef -> Obj.magic (fun _ dH -> dH)
1067     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1068    y
1069
1070(** val bebit_jmdiscr : bebit -> bebit -> __ **)
1071let bebit_jmdiscr x y =
1072  Logic.eq_rect_Type2 x
1073    (match x with
1074     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
1075     | BBundef -> Obj.magic (fun _ dH -> dH)
1076     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
1077    y
1078
1079(** val bit_of_val :
1080    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
1081let bit_of_val err = function
1082| BBbit b0 -> Errors.OK b0
1083| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1084| BBptrcarry (x, x0, x1, x2) ->
1085  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
1086
Note: See TracBrowser for help on using the repository browser.