source: extracted/backEndOps.ml @ 2873

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

Extracted again.

File size: 45.3 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_19271 =
405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19271 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_19273 =
414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19273 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_19275 =
423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19275 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_19277 =
432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19277 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_19279 =
441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19279 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_19281 =
450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_19281 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 be_add_sub_byte :
651    Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
652    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
653let be_add_sub_byte is_add carry a1 b2 =
654  let op =
655    match is_add with
656    | Bool.True -> Addc
657    | Bool.False -> Sub
658  in
659  (match a1 with
660   | ByteValues.BVundef ->
661     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
662       List.Nil))
663   | ByteValues.BVnonzero ->
664     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
665       List.Nil))
666   | ByteValues.BVXor (x, x0, x1) ->
667     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
668       List.Nil))
669   | ByteValues.BVByte b1 ->
670     Obj.magic
671       (Monad.m_bind0 (Monad.max_def Errors.res0)
672         (Obj.magic
673           (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
674         (fun carry' ->
675         let { Types.fst = rslt; Types.snd = carry'' } =
676           eval0.op3 carry' op b1 b2
677         in
678         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
679           (ByteValues.BVByte rslt); Types.snd = (ByteValues.BBbit carry'') }))
680   | ByteValues.BVnull x ->
681     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
682       List.Nil))
683   | ByteValues.BVptr (ptr, p) ->
684     (match Pointers.ptype ptr with
685      | AST.XData ->
686        (match ByteValues.part_no p with
687         | Nat.O ->
688           Obj.magic
689             (Monad.m_bind0 (Monad.max_def Errors.res0)
690               (Obj.magic
691                 (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
692               (fun carry' ->
693               match carry' with
694               | Bool.True ->
695                 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
696                   ErrorMessages.UnsupportedOp), List.Nil)))
697               | Bool.False ->
698                 let o1o0 =
699                   Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
700                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
701                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
702                     (Pointers.offv ptr.Pointers.poff)
703                 in
704                 let { Types.fst = rslt; Types.snd = carry0 } =
705                   eval0.op3 Bool.False op b2 o1o0.Types.snd
706                 in
707                 let p0 = Nat.O in
708                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
709                   Pointers.poff =
710                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
711                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
712                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
713                     rslt) }
714                 in
715                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
716                   (ByteValues.BVptr (ptr', p)); Types.snd =
717                   (ByteValues.BBptrcarry (is_add, ptr, p0, b2)) }))
718         | Nat.S x ->
719           (match carry with
720            | ByteValues.BBbit x0 ->
721              Errors.Error (List.Cons ((Errors.MSG
722                ErrorMessages.UnsupportedOp), List.Nil))
723            | ByteValues.BBundef ->
724              Errors.Error (List.Cons ((Errors.MSG
725                ErrorMessages.UnsupportedOp), List.Nil))
726            | ByteValues.BBptrcarry (is_add', ptr', p', by') ->
727              (match Bool.andb
728                       (Bool.andb (BitVector.eq_b is_add is_add')
729                         (Pointers.eq_block ptr.Pointers.pblock
730                           ptr'.Pointers.pblock))
731                       (ByteValues.eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S
732                         (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S
733                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
734                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
735                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
736                         (Pointers.offv ptr.Pointers.poff)
737                         (Pointers.offv ptr'.Pointers.poff)) with
738               | Bool.True ->
739                 Util.if_then_else_safe
740                   (Nat.eqb (ByteValues.part_no p') Nat.O) (fun _ ->
741                   let by'0 = (fun _ _ -> by') __ __ in
742                   let o1o0 =
743                     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
744                       (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S
745                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
746                       (Pointers.offv ptr.Pointers.poff)
747                   in
748                   let o1o1 = Vector.VCons ((Nat.S Nat.O), o1o0.Types.fst,
749                     (Vector.VCons (Nat.O, o1o0.Types.snd, Vector.VEmpty)))
750                   in
751                   let { Types.fst = rslt; Types.snd = ignore } =
752                     op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
753                       (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
754                       (Nat.O, by'0, Vector.VEmpty))))
755                   in
756                   let part1 = Nat.S Nat.O in
757                   let ptr'0 = { Pointers.pblock = ptr.Pointers.pblock;
758                     Pointers.poff =
759                     (Vector.vflatten (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S
760                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
761                       Nat.O)))))))) rslt) }
762                   in
763                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1));
764                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1,
765                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
766                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
767                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
768                   (fun _ -> Errors.Error (List.Cons ((Errors.MSG
769                   ErrorMessages.UnsupportedOp), List.Nil)))
770               | Bool.False ->
771                 Errors.Error (List.Cons ((Errors.MSG
772                   ErrorMessages.UnsupportedOp), List.Nil)))))
773      | AST.Code ->
774        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
775          List.Nil)))
776   | ByteValues.BVpc (x, x0) ->
777     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
778       List.Nil)))
779
780(** val byte_at :
781    Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte **)
782let byte_at n v p =
783  let suffix =
784    (Vector.vsplit
785      (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
786        Nat.O)))))))) (Nat.minus n (Nat.S p)))
787      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
788        Nat.O))))))))
789        (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
790          Nat.O)))))))) p)) v).Types.snd
791  in
792  (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
793    Nat.O))))))))
794    (Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
795      Nat.O)))))))) p) suffix).Types.fst
796
797(** val eq_opt :
798    ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
799    Bool.bool **)
800let eq_opt eq m n =
801  match m with
802  | Types.None ->
803    (match m with
804     | Types.None -> Bool.True
805     | Types.Some x -> Bool.False)
806  | Types.Some a ->
807    (match n with
808     | Types.None -> Bool.False
809     | Types.Some b -> eq a b)
810
811(** val be_op2 :
812    ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
813    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
814let be_op2 carry op a1 a2 =
815  match op with
816  | Add ->
817    (match a1 with
818     | ByteValues.BVundef ->
819       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
820         List.Nil))
821     | ByteValues.BVnonzero ->
822       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
823         List.Nil))
824     | ByteValues.BVXor (x, x0, x1) ->
825       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
826         List.Nil))
827     | ByteValues.BVByte b1 ->
828       be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
829     | ByteValues.BVnull x ->
830       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
831         List.Nil))
832     | ByteValues.BVptr (ptr1, p1) ->
833       (match a2 with
834        | ByteValues.BVundef ->
835          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
836            List.Nil))
837        | ByteValues.BVnonzero ->
838          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
839            List.Nil))
840        | ByteValues.BVXor (x, x0, x1) ->
841          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
842            List.Nil))
843        | ByteValues.BVByte b2 ->
844          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
845        | ByteValues.BVnull x ->
846          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
847            List.Nil))
848        | ByteValues.BVptr (x, x0) ->
849          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
850            List.Nil))
851        | ByteValues.BVpc (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  | Addc ->
858    (match a1 with
859     | ByteValues.BVundef ->
860       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
861         List.Nil))
862     | ByteValues.BVnonzero ->
863       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
864         List.Nil))
865     | ByteValues.BVXor (x, x0, x1) ->
866       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
867         List.Nil))
868     | ByteValues.BVByte b1 -> be_add_sub_byte Bool.True carry a2 b1
869     | ByteValues.BVnull x ->
870       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
871         List.Nil))
872     | ByteValues.BVptr (ptr1, p1) ->
873       (match a2 with
874        | ByteValues.BVundef ->
875          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
876            List.Nil))
877        | ByteValues.BVnonzero ->
878          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
879            List.Nil))
880        | ByteValues.BVXor (x, x0, x1) ->
881          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
882            List.Nil))
883        | ByteValues.BVByte b2 -> be_add_sub_byte Bool.True carry a1 b2
884        | ByteValues.BVnull x ->
885          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
886            List.Nil))
887        | ByteValues.BVptr (x, x0) ->
888          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
889            List.Nil))
890        | ByteValues.BVpc (x, x0) ->
891          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
892            List.Nil)))
893     | ByteValues.BVpc (x, x0) ->
894       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
895         List.Nil)))
896  | Sub ->
897    (match a1 with
898     | ByteValues.BVundef ->
899       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
900         List.Nil))
901     | ByteValues.BVnonzero ->
902       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
903         List.Nil))
904     | ByteValues.BVXor (x, x0, x1) ->
905       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
906         List.Nil))
907     | ByteValues.BVByte b1 -> be_add_sub_byte Bool.False carry a2 b1
908     | ByteValues.BVnull x ->
909       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
910         List.Nil))
911     | ByteValues.BVptr (ptr1, p1) ->
912       (match a2 with
913        | ByteValues.BVundef ->
914          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
915            List.Nil))
916        | ByteValues.BVnonzero ->
917          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
918            List.Nil))
919        | ByteValues.BVXor (x, x0, x1) ->
920          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
921            List.Nil))
922        | ByteValues.BVByte b2 -> be_add_sub_byte Bool.False carry a1 b2
923        | ByteValues.BVnull x ->
924          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
925            List.Nil))
926        | ByteValues.BVptr (ptr2, p2) ->
927          (match Pointers.ptype ptr1 with
928           | AST.XData ->
929             (match Bool.andb
930                      (Pointers.eq_block ptr1.Pointers.pblock
931                        ptr2.Pointers.pblock)
932                      (Nat.eqb (ByteValues.part_no p1)
933                        (ByteValues.part_no p2)) with
934              | Bool.True ->
935                Obj.magic
936                  (Monad.m_bind0 (Monad.max_def Errors.res0)
937                    (Obj.magic
938                      (ByteValues.bit_of_val ErrorMessages.UnsupportedOp
939                        carry)) (fun carry0 ->
940                    let by1 =
941                      byte_at AST.size_pointer
942                        (Pointers.offv ptr1.Pointers.poff)
943                        (ByteValues.part_no p1)
944                    in
945                    let by2 =
946                      byte_at AST.size_pointer
947                        (Pointers.offv ptr2.Pointers.poff)
948                        (ByteValues.part_no p1)
949                    in
950                    let { Types.fst = result; Types.snd = carry1 } =
951                      eval0.op3 carry0 Sub by1 by2
952                    in
953                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
954                      (ByteValues.BVByte result); Types.snd =
955                      (ByteValues.BBbit carry1) }))
956              | Bool.False ->
957                Errors.Error (List.Cons ((Errors.MSG
958                  ErrorMessages.UnsupportedOp), List.Nil)))
959           | AST.Code ->
960             Errors.Error (List.Cons ((Errors.MSG
961               ErrorMessages.UnsupportedOp), List.Nil)))
962        | ByteValues.BVpc (x, x0) ->
963          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
964            List.Nil)))
965     | ByteValues.BVpc (x, x0) ->
966       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
967         List.Nil)))
968  | And ->
969    Obj.magic
970      (Monad.m_bind0 (Monad.max_def Errors.res0)
971        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a1))
972        (fun b1 ->
973        Monad.m_bind0 (Monad.max_def Errors.res0)
974          (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp a2))
975          (fun b2 ->
976          let res = (eval0.op3 Bool.False And b1 b2).Types.fst in
977          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
978            (ByteValues.BVByte res); Types.snd = carry })))
979  | Or ->
980    (match a1 with
981     | ByteValues.BVundef ->
982       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
983         List.Nil))
984     | ByteValues.BVnonzero ->
985       (match a2 with
986        | ByteValues.BVundef ->
987          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
988            List.Nil))
989        | ByteValues.BVnonzero ->
990          Obj.magic
991            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
992              ByteValues.BVnonzero; Types.snd = carry })
993        | ByteValues.BVXor (x, x0, x1) ->
994          Obj.magic
995            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
996              ByteValues.BVnonzero; Types.snd = carry })
997        | ByteValues.BVByte x ->
998          Obj.magic
999            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1000              ByteValues.BVnonzero; Types.snd = carry })
1001        | ByteValues.BVnull x ->
1002          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1003            List.Nil))
1004        | ByteValues.BVptr (x, x0) ->
1005          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1006            List.Nil))
1007        | ByteValues.BVpc (x, x0) ->
1008          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1009            List.Nil)))
1010     | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
1011       (match a2 with
1012        | ByteValues.BVundef ->
1013          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1014            List.Nil))
1015        | ByteValues.BVnonzero ->
1016          Obj.magic
1017            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1018              ByteValues.BVnonzero; Types.snd = carry })
1019        | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
1020          (match Bool.orb
1021                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
1022                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
1023                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
1024                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
1025           | Bool.True ->
1026             let eq_at = fun p ptr1 ptr2 ->
1027               Bool.andb
1028                 (Pointers.eq_block ptr1.Pointers.pblock
1029                   ptr2.Pointers.pblock)
1030                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1031                   (Nat.S (Nat.S Nat.O))))))))
1032                   (byte_at AST.size_pointer
1033                     (Pointers.offv ptr1.Pointers.poff)
1034                     (ByteValues.part_no p))
1035                   (byte_at AST.size_pointer
1036                     (Pointers.offv ptr2.Pointers.poff)
1037                     (ByteValues.part_no p)))
1038             in
1039             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
1040                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
1041              | Bool.True ->
1042                Obj.magic
1043                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1044                    (ByteValues.BVByte
1045                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1046                      (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
1047              | Bool.False ->
1048                Obj.magic
1049                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1050                    ByteValues.BVnonzero; Types.snd = carry }))
1051           | Bool.False ->
1052             Errors.Error (List.Cons ((Errors.MSG
1053               ErrorMessages.UnsupportedOp), List.Nil)))
1054        | ByteValues.BVByte x ->
1055          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1056            List.Nil))
1057        | ByteValues.BVnull x ->
1058          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1059            List.Nil))
1060        | ByteValues.BVptr (x, x0) ->
1061          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1062            List.Nil))
1063        | ByteValues.BVpc (x, x0) ->
1064          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1065            List.Nil)))
1066     | ByteValues.BVByte b1 ->
1067       (match a2 with
1068        | ByteValues.BVundef ->
1069          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1070            List.Nil))
1071        | ByteValues.BVnonzero ->
1072          Obj.magic
1073            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1074              ByteValues.BVnonzero; Types.snd = carry })
1075        | ByteValues.BVXor (x, x0, x1) ->
1076          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1077            List.Nil))
1078        | ByteValues.BVByte b2 ->
1079          let res = (eval0.op3 Bool.False Or b1 b2).Types.fst in
1080          Obj.magic
1081            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1082              (ByteValues.BVByte res); Types.snd = carry })
1083        | ByteValues.BVnull x ->
1084          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1085            List.Nil))
1086        | ByteValues.BVptr (x, x0) ->
1087          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1088            List.Nil))
1089        | ByteValues.BVpc (x, x0) ->
1090          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1091            List.Nil)))
1092     | ByteValues.BVnull x ->
1093       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1094         List.Nil))
1095     | ByteValues.BVptr (x, x0) ->
1096       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1097         List.Nil))
1098     | ByteValues.BVpc (x, x0) ->
1099       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1100         List.Nil)))
1101  | Xor ->
1102    (match a1 with
1103     | ByteValues.BVundef ->
1104       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1105         List.Nil))
1106     | ByteValues.BVnonzero ->
1107       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1108         List.Nil))
1109     | ByteValues.BVXor (x, x0, x1) ->
1110       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1111         List.Nil))
1112     | ByteValues.BVByte b1 ->
1113       (match a2 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 b2 ->
1124          let res = (eval0.op3 Bool.False Xor b1 b2).Types.fst in
1125          Obj.magic
1126            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1127              (ByteValues.BVByte res); Types.snd = carry })
1128        | ByteValues.BVnull x ->
1129          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1130            List.Nil))
1131        | ByteValues.BVptr (x, x0) ->
1132          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1133            List.Nil))
1134        | ByteValues.BVpc (x, x0) ->
1135          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1136            List.Nil)))
1137     | ByteValues.BVnull p1 ->
1138       (match a2 with
1139        | ByteValues.BVundef ->
1140          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1141            List.Nil))
1142        | ByteValues.BVnonzero ->
1143          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1144            List.Nil))
1145        | ByteValues.BVXor (x, x0, x1) ->
1146          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1147            List.Nil))
1148        | ByteValues.BVByte x ->
1149          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1150            List.Nil))
1151        | ByteValues.BVnull p2 ->
1152          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1153           | Bool.True ->
1154             Obj.magic
1155               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1156                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
1157                 carry })
1158           | Bool.False ->
1159             Errors.Error (List.Cons ((Errors.MSG
1160               ErrorMessages.UnsupportedOp), List.Nil)))
1161        | ByteValues.BVptr (ptr2, p2) ->
1162          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1163           | Bool.True ->
1164             Obj.magic
1165               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1166                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
1167                 Types.snd = carry })
1168           | Bool.False ->
1169             Errors.Error (List.Cons ((Errors.MSG
1170               ErrorMessages.UnsupportedOp), List.Nil)))
1171        | ByteValues.BVpc (x, x0) ->
1172          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1173            List.Nil)))
1174     | ByteValues.BVptr (ptr1, p1) ->
1175       (match a2 with
1176        | ByteValues.BVundef ->
1177          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1178            List.Nil))
1179        | ByteValues.BVnonzero ->
1180          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1181            List.Nil))
1182        | ByteValues.BVXor (x, x0, x1) ->
1183          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1184            List.Nil))
1185        | ByteValues.BVByte x ->
1186          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1187            List.Nil))
1188        | ByteValues.BVnull p2 ->
1189          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1190           | Bool.True ->
1191             Obj.magic
1192               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1193                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
1194                 Types.snd = carry })
1195           | Bool.False ->
1196             Errors.Error (List.Cons ((Errors.MSG
1197               ErrorMessages.UnsupportedOp), List.Nil)))
1198        | ByteValues.BVptr (ptr2, p2) ->
1199          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
1200           | Bool.True ->
1201             Obj.magic
1202               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1203                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
1204                 p1)); Types.snd = carry })
1205           | Bool.False ->
1206             Errors.Error (List.Cons ((Errors.MSG
1207               ErrorMessages.UnsupportedOp), List.Nil)))
1208        | ByteValues.BVpc (x, x0) ->
1209          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1210            List.Nil)))
1211     | ByteValues.BVpc (x, x0) ->
1212       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1213         List.Nil)))
1214
Note: See TracBrowser for help on using the repository browser.