source: extracted/arithmetic.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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