source: extracted/backEndOps.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

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