source: extracted/arithmetic.ml @ 2649

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

...

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