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