source: extracted/byteValues.ml @ 3001

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_2980 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2980 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_2982 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2982 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_2984 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2984 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_2986 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2986 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_2988 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2988 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_2990 =
  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2990 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_3006 =
  let part_no = x_3006 in h_mk_part part_no __

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

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

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

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

(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
let rec part_rect_Type0 h_mk_part x_3016 =
  let part_no = x_3016 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_3050, x_3049, x_3048) -> h_BVXor x_3050 x_3049 x_3048
| BVByte x_3051 -> h_BVByte x_3051
| BVnull x_3052 -> h_BVnull x_3052
| BVptr (x_3054, x_3053) -> h_BVptr x_3054 x_3053
| BVpc (x_3056, x_3055) -> h_BVpc x_3056 x_3055

(** 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_3067, x_3066, x_3065) -> h_BVXor x_3067 x_3066 x_3065
| BVByte x_3068 -> h_BVByte x_3068
| BVnull x_3069 -> h_BVnull x_3069
| BVptr (x_3071, x_3070) -> h_BVptr x_3071 x_3070
| BVpc (x_3073, x_3072) -> h_BVpc x_3073 x_3072

(** 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_3084, x_3083, x_3082) -> h_BVXor x_3084 x_3083 x_3082
| BVByte x_3085 -> h_BVByte x_3085
| BVnull x_3086 -> h_BVnull x_3086
| BVptr (x_3088, x_3087) -> h_BVptr x_3088 x_3087
| BVpc (x_3090, x_3089) -> h_BVpc x_3090 x_3089

(** 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_3101, x_3100, x_3099) -> h_BVXor x_3101 x_3100 x_3099
| BVByte x_3102 -> h_BVByte x_3102
| BVnull x_3103 -> h_BVnull x_3103
| BVptr (x_3105, x_3104) -> h_BVptr x_3105 x_3104
| BVpc (x_3107, x_3106) -> h_BVpc x_3107 x_3106

(** 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_3118, x_3117, x_3116) -> h_BVXor x_3118 x_3117 x_3116
| BVByte x_3119 -> h_BVByte x_3119
| BVnull x_3120 -> h_BVnull x_3120
| BVptr (x_3122, x_3121) -> h_BVptr x_3122 x_3121
| BVpc (x_3124, x_3123) -> h_BVpc x_3124 x_3123

(** 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_3135, x_3134, x_3133) -> h_BVXor x_3135 x_3134 x_3133
| BVByte x_3136 -> h_BVByte x_3136
| BVnull x_3137 -> h_BVnull x_3137
| BVptr (x_3139, x_3138) -> h_BVptr x_3139 x_3138
| BVpc (x_3141, x_3140) -> h_BVpc x_3141 x_3140

(** 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 (Pointers.pblock ptr1)
                           (Pointers.pblock ptr2)))
                       (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 (Pointers.poff ptr1))
                         (Pointers.offv (Pointers.poff 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)))
            | 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_3299 -> h_BBbit x_3299
| BBundef -> h_BBundef
| BBptrcarry (x_3302, x_3301, p, x_3300) ->
  h_BBptrcarry x_3302 x_3301 p x_3300

(** 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_3307 -> h_BBbit x_3307
| BBundef -> h_BBundef
| BBptrcarry (x_3310, x_3309, p, x_3308) ->
  h_BBptrcarry x_3310 x_3309 p x_3308

(** 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_3315 -> h_BBbit x_3315
| BBundef -> h_BBundef
| BBptrcarry (x_3318, x_3317, p, x_3316) ->
  h_BBptrcarry x_3318 x_3317 p x_3316

(** 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_3323 -> h_BBbit x_3323
| BBundef -> h_BBundef
| BBptrcarry (x_3326, x_3325, p, x_3324) ->
  h_BBptrcarry x_3326 x_3325 p x_3324

(** 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_3331 -> h_BBbit x_3331
| BBundef -> h_BBundef
| BBptrcarry (x_3334, x_3333, p, x_3332) ->
  h_BBptrcarry x_3334 x_3333 p x_3332

(** 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_3339 -> h_BBbit x_3339
| BBundef -> h_BBundef
| BBptrcarry (x_3342, x_3341, p, x_3340) ->
  h_BBptrcarry x_3342 x_3341 p x_3340

(** 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))