open Preamble

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open Types

open List

open Util

open FoldStuff

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open BitVector

open Exp

(** val addr16_of_addr11 :
    BitVector.word -> BitVector.word11 -> BitVector.word **)
let addr16_of_addr11 pc a =
  let { Types.fst = pc_upper; Types.snd = ignore } =
    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))) pc
  in
  let { Types.fst = n1; Types.snd = n2 } =
    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O)))) pc_upper
  in
  let { Types.fst = b123; Types.snd = b } =
    Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) a
  in
  let b1 = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 Nat.O in
  let b2 =
    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S Nat.O)
  in
  let b3 =
    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) b123 (Nat.S (Nat.S
      Nat.O))
  in
  let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
  in
  Vector.append
    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O))))))))
    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), p5,
      (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons ((Nat.S Nat.O),
      b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b

(** val nat_of_bool : Bool.bool -> Nat.nat **)
let nat_of_bool = function
| Bool.True -> Nat.S Nat.O
| Bool.False -> Nat.O

(** val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
let carry_of a b c =
  match a with
  | Bool.True -> Bool.orb b c
  | Bool.False -> Bool.andb b c

(** val add_with_carries :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let add_with_carries n x y init_carry =
  Vector.fold_right2_i (fun n0 b c r ->
    let { Types.fst = lower_bits; Types.snd = carries } = r in
    let last_carry =
      match carries with
      | Vector.VEmpty -> init_carry
      | Vector.VCons (x0, cy, x1) -> cy
    in
    (match last_carry with
     | Bool.True ->
       let bit = Bool.xorb (Bool.xorb b c) Bool.True in
       let carry = carry_of b c Bool.True in
       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
       (Vector.VCons (n0, carry, carries)) }
     | Bool.False ->
       let bit = Bool.xorb (Bool.xorb b c) Bool.False in
       let carry = carry_of b c Bool.False in
       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
       (Vector.VCons (n0, carry, carries)) })) { Types.fst = Vector.VEmpty;
    Types.snd = Vector.VEmpty } n x y

(** val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool **)
let borrow_of a b c =
  match a with
  | Bool.True -> Bool.andb b c
  | Bool.False -> Bool.orb b c

(** val sub_with_borrows :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let sub_with_borrows n x y init_borrow =
  Vector.fold_right2_i (fun n0 b c r ->
    let { Types.fst = lower_bits; Types.snd = borrows } = r in
    let last_borrow =
      match borrows with
      | Vector.VEmpty -> init_borrow
      | Vector.VCons (x0, bw, x1) -> bw
    in
    let bit = Bool.xorb (Bool.xorb b c) last_borrow in
    let borrow = borrow_of b c last_borrow in
    { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    (Vector.VCons (n0, borrow, borrows)) }) { Types.fst = Vector.VEmpty;
    Types.snd = Vector.VEmpty } n x y

(** val add_n_with_carry :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let add_n_with_carry n b c carry =
  let { Types.fst = result; Types.snd = carries } =
    add_with_carries n b c carry
  in
  let cy_flag = Vector.get_index_v n carries Nat.O in
  let ov_flag =
    Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
  in
  let ac_flag =
    Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
  in
  { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
  cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
  ov_flag, Vector.VEmpty)))))) }

(** val sub_n_with_carry :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let sub_n_with_carry n b c carry =
  let { Types.fst = result; Types.snd = carries } =
    sub_with_borrows n b c carry
  in
  let cy_flag = Vector.get_index_v n carries Nat.O in
  let ov_flag =
    Bool.xorb cy_flag (Vector.get_index_v n carries (Nat.S Nat.O))
  in
  let ac_flag =
    Vector.get_index_v n carries (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
  in
  { Types.fst = result; Types.snd = (Vector.VCons ((Nat.S (Nat.S Nat.O)),
  cy_flag, (Vector.VCons ((Nat.S Nat.O), ac_flag, (Vector.VCons (Nat.O,
  ov_flag, Vector.VEmpty)))))) }

(** val add_8_with_carry :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let add_8_with_carry b c carry =
  add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) b c carry

(** val add_16_with_carry :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let add_16_with_carry b c carry =
  add_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))))))))))) b c carry

(** val sub_7_with_carry :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let sub_7_with_carry b c carry =
  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))))) b c carry

(** val sub_8_with_carry :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let sub_8_with_carry b c carry =
  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) b c carry

(** val sub_16_with_carry :
    BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let sub_16_with_carry b c carry =
  sub_n_with_carry (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))))))))))) b c carry

(** val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let increment n b =
  (add_with_carries n b (BitVector.zero n) Bool.True).Types.fst

(** val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let decrement n b =
  (sub_with_borrows n b (BitVector.zero n) Bool.True).Types.fst

(** val bitvector_of_nat_aux :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let rec bitvector_of_nat_aux n m v =
  match m with
  | Nat.O -> v
  | Nat.S m' -> bitvector_of_nat_aux n m' (increment n v)

(** val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector **)
let bitvector_of_nat n m =
  bitvector_of_nat_aux n m (BitVector.zero n)

(** val nat_of_bitvector_aux :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat **)
let rec nat_of_bitvector_aux n m = function
| Vector.VEmpty -> m
| Vector.VCons (n', hd, tl) ->
  nat_of_bitvector_aux n'
    (match hd with
     | Bool.True ->
       Nat.plus (Nat.times (Nat.S (Nat.S Nat.O)) m) (Nat.S Nat.O)
     | Bool.False -> Nat.times (Nat.S (Nat.S Nat.O)) m) tl

(** val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat **)
let nat_of_bitvector n v =
  nat_of_bitvector_aux n Nat.O v

(** val two_complement_negation :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let two_complement_negation n b =
  let new_b = BitVector.negation_bv n b in increment n new_b

(** val addition_n :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let addition_n n b c =
  (add_with_carries n b c Bool.False).Types.fst

(** val subtraction :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let subtraction n b c =
  addition_n n b (two_complement_negation n c)

(** val mult_aux :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector -> BitVector.bitVector **)
let rec mult_aux m n b c acc =
  match b with
  | Vector.VEmpty -> acc
  | Vector.VCons (m', hd, tl) ->
    let acc' =
      match hd with
      | Bool.True -> addition_n (Nat.S n) c acc
      | Bool.False -> acc
    in
    mult_aux m' n tl (Vector.shift_right_1 n c Bool.False) acc'

(** val multiplication :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let multiplication = function
| Nat.O -> (fun x x0 -> Vector.VEmpty)
| Nat.S m ->
  (fun b c ->
    let c' = BitVector.pad (Nat.S m) (Nat.S m) c in
    mult_aux (Nat.S m) (Nat.plus m (Nat.S m)) b
      (Vector.shift_left (Nat.plus (Nat.S m) (Nat.S m)) m c' Bool.False)
      (BitVector.zero (Nat.S (Nat.plus m (Nat.S m)))))

(** val short_multiplication :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let short_multiplication n x y =
  (Vector.vsplit n n (multiplication n x y)).Types.snd

type fbs_diff =
| Fbs_diff' of Nat.nat * Nat.nat

(** val fbs_diff_rect_Type4 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_rect_Type5 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_rect_Type3 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_rect_Type2 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_rect_Type1 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_rect_Type0 :
    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
| Fbs_diff' (n, m) -> h_fbs_diff' n m

(** val fbs_diff_inv_rect_Type4 :
    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let fbs_diff_inv_rect_Type4 x1 hterm h1 =
  let hcut = fbs_diff_rect_Type4 h1 x1 hterm in hcut __ __

(** val fbs_diff_inv_rect_Type3 :
    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let fbs_diff_inv_rect_Type3 x1 hterm h1 =
  let hcut = fbs_diff_rect_Type3 h1 x1 hterm in hcut __ __

(** val fbs_diff_inv_rect_Type2 :
    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let fbs_diff_inv_rect_Type2 x1 hterm h1 =
  let hcut = fbs_diff_rect_Type2 h1 x1 hterm in hcut __ __

(** val fbs_diff_inv_rect_Type1 :
    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let fbs_diff_inv_rect_Type1 x1 hterm h1 =
  let hcut = fbs_diff_rect_Type1 h1 x1 hterm in hcut __ __

(** val fbs_diff_inv_rect_Type0 :
    Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let fbs_diff_inv_rect_Type0 x1 hterm h1 =
  let hcut = fbs_diff_rect_Type0 h1 x1 hterm in hcut __ __

(** val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
let fbs_diff_discr a1 x y =
  Logic.eq_rect_Type2 x
    (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __ **)
let fbs_diff_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let Fbs_diff' (a0, a10) = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val first_bit_set :
    Nat.nat -> BitVector.bitVector -> fbs_diff Types.option **)
let rec first_bit_set n = function
| Vector.VEmpty -> Types.None
| Vector.VCons (m, h, t) ->
  (match h with
   | Bool.True -> Types.Some (Fbs_diff' (Nat.O, m))
   | Bool.False ->
     (match first_bit_set m t with
      | Types.None -> Types.None
      | Types.Some o ->
        let Fbs_diff' (x, y) = o in Types.Some (Fbs_diff' ((Nat.S x), y))))

(** val divmod_u_aux :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod **)
let rec divmod_u_aux n m q d =
  match m with
  | Nat.O -> { Types.fst = Vector.VEmpty; Types.snd = q }
  | Nat.S m' ->
    let { Types.fst = q'; Types.snd = flags } =
      add_with_carries (Nat.S n) q (two_complement_negation (Nat.S n) d)
        Bool.False
    in
    let bit = Vector.head' n flags in
    let q'' =
      match bit with
      | Bool.True -> q'
      | Bool.False -> q
    in
    let { Types.fst = tl; Types.snd = md } =
      divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
    in
    { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }

(** val divmod_u :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option **)
let divmod_u n b c =
  match first_bit_set (Nat.S n) c with
  | Types.None -> Types.None
  | Types.Some fbs' ->
    let Fbs_diff' (fbs, m) = fbs' in
    let { Types.fst = d; Types.snd = m0 } =
      divmod_u_aux n (Nat.S fbs) b
        (Vector.shift_left (Nat.S n) fbs c Bool.False)
    in
    Types.Some { Types.fst =
    (Vector.switch_bv_plus m (Nat.S fbs) (BitVector.pad m (Nat.S fbs) d));
    Types.snd = m0 }

(** val division_u :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector Types.option **)
let division_u n q d =
  match divmod_u n q d with
  | Types.None -> Types.None
  | Types.Some p -> Types.Some p.Types.fst

(** val division_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector Types.option **)
let division_s = function
| Nat.O -> (fun b c -> Types.None)
| Nat.S p ->
  (fun b c ->
    let b_sign_bit = Vector.get_index_v (Nat.S p) b Nat.O in
    let c_sign_bit = Vector.get_index_v (Nat.S p) c Nat.O in
    (match b_sign_bit with
     | Bool.True ->
       let neg_b = two_complement_negation (Nat.S p) b in
       (match c_sign_bit with
        | Bool.True ->
          division_u p neg_b (two_complement_negation (Nat.S p) c)
        | Bool.False ->
          (match division_u p neg_b c with
           | Types.None -> Types.None
           | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r)))
     | Bool.False ->
       (match c_sign_bit with
        | Bool.True ->
          (match division_u p b (two_complement_negation (Nat.S p) c) with
           | Types.None -> Types.None
           | Types.Some r -> Types.Some (two_complement_negation (Nat.S p) r))
        | Bool.False -> division_u p b c)))

(** val modulus_u :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector Types.option **)
let modulus_u n q d =
  match divmod_u n q d with
  | Types.None -> Types.None
  | Types.Some p -> Types.Some p.Types.snd

(** val modulus_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector Types.option **)
let modulus_s n b c =
  match division_s n b c with
  | Types.None -> Types.None
  | Types.Some result ->
    let { Types.fst = high_bits; Types.snd = low_bits } =
      Vector.vsplit n n (multiplication n result c)
    in
    Types.Some (subtraction n b low_bits)

(** val lt_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool **)
let lt_u =
  Vector.fold_right2_i (fun x a b r ->
    match a with
    | Bool.True -> Bool.andb b r
    | Bool.False -> Bool.orb b r) Bool.False

(** val gt_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool **)
let gt_u n b c =
  lt_u n c b

(** val lte_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool **)
let lte_u n b c =
  Bool.notb (gt_u n b c)

(** val gte_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool **)
let gte_u n b c =
  Bool.notb (lt_u n b c)

(** val lt_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
let lt_s n b c =
  let { Types.fst = result; Types.snd = borrows } =
    sub_with_borrows n b c Bool.False
  in
  (match borrows with
   | Vector.VEmpty -> Bool.False
   | Vector.VCons (x, bwn, tl) ->
     (match tl with
      | Vector.VEmpty -> Bool.False
      | Vector.VCons (x0, bwpn, x1) ->
        (match Bool.xorb bwn bwpn with
         | Bool.True ->
           (match result with
            | Vector.VEmpty -> Bool.False
            | Vector.VCons (x2, b7, x3) -> b7)
         | Bool.False ->
           (match result with
            | Vector.VEmpty -> Bool.False
            | Vector.VCons (x2, b7, x3) -> b7))))

(** val gt_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
let gt_s n b c =
  lt_s n c b

(** val lte_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
let lte_s n b c =
  Bool.notb (gt_s n b c)

(** val gte_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool **)
let gte_s n b c =
  Bool.notb (lt_s n b c)

type ternary =
| Zero_carry
| One_carry
| Two_carry

(** val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type4 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type5 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type3 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type2 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type1 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1 **)
let rec ternary_rect_Type0 h_Zero_carry h_One_carry h_Two_carry = function
| Zero_carry -> h_Zero_carry
| One_carry -> h_One_carry
| Two_carry -> h_Two_carry

(** val ternary_inv_rect_Type4 :
    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let ternary_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = ternary_rect_Type4 h1 h2 h3 hterm in hcut __

(** val ternary_inv_rect_Type3 :
    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let ternary_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = ternary_rect_Type3 h1 h2 h3 hterm in hcut __

(** val ternary_inv_rect_Type2 :
    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let ternary_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = ternary_rect_Type2 h1 h2 h3 hterm in hcut __

(** val ternary_inv_rect_Type1 :
    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let ternary_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = ternary_rect_Type1 h1 h2 h3 hterm in hcut __

(** val ternary_inv_rect_Type0 :
    ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let ternary_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = ternary_rect_Type0 h1 h2 h3 hterm in hcut __

(** val ternary_discr : ternary -> ternary -> __ **)
let ternary_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Zero_carry -> Obj.magic (fun _ dH -> dH)
     | One_carry -> Obj.magic (fun _ dH -> dH)
     | Two_carry -> Obj.magic (fun _ dH -> dH)) y

(** val ternary_jmdiscr : ternary -> ternary -> __ **)
let ternary_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Zero_carry -> Obj.magic (fun _ dH -> dH)
     | One_carry -> Obj.magic (fun _ dH -> dH)
     | Two_carry -> Obj.magic (fun _ dH -> dH)) y

(** val carry_0 : ternary -> (Bool.bool, ternary) Types.prod **)
let carry_0 = function
| Zero_carry -> { Types.fst = Bool.False; Types.snd = Zero_carry }
| One_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
| Two_carry -> { Types.fst = Bool.False; Types.snd = One_carry }

(** val carry_1 : ternary -> (Bool.bool, ternary) Types.prod **)
let carry_1 = function
| Zero_carry -> { Types.fst = Bool.True; Types.snd = Zero_carry }
| One_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
| Two_carry -> { Types.fst = Bool.True; Types.snd = One_carry }

(** val carry_2 : ternary -> (Bool.bool, ternary) Types.prod **)
let carry_2 = function
| Zero_carry -> { Types.fst = Bool.False; Types.snd = One_carry }
| One_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
| Two_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }

(** val carry_3 : ternary -> (Bool.bool, ternary) Types.prod **)
let carry_3 = function
| Zero_carry -> { Types.fst = Bool.True; Types.snd = One_carry }
| One_carry -> { Types.fst = Bool.False; Types.snd = Two_carry }
| Two_carry -> { Types.fst = Bool.True; Types.snd = Two_carry }

(** val ternary_carry_of :
    Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
    Types.prod **)
let ternary_carry_of xa xb xc carry =
  match xa with
  | Bool.True ->
    (match xb with
     | Bool.True ->
       (match xc with
        | Bool.True -> carry_3 carry
        | Bool.False -> carry_2 carry)
     | Bool.False ->
       (match xc with
        | Bool.True -> carry_2 carry
        | Bool.False -> carry_1 carry))
  | Bool.False ->
    (match xb with
     | Bool.True ->
       (match xc with
        | Bool.True -> carry_2 carry
        | Bool.False -> carry_1 carry)
     | Bool.False ->
       (match xc with
        | Bool.True -> carry_1 carry
        | Bool.False -> carry_0 carry))

(** val canonical_add :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary)
    Types.prod **)
let rec canonical_add n a b c init =
  (match a with
   | Vector.VEmpty ->
     (fun x x0 -> { Types.fst = Vector.VEmpty; Types.snd = init })
   | Vector.VCons (sz', xa, tla) ->
     (fun b' c' ->
       let xb = Vector.head' sz' b' in
       let xc = Vector.head' sz' c' in
       let tlb = Vector.tail sz' b' in
       let tlc = Vector.tail sz' c' in
       let { Types.fst = bits; Types.snd = last } =
         canonical_add sz' tla tlb tlc init
       in
       let { Types.fst = bit; Types.snd = carry } =
         ternary_carry_of xa xb xc last
       in
       { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
    c

(** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
let carries_to_ternary carry1 carry2 =
  match carry1 with
  | Bool.True ->
    (match carry2 with
     | Bool.True -> Two_carry
     | Bool.False -> One_carry)
  | Bool.False ->
    (match carry2 with
     | Bool.True -> One_carry
     | Bool.False -> Zero_carry)

(** val max_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool Vector.vector **)
let max_u n a b =
  match lt_u n a b with
  | Bool.True -> b
  | Bool.False -> a

(** val min_u :
    Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector ->
    Bool.bool Vector.vector **)
let min_u n a b =
  match lt_u n a b with
  | Bool.True -> a
  | Bool.False -> b

(** val max_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let max_s n a b =
  match lt_s n a b with
  | Bool.True -> b
  | Bool.False -> a

(** val min_s :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let min_s n a b =
  match lt_s n a b with
  | Bool.True -> a
  | Bool.False -> b

(** val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector **)
let bitvector_of_bool n b =
  BitVector.pad n (Nat.S Nat.O) (Vector.VCons (Nat.O, b, Vector.VEmpty))

(** val full_add :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
    (BitVector.bit, BitVector.bitVector) Types.prod **)
let full_add n b c d =
  Vector.fold_right2_i (fun n0 b1 b2 d0 ->
    let { Types.fst = c1; Types.snd = r } = d0 in
    { Types.fst =
    (Bool.orb (Bool.andb b1 b2) (Bool.andb c1 (Bool.orb b1 b2))); Types.snd =
    (Vector.VCons (n0, (Bool.xorb (Bool.xorb b1 b2) c1), r)) }) { Types.fst =
    d; Types.snd = Vector.VEmpty } n b c

(** val half_add :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
    BitVector.bitVector) Types.prod **)
let half_add n b c =
  full_add n b c Bool.False

(** val add :
    Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
    BitVector.bitVector **)
let add n l r =
  (half_add n l r).Types.snd

(** val sign_extension : BitVector.byte -> BitVector.word **)
let sign_extension c =
  let b =
    Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S Nat.O)))))))) c Nat.O
  in
  Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O))))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O)))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O))))), b, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), b,
    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), b, (Vector.VCons ((Nat.S
    (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S Nat.O), b, (Vector.VCons (Nat.O,
    b, Vector.VEmpty)))))))))))))))) c

(** val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool **)
let sign_bit n = function
| Vector.VEmpty -> Bool.False
| Vector.VCons (x, h, x0) -> h

(** val sign_extend :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let sign_extend m n v =
  Vector.pad_vector (sign_bit m v) n m v

(** val zero_ext :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let zero_ext m n =
  match Extranat.nat_compare m n with
  | Extranat.Nat_lt (m', n') ->
    (fun v ->
      Vector.switch_bv_plus (Nat.S n') m' (BitVector.pad (Nat.S n') m' v))
  | Extranat.Nat_eq n' -> (fun v -> v)
  | Extranat.Nat_gt (m', n') ->
    (fun v ->
      (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)

(** val sign_ext :
    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
let sign_ext m n =
  match Extranat.nat_compare m n with
  | Extranat.Nat_lt (m', n') ->
    (fun v ->
      Vector.switch_bv_plus (Nat.S n') m' (sign_extend m' (Nat.S n') v))
  | Extranat.Nat_eq n' -> (fun v -> v)
  | Extranat.Nat_gt (m', n') ->
    (fun v ->
      (Vector.vsplit (Nat.S m') n' (Vector.switch_bv_plus n' (Nat.S m') v)).Types.snd)