29 open Hints_declaration
45 (** val addr16_of_addr11 :
46 BitVector.word -> BitVector.word11 -> BitVector.word **)
47 let 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
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
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
61 let b1 = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 Nat.O in
63 Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S Nat.O)
66 Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S (Nat.S
69 let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
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
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
80 (** val nat_of_bool : Bool.bool -> Nat.nat **)
81 let nat_of_bool = function
82 | Bool.True -> Nat.S Nat.O
85 (** val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
88 | Bool.True -> Bool.orb b c
89 | Bool.False -> Bool.andb b c
91 (** val add_with_carries :
92 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
93 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
94 let 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
99 | Vector.VEmpty -> init_carry
100 | Vector.VCons (x0, cy, x1) -> cy
102 (match last_carry with
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)) }
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
115 (** val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
116 let borrow_of a b c =
118 | Bool.True -> Bool.andb b c
119 | Bool.False -> Bool.orb b c
121 (** val sub_with_borrows :
122 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
123 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
124 let 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
129 | Vector.VEmpty -> init_borrow
130 | Vector.VCons (x0, bw, x1) -> bw
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
138 (** val add_n_with_carry :
139 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
140 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
141 let add_n_with_carry n b c carry =
142 let { Types.fst = result; Types.snd = carries } =
143 add_with_carries n b c carry
145 let cy_flag = Vector.get_index_v n carries Nat.O in
147 Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
150 Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
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)))))) }
156 (** val sub_n_with_carry :
157 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
158 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
159 let sub_n_with_carry n b c carry =
160 let { Types.fst = result; Types.snd = carries } =
161 sub_with_borrows n b c carry
163 let cy_flag = Vector.get_index_v n carries Nat.O in
165 Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
168 Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
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)))))) }
174 (** val add_8_with_carry :
175 BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
176 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
177 let 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
181 (** val add_16_with_carry :
182 BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
183 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
184 let 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
189 (** val sub_7_with_carry :
190 BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
191 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
192 let 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
196 (** val sub_8_with_carry :
197 BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
198 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
199 let 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
203 (** val sub_16_with_carry :
204 BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
205 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
206 let 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
211 (** val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
213 (add_with_carries n b (BitVector.zero n) Bool.True).Types.fst
215 (** val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
217 (sub_with_borrows n b (BitVector.zero n) Bool.True).Types.fst
219 (** val bitvector_of_nat_aux :
220 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
221 let rec bitvector_of_nat_aux n m v =
224 | Nat.S m' -> bitvector_of_nat_aux n m' (increment n v)
226 (** val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector **)
227 let bitvector_of_nat n m =
228 bitvector_of_nat_aux n m (BitVector.zero n)
230 (** val nat_of_bitvector_aux :
231 Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat **)
232 let rec nat_of_bitvector_aux n m = function
234 | Vector.VCons (n', hd, tl) ->
235 nat_of_bitvector_aux n'
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
241 (** val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat **)
242 let nat_of_bitvector n v =
243 nat_of_bitvector_aux n Nat.O v
245 (** val two_complement_negation :
246 Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
247 let two_complement_negation n b =
248 let new_b = BitVector.negation_bv n b in increment n new_b
251 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
252 BitVector.bitVector **)
253 let addition_n n b c =
254 (add_with_carries n b c Bool.False).Types.fst
256 (** val subtraction :
257 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
258 BitVector.bitVector **)
259 let subtraction n b c =
260 addition_n n b (two_complement_negation n c)
263 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
264 BitVector.bitVector -> BitVector.bitVector **)
265 let rec mult_aux m n b c acc =
267 | Vector.VEmpty -> acc
268 | Vector.VCons (m', hd, tl) ->
271 | Bool.True -> addition_n (Nat.S n) c acc
274 mult_aux m' n tl (Vector.shift_right_1 n c Bool.False) acc'
276 (** val multiplication :
277 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
278 BitVector.bitVector **)
279 let multiplication = function
280 | Nat.O -> (fun x x0 -> Vector.VEmpty)
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)))))
288 (** val short_multiplication :
289 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
290 BitVector.bitVector **)
291 let short_multiplication n x y =
292 (Vector.vsplit n n (multiplication n x y)).Types.snd
295 | Fbs_diff' of Nat.nat * Nat.nat
297 (** val fbs_diff_rect_Type4 :
298 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
300 | Fbs_diff' (n, m) -> h_fbs_diff' n m
302 (** val fbs_diff_rect_Type5 :
303 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
305 | Fbs_diff' (n, m) -> h_fbs_diff' n m
307 (** val fbs_diff_rect_Type3 :
308 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
310 | Fbs_diff' (n, m) -> h_fbs_diff' n m
312 (** val fbs_diff_rect_Type2 :
313 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
315 | Fbs_diff' (n, m) -> h_fbs_diff' n m
317 (** val fbs_diff_rect_Type1 :
318 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
320 | Fbs_diff' (n, m) -> h_fbs_diff' n m
322 (** val fbs_diff_rect_Type0 :
323 (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
325 | Fbs_diff' (n, m) -> h_fbs_diff' n m
327 (** val fbs_diff_inv_rect_Type4 :
328 Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
329 let fbs_diff_inv_rect_Type4 x1 hterm h1 =
330 let hcut = fbs_diff_rect_Type4 h1 x1 hterm in hcut __ __
332 (** val fbs_diff_inv_rect_Type3 :
333 Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
334 let fbs_diff_inv_rect_Type3 x1 hterm h1 =
335 let hcut = fbs_diff_rect_Type3 h1 x1 hterm in hcut __ __
337 (** val fbs_diff_inv_rect_Type2 :
338 Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
339 let fbs_diff_inv_rect_Type2 x1 hterm h1 =
340 let hcut = fbs_diff_rect_Type2 h1 x1 hterm in hcut __ __
342 (** val fbs_diff_inv_rect_Type1 :
343 Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
344 let fbs_diff_inv_rect_Type1 x1 hterm h1 =
345 let hcut = fbs_diff_rect_Type1 h1 x1 hterm in hcut __ __
347 (** val fbs_diff_inv_rect_Type0 :
348 Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
349 let fbs_diff_inv_rect_Type0 x1 hterm h1 =
350 let hcut = fbs_diff_rect_Type0 h1 x1 hterm in hcut __ __
352 (** val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
353 let 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
357 (** val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
358 let 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
362 (** val first_bit_set :
363 Nat.nat -> BitVector.bitVector -> fbs_diff Types.option **)
364 let rec first_bit_set n = function
365 | Vector.VEmpty -> Types.None
366 | Vector.VCons (m, h, t) ->
368 | Bool.True -> Types.Some (Fbs_diff' (Nat.O, m))
370 (match first_bit_set m t with
371 | Types.None -> Types.None
373 let Fbs_diff' (x, y) = o in Types.Some (Fbs_diff' ((Nat.S x), y))))
375 (** val divmod_u_aux :
376 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
377 (BitVector.bitVector, BitVector.bitVector) Types.prod **)
378 let rec divmod_u_aux n m q d =
380 | Nat.O -> { Types.fst = Vector.VEmpty; Types.snd = q }
382 let { Types.fst = q'; Types.snd = flags } =
383 add_with_carries (Nat.S n) q (two_complement_negation (Nat.S n) d)
386 let bit = Vector.head' n flags in
392 let { Types.fst = tl; Types.snd = md } =
393 divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
395 { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }
398 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
399 (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option **)
401 match first_bit_set (Nat.S n) c with
402 | Types.None -> Types.None
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)
409 Types.Some { Types.fst =
410 (Vector.switch_bv_plus m (Nat.S fbs) (BitVector.pad m (Nat.S fbs) d));
414 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
415 BitVector.bitVector Types.option **)
416 let 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
422 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
423 BitVector.bitVector Types.option **)
424 let division_s = function
425 | Nat.O -> (fun b c -> Types.None)
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
432 let neg_b = two_complement_negation (Nat.S p) b in
433 (match c_sign_bit with
435 division_u p neg_b (two_complement_negation (Nat.S p) c)
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)))
441 (match c_sign_bit with
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)))
449 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
450 BitVector.bitVector Types.option **)
451 let 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
457 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
458 BitVector.bitVector Types.option **)
459 let 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)
466 Types.Some (subtraction n b low_bits)
469 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
472 Vector.fold_right2_i (fun x a b r ->
474 | Bool.True -> Bool.andb b r
475 | Bool.False -> Bool.orb b r) Bool.False
478 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
484 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
487 Bool.notb (gt_u n b c)
490 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
493 Bool.notb (lt_u n b c)
496 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
498 let { Types.fst = result; Types.snd = borrows } =
499 sub_with_borrows n b c Bool.False
502 | Vector.VEmpty -> Bool.False
503 | Vector.VCons (x, bwn, tl) ->
505 | Vector.VEmpty -> Bool.False
506 | Vector.VCons (x0, bwpn, x1) ->
507 (match Bool.xorb bwn bwpn with
510 | Vector.VEmpty -> Bool.False
511 | Vector.VCons (x2, b7, x3) -> b7)
514 | Vector.VEmpty -> Bool.False
515 | Vector.VCons (x2, b7, x3) -> b7))))
518 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
523 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
525 Bool.notb (gt_s n b c)
528 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
530 Bool.notb (lt_s n b c)
537 (** val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
538 let 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
543 (** val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
544 let 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
549 (** val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
550 let 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
555 (** val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
556 let 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
561 (** val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
562 let 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
567 (** val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
568 let 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
573 (** val ternary_inv_rect_Type4 :
574 ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
575 let ternary_inv_rect_Type4 hterm h1 h2 h3 =
576 let hcut = ternary_rect_Type4 h1 h2 h3 hterm in hcut __
578 (** val ternary_inv_rect_Type3 :
579 ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
580 let ternary_inv_rect_Type3 hterm h1 h2 h3 =
581 let hcut = ternary_rect_Type3 h1 h2 h3 hterm in hcut __
583 (** val ternary_inv_rect_Type2 :
584 ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
585 let ternary_inv_rect_Type2 hterm h1 h2 h3 =
586 let hcut = ternary_rect_Type2 h1 h2 h3 hterm in hcut __
588 (** val ternary_inv_rect_Type1 :
589 ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
590 let ternary_inv_rect_Type1 hterm h1 h2 h3 =
591 let hcut = ternary_rect_Type1 h1 h2 h3 hterm in hcut __
593 (** val ternary_inv_rect_Type0 :
594 ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
595 let ternary_inv_rect_Type0 hterm h1 h2 h3 =
596 let hcut = ternary_rect_Type0 h1 h2 h3 hterm in hcut __
598 (** val ternary_discr : ternary -> ternary -> __ **)
599 let ternary_discr x y =
600 Logic.eq_rect_Type2 x
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
606 (** val ternary_jmdiscr : ternary -> ternary -> __ **)
607 let ternary_jmdiscr x y =
608 Logic.eq_rect_Type2 x
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
614 (** val carry_0 : ternary -> (Bool.bool, ternary) Types.prod **)
615 let 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 }
620 (** val carry_1 : ternary -> (Bool.bool, ternary) Types.prod **)
621 let 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 }
626 (** val carry_2 : ternary -> (Bool.bool, ternary) Types.prod **)
627 let 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 }
632 (** val carry_3 : ternary -> (Bool.bool, ternary) Types.prod **)
633 let 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 }
638 (** val ternary_carry_of :
639 Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
641 let ternary_carry_of xa xb xc carry =
647 | Bool.True -> carry_3 carry
648 | Bool.False -> carry_2 carry)
651 | Bool.True -> carry_2 carry
652 | Bool.False -> carry_1 carry))
657 | Bool.True -> carry_2 carry
658 | Bool.False -> carry_1 carry)
661 | Bool.True -> carry_1 carry
662 | Bool.False -> carry_0 carry))
664 (** val canonical_add :
665 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
666 BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary)
668 let rec canonical_add n a b c init =
671 (fun x x0 -> { Types.fst = Vector.VEmpty; Types.snd = init })
672 | Vector.VCons (sz', xa, tla) ->
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
681 let { Types.fst = bit; Types.snd = carry } =
682 ternary_carry_of xa xb xc last
684 { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
687 (** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
688 let carries_to_ternary carry1 carry2 =
692 | Bool.True -> Two_carry
693 | Bool.False -> One_carry)
696 | Bool.True -> One_carry
697 | Bool.False -> Zero_carry)
700 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
701 Bool.bool Vector.vector **)
703 match lt_u n a b with
708 Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
709 Bool.bool Vector.vector **)
711 match lt_u n a b with
716 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
717 BitVector.bitVector **)
719 match lt_s n a b with
724 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
725 BitVector.bitVector **)
727 match lt_s n a b with
731 (** val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector **)
732 let bitvector_of_bool n b =
733 BitVector.pad n (Nat.S Nat.O) (Vector.VCons (Nat.O, b, Vector.VEmpty))
736 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
737 (BitVector.bit, BitVector.bitVector) Types.prod **)
738 let 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
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
747 Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
748 BitVector.bitVector) Types.prod **)
750 full_add n b c Bool.False
753 Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
754 BitVector.bitVector **)
756 (half_add n l r).Types.snd
758 (** val sign_extension : BitVector.byte -> BitVector.word **)
759 let sign_extension c =
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
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
774 (** val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool **)
775 let sign_bit n = function
776 | Vector.VEmpty -> Bool.False
777 | Vector.VCons (x, h, x0) -> h
779 (** val sign_extend :
780 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
781 let sign_extend m n v =
782 Vector.pad_vector (sign_bit m v) n m v
785 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
787 match Extranat.nat_compare m n with
788 | Extranat.Nat_lt (m', n') ->
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') ->
794 (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)
797 Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
799 match Extranat.nat_compare m n with
800 | Extranat.Nat_lt (m', n') ->
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') ->
806 (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)