source: driver/extracted/arithmetic.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 27.1 KB
Line 
1open Preamble
2
3open Setoids
4
5open Monad
6
7open Option
8
9open Extranat
10
11open Vector
12
13open Div_and_mod
14
15open Jmeq
16
17open Russell
18
19open Types
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Hints_declaration
30
31open Core_notation
32
33open Pts
34
35open Logic
36
37open Relations
38
39open Nat
40
41open BitVector
42
43open Exp
44
45(** val addr16_of_addr11 :
46    BitVector.word -> BitVector.word11 -> BitVector.word **)
47let addr16_of_addr11 pc a =
48  let { Types.fst = pc_upper; Types.snd = ignore } =
49    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
50      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
51      Nat.O)))))))) pc
52  in
53  let { Types.fst = n1; Types.snd = n2 } =
54    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
55      (Nat.S Nat.O)))) pc_upper
56  in
57  let { Types.fst = b123; Types.snd = b } =
58    Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
59      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) a
60  in
61  let b1 = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 Nat.O in
62  let b2 =
63    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S Nat.O)
64  in
65  let b3 =
66    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S (Nat.S
67      Nat.O))
68  in
69  let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
70  in
71  Vector.append
72    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
73      (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
74    (Nat.S Nat.O))))))))
75    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
76      (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), p5,
77      (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons ((Nat.S Nat.O),
78      b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
79
80(** val nat_of_bool : Bool.bool -> Nat.nat **)
81let nat_of_bool = function
82| Bool.True -> Nat.S Nat.O
83| Bool.False -> Nat.O
84
85(** val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
86let carry_of a b c =
87  match a with
88  | Bool.True -> Bool.orb b c
89  | Bool.False -> Bool.andb b c
90
91(** val add_with_carries :
92    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
93    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
94let add_with_carries n x y init_carry =
95  Vector.fold_right2_i (fun n0 b c r ->
96    let { Types.fst = lower_bits; Types.snd = carries } = r in
97    let last_carry =
98      match carries with
99      | Vector.VEmpty -> init_carry
100      | Vector.VCons (x0, cy, x1) -> cy
101    in
102    (match last_carry with
103     | Bool.True ->
104       let bit = Bool.xorb (Bool.xorb b c) Bool.True in
105       let carry = carry_of b c Bool.True in
106       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
107       (Vector.VCons (n0, carry, carries)) }
108     | Bool.False ->
109       let bit = Bool.xorb (Bool.xorb b c) Bool.False in
110       let carry = carry_of b c Bool.False in
111       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
112       (Vector.VCons (n0, carry, carries)) })) { Types.fst = Vector.VEmpty;
113    Types.snd = Vector.VEmpty } n x y
114
115(** val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
116let borrow_of a b c =
117  match a with
118  | Bool.True -> Bool.andb b c
119  | Bool.False -> Bool.orb b c
120
121(** val sub_with_borrows :
122    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
123    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
124let sub_with_borrows n x y init_borrow =
125  Vector.fold_right2_i (fun n0 b c r ->
126    let { Types.fst = lower_bits; Types.snd = borrows } = r in
127    let last_borrow =
128      match borrows with
129      | Vector.VEmpty -> init_borrow
130      | Vector.VCons (x0, bw, x1) -> bw
131    in
132    let bit = Bool.xorb (Bool.xorb b c) last_borrow in
133    let borrow = borrow_of b c last_borrow in
134    { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
135    (Vector.VCons (n0, borrow, borrows)) }) { Types.fst = Vector.VEmpty;
136    Types.snd = Vector.VEmpty } n x y
137
138(** val add_n_with_carry :
139    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
140    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
141let add_n_with_carry n b c carry =
142  let { Types.fst = result; Types.snd = carries } =
143    add_with_carries n b c carry
144  in
145  let cy_flag = Vector.get_index_v n carries Nat.O in
146  let ov_flag =
147    Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
148  in
149  let ac_flag =
150    Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
151  in
152  { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
153  cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
154  ov_flag, Vector.VEmpty)))))) }
155
156(** val sub_n_with_carry :
157    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
158    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
159let sub_n_with_carry n b c carry =
160  let { Types.fst = result; Types.snd = carries } =
161    sub_with_borrows n b c carry
162  in
163  let cy_flag = Vector.get_index_v n carries Nat.O in
164  let ov_flag =
165    Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
166  in
167  let ac_flag =
168    Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
169  in
170  { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
171  cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
172  ov_flag, Vector.VEmpty)))))) }
173
174(** val add_8_with_carry :
175    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
176    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
177let add_8_with_carry b c carry =
178  add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
179    Nat.O)))))))) b c carry
180
181(** val add_16_with_carry :
182    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
183    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
184let add_16_with_carry b c carry =
185  add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
187    Nat.O)))))))))))))))) b c carry
188
189(** val sub_7_with_carry :
190    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
191    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
192let sub_7_with_carry b c carry =
193  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
194    Nat.O))))))) b c carry
195
196(** val sub_8_with_carry :
197    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
198    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
199let sub_8_with_carry b c carry =
200  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
201    Nat.O)))))))) b c carry
202
203(** val sub_16_with_carry :
204    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
205    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
206let sub_16_with_carry b c carry =
207  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
208    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
209    Nat.O)))))))))))))))) b c carry
210
211(** val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
212let increment n b =
213  (add_with_carries n b (BitVector.zero n) Bool.True).Types.fst
214
215(** val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
216let decrement n b =
217  (sub_with_borrows n b (BitVector.zero n) Bool.True).Types.fst
218
219(** val bitvector_of_nat_aux :
220    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
221let rec bitvector_of_nat_aux n m v =
222  match m with
223  | Nat.O -> v
224  | Nat.S m' -> bitvector_of_nat_aux n m' (increment n v)
225
226(** val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector **)
227let bitvector_of_nat n m =
228  bitvector_of_nat_aux n m (BitVector.zero n)
229
230(** val nat_of_bitvector_aux :
231    Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat **)
232let rec nat_of_bitvector_aux n m = function
233| Vector.VEmpty -> m
234| Vector.VCons (n', hd, tl) ->
235  nat_of_bitvector_aux n'
236    (match hd with
237     | Bool.True ->
238       Nat.plus (Nat.times (Nat.S (Nat.S Nat.O)) m) (Nat.S Nat.O)
239     | Bool.False -> Nat.times (Nat.S (Nat.S Nat.O)) m) tl
240
241(** val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat **)
242let nat_of_bitvector n v =
243  nat_of_bitvector_aux n Nat.O v
244
245(** val two_complement_negation :
246    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
247let two_complement_negation n b =
248  let new_b = BitVector.negation_bv n b in increment n new_b
249
250(** val addition_n :
251    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
252    BitVector.bitVector **)
253let addition_n n b c =
254  (add_with_carries n b c Bool.False).Types.fst
255
256(** val subtraction :
257    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
258    BitVector.bitVector **)
259let subtraction n b c =
260  addition_n n b (two_complement_negation n c)
261
262(** val mult_aux :
263    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
264    BitVector.bitVector -> BitVector.bitVector **)
265let rec mult_aux m n b c acc =
266  match b with
267  | Vector.VEmpty -> acc
268  | Vector.VCons (m', hd, tl) ->
269    let acc' =
270      match hd with
271      | Bool.True -> addition_n (Nat.S n) c acc
272      | Bool.False -> acc
273    in
274    mult_aux m' n tl (Vector.shift_right_1 n c Bool.False) acc'
275
276(** val multiplication :
277    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
278    BitVector.bitVector **)
279let multiplication = function
280| Nat.O -> (fun x x0 -> Vector.VEmpty)
281| Nat.S m ->
282  (fun b c ->
283    let c' = BitVector.pad (Nat.S m) (Nat.S m) c in
284    mult_aux (Nat.S m) (Nat.plus m (Nat.S m)) b
285      (Vector.shift_left (Nat.plus (Nat.S m) (Nat.S m)) m c' Bool.False)
286      (BitVector.zero (Nat.S (Nat.plus m (Nat.S m)))))
287
288(** val short_multiplication :
289    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
290    BitVector.bitVector **)
291let short_multiplication n x y =
292  (Vector.vsplit n n (multiplication n x y)).Types.snd
293
294type fbs_diff =
295| Fbs_diff' of Nat.nat * Nat.nat
296
297(** val fbs_diff_rect_Type4 :
298    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
299let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
300| Fbs_diff' (n, m) -> h_fbs_diff' n m
301
302(** val fbs_diff_rect_Type5 :
303    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
304let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
305| Fbs_diff' (n, m) -> h_fbs_diff' n m
306
307(** val fbs_diff_rect_Type3 :
308    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
309let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
310| Fbs_diff' (n, m) -> h_fbs_diff' n m
311
312(** val fbs_diff_rect_Type2 :
313    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
314let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
315| Fbs_diff' (n, m) -> h_fbs_diff' n m
316
317(** val fbs_diff_rect_Type1 :
318    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
319let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
320| Fbs_diff' (n, m) -> h_fbs_diff' n m
321
322(** val fbs_diff_rect_Type0 :
323    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
324let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
325| Fbs_diff' (n, m) -> h_fbs_diff' n m
326
327(** val fbs_diff_inv_rect_Type4 :
328    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
329let fbs_diff_inv_rect_Type4 x1 hterm h1 =
330  let hcut = fbs_diff_rect_Type4 h1 x1 hterm in hcut __ __
331
332(** val fbs_diff_inv_rect_Type3 :
333    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
334let fbs_diff_inv_rect_Type3 x1 hterm h1 =
335  let hcut = fbs_diff_rect_Type3 h1 x1 hterm in hcut __ __
336
337(** val fbs_diff_inv_rect_Type2 :
338    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
339let fbs_diff_inv_rect_Type2 x1 hterm h1 =
340  let hcut = fbs_diff_rect_Type2 h1 x1 hterm in hcut __ __
341
342(** val fbs_diff_inv_rect_Type1 :
343    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
344let fbs_diff_inv_rect_Type1 x1 hterm h1 =
345  let hcut = fbs_diff_rect_Type1 h1 x1 hterm in hcut __ __
346
347(** val fbs_diff_inv_rect_Type0 :
348    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
349let fbs_diff_inv_rect_Type0 x1 hterm h1 =
350  let hcut = fbs_diff_rect_Type0 h1 x1 hterm in hcut __ __
351
352(** val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
353let fbs_diff_discr a1 x y =
354  Logic.eq_rect_Type2 x
355    (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y
356
357(** val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
358let fbs_diff_jmdiscr a1 x y =
359  Logic.eq_rect_Type2 x
360    (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y
361
362(** val first_bit_set :
363    Nat.nat -> BitVector.bitVector -> fbs_diff Types.option **)
364let rec first_bit_set n = function
365| Vector.VEmpty -> Types.None
366| Vector.VCons (m, h, t) ->
367  (match h with
368   | Bool.True -> Types.Some (Fbs_diff' (Nat.O, m))
369   | Bool.False ->
370     (match first_bit_set m t with
371      | Types.None -> Types.None
372      | Types.Some o ->
373        let Fbs_diff' (x, y) = o in Types.Some (Fbs_diff' ((Nat.S x), y))))
374
375(** val divmod_u_aux :
376    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
377    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
378let rec divmod_u_aux n m q d =
379  match m with
380  | Nat.O -> { Types.fst = Vector.VEmpty; Types.snd = q }
381  | Nat.S m' ->
382    let { Types.fst = q'; Types.snd = flags } =
383      add_with_carries (Nat.S n) q (two_complement_negation (Nat.S n) d)
384        Bool.False
385    in
386    let bit = Vector.head' n flags in
387    let q'' =
388      match bit with
389      | Bool.True -> q'
390      | Bool.False -> q
391    in
392    let { Types.fst = tl; Types.snd = md } =
393      divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
394    in
395    { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }
396
397(** val divmod_u :
398    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
399    (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option **)
400let divmod_u n b c =
401  match first_bit_set (Nat.S n) c with
402  | Types.None -> Types.None
403  | Types.Some fbs' ->
404    let Fbs_diff' (fbs, m) = fbs' in
405    let { Types.fst = d; Types.snd = m0 } =
406      divmod_u_aux n (Nat.S fbs) b
407        (Vector.shift_left (Nat.S n) fbs c Bool.False)
408    in
409    Types.Some { Types.fst =
410    (Vector.switch_bv_plus m (Nat.S fbs) (BitVector.pad m (Nat.S fbs) d));
411    Types.snd = m0 }
412
413(** val division_u :
414    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
415    BitVector.bitVector Types.option **)
416let division_u n q d =
417  match divmod_u n q d with
418  | Types.None -> Types.None
419  | Types.Some p -> Types.Some p.Types.fst
420
421(** val division_s :
422    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
423    BitVector.bitVector Types.option **)
424let division_s = function
425| Nat.O -> (fun b c -> Types.None)
426| Nat.S p ->
427  (fun b c ->
428    let b_sign_bit = Vector.get_index_v (Nat.S p) b Nat.O in
429    let c_sign_bit = Vector.get_index_v (Nat.S p) c Nat.O in
430    (match b_sign_bit with
431     | Bool.True ->
432       let neg_b = two_complement_negation (Nat.S p) b in
433       (match c_sign_bit with
434        | Bool.True ->
435          division_u p neg_b (two_complement_negation (Nat.S p) c)
436        | Bool.False ->
437          (match division_u p neg_b c with
438           | Types.None -> Types.None
439           | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r)))
440     | Bool.False ->
441       (match c_sign_bit with
442        | Bool.True ->
443          (match division_u p b (two_complement_negation (Nat.S p) c) with
444           | Types.None -> Types.None
445           | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r))
446        | Bool.False -> division_u p b c)))
447
448(** val modulus_u :
449    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
450    BitVector.bitVector Types.option **)
451let modulus_u n q d =
452  match divmod_u n q d with
453  | Types.None -> Types.None
454  | Types.Some p -> Types.Some p.Types.snd
455
456(** val modulus_s :
457    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
458    BitVector.bitVector Types.option **)
459let modulus_s n b c =
460  match division_s n b c with
461  | Types.None -> Types.None
462  | Types.Some result ->
463    let { Types.fst = high_bits; Types.snd = low_bits } =
464      Vector.vsplit n n (multiplication n result c)
465    in
466    Types.Some (subtraction n b low_bits)
467
468(** val lt_u :
469    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
470    Bool.bool **)
471let lt_u =
472  Vector.fold_right2_i (fun x a b r ->
473    match a with
474    | Bool.True -> Bool.andb b r
475    | Bool.False -> Bool.orb b r) Bool.False
476
477(** val gt_u :
478    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
479    Bool.bool **)
480let gt_u n b c =
481  lt_u n c b
482
483(** val lte_u :
484    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
485    Bool.bool **)
486let lte_u n b c =
487  Bool.notb (gt_u n b c)
488
489(** val gte_u :
490    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
491    Bool.bool **)
492let gte_u n b c =
493  Bool.notb (lt_u n b c)
494
495(** val lt_s :
496    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
497let lt_s n b c =
498  let { Types.fst = result; Types.snd = borrows } =
499    sub_with_borrows n b c Bool.False
500  in
501  (match borrows with
502   | Vector.VEmpty -> Bool.False
503   | Vector.VCons (x, bwn, tl) ->
504     (match tl with
505      | Vector.VEmpty -> Bool.False
506      | Vector.VCons (x0, bwpn, x1) ->
507        (match Bool.xorb bwn bwpn with
508         | Bool.True ->
509           (match result with
510            | Vector.VEmpty -> Bool.False
511            | Vector.VCons (x2, b7, x3) -> b7)
512         | Bool.False ->
513           (match result with
514            | Vector.VEmpty -> Bool.False
515            | Vector.VCons (x2, b7, x3) -> b7))))
516
517(** val gt_s :
518    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
519let gt_s n b c =
520  lt_s n c b
521
522(** val lte_s :
523    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
524let lte_s n b c =
525  Bool.notb (gt_s n b c)
526
527(** val gte_s :
528    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
529let gte_s n b c =
530  Bool.notb (lt_s n b c)
531
532type ternary =
533| Zero_carry
534| One_carry
535| Two_carry
536
537(** val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
538let rec ternary_rect_Type4 h_Zero_carry h_One_carry h_Two_carry = function
539| Zero_carry -> h_Zero_carry
540| One_carry -> h_One_carry
541| Two_carry -> h_Two_carry
542
543(** val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
544let rec ternary_rect_Type5 h_Zero_carry h_One_carry h_Two_carry = function
545| Zero_carry -> h_Zero_carry
546| One_carry -> h_One_carry
547| Two_carry -> h_Two_carry
548
549(** val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
550let rec ternary_rect_Type3 h_Zero_carry h_One_carry h_Two_carry = function
551| Zero_carry -> h_Zero_carry
552| One_carry -> h_One_carry
553| Two_carry -> h_Two_carry
554
555(** val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
556let rec ternary_rect_Type2 h_Zero_carry h_One_carry h_Two_carry = function
557| Zero_carry -> h_Zero_carry
558| One_carry -> h_One_carry
559| Two_carry -> h_Two_carry
560
561(** val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
562let rec ternary_rect_Type1 h_Zero_carry h_One_carry h_Two_carry = function
563| Zero_carry -> h_Zero_carry
564| One_carry -> h_One_carry
565| Two_carry -> h_Two_carry
566
567(** val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
568let rec ternary_rect_Type0 h_Zero_carry h_One_carry h_Two_carry = function
569| Zero_carry -> h_Zero_carry
570| One_carry -> h_One_carry
571| Two_carry -> h_Two_carry
572
573(** val ternary_inv_rect_Type4 :
574    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
575let ternary_inv_rect_Type4 hterm h1 h2 h3 =
576  let hcut = ternary_rect_Type4 h1 h2 h3 hterm in hcut __
577
578(** val ternary_inv_rect_Type3 :
579    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
580let ternary_inv_rect_Type3 hterm h1 h2 h3 =
581  let hcut = ternary_rect_Type3 h1 h2 h3 hterm in hcut __
582
583(** val ternary_inv_rect_Type2 :
584    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
585let ternary_inv_rect_Type2 hterm h1 h2 h3 =
586  let hcut = ternary_rect_Type2 h1 h2 h3 hterm in hcut __
587
588(** val ternary_inv_rect_Type1 :
589    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
590let ternary_inv_rect_Type1 hterm h1 h2 h3 =
591  let hcut = ternary_rect_Type1 h1 h2 h3 hterm in hcut __
592
593(** val ternary_inv_rect_Type0 :
594    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
595let ternary_inv_rect_Type0 hterm h1 h2 h3 =
596  let hcut = ternary_rect_Type0 h1 h2 h3 hterm in hcut __
597
598(** val ternary_discr : ternary -> ternary -> __ **)
599let ternary_discr x y =
600  Logic.eq_rect_Type2 x
601    (match x with
602     | Zero_carry -> Obj.magic (fun _ dH -> dH)
603     | One_carry -> Obj.magic (fun _ dH -> dH)
604     | Two_carry -> Obj.magic (fun _ dH -> dH)) y
605
606(** val ternary_jmdiscr : ternary -> ternary -> __ **)
607let ternary_jmdiscr x y =
608  Logic.eq_rect_Type2 x
609    (match x with
610     | Zero_carry -> Obj.magic (fun _ dH -> dH)
611     | One_carry -> Obj.magic (fun _ dH -> dH)
612     | Two_carry -> Obj.magic (fun _ dH -> dH)) y
613
614(** val carry_0 : ternary -> (Bool.bool, ternary) Types.prod **)
615let carry_0 = function
616| Zero_carry -> { Types.fst = Bool.False; Types.snd = Zero_carry }
617| One_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
618| Two_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
619
620(** val carry_1 : ternary -> (Bool.bool, ternary) Types.prod **)
621let carry_1 = function
622| Zero_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
623| One_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
624| Two_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
625
626(** val carry_2 : ternary -> (Bool.bool, ternary) Types.prod **)
627let carry_2 = function
628| Zero_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
629| One_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
630| Two_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }
631
632(** val carry_3 : ternary -> (Bool.bool, ternary) Types.prod **)
633let carry_3 = function
634| Zero_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
635| One_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }
636| Two_carry -> { Types.fst = Bool.True; Types.snd = Two_carry }
637
638(** val ternary_carry_of :
639    Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
640    Types.prod **)
641let ternary_carry_of xa xb xc carry =
642  match xa with
643  | Bool.True ->
644    (match xb with
645     | Bool.True ->
646       (match xc with
647        | Bool.True -> carry_3 carry
648        | Bool.False -> carry_2 carry)
649     | Bool.False ->
650       (match xc with
651        | Bool.True -> carry_2 carry
652        | Bool.False -> carry_1 carry))
653  | Bool.False ->
654    (match xb with
655     | Bool.True ->
656       (match xc with
657        | Bool.True -> carry_2 carry
658        | Bool.False -> carry_1 carry)
659     | Bool.False ->
660       (match xc with
661        | Bool.True -> carry_1 carry
662        | Bool.False -> carry_0 carry))
663
664(** val canonical_add :
665    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
666    BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary)
667    Types.prod **)
668let rec canonical_add n a b c init =
669  (match a with
670   | Vector.VEmpty ->
671     (fun x x0 -> { Types.fst = Vector.VEmpty; Types.snd = init })
672   | Vector.VCons (sz', xa, tla) ->
673     (fun b' c' ->
674       let xb = Vector.head' sz' b' in
675       let xc = Vector.head' sz' c' in
676       let tlb = Vector.tail sz' b' in
677       let tlc = Vector.tail sz' c' in
678       let { Types.fst = bits; Types.snd = last } =
679         canonical_add sz' tla tlb tlc init
680       in
681       let { Types.fst = bit; Types.snd = carry } =
682         ternary_carry_of xa xb xc last
683       in
684       { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
685    c
686
687(** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
688let carries_to_ternary carry1 carry2 =
689  match carry1 with
690  | Bool.True ->
691    (match carry2 with
692     | Bool.True -> Two_carry
693     | Bool.False -> One_carry)
694  | Bool.False ->
695    (match carry2 with
696     | Bool.True -> One_carry
697     | Bool.False -> Zero_carry)
698
699(** val max_u :
700    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
701    Bool.bool Vector.vector **)
702let max_u n a b =
703  match lt_u n a b with
704  | Bool.True -> b
705  | Bool.False -> a
706
707(** val min_u :
708    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
709    Bool.bool Vector.vector **)
710let min_u n a b =
711  match lt_u n a b with
712  | Bool.True -> a
713  | Bool.False -> b
714
715(** val max_s :
716    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
717    BitVector.bitVector **)
718let max_s n a b =
719  match lt_s n a b with
720  | Bool.True -> b
721  | Bool.False -> a
722
723(** val min_s :
724    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
725    BitVector.bitVector **)
726let min_s n a b =
727  match lt_s n a b with
728  | Bool.True -> a
729  | Bool.False -> b
730
731(** val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector **)
732let bitvector_of_bool n b =
733  BitVector.pad n (Nat.S Nat.O) (Vector.VCons (Nat.O, b, Vector.VEmpty))
734
735(** val full_add :
736    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
737    (BitVector.bit, BitVector.bitVector) Types.prod **)
738let full_add n b c d =
739  Vector.fold_right2_i (fun n0 b1 b2 d0 ->
740    let { Types.fst = c1; Types.snd = r } = d0 in
741    { Types.fst =
742    (Bool.orb (Bool.andb b1 b2) (Bool.andb c1 (Bool.orb b1 b2))); Types.snd =
743    (Vector.VCons (n0, (Bool.xorb (Bool.xorb b1 b2) c1), r)) }) { Types.fst =
744    d; Types.snd = Vector.VEmpty } n b c
745
746(** val half_add :
747    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
748    BitVector.bitVector) Types.prod **)
749let half_add n b c =
750  full_add n b c Bool.False
751
752(** val add :
753    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
754    BitVector.bitVector **)
755let add n l r =
756  (half_add n l r).Types.snd
757
758(** val sign_extension : BitVector.byte -> BitVector.word **)
759let sign_extension c =
760  let b =
761    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
762      (Nat.S Nat.O)))))))) c Nat.O
763  in
764  Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
765    Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
766    Nat.O)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
767    (Nat.S Nat.O))))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
768    (Nat.S Nat.O)))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
769    Nat.O))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), b,
770    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), b, (Vector.VCons ((Nat.S
771    (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S Nat.O), b, (Vector.VCons (Nat.O,
772    b, Vector.VEmpty)))))))))))))))) c
773
774(** val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool **)
775let sign_bit n = function
776| Vector.VEmpty -> Bool.False
777| Vector.VCons (x, h, x0) -> h
778
779(** val sign_extend :
780    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
781let sign_extend m n v =
782  Vector.pad_vector (sign_bit m v) n m v
783
784(** val zero_ext :
785    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
786let zero_ext m n =
787  match Extranat.nat_compare m n with
788  | Extranat.Nat_lt (m', n') ->
789    (fun v ->
790      Vector.switch_bv_plus (Nat.S n') m' (BitVector.pad (Nat.S n') m' v))
791  | Extranat.Nat_eq n' -> (fun v -> v)
792  | Extranat.Nat_gt (m', n') ->
793    (fun v ->
794      (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)
795
796(** val sign_ext :
797    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
798let sign_ext m n =
799  match Extranat.nat_compare m n with
800  | Extranat.Nat_lt (m', n') ->
801    (fun v ->
802      Vector.switch_bv_plus (Nat.S n') m' (sign_extend m' (Nat.S n') v))
803  | Extranat.Nat_eq n' -> (fun v -> v)
804  | Extranat.Nat_gt (m', n') ->
805    (fun v ->
806      (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)
807
Note: See TracBrowser for help on using the repository browser.