source: extracted/backEndOps.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 46.1 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 Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
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_18831 =
405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18831 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_18833 =
414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18833 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_18835 =
423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18835 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_18837 =
432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18837 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_18839 =
441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18839 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_18841 =
450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18841 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 op4 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 op4 with
534   | Mul ->
535     let prod0 =
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 = prod0.Types.snd; Types.snd = prod0.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 op4 by =
558  match op4 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 op4 by1 by2 =
575  match op4 with
576  | Add ->
577    let { Types.fst = res1; Types.snd = flags } =
578      Arithmetic.add_8_with_carry by1 by2 Bool.False
579    in
580    { Types.fst = res1; Types.snd =
581    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
582  | Addc ->
583    let { Types.fst = res1; Types.snd = flags } =
584      Arithmetic.add_8_with_carry by1 by2 carry
585    in
586    { Types.fst = res1; Types.snd =
587    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
588  | Sub ->
589    let { Types.fst = res1; Types.snd = flags } =
590      Arithmetic.sub_8_with_carry by1 by2 carry
591    in
592    { Types.fst = res1; 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 op4 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 op4 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 op4 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 op4 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 op4 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 op4 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 op4 =
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' op4 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 op4 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.append0 (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 op4 (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.append0 (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 eq0 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 -> eq0 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 op4 a1 a2 =
815  match a1 with
816  | ByteValues.BVundef ->
817    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
818      List.Nil))
819  | ByteValues.BVnonzero ->
820    (match a2 with
821     | ByteValues.BVundef ->
822       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
823         List.Nil))
824     | ByteValues.BVnonzero ->
825       (match op4 with
826        | Add ->
827          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
828            List.Nil))
829        | Addc ->
830          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
831            List.Nil))
832        | Sub ->
833          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
834            List.Nil))
835        | And ->
836          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
837            List.Nil))
838        | Or ->
839          Obj.magic
840            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
841              ByteValues.BVnonzero; Types.snd = carry })
842        | Xor ->
843          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
844            List.Nil)))
845     | ByteValues.BVXor (x, x0, x1) ->
846       (match op4 with
847        | Add ->
848          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
849            List.Nil))
850        | Addc ->
851          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
852            List.Nil))
853        | Sub ->
854          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
855            List.Nil))
856        | And ->
857          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
858            List.Nil))
859        | Or ->
860          Obj.magic
861            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
862              ByteValues.BVnonzero; Types.snd = carry })
863        | Xor ->
864          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
865            List.Nil)))
866     | ByteValues.BVByte x ->
867       (match op4 with
868        | Add ->
869          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
870            List.Nil))
871        | Addc ->
872          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
873            List.Nil))
874        | Sub ->
875          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
876            List.Nil))
877        | And ->
878          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
879            List.Nil))
880        | Or ->
881          Obj.magic
882            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
883              ByteValues.BVnonzero; Types.snd = carry })
884        | Xor ->
885          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
886            List.Nil)))
887     | ByteValues.BVnull x ->
888       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
889         List.Nil))
890     | ByteValues.BVptr (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  | ByteValues.BVXor (ptr1_opt, ptr1_opt', p3) ->
897    (match a2 with
898     | ByteValues.BVundef ->
899       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
900         List.Nil))
901     | ByteValues.BVnonzero ->
902       (match op4 with
903        | Add ->
904          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
905            List.Nil))
906        | Addc ->
907          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
908            List.Nil))
909        | Sub ->
910          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
911            List.Nil))
912        | And ->
913          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
914            List.Nil))
915        | Or ->
916          Obj.magic
917            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
918              ByteValues.BVnonzero; Types.snd = carry })
919        | Xor ->
920          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
921            List.Nil)))
922     | ByteValues.BVXor (ptr2_opt, ptr2_opt', p4) ->
923       (match op4 with
924        | Add ->
925          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
926            List.Nil))
927        | Addc ->
928          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
929            List.Nil))
930        | Sub ->
931          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
932            List.Nil))
933        | And ->
934          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
935            List.Nil))
936        | Or ->
937          (match Bool.orb
938                   (Bool.andb (Nat.eqb (ByteValues.part_no p3) Nat.O)
939                     (Nat.eqb (ByteValues.part_no p4) (Nat.S Nat.O)))
940                   (Bool.andb (Nat.eqb (ByteValues.part_no p3) (Nat.S Nat.O))
941                     (Nat.eqb (ByteValues.part_no p4) Nat.O)) with
942           | Bool.True ->
943             let eq_at = fun p ptr1 ptr2 ->
944               Bool.andb
945                 (Pointers.eq_block ptr1.Pointers.pblock
946                   ptr2.Pointers.pblock)
947                 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
948                   (Nat.S (Nat.S Nat.O))))))))
949                   (byte_at AST.size_pointer
950                     (Pointers.offv ptr1.Pointers.poff)
951                     (ByteValues.part_no p))
952                   (byte_at AST.size_pointer
953                     (Pointers.offv ptr2.Pointers.poff)
954                     (ByteValues.part_no p)))
955             in
956             (match Bool.andb (eq_opt (eq_at p3) ptr1_opt ptr1_opt')
957                      (eq_opt (eq_at p4) ptr2_opt ptr2_opt') with
958              | Bool.True ->
959                Obj.magic
960                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
961                    (ByteValues.BVByte
962                    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
963                      (Nat.S (Nat.S Nat.O)))))))))); Types.snd = carry })
964              | Bool.False ->
965                Obj.magic
966                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
967                    ByteValues.BVnonzero; Types.snd = carry }))
968           | Bool.False ->
969             Errors.Error (List.Cons ((Errors.MSG
970               ErrorMessages.UnsupportedOp), List.Nil)))
971        | Xor ->
972          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
973            List.Nil)))
974     | ByteValues.BVByte b2 ->
975       (match op4 with
976        | Add ->
977          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
978            List.Nil))
979        | Addc ->
980          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
981            List.Nil))
982        | Sub ->
983          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
984            List.Nil))
985        | And ->
986          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
987            List.Nil))
988        | Or ->
989          (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
990                   (Nat.S (Nat.S Nat.O))))))))
991                   (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
992                     (Nat.S (Nat.S Nat.O))))))))) b2 with
993           | Bool.True ->
994             Obj.magic
995               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = a1;
996                 Types.snd = carry })
997           | Bool.False ->
998             Errors.Error (List.Cons ((Errors.MSG
999               ErrorMessages.UnsupportedOp), List.Nil)))
1000        | Xor ->
1001          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1002            List.Nil)))
1003     | ByteValues.BVnull x ->
1004       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1005         List.Nil))
1006     | ByteValues.BVptr (x, x0) ->
1007       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1008         List.Nil))
1009     | ByteValues.BVpc (x, x0) ->
1010       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1011         List.Nil)))
1012  | ByteValues.BVByte b1 ->
1013    (match a2 with
1014     | ByteValues.BVundef ->
1015       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1016         List.Nil))
1017     | ByteValues.BVnonzero ->
1018       (match op4 with
1019        | Add ->
1020          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1021            List.Nil))
1022        | Addc ->
1023          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1024            List.Nil))
1025        | Sub ->
1026          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1027            List.Nil))
1028        | And ->
1029          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1030            List.Nil))
1031        | Or ->
1032          Obj.magic
1033            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1034              ByteValues.BVnonzero; Types.snd = carry })
1035        | Xor ->
1036          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1037            List.Nil)))
1038     | ByteValues.BVXor (x, x0, x1) ->
1039       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1040         List.Nil))
1041     | ByteValues.BVByte b2 ->
1042       Obj.magic
1043         (Monad.m_bind0 (Monad.max_def Errors.res0)
1044           (Obj.magic
1045             (ByteValues.bit_of_val ErrorMessages.UnsupportedOp carry))
1046           (fun carry0 ->
1047           let { Types.fst = result; Types.snd = carry1 } =
1048             eval0.op3 carry0 op4 b1 b2
1049           in
1050           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1051             (ByteValues.BVByte result); Types.snd = (ByteValues.BBbit
1052             carry1) }))
1053     | ByteValues.BVnull x ->
1054       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1055         List.Nil))
1056     | ByteValues.BVptr (x, x0) ->
1057       (match op4 with
1058        | Add ->
1059          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
1060        | Addc -> be_add_sub_byte Bool.True carry a2 b1
1061        | Sub ->
1062          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1063            List.Nil))
1064        | And ->
1065          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1066            List.Nil))
1067        | Or ->
1068          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1069            List.Nil))
1070        | Xor ->
1071          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1072            List.Nil)))
1073     | ByteValues.BVpc (x, x0) ->
1074       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1075         List.Nil)))
1076  | ByteValues.BVnull p3 ->
1077    (match a2 with
1078     | ByteValues.BVundef ->
1079       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1080         List.Nil))
1081     | ByteValues.BVnonzero ->
1082       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1083         List.Nil))
1084     | ByteValues.BVXor (x, x0, x1) ->
1085       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1086         List.Nil))
1087     | ByteValues.BVByte x ->
1088       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1089         List.Nil))
1090     | ByteValues.BVnull p4 ->
1091       (match op4 with
1092        | Add ->
1093          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1094            List.Nil))
1095        | Addc ->
1096          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1097            List.Nil))
1098        | Sub ->
1099          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1100            List.Nil))
1101        | And ->
1102          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1103            List.Nil))
1104        | Or ->
1105          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1106            List.Nil))
1107        | Xor ->
1108          (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
1109           | Bool.True ->
1110             Obj.magic
1111               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1112                 (ByteValues.BVXor (Types.None, Types.None, p3)); Types.snd =
1113                 carry })
1114           | Bool.False ->
1115             Errors.Error (List.Cons ((Errors.MSG
1116               ErrorMessages.UnsupportedOp), List.Nil))))
1117     | ByteValues.BVptr (ptr2, p4) ->
1118       (match op4 with
1119        | Add ->
1120          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1121            List.Nil))
1122        | Addc ->
1123          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1124            List.Nil))
1125        | Sub ->
1126          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1127            List.Nil))
1128        | And ->
1129          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1130            List.Nil))
1131        | Or ->
1132          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1133            List.Nil))
1134        | Xor ->
1135          (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
1136           | Bool.True ->
1137             Obj.magic
1138               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1139                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p3));
1140                 Types.snd = carry })
1141           | Bool.False ->
1142             Errors.Error (List.Cons ((Errors.MSG
1143               ErrorMessages.UnsupportedOp), List.Nil))))
1144     | ByteValues.BVpc (x, x0) ->
1145       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1146         List.Nil)))
1147  | ByteValues.BVptr (ptr1, p3) ->
1148    (match a2 with
1149     | ByteValues.BVundef ->
1150       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1151         List.Nil))
1152     | ByteValues.BVnonzero ->
1153       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1154         List.Nil))
1155     | ByteValues.BVXor (x, x0, x1) ->
1156       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1157         List.Nil))
1158     | ByteValues.BVByte b2 ->
1159       (match op4 with
1160        | Add ->
1161          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
1162        | Addc -> be_add_sub_byte Bool.True carry a1 b2
1163        | Sub -> be_add_sub_byte Bool.False carry a1 b2
1164        | And ->
1165          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1166            List.Nil))
1167        | Or ->
1168          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1169            List.Nil))
1170        | Xor ->
1171          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1172            List.Nil)))
1173     | ByteValues.BVnull p4 ->
1174       (match op4 with
1175        | Add ->
1176          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1177            List.Nil))
1178        | Addc ->
1179          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1180            List.Nil))
1181        | Sub ->
1182          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1183            List.Nil))
1184        | And ->
1185          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1186            List.Nil))
1187        | Or ->
1188          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1189            List.Nil))
1190        | Xor ->
1191          (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
1192           | Bool.True ->
1193             Obj.magic
1194               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1195                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p3));
1196                 Types.snd = carry })
1197           | Bool.False ->
1198             Errors.Error (List.Cons ((Errors.MSG
1199               ErrorMessages.UnsupportedOp), List.Nil))))
1200     | ByteValues.BVptr (ptr2, p4) ->
1201       (match op4 with
1202        | Add ->
1203          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1204            List.Nil))
1205        | Addc ->
1206          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1207            List.Nil))
1208        | Sub ->
1209          (match Pointers.ptype ptr1 with
1210           | AST.XData ->
1211             (match Bool.andb
1212                      (Pointers.eq_block ptr1.Pointers.pblock
1213                        ptr2.Pointers.pblock)
1214                      (Nat.eqb (ByteValues.part_no p3)
1215                        (ByteValues.part_no p4)) with
1216              | Bool.True ->
1217                Obj.magic
1218                  (Monad.m_bind0 (Monad.max_def Errors.res0)
1219                    (Obj.magic
1220                      (ByteValues.bit_of_val ErrorMessages.UnsupportedOp
1221                        carry)) (fun carry0 ->
1222                    let by1 =
1223                      byte_at AST.size_pointer
1224                        (Pointers.offv ptr1.Pointers.poff)
1225                        (ByteValues.part_no p3)
1226                    in
1227                    let by2 =
1228                      byte_at AST.size_pointer
1229                        (Pointers.offv ptr2.Pointers.poff)
1230                        (ByteValues.part_no p3)
1231                    in
1232                    let { Types.fst = result; Types.snd = carry1 } =
1233                      eval0.op3 carry0 Sub by1 by2
1234                    in
1235                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1236                      (ByteValues.BVByte result); Types.snd =
1237                      (ByteValues.BBbit carry1) }))
1238              | Bool.False ->
1239                Errors.Error (List.Cons ((Errors.MSG
1240                  ErrorMessages.UnsupportedOp), List.Nil)))
1241           | AST.Code ->
1242             Errors.Error (List.Cons ((Errors.MSG
1243               ErrorMessages.UnsupportedOp), List.Nil)))
1244        | And ->
1245          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1246            List.Nil))
1247        | Or ->
1248          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1249            List.Nil))
1250        | Xor ->
1251          (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
1252           | Bool.True ->
1253             Obj.magic
1254               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1255                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
1256                 p3)); Types.snd = carry })
1257           | Bool.False ->
1258             Errors.Error (List.Cons ((Errors.MSG
1259               ErrorMessages.UnsupportedOp), List.Nil))))
1260     | ByteValues.BVpc (x, x0) ->
1261       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1262         List.Nil)))
1263  | ByteValues.BVpc (x, x0) ->
1264    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
1265      List.Nil))
1266
Note: See TracBrowser for help on using the repository browser.