source: extracted/backEndOps.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: 45.7 KB
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83(** val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod **)
84let divmodZ x y =
85  match x with
86  | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
87  | Z.Pos n ->
88    (match y with
89     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
90     | Z.Pos m ->
91       let { Types.fst = q; Types.snd = r } = Division.divide n m in
92       { Types.fst = (Division.natp_to_Z q); Types.snd =
93       (Division.natp_to_Z r) }
94     | Z.Neg m ->
95       let { Types.fst = q; Types.snd = r } = Division.divide n m in
96       (match r with
97        | Division.Pzero ->
98          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
99        | Division.Ppos x0 ->
100          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
101            (Z.zplus y (Division.natp_to_Z r)) }))
102  | Z.Neg n ->
103    (match y with
104     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
105     | Z.Pos m ->
106       let { Types.fst = q; Types.snd = r } = Division.divide n m in
107       (match r with
108        | Division.Pzero ->
109          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
110        | Division.Ppos x0 ->
111          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
112            (Z.zminus y (Division.natp_to_Z r)) })
113     | Z.Neg m ->
114       let { Types.fst = q; Types.snd = r } = Division.divide n m in
115       { Types.fst = (Division.natp_to_Z q); Types.snd =
116       (Division.natp_to_Z r) })
117
118type opAccs =
119| Mul
120| DivuModu
121
122(** val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
123let rec opAccs_rect_Type4 h_Mul h_DivuModu = function
124| Mul -> h_Mul
125| DivuModu -> h_DivuModu
126
127(** val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
128let rec opAccs_rect_Type5 h_Mul h_DivuModu = function
129| Mul -> h_Mul
130| DivuModu -> h_DivuModu
131
132(** val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
133let rec opAccs_rect_Type3 h_Mul h_DivuModu = function
134| Mul -> h_Mul
135| DivuModu -> h_DivuModu
136
137(** val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
138let rec opAccs_rect_Type2 h_Mul h_DivuModu = function
139| Mul -> h_Mul
140| DivuModu -> h_DivuModu
141
142(** val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
143let rec opAccs_rect_Type1 h_Mul h_DivuModu = function
144| Mul -> h_Mul
145| DivuModu -> h_DivuModu
146
147(** val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1 **)
148let rec opAccs_rect_Type0 h_Mul h_DivuModu = function
149| Mul -> h_Mul
150| DivuModu -> h_DivuModu
151
152(** val opAccs_inv_rect_Type4 :
153    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
154let opAccs_inv_rect_Type4 hterm h1 h2 =
155  let hcut = opAccs_rect_Type4 h1 h2 hterm in hcut __
156
157(** val opAccs_inv_rect_Type3 :
158    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
159let opAccs_inv_rect_Type3 hterm h1 h2 =
160  let hcut = opAccs_rect_Type3 h1 h2 hterm in hcut __
161
162(** val opAccs_inv_rect_Type2 :
163    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
164let opAccs_inv_rect_Type2 hterm h1 h2 =
165  let hcut = opAccs_rect_Type2 h1 h2 hterm in hcut __
166
167(** val opAccs_inv_rect_Type1 :
168    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
169let opAccs_inv_rect_Type1 hterm h1 h2 =
170  let hcut = opAccs_rect_Type1 h1 h2 hterm in hcut __
171
172(** val opAccs_inv_rect_Type0 :
173    opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
174let opAccs_inv_rect_Type0 hterm h1 h2 =
175  let hcut = opAccs_rect_Type0 h1 h2 hterm in hcut __
176
177(** val opAccs_discr : opAccs -> opAccs -> __ **)
178let opAccs_discr x y =
179  Logic.eq_rect_Type2 x
180    (match x with
181     | Mul -> Obj.magic (fun _ dH -> dH)
182     | DivuModu -> Obj.magic (fun _ dH -> dH)) y
183
184(** val opAccs_jmdiscr : opAccs -> opAccs -> __ **)
185let opAccs_jmdiscr x y =
186  Logic.eq_rect_Type2 x
187    (match x with
188     | Mul -> Obj.magic (fun _ dH -> dH)
189     | DivuModu -> Obj.magic (fun _ dH -> dH)) y
190
191type op1 =
192| Cmpl
193| Inc
194| Rl
195
196(** val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
197let rec op1_rect_Type4 h_Cmpl h_Inc h_Rl = function
198| Cmpl -> h_Cmpl
199| Inc -> h_Inc
200| Rl -> h_Rl
201
202(** val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
203let rec op1_rect_Type5 h_Cmpl h_Inc h_Rl = function
204| Cmpl -> h_Cmpl
205| Inc -> h_Inc
206| Rl -> h_Rl
207
208(** val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
209let rec op1_rect_Type3 h_Cmpl h_Inc h_Rl = function
210| Cmpl -> h_Cmpl
211| Inc -> h_Inc
212| Rl -> h_Rl
213
214(** val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
215let rec op1_rect_Type2 h_Cmpl h_Inc h_Rl = function
216| Cmpl -> h_Cmpl
217| Inc -> h_Inc
218| Rl -> h_Rl
219
220(** val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
221let rec op1_rect_Type1 h_Cmpl h_Inc h_Rl = function
222| Cmpl -> h_Cmpl
223| Inc -> h_Inc
224| Rl -> h_Rl
225
226(** val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1 **)
227let rec op1_rect_Type0 h_Cmpl h_Inc h_Rl = function
228| Cmpl -> h_Cmpl
229| Inc -> h_Inc
230| Rl -> h_Rl
231
232(** val op1_inv_rect_Type4 :
233    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
234let op1_inv_rect_Type4 hterm h1 h2 h3 =
235  let hcut = op1_rect_Type4 h1 h2 h3 hterm in hcut __
236
237(** val op1_inv_rect_Type3 :
238    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
239let op1_inv_rect_Type3 hterm h1 h2 h3 =
240  let hcut = op1_rect_Type3 h1 h2 h3 hterm in hcut __
241
242(** val op1_inv_rect_Type2 :
243    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
244let op1_inv_rect_Type2 hterm h1 h2 h3 =
245  let hcut = op1_rect_Type2 h1 h2 h3 hterm in hcut __
246
247(** val op1_inv_rect_Type1 :
248    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
249let op1_inv_rect_Type1 hterm h1 h2 h3 =
250  let hcut = op1_rect_Type1 h1 h2 h3 hterm in hcut __
251
252(** val op1_inv_rect_Type0 :
253    op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
254let op1_inv_rect_Type0 hterm h1 h2 h3 =
255  let hcut = op1_rect_Type0 h1 h2 h3 hterm in hcut __
256
257(** val op1_discr : op1 -> op1 -> __ **)
258let op1_discr x y =
259  Logic.eq_rect_Type2 x
260    (match x with
261     | Cmpl -> Obj.magic (fun _ dH -> dH)
262     | Inc -> Obj.magic (fun _ dH -> dH)
263     | Rl -> Obj.magic (fun _ dH -> dH)) y
264
265(** val op1_jmdiscr : op1 -> op1 -> __ **)
266let op1_jmdiscr x y =
267  Logic.eq_rect_Type2 x
268    (match x with
269     | Cmpl -> Obj.magic (fun _ dH -> dH)
270     | Inc -> Obj.magic (fun _ dH -> dH)
271     | Rl -> Obj.magic (fun _ dH -> dH)) y
272
273type op2 =
274| Add
275| Addc
276| Sub
277| And
278| Or
279| Xor
280
281(** val op2_rect_Type4 :
282    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
283let rec op2_rect_Type4 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
284| Add -> h_Add
285| Addc -> h_Addc
286| Sub -> h_Sub
287| And -> h_And
288| Or -> h_Or
289| Xor -> h_Xor
290
291(** val op2_rect_Type5 :
292    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
293let rec op2_rect_Type5 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
294| Add -> h_Add
295| Addc -> h_Addc
296| Sub -> h_Sub
297| And -> h_And
298| Or -> h_Or
299| Xor -> h_Xor
300
301(** val op2_rect_Type3 :
302    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
303let rec op2_rect_Type3 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
304| Add -> h_Add
305| Addc -> h_Addc
306| Sub -> h_Sub
307| And -> h_And
308| Or -> h_Or
309| Xor -> h_Xor
310
311(** val op2_rect_Type2 :
312    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
313let rec op2_rect_Type2 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
314| Add -> h_Add
315| Addc -> h_Addc
316| Sub -> h_Sub
317| And -> h_And
318| Or -> h_Or
319| Xor -> h_Xor
320
321(** val op2_rect_Type1 :
322    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
323let rec op2_rect_Type1 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
324| Add -> h_Add
325| Addc -> h_Addc
326| Sub -> h_Sub
327| And -> h_And
328| Or -> h_Or
329| Xor -> h_Xor
330
331(** val op2_rect_Type0 :
332    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1 **)
333let rec op2_rect_Type0 h_Add h_Addc h_Sub h_And h_Or h_Xor = function
334| Add -> h_Add
335| Addc -> h_Addc
336| Sub -> h_Sub
337| And -> h_And
338| Or -> h_Or
339| Xor -> h_Xor
340
341(** val op2_inv_rect_Type4 :
342    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
343    'a1) -> (__ -> 'a1) -> 'a1 **)
344let op2_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
345  let hcut = op2_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
346
347(** val op2_inv_rect_Type3 :
348    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
349    'a1) -> (__ -> 'a1) -> 'a1 **)
350let op2_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
351  let hcut = op2_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
352
353(** val op2_inv_rect_Type2 :
354    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
355    'a1) -> (__ -> 'a1) -> 'a1 **)
356let op2_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
357  let hcut = op2_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
358
359(** val op2_inv_rect_Type1 :
360    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
361    'a1) -> (__ -> 'a1) -> 'a1 **)
362let op2_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
363  let hcut = op2_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
364
365(** val op2_inv_rect_Type0 :
366    op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
367    'a1) -> (__ -> 'a1) -> 'a1 **)
368let op2_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
369  let hcut = op2_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
370
371(** val op2_discr : op2 -> op2 -> __ **)
372let op2_discr x y =
373  Logic.eq_rect_Type2 x
374    (match x with
375     | Add -> Obj.magic (fun _ dH -> dH)
376     | Addc -> Obj.magic (fun _ dH -> dH)
377     | Sub -> Obj.magic (fun _ dH -> dH)
378     | And -> Obj.magic (fun _ dH -> dH)
379     | Or -> Obj.magic (fun _ dH -> dH)
380     | Xor -> Obj.magic (fun _ dH -> dH)) y
381
382(** val op2_jmdiscr : op2 -> op2 -> __ **)
383let op2_jmdiscr x y =
384  Logic.eq_rect_Type2 x
385    (match x with
386     | Add -> Obj.magic (fun _ dH -> dH)
387     | Addc -> Obj.magic (fun _ dH -> dH)
388     | Sub -> Obj.magic (fun _ dH -> dH)
389     | And -> Obj.magic (fun _ dH -> dH)
390     | Or -> Obj.magic (fun _ dH -> dH)
391     | Xor -> Obj.magic (fun _ dH -> dH)) y
392
393type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
394                       (BitVector.byte, BitVector.byte) Types.prod);
395              op0 : (op1 -> BitVector.byte -> BitVector.byte);
396              op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
397                    -> (BitVector.byte, BitVector.bit) Types.prod) }
398
399(** val eval_rect_Type4 :
400    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
401    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
404let rec eval_rect_Type4 h_mk_Eval x_601 =
405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_601 in
406  h_mk_Eval opaccs0 op4 op5
407
408(** val eval_rect_Type5 :
409    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
410    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
413let rec eval_rect_Type5 h_mk_Eval x_603 =
414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_603 in
415  h_mk_Eval opaccs0 op4 op5
416
417(** val eval_rect_Type3 :
418    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
419    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
422let rec eval_rect_Type3 h_mk_Eval x_605 =
423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_605 in
424  h_mk_Eval opaccs0 op4 op5
425
426(** val eval_rect_Type2 :
427    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
428    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
431let rec eval_rect_Type2 h_mk_Eval x_607 =
432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_607 in
433  h_mk_Eval opaccs0 op4 op5
434
435(** val eval_rect_Type1 :
436    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
437    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
440let rec eval_rect_Type1 h_mk_Eval x_609 =
441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_609 in
442  h_mk_Eval opaccs0 op4 op5
443
444(** val eval_rect_Type0 :
445    ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
446    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
449let rec eval_rect_Type0 h_mk_Eval x_611 =
450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_611 in
451  h_mk_Eval opaccs0 op4 op5
452
453(** val opaccs :
454    eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
455    BitVector.byte) Types.prod **)
456let rec opaccs xxx =
457  xxx.opaccs
458
459(** val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte **)
460let rec op0 xxx =
461  xxx.op0
462
463(** val op3 :
464    eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
465    (BitVector.byte, BitVector.bit) Types.prod **)
466let rec op3 xxx =
467  xxx.op3
468
469(** val eval_inv_rect_Type4 :
470    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
471    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
472    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
473    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
474let eval_inv_rect_Type4 hterm h1 =
475  let hcut = eval_rect_Type4 h1 hterm in hcut __
476
477(** val eval_inv_rect_Type3 :
478    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
479    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
480    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
481    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
482let eval_inv_rect_Type3 hterm h1 =
483  let hcut = eval_rect_Type3 h1 hterm in hcut __
484
485(** val eval_inv_rect_Type2 :
486    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
487    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
488    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
489    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
490let eval_inv_rect_Type2 hterm h1 =
491  let hcut = eval_rect_Type2 h1 hterm in hcut __
492
493(** val eval_inv_rect_Type1 :
494    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
495    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
496    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
497    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
498let eval_inv_rect_Type1 hterm h1 =
499  let hcut = eval_rect_Type1 h1 hterm in hcut __
500
501(** val eval_inv_rect_Type0 :
502    eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
503    BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte)
504    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
505    (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1 **)
506let eval_inv_rect_Type0 hterm h1 =
507  let hcut = eval_rect_Type0 h1 hterm in hcut __
508
509(** val eval_discr : eval -> eval -> __ **)
510let eval_discr x y =
511  Logic.eq_rect_Type2 x
512    (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
513    Obj.magic (fun _ dH -> dH __ __ __)) y
514
515(** val eval_jmdiscr : eval -> eval -> __ **)
516let eval_jmdiscr x y =
517  Logic.eq_rect_Type2 x
518    (let { opaccs = a0; op0 = a1; op3 = a2 } = x in
519    Obj.magic (fun _ dH -> dH __ __ __)) y
520
521(** val opaccs_implementation :
522    opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
523    BitVector.byte) Types.prod **)
524let opaccs_implementation op by1 by2 =
525  let n1 =
526    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
527      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1
528  in
529  let n2 =
530    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
532  in
533  (match op with
534   | Mul ->
535     let prod =
536       Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
537         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
538         (Nat.S Nat.O))))))))
539         (BitVectorZ.bitvector_of_Z
540           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
541             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
542             (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
543     in
544     { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst }
545   | DivuModu ->
546     (match Z.eqZb n2 Z.OZ with
547      | Bool.True -> { Types.fst = by1; Types.snd = by2 }
548      | Bool.False ->
549        let { Types.fst = q; Types.snd = r } = divmodZ n1 n2 in
550        { Types.fst =
551        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552          (Nat.S (Nat.S Nat.O)))))))) q); Types.snd =
553        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
554          (Nat.S (Nat.S Nat.O)))))))) r) }))
555
556(** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
557let op1_implementation op by =
558  match op with
559  | Cmpl ->
560    BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
561      (Nat.S Nat.O)))))))) by
562  | Inc ->
563    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
564      Nat.O)))))))) by
565      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
566        (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
567  | Rl ->
568    Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
569      (Nat.S Nat.O)))))))) (Nat.S Nat.O) by
570
571(** val op2_implementation :
572    BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
573    (BitVector.byte, BitVector.bit) Types.prod **)
574let op2_implementation carry op by1 by2 =
575  match op with
576  | Add ->
577    let { Types.fst = res; Types.snd = flags } =
578      Arithmetic.add_8_with_carry by1 by2 Bool.False
579    in
580    { Types.fst = res; Types.snd =
581    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
582  | Addc ->
583    let { Types.fst = res; Types.snd = flags } =
584      Arithmetic.add_8_with_carry by1 by2 carry
585    in
586    { Types.fst = res; Types.snd =
587    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
588  | Sub ->
589    let { Types.fst = res; Types.snd = flags } =
590      Arithmetic.sub_8_with_carry by1 by2 carry
591    in
592    { Types.fst = res; Types.snd =
593    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
594  | And ->
595    { Types.fst =
596      (BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
597        (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
598  | Or ->
599    { Types.fst =
600      (BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
601        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
602  | Xor ->
603    { Types.fst =
604      (BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
605        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
606
607(** val eval0 : eval **)
608let eval0 =
609  { opaccs = opaccs_implementation; op0 = op1_implementation; op3 =
610    op2_implementation }
611
612(** val be_opaccs :
613    opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
614    ByteValues.beval) Types.prod Errors.res **)
615let be_opaccs op a b =
616  Obj.magic
617    (Monad.m_bind0 (Monad.max_def Errors.res0)
618      (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
619      (fun a' ->
620      Monad.m_bind0 (Monad.max_def Errors.res0)
621        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b))
622        (fun b' ->
623        let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in
624        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
625          (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') })))
626
627(** val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res **)
628let be_op1 op a =
629  Obj.magic
630    (Monad.m_bind0 (Monad.max_def Errors.res0)
631      (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a))
632      (fun a' ->
633      Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte
634        (eval0.op0 op a'))))
635
636(** val op2_bytes :
637    op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
638    BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
639    BitVector.bit) Types.prod **)
640let op2_bytes op n carry =
641  let f = fun n0 b1 b2 pr ->
642    let { Types.fst = res_tl; Types.snd = carry0 } = pr in
643    let { Types.fst = res_hd; Types.snd = carry' } =
644      eval0.op3 carry0 op b1 b2
645    in
646    { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' }
647  in
648  Vector.fold_right2_i f { Types.fst = Vector.VEmpty; Types.snd = carry } n
649
650(** val op_of_add_or_sub : ByteValues.add_or_sub -> op2 **)
651let op_of_add_or_sub = function
652| ByteValues.Do_add -> Addc
653| ByteValues.Do_sub -> Sub
654
655(** val be_add_sub_byte :
656    ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
657    BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
658    Errors.res **)
659let be_add_sub_byte is_add carry a1 b2 =
660  let op = op_of_add_or_sub is_add in
661  (match a1 with
662   | ByteValues.BVundef ->
663     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
664       List.Nil))
665   | ByteValues.BVnonzero ->
666     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
667       List.Nil))
668   | ByteValues.BVXor (x, x0, x1) ->
669     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
670       List.Nil))
671   | ByteValues.BVByte b1 ->
672     Obj.magic
673       (Monad.m_bind0 (Monad.max_def Errors.res0)
674         (Obj.magic
675           (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
676         (fun carry' ->
677         let { Types.fst = rslt; Types.snd = carry'' } =
678           eval0.op3 carry' op b1 b2
679         in
680         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
681           (ByteValues.BVByte rslt); Types.snd = (ByteValues.BBbit carry'') }))
682   | ByteValues.BVnull x ->
683     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
684       List.Nil))
685   | ByteValues.BVptr (ptr, p) ->
686     (match Pointers.ptype ptr with
687      | AST.XData ->
688        (match ByteValues.part_no p with
689         | Nat.O ->
690           Obj.magic
691             (Monad.m_bind0 (Monad.max_def Errors.res0)
692               (Obj.magic
693                 (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
694               (fun carry' ->
695               match carry' with
696               | Bool.True ->
697                 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
698                   ErrorMessages.UnsupportedOp), List.Nil)))
699               | Bool.False ->
700                 let o1o0 =
701                   Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
702                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
703                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
704                     (Pointers.offv ptr.Pointers.poff)
705                 in
706                 let { Types.fst = rslt; Types.snd = carry0 } =
707                   eval0.op3 Bool.False op b2 o1o0.Types.snd
708                 in
709                 let p0 = Nat.O in
710                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
711                   Pointers.poff =
712                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
713                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
714                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
715                     rslt) }
716                 in
717                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
718                   (ByteValues.BVptr (ptr', p)); Types.snd =
719                   (ByteValues.BBptrcarry (is_add, ptr, p0, b2)) }))
720         | Nat.S x ->
721           (match carry with
722            | ByteValues.BBbit x0 ->
723              Errors.Error (List.Cons ((Errors.MSG
724                ErrorMessages.UnsupportedOp), List.Nil))
725            | ByteValues.BBundef ->
726              Errors.Error (List.Cons ((Errors.MSG
727                ErrorMessages.UnsupportedOp), List.Nil))
728            | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
729              (match Bool.andb
730                       (Bool.andb (ByteValues.eq_add_or_sub is_add is_add')
731                         (Pointers.eq_block ptr.Pointers.pblock
732                           ptr'.Pointers.pblock))
733                       (ByteValues.eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S
734                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S
735                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
736                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
737                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
738                         (Pointers.offv ptr.Pointers.poff)
739                         (Pointers.offv ptr'.Pointers.poff)) with
740               | Bool.True ->
741                 Util.if_then_else_safe
742                   (Nat.eqb (ByteValues.part_no p') Nat.O) (fun _ ->
743                   let by'0 = (fun _ _ -> by') __ __ in
744                   let o1o0 =
745                     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
746                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
747                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
748                       (Pointers.offv ptr.Pointers.poff)
749                   in
750                   let o1o1 = Vector.VCons ((Nat.S Nat.O), o1o0.Types.fst,
751                     (Vector.VCons (Nat.O, o1o0.Types.snd, Vector.VEmpty)))
752                   in
753                   let { Types.fst = rslt; Types.snd = ignore } =
754                     op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
755                       (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
756                       (Nat.O, by'0, Vector.VEmpty))))
757                   in
758                   let part1 = Nat.S Nat.O in
759                   let ptr'' = { Pointers.pblock = ptr.Pointers.pblock;
760                     Pointers.poff =
761                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
762                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
763                       Nat.O)))))))) rslt) }
764                   in
765                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'', part1));
766                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr', part1,
767                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
768                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
769                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
770                   (fun _ -> Errors.Error (List.Cons ((Errors.MSG
771                   ErrorMessages.UnsupportedOp), List.Nil)))
772               | Bool.False ->
773                 Errors.Error (List.Cons ((Errors.MSG
774                   ErrorMessages.UnsupportedOp), List.Nil)))))
775      | AST.Code ->
776        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
777          List.Nil)))
778   | ByteValues.BVpc (x, x0) ->
779     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
780       List.Nil)))
781
782(** val byte_at :
783    Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte **)
784let byte_at n v p =
785  let suffix =
786    (Vector.vsplit
787      (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
788        Nat.O)))))))) (Nat.minus n (Nat.S p)))
789      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
790        Nat.O))))))))
791        (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
792          Nat.O)))))))) p)) v).Types.snd
793  in
794  (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
795    Nat.O))))))))
796    (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
797      Nat.O)))))))) p) suffix).Types.fst
798
799(** val eq_opt :
800    ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
801    Bool.bool **)
802let eq_opt eq m n =
803  match m with
804  | Types.None ->
805    (match m with
806     | Types.None -> Bool.True
807     | Types.Some x -> Bool.False)
808  | Types.Some a ->
809    (match n with
810     | Types.None -> Bool.False
811     | Types.Some b -> eq a b)
812
813(** val be_op2 :
814    ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
815    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
816let be_op2 carry op a1 a2 =
817  match op with
818  | Add ->
819    (match a1 with
820     | ByteValues.BVundef ->
821       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
822         List.Nil))
823     | ByteValues.BVnonzero ->
824       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
825         List.Nil))
826     | ByteValues.BVXor (x, x0, x1) ->
827       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
828         List.Nil))
829     | ByteValues.BVByte b1 ->
830       be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a2 b1
831     | ByteValues.BVnull x ->
832       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
833         List.Nil))
834     | ByteValues.BVptr (ptr1, p1) ->
835       (match a2 with
836        | ByteValues.BVundef ->
837          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
838            List.Nil))
839        | ByteValues.BVnonzero ->
840          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
841            List.Nil))
842        | ByteValues.BVXor (x, x0, x1) ->
843          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
844            List.Nil))
845        | ByteValues.BVByte b2 ->
846          be_add_sub_byte ByteValues.Do_add (ByteValues.BBbit Bool.False) a1
847            b2
848        | ByteValues.BVnull x ->
849          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
850            List.Nil))
851        | ByteValues.BVptr (x, x0) ->
852          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
853            List.Nil))
854        | ByteValues.BVpc (x, x0) ->
855          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
856            List.Nil)))
857     | ByteValues.BVpc (x, x0) ->
858       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
859         List.Nil)))
860  | Addc ->
861    (match a1 with
862     | ByteValues.BVundef ->
863       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
864         List.Nil))
865     | ByteValues.BVnonzero ->
866       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
867         List.Nil))
868     | ByteValues.BVXor (x, x0, x1) ->
869       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
870         List.Nil))
871     | ByteValues.BVByte b1 -> be_add_sub_byte ByteValues.Do_add carry a2 b1
872     | ByteValues.BVnull x ->
873       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
874         List.Nil))
875     | ByteValues.BVptr (ptr1, p1) ->
876       (match a2 with
877        | ByteValues.BVundef ->
878          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
879            List.Nil))
880        | ByteValues.BVnonzero ->
881          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
882            List.Nil))
883        | ByteValues.BVXor (x, x0, x1) ->
884          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
885            List.Nil))
886        | ByteValues.BVByte b2 ->
887          be_add_sub_byte ByteValues.Do_add carry a1 b2
888        | ByteValues.BVnull x ->
889          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
890            List.Nil))
891        | ByteValues.BVptr (x, x0) ->
892          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
893            List.Nil))
894        | ByteValues.BVpc (x, x0) ->
895          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
896            List.Nil)))
897     | ByteValues.BVpc (x, x0) ->
898       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
899         List.Nil)))
900  | Sub ->
901    (match a1 with
902     | ByteValues.BVundef ->
903       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
904         List.Nil))
905     | ByteValues.BVnonzero ->
906       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
907         List.Nil))
908     | ByteValues.BVXor (x, x0, x1) ->
909       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
910         List.Nil))
911     | ByteValues.BVByte b1 ->
912       Obj.magic
913         (Monad.m_bind0 (Monad.max_def Errors.res0)
914           (Obj.magic
915             (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
916           (fun b2 ->
917           Obj.magic (be_add_sub_byte ByteValues.Do_sub carry a1 b2)))
918     | ByteValues.BVnull x ->
919       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
920         List.Nil))
921     | ByteValues.BVptr (ptr1, p1) ->
922       (match a2 with
923        | ByteValues.BVundef ->
924          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
925            List.Nil))
926        | ByteValues.BVnonzero ->
927          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
928            List.Nil))
929        | ByteValues.BVXor (x, x0, x1) ->
930          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
931            List.Nil))
932        | ByteValues.BVByte b2 ->
933          be_add_sub_byte ByteValues.Do_sub carry a1 b2
934        | ByteValues.BVnull x ->
935          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
936            List.Nil))
937        | ByteValues.BVptr (ptr2, p2) ->
938          (match Pointers.ptype ptr1 with
939           | AST.XData ->
940             (match Bool.andb
941                      (Pointers.eq_block ptr1.Pointers.pblock
942                        ptr2.Pointers.pblock)
943                      (Nat.eqb (ByteValues.part_no p1)
944                        (ByteValues.part_no p2)) with
945              | Bool.True ->
946                Obj.magic
947                  (Monad.m_bind0 (Monad.max_def Errors.res0)
948                    (Obj.magic
949                      (ByteValues.bit_of_val ErrorMessages.UnsupportedOp
950                        carry)) (fun carry0 ->
951                    let by1 =
952                      byte_at AST.size_pointer
953                        (Pointers.offv ptr1.Pointers.poff)
954                        (ByteValues.part_no p1)
955                    in
956                    let by2 =
957                      byte_at AST.size_pointer
958                        (Pointers.offv ptr2.Pointers.poff)
959                        (ByteValues.part_no p1)
960                    in
961                    let { Types.fst = result; Types.snd = carry1 } =
962                      eval0.op3 carry0 Sub by1 by2
963                    in
964                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
965                      (ByteValues.BVByte result); Types.snd =
966                      (ByteValues.BBbit carry1) }))
967              | Bool.False ->
968                Errors.Error (List.Cons ((Errors.MSG
969                  ErrorMessages.UnsupportedOp), List.Nil)))
970           | AST.Code ->
971             Errors.Error (List.Cons ((Errors.MSG
972               ErrorMessages.UnsupportedOp), List.Nil)))
973        | ByteValues.BVpc (x, x0) ->
974          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
975            List.Nil)))
976     | ByteValues.BVpc (x, x0) ->
977       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
978         List.Nil)))
979  | And ->
980    Obj.magic
981      (Monad.m_bind0 (Monad.max_def Errors.res0)
982        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a1))
983        (fun b1 ->
984        Monad.m_bind0 (Monad.max_def Errors.res0)
985          (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
986          (fun b2 ->
987          let res = (eval0.op3 Bool.False And b1 b2).Types.fst in
988          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
989            (ByteValues.BVByte res); Types.snd = carry })))
990  | Or ->
991    (match a1 with
992     | ByteValues.BVundef ->
993       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
994         List.Nil))
995     | ByteValues.BVnonzero ->
996       (match a2 with
997        | ByteValues.BVundef ->
998          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
999            List.Nil))
1000        | ByteValues.BVnonzero ->
1001          Obj.magic
1002            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1003              ByteValues.BVnonzero; Types.snd = carry })
1004        | ByteValues.BVXor (x, x0, x1) ->
1005          Obj.magic
1006            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1007              ByteValues.BVnonzero; Types.snd = carry })
1008        | ByteValues.BVByte x ->
1009          Obj.magic
1010            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1011              ByteValues.BVnonzero; Types.snd = carry })
1012        | ByteValues.BVnull x ->
1013          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1014            List.Nil))
1015        | ByteValues.BVptr (x, x0) ->
1016          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1017            List.Nil))
1018        | ByteValues.BVpc (x, x0) ->
1019          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1020            List.Nil)))
1021     | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
1022       (match a2 with
1023        | ByteValues.BVundef ->
1024          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1025            List.Nil))
1026        | ByteValues.BVnonzero ->
1027          Obj.magic
1028            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1029              ByteValues.BVnonzero; Types.snd = carry })
1030        | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
1031          (match Bool.orb
1032                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
1033                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
1034                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
1035                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
1036           | Bool.True ->
1037             let eq_at = fun p ptr1 ptr2 ->
1038               Bool.andb
1039                 (Pointers.eq_block ptr1.Pointers.pblock
1040                   ptr2.Pointers.pblock)
1041                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1042                   (Nat.S (Nat.S Nat.O))))))))
1043                   (byte_at AST.size_pointer
1044                     (Pointers.offv ptr1.Pointers.poff)
1045                     (ByteValues.part_no p))
1046                   (byte_at AST.size_pointer
1047                     (Pointers.offv ptr2.Pointers.poff)
1048                     (ByteValues.part_no p)))
1049             in
1050             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
1051                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
1052              | Bool.True ->
1053                Obj.magic
1054                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1055                    (ByteValues.BVByte
1056                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1057                      (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
1058              | Bool.False ->
1059                Obj.magic
1060                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1061                    ByteValues.BVnonzero; Types.snd = carry }))
1062           | Bool.False ->
1063             Errors.Error (List.Cons ((Errors.MSG
1064               ErrorMessages.UnsupportedOp), List.Nil)))
1065        | ByteValues.BVByte x ->
1066          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1067            List.Nil))
1068        | ByteValues.BVnull x ->
1069          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1070            List.Nil))
1071        | ByteValues.BVptr (x, x0) ->
1072          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1073            List.Nil))
1074        | ByteValues.BVpc (x, x0) ->
1075          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1076            List.Nil)))
1077     | ByteValues.BVByte b1 ->
1078       (match a2 with
1079        | ByteValues.BVundef ->
1080          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1081            List.Nil))
1082        | ByteValues.BVnonzero ->
1083          Obj.magic
1084            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1085              ByteValues.BVnonzero; Types.snd = carry })
1086        | ByteValues.BVXor (x, x0, x1) ->
1087          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1088            List.Nil))
1089        | ByteValues.BVByte b2 ->
1090          let res = (eval0.op3 Bool.False Or b1 b2).Types.fst in
1091          Obj.magic
1092            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1093              (ByteValues.BVByte res); Types.snd = carry })
1094        | ByteValues.BVnull x ->
1095          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1096            List.Nil))
1097        | ByteValues.BVptr (x, x0) ->
1098          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1099            List.Nil))
1100        | ByteValues.BVpc (x, x0) ->
1101          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1102            List.Nil)))
1103     | ByteValues.BVnull x ->
1104       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1105         List.Nil))
1106     | ByteValues.BVptr (x, x0) ->
1107       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1108         List.Nil))
1109     | ByteValues.BVpc (x, x0) ->
1110       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1111         List.Nil)))
1112  | Xor ->
1113    (match a1 with
1114     | ByteValues.BVundef ->
1115       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1116         List.Nil))
1117     | ByteValues.BVnonzero ->
1118       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1119         List.Nil))
1120     | ByteValues.BVXor (x, x0, x1) ->
1121       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1122         List.Nil))
1123     | ByteValues.BVByte b1 ->
1124       (match a2 with
1125        | ByteValues.BVundef ->
1126          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1127            List.Nil))
1128        | ByteValues.BVnonzero ->
1129          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1130            List.Nil))
1131        | ByteValues.BVXor (x, x0, x1) ->
1132          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1133            List.Nil))
1134        | ByteValues.BVByte b2 ->
1135          let res = (eval0.op3 Bool.False Xor b1 b2).Types.fst in
1136          Obj.magic
1137            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1138              (ByteValues.BVByte res); Types.snd = carry })
1139        | ByteValues.BVnull x ->
1140          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1141            List.Nil))
1142        | ByteValues.BVptr (x, x0) ->
1143          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1144            List.Nil))
1145        | ByteValues.BVpc (x, x0) ->
1146          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1147            List.Nil)))
1148     | ByteValues.BVnull p1 ->
1149       (match a2 with
1150        | ByteValues.BVundef ->
1151          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1152            List.Nil))
1153        | ByteValues.BVnonzero ->
1154          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1155            List.Nil))
1156        | ByteValues.BVXor (x, x0, x1) ->
1157          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1158            List.Nil))
1159        | ByteValues.BVByte x ->
1160          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1161            List.Nil))
1162        | ByteValues.BVnull p2 ->
1163          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1164           | Bool.True ->
1165             Obj.magic
1166               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1167                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
1168                 carry })
1169           | Bool.False ->
1170             Errors.Error (List.Cons ((Errors.MSG
1171               ErrorMessages.UnsupportedOp), List.Nil)))
1172        | ByteValues.BVptr (ptr2, p2) ->
1173          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1174           | Bool.True ->
1175             Obj.magic
1176               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1177                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
1178                 Types.snd = carry })
1179           | Bool.False ->
1180             Errors.Error (List.Cons ((Errors.MSG
1181               ErrorMessages.UnsupportedOp), List.Nil)))
1182        | ByteValues.BVpc (x, x0) ->
1183          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1184            List.Nil)))
1185     | ByteValues.BVptr (ptr1, p1) ->
1186       (match a2 with
1187        | ByteValues.BVundef ->
1188          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1189            List.Nil))
1190        | ByteValues.BVnonzero ->
1191          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1192            List.Nil))
1193        | ByteValues.BVXor (x, x0, x1) ->
1194          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1195            List.Nil))
1196        | ByteValues.BVByte x ->
1197          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1198            List.Nil))
1199        | ByteValues.BVnull p2 ->
1200          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1201           | Bool.True ->
1202             Obj.magic
1203               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1204                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
1205                 Types.snd = carry })
1206           | Bool.False ->
1207             Errors.Error (List.Cons ((Errors.MSG
1208               ErrorMessages.UnsupportedOp), List.Nil)))
1209        | ByteValues.BVptr (ptr2, p2) ->
1210          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1211           | Bool.True ->
1212             Obj.magic
1213               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1214                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
1215                 p1)); Types.snd = carry })
1216           | Bool.False ->
1217             Errors.Error (List.Cons ((Errors.MSG
1218               ErrorMessages.UnsupportedOp), List.Nil)))
1219        | ByteValues.BVpc (x, x0) ->
1220          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1221            List.Nil)))
1222     | ByteValues.BVpc (x, x0) ->
1223       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1224         List.Nil)))
1225
Note: See TracBrowser for help on using the repository browser.