open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open Hide

type cpointer = Pointers.pointer Types.sig0

type xpointer = Pointers.pointer Types.sig0

type program_counter = { pc_block : Pointers.block Types.sig0;
                         pc_offset : Positive.pos }

(** val program_counter_rect_Type4 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type4 h_mk_program_counter x_6152 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6152 in
  h_mk_program_counter pc_block0 pc_offset0

(** val program_counter_rect_Type5 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type5 h_mk_program_counter x_6154 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6154 in
  h_mk_program_counter pc_block0 pc_offset0

(** val program_counter_rect_Type3 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type3 h_mk_program_counter x_6156 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6156 in
  h_mk_program_counter pc_block0 pc_offset0

(** val program_counter_rect_Type2 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type2 h_mk_program_counter x_6158 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6158 in
  h_mk_program_counter pc_block0 pc_offset0

(** val program_counter_rect_Type1 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type1 h_mk_program_counter x_6160 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6160 in
  h_mk_program_counter pc_block0 pc_offset0

(** val program_counter_rect_Type0 :
    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    'a1 **)
let rec program_counter_rect_Type0 h_mk_program_counter x_6162 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6162 in
  h_mk_program_counter pc_block0 pc_offset0

(** val pc_block : program_counter -> Pointers.block Types.sig0 **)
let rec pc_block xxx =
  xxx.pc_block

(** val pc_offset : program_counter -> Positive.pos **)
let rec pc_offset xxx =
  xxx.pc_offset

(** val program_counter_inv_rect_Type4 :
    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
    'a1) -> 'a1 **)
let program_counter_inv_rect_Type4 hterm h1 =
  let hcut = program_counter_rect_Type4 h1 hterm in hcut __

(** val program_counter_inv_rect_Type3 :
    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
    'a1) -> 'a1 **)
let program_counter_inv_rect_Type3 hterm h1 =
  let hcut = program_counter_rect_Type3 h1 hterm in hcut __

(** val program_counter_inv_rect_Type2 :
    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
    'a1) -> 'a1 **)
let program_counter_inv_rect_Type2 hterm h1 =
  let hcut = program_counter_rect_Type2 h1 hterm in hcut __

(** val program_counter_inv_rect_Type1 :
    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
    'a1) -> 'a1 **)
let program_counter_inv_rect_Type1 hterm h1 =
  let hcut = program_counter_rect_Type1 h1 hterm in hcut __

(** val program_counter_inv_rect_Type0 :
    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
    'a1) -> 'a1 **)
let program_counter_inv_rect_Type0 hterm h1 =
  let hcut = program_counter_rect_Type0 h1 hterm in hcut __

(** val program_counter_discr : program_counter -> program_counter -> __ **)
let program_counter_discr x y =
  Logic.eq_rect_Type2 x
    (let { pc_block = a0; pc_offset = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val program_counter_jmdiscr :
    program_counter -> program_counter -> __ **)
let program_counter_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { pc_block = a0; pc_offset = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val eq_program_counter :
    program_counter -> program_counter -> Bool.bool **)
let eq_program_counter pc1 pc2 =
  Bool.andb
    (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
    (Positive.eqb pc1.pc_offset pc2.pc_offset)

(** val bitvector_from_pos :
    Nat.nat -> Positive.pos -> BitVector.bitVector **)
let bitvector_from_pos n p =
  BitVectorZ.bitvector_of_Z n (Z.zpred (Z.Pos p))

(** val pos_from_bitvector :
    Nat.nat -> BitVector.bitVector -> Positive.pos **)
let pos_from_bitvector n v =
  (match Z.zsucc (BitVectorZ.z_of_unsigned_bitvector n v) with
   | Z.OZ -> (fun _ -> assert false (* absurd case *))
   | Z.Pos x -> (fun _ -> x)
   | Z.Neg x -> (fun _ -> assert false (* absurd case *))) __

(** val cpointer_of_pc : program_counter -> cpointer Types.option **)
let cpointer_of_pc pc =
  let pc_off = pc.pc_offset in
  (match Positive.leb pc_off (Positive.two_power_nat Pointers.offset_size) with
   | Bool.True ->
     Obj.magic
       (Monad.m_return0 (Monad.max_def Option.option) { Pointers.pblock =
         (Types.pi1 pc.pc_block); Pointers.poff =
         (bitvector_from_pos Pointers.offset_size pc_off) })
   | Bool.False -> Types.None)

type part =
  Nat.nat
  (* singleton inductive, whose constructor was mk_part *)

(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type4 h_mk_part x_6178 =
  let part_no = x_6178 in h_mk_part part_no __

(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type5 h_mk_part x_6180 =
  let part_no = x_6180 in h_mk_part part_no __

(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type3 h_mk_part x_6182 =
  let part_no = x_6182 in h_mk_part part_no __

(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type2 h_mk_part x_6184 =
  let part_no = x_6184 in h_mk_part part_no __

(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type1 h_mk_part x_6186 =
  let part_no = x_6186 in h_mk_part part_no __

(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type0 h_mk_part x_6188 =
  let part_no = x_6188 in h_mk_part part_no __

(** val part_no : part -> Nat.nat **)
let rec part_no xxx =
  let yyy = xxx in yyy

(** val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let part_inv_rect_Type4 hterm h1 =
  let hcut = part_rect_Type4 h1 hterm in hcut __

(** val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let part_inv_rect_Type3 hterm h1 =
  let hcut = part_rect_Type3 h1 hterm in hcut __

(** val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let part_inv_rect_Type2 hterm h1 =
  let hcut = part_rect_Type2 h1 hterm in hcut __

(** val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let part_inv_rect_Type1 hterm h1 =
  let hcut = part_rect_Type1 h1 hterm in hcut __

(** val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
let part_inv_rect_Type0 hterm h1 =
  let hcut = part_rect_Type0 h1 hterm in hcut __

(** val part_discr : part -> part -> __ **)
let part_discr x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val part_jmdiscr : part -> part -> __ **)
let part_jmdiscr x y =
  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__part_no__o__inject :
    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
let dpi1__o__part_no__o__inject x2 =
  part_no x2.Types.dpi1

(** val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z **)
let dpi1__o__part_no__o__Z_of_nat x1 =
  Z.z_of_nat (part_no x1.Types.dpi1)

(** val eject__o__part_no__o__inject :
    part Types.sig0 -> Nat.nat Types.sig0 **)
let eject__o__part_no__o__inject x2 =
  part_no (Types.pi1 x2)

(** val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z **)
let eject__o__part_no__o__Z_of_nat x1 =
  Z.z_of_nat (part_no (Types.pi1 x1))

(** val part_no__o__Z_of_nat : part -> Z.z **)
let part_no__o__Z_of_nat x0 =
  Z.z_of_nat (part_no x0)

(** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
let part_no__o__inject x1 =
  part_no x1

(** val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat **)
let dpi1__o__part_no x1 =
  part_no x1.Types.dpi1

(** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
let eject__o__part_no x1 =
  part_no (Types.pi1 x1)

(** val part_from_sig : Nat.nat Types.sig0 -> part **)
let part_from_sig n_sig =
  Types.pi1 n_sig

(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
    (part, 'a1) Types.dPair -> part Types.sig0 **)
let dpi1__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
  part_from_sig (dpi1__o__part_no__o__inject x2)

(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
  part_no__o__inject (part_from_sig (dpi1__o__part_no__o__inject x2))

(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
    (part, 'a1) Types.dPair -> Z.z **)
let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
  part_no__o__Z_of_nat (part_from_sig (dpi1__o__part_no__o__inject x1))

(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
    (part, 'a1) Types.dPair -> Nat.nat **)
let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
  part_no (part_from_sig (dpi1__o__part_no__o__inject x1))

(** val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
    part Types.sig0 -> part Types.sig0 **)
let eject__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
  part_from_sig (eject__o__part_no__o__inject x2)

(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
    part Types.sig0 -> Nat.nat Types.sig0 **)
let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
  part_no__o__inject (part_from_sig (eject__o__part_no__o__inject x2))

(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
    part Types.sig0 -> Z.z **)
let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
  part_no__o__Z_of_nat (part_from_sig (eject__o__part_no__o__inject x1))

(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
    part Types.sig0 -> Nat.nat **)
let eject__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
  part_no (part_from_sig (eject__o__part_no__o__inject x1))

(** val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0 **)
let inject__o__sig_to_part__o__inject x0 =
  part_from_sig x0

(** val inject__o__sig_to_part__o__part_no__o__inject :
    Nat.nat -> Nat.nat Types.sig0 **)
let inject__o__sig_to_part__o__part_no__o__inject x0 =
  part_no__o__inject (part_from_sig x0)

(** val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z **)
let inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
  part_no__o__Z_of_nat (part_from_sig x0)

(** val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat **)
let inject__o__sig_to_part__o__part_no x0 =
  part_no (part_from_sig x0)

(** val part_no__o__inject__o__sig_to_part__o__inject :
    part -> part Types.sig0 **)
let part_no__o__inject__o__sig_to_part__o__inject x0 =
  part_from_sig (part_no__o__inject x0)

(** val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
    part -> Nat.nat Types.sig0 **)
let part_no__o__inject__o__sig_to_part__o__part_no__o__inject x0 =
  part_no__o__inject (part_from_sig (part_no__o__inject x0))

(** val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
    part -> Z.z **)
let part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
  part_no__o__Z_of_nat (part_from_sig (part_no__o__inject x0))

(** val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat **)
let part_no__o__inject__o__sig_to_part__o__part_no x0 =
  part_no (part_from_sig (part_no__o__inject x0))

(** val dpi1__o__sig_to_part__o__inject :
    (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0 **)
let dpi1__o__sig_to_part__o__inject x2 =
  part_from_sig x2.Types.dpi1

(** val dpi1__o__sig_to_part__o__part_no__o__inject :
    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
let dpi1__o__sig_to_part__o__part_no__o__inject x2 =
  part_no__o__inject (part_from_sig x2.Types.dpi1)

(** val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
    (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z **)
let dpi1__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
  part_no__o__Z_of_nat (part_from_sig x1.Types.dpi1)

(** val dpi1__o__sig_to_part__o__part_no :
    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat **)
let dpi1__o__sig_to_part__o__part_no x1 =
  part_no (part_from_sig x1.Types.dpi1)

(** val eject__o__sig_to_part__o__inject :
    Nat.nat Types.sig0 Types.sig0 -> part Types.sig0 **)
let eject__o__sig_to_part__o__inject x2 =
  part_from_sig (Types.pi1 x2)

(** val eject__o__sig_to_part__o__part_no__o__inject :
    Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0 **)
let eject__o__sig_to_part__o__part_no__o__inject x2 =
  part_no__o__inject (part_from_sig (Types.pi1 x2))

(** val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
    Nat.nat Types.sig0 Types.sig0 -> Z.z **)
let eject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
  part_no__o__Z_of_nat (part_from_sig (Types.pi1 x1))

(** val eject__o__sig_to_part__o__part_no :
    Nat.nat Types.sig0 Types.sig0 -> Nat.nat **)
let eject__o__sig_to_part__o__part_no x1 =
  part_no (part_from_sig (Types.pi1 x1))

(** val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat **)
let sig_to_part__o__part_no x0 =
  part_no (part_from_sig x0)

(** val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z **)
let sig_to_part__o__part_no__o__Z_of_nat x0 =
  part_no__o__Z_of_nat (part_from_sig x0)

(** val sig_to_part__o__part_no__o__inject :
    Nat.nat Types.sig0 -> Nat.nat Types.sig0 **)
let sig_to_part__o__part_no__o__inject x1 =
  part_no__o__inject (part_from_sig x1)

(** val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0 **)
let sig_to_part__o__inject x1 =
  part_from_sig x1

(** val dpi1__o__part_no__o__inject__o__sig_to_part :
    (part, 'a1) Types.dPair -> part **)
let dpi1__o__part_no__o__inject__o__sig_to_part x1 =
  part_from_sig (dpi1__o__part_no__o__inject x1)

(** val eject__o__part_no__o__inject__o__sig_to_part :
    part Types.sig0 -> part **)
let eject__o__part_no__o__inject__o__sig_to_part x1 =
  part_from_sig (eject__o__part_no__o__inject x1)

(** val inject__o__sig_to_part : Nat.nat -> part **)
let inject__o__sig_to_part x0 =
  part_from_sig x0

(** val part_no__o__inject__o__sig_to_part : part -> part **)
let part_no__o__inject__o__sig_to_part x0 =
  part_from_sig (part_no__o__inject x0)

(** val dpi1__o__sig_to_part :
    (Nat.nat Types.sig0, 'a1) Types.dPair -> part **)
let dpi1__o__sig_to_part x1 =
  part_from_sig x1.Types.dpi1

(** val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part **)
let eject__o__sig_to_part x1 =
  part_from_sig (Types.pi1 x1)

type beval =
| BVundef
| BVnonzero
| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
   * part
| BVByte of BitVector.byte
| BVnull of part
| BVptr of Pointers.pointer * part
| BVpc of program_counter * part

(** val beval_rect_Type4 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type4 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6222, x_6221, x_6220) -> h_BVXor x_6222 x_6221 x_6220
| BVByte x_6223 -> h_BVByte x_6223
| BVnull x_6224 -> h_BVnull x_6224
| BVptr (x_6226, x_6225) -> h_BVptr x_6226 x_6225
| BVpc (x_6228, x_6227) -> h_BVpc x_6228 x_6227

(** val beval_rect_Type5 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type5 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6239, x_6238, x_6237) -> h_BVXor x_6239 x_6238 x_6237
| BVByte x_6240 -> h_BVByte x_6240
| BVnull x_6241 -> h_BVnull x_6241
| BVptr (x_6243, x_6242) -> h_BVptr x_6243 x_6242
| BVpc (x_6245, x_6244) -> h_BVpc x_6245 x_6244

(** val beval_rect_Type3 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type3 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6256, x_6255, x_6254) -> h_BVXor x_6256 x_6255 x_6254
| BVByte x_6257 -> h_BVByte x_6257
| BVnull x_6258 -> h_BVnull x_6258
| BVptr (x_6260, x_6259) -> h_BVptr x_6260 x_6259
| BVpc (x_6262, x_6261) -> h_BVpc x_6262 x_6261

(** val beval_rect_Type2 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type2 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6273, x_6272, x_6271) -> h_BVXor x_6273 x_6272 x_6271
| BVByte x_6274 -> h_BVByte x_6274
| BVnull x_6275 -> h_BVnull x_6275
| BVptr (x_6277, x_6276) -> h_BVptr x_6277 x_6276
| BVpc (x_6279, x_6278) -> h_BVpc x_6279 x_6278

(** val beval_rect_Type1 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type1 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6290, x_6289, x_6288) -> h_BVXor x_6290 x_6289 x_6288
| BVByte x_6291 -> h_BVByte x_6291
| BVnull x_6292 -> h_BVnull x_6292
| BVptr (x_6294, x_6293) -> h_BVptr x_6294 x_6293
| BVpc (x_6296, x_6295) -> h_BVpc x_6296 x_6295

(** val beval_rect_Type0 :
    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
    -> beval -> 'a1 **)
let rec beval_rect_Type0 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
| BVundef -> h_BVundef
| BVnonzero -> h_BVnonzero
| BVXor (x_6307, x_6306, x_6305) -> h_BVXor x_6307 x_6306 x_6305
| BVByte x_6308 -> h_BVByte x_6308
| BVnull x_6309 -> h_BVnull x_6309
| BVptr (x_6311, x_6310) -> h_BVptr x_6311 x_6310
| BVpc (x_6313, x_6312) -> h_BVpc x_6313 x_6312

(** val beval_inv_rect_Type4 :
    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
let beval_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = beval_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val beval_inv_rect_Type3 :
    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
let beval_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = beval_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val beval_inv_rect_Type2 :
    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
let beval_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = beval_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val beval_inv_rect_Type1 :
    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
let beval_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = beval_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val beval_inv_rect_Type0 :
    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
let beval_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
  let hcut = beval_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __

(** val beval_discr : beval -> beval -> __ **)
let beval_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | BVundef -> Obj.magic (fun _ dH -> dH)
     | BVnonzero -> Obj.magic (fun _ dH -> dH)
     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val beval_jmdiscr : beval -> beval -> __ **)
let beval_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | BVundef -> Obj.magic (fun _ dH -> dH)
     | BVnonzero -> Obj.magic (fun _ dH -> dH)
     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val eq_bv_suffix :
    Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector ->
    BitVector.bitVector -> Bool.bool **)
let eq_bv_suffix n m p v1 v2 =
  let b1 = (Vector.vsplit n p v1).Types.snd in
  let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2

(** val pointer_of_bevals :
    beval List.list -> Pointers.pointer Errors.res **)
let pointer_of_bevals = function
| List.Nil ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
    List.Nil))
| List.Cons (bv1, tl) ->
  (match tl with
   | List.Nil ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
       List.Nil))
   | List.Cons (bv2, tl') ->
     (match tl' with
      | List.Nil ->
        (match bv1 with
         | BVundef ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVnonzero ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVXor (x, x0, x1) ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVByte x ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVnull x ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVptr (ptr1, p1) ->
           (match bv2 with
            | BVundef ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVnonzero ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVXor (x, x0, x1) ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVByte x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVnull x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVptr (ptr2, p2) ->
              (match Bool.andb
                       (Bool.andb
                         (Bool.andb (Nat.eqb (part_no p1) Nat.O)
                           (Nat.eqb (part_no p2) (Nat.S Nat.O)))
                         (Pointers.eq_block ptr1.Pointers.pblock
                           ptr2.Pointers.pblock))
                       (eq_bv_suffix (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)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
                         (Pointers.offv ptr1.Pointers.poff)
                         (Pointers.offv ptr2.Pointers.poff)) with
               | Bool.True ->
                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
               | Bool.False ->
                 Errors.Error (List.Cons ((Errors.MSG
                   ErrorMessages.CorruptedPointer), List.Nil)))
            | BVpc (x, x0) ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil)))
         | BVpc (x, x0) ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil)))
      | List.Cons (x, x0) ->
        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
          List.Nil))))

(** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
let pc_of_bevals = function
| List.Nil ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
    List.Nil))
| List.Cons (bv1, tl) ->
  (match tl with
   | List.Nil ->
     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
       List.Nil))
   | List.Cons (bv2, tl') ->
     (match tl' with
      | List.Nil ->
        (match bv1 with
         | BVundef ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVnonzero ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVXor (x, x0, x1) ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVByte x ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVnull x ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVptr (x, x0) ->
           Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.CorruptedPointer), List.Nil))
         | BVpc (ptr1, p1) ->
           (match bv2 with
            | BVundef ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVnonzero ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVXor (x, x0, x1) ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVByte x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVnull x ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVptr (x, x0) ->
              Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.CorruptedPointer), List.Nil))
            | BVpc (ptr2, p2) ->
              (match Bool.andb
                       (Bool.andb (Nat.eqb (part_no p1) Nat.O)
                         (Nat.eqb (part_no p2) (Nat.S Nat.O)))
                       (eq_program_counter ptr1 ptr2) with
               | Bool.True ->
                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
               | Bool.False ->
                 Errors.Error (List.Cons ((Errors.MSG
                   ErrorMessages.CorruptedPointer), List.Nil)))))
      | List.Cons (x, x0) ->
        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
          List.Nil))))

(** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
let bevals_of_pointer p =
  List.map (fun n_sig -> BVptr (p, (part_from_sig n_sig)))
    (Lists.range_strong AST.size_pointer)

(** val bevals_of_pc : program_counter -> beval List.list **)
let bevals_of_pc p =
  List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
    (Lists.range_strong AST.size_pointer)

(** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
let list_to_pair l =
  (match l with
   | List.Nil ->
     (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
   | List.Cons (a, tl) ->
     (match tl with
      | List.Nil ->
        (fun _ ->
          Obj.magic Nat.nat_discr (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) __
            (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S Nat.O) __))
      | List.Cons (b, tl') ->
        (match tl' with
         | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
         | List.Cons (c, tl'') ->
           (fun _ ->
             Obj.magic Nat.nat_discr (Nat.S (Nat.S (Nat.S
               (List.length tl'')))) (Nat.S (Nat.S Nat.O)) __ (fun _ ->
               Obj.magic Nat.nat_discr (Nat.S (Nat.S (List.length tl'')))
                 (Nat.S Nat.O) __ (fun _ ->
                 Obj.magic Nat.nat_discr (Nat.S (List.length tl'')) Nat.O __))))))
    __

(** val beval_pair_of_pointer :
    Pointers.pointer -> (beval, beval) Types.prod **)
let beval_pair_of_pointer p =
  list_to_pair (bevals_of_pointer p)

(** val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod **)
let beval_pair_of_pc p =
  list_to_pair (bevals_of_pc p)

(** val bool_of_beval : beval -> Bool.bool Errors.res **)
let bool_of_beval = function
| BVundef ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
    List.Nil))
| BVnonzero -> Errors.OK Bool.True
| BVXor (x, x0, x1) ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
    List.Nil))
| BVByte b ->
  Errors.OK
    (Bool.notb
      (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S Nat.O))))))))
        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))) b))
| BVnull x -> Errors.OK Bool.False
| BVptr (x, x0) -> Errors.OK Bool.True
| BVpc (x, x0) ->
  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
    List.Nil))

(** val byte_of_val :
    ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
let byte_of_val err = function
| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BVByte b0 -> Errors.OK b0
| BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))

(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
let word_of_list_beval l =
  let first_byte = fun l0 ->
    match l0 with
    | List.Nil ->
      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
        ErrorMessages.NotAnInt32Val), List.Nil)))
    | List.Cons (hd, tl) ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd)) (fun b ->
        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
  in
  Obj.magic
    (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
      Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
        Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
          (fun b3 l2 ->
          Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
            (fun b4 l3 ->
            match l3 with
            | List.Nil ->
              Obj.magic (Errors.OK
                (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                  (Nat.S (Nat.S Nat.O))))))))
                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S Nat.O))))))))
                    (Nat.plus (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)))))))))) b4
                  (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                    (Nat.S (Nat.S Nat.O))))))))
                    (Nat.plus (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))))))))) b3
                    (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)))))))) b2 b1))))
            | List.Cons (x, x0) ->
              Obj.magic (Errors.Error (List.Cons ((Errors.MSG
                ErrorMessages.NotAnInt32Val), List.Nil))))))))

type add_or_sub =
| Do_add
| Do_sub

(** val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function
| Do_add -> h_do_add
| Do_sub -> h_do_sub

(** val add_or_sub_inv_rect_Type4 :
    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let add_or_sub_inv_rect_Type4 hterm h1 h2 =
  let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __

(** val add_or_sub_inv_rect_Type3 :
    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let add_or_sub_inv_rect_Type3 hterm h1 h2 =
  let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __

(** val add_or_sub_inv_rect_Type2 :
    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let add_or_sub_inv_rect_Type2 hterm h1 h2 =
  let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __

(** val add_or_sub_inv_rect_Type1 :
    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let add_or_sub_inv_rect_Type1 hterm h1 h2 =
  let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __

(** val add_or_sub_inv_rect_Type0 :
    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let add_or_sub_inv_rect_Type0 hterm h1 h2 =
  let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __

(** val add_or_sub_discr : add_or_sub -> add_or_sub -> __ **)
let add_or_sub_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Do_add -> Obj.magic (fun _ dH -> dH)
     | Do_sub -> Obj.magic (fun _ dH -> dH)) y

(** val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __ **)
let add_or_sub_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Do_add -> Obj.magic (fun _ dH -> dH)
     | Do_sub -> Obj.magic (fun _ dH -> dH)) y

(** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
let eq_add_or_sub x y =
  match x with
  | Do_add ->
    (match y with
     | Do_add -> Bool.True
     | Do_sub -> Bool.False)
  | Do_sub ->
    (match y with
     | Do_add -> Bool.False
     | Do_sub -> Bool.True)

type bebit =
| BBbit of Bool.bool
| BBundef
| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector

(** val bebit_rect_Type4 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6471 -> h_BBbit x_6471
| BBundef -> h_BBundef
| BBptrcarry (x_6474, x_6473, p, x_6472) ->
  h_BBptrcarry x_6474 x_6473 p x_6472

(** val bebit_rect_Type5 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6479 -> h_BBbit x_6479
| BBundef -> h_BBundef
| BBptrcarry (x_6482, x_6481, p, x_6480) ->
  h_BBptrcarry x_6482 x_6481 p x_6480

(** val bebit_rect_Type3 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6487 -> h_BBbit x_6487
| BBundef -> h_BBundef
| BBptrcarry (x_6490, x_6489, p, x_6488) ->
  h_BBptrcarry x_6490 x_6489 p x_6488

(** val bebit_rect_Type2 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6495 -> h_BBbit x_6495
| BBundef -> h_BBundef
| BBptrcarry (x_6498, x_6497, p, x_6496) ->
  h_BBptrcarry x_6498 x_6497 p x_6496

(** val bebit_rect_Type1 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6503 -> h_BBbit x_6503
| BBundef -> h_BBundef
| BBptrcarry (x_6506, x_6505, p, x_6504) ->
  h_BBptrcarry x_6506 x_6505 p x_6504

(** val bebit_rect_Type0 :
    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
| BBbit x_6511 -> h_BBbit x_6511
| BBundef -> h_BBundef
| BBptrcarry (x_6514, x_6513, p, x_6512) ->
  h_BBptrcarry x_6514 x_6513 p x_6512

(** val bebit_inv_rect_Type4 :
    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let bebit_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __

(** val bebit_inv_rect_Type3 :
    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let bebit_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __

(** val bebit_inv_rect_Type2 :
    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let bebit_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __

(** val bebit_inv_rect_Type1 :
    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let bebit_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __

(** val bebit_inv_rect_Type0 :
    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let bebit_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __

(** val bebit_discr : bebit -> bebit -> __ **)
let bebit_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
     | BBundef -> Obj.magic (fun _ dH -> dH)
     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
    y

(** val bebit_jmdiscr : bebit -> bebit -> __ **)
let bebit_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
     | BBundef -> Obj.magic (fun _ dH -> dH)
     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
    y

(** val bit_of_val :
    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
let bit_of_val err = function
| BBbit b0 -> Errors.OK b0
| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
| BBptrcarry (x, x0, x1, x2) ->
  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))