open Preamble

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 Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

type block =
  Z.z
  (* singleton inductive, whose constructor was mk_block *)

(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type4 h_mk_block x_5028 =
  let block_id = x_5028 in h_mk_block block_id

(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type5 h_mk_block x_5030 =
  let block_id = x_5030 in h_mk_block block_id

(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type3 h_mk_block x_5032 =
  let block_id = x_5032 in h_mk_block block_id

(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type2 h_mk_block x_5034 =
  let block_id = x_5034 in h_mk_block block_id

(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type1 h_mk_block x_5036 =
  let block_id = x_5036 in h_mk_block block_id

(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
let rec block_rect_Type0 h_mk_block x_5038 =
  let block_id = x_5038 in h_mk_block block_id

(** val block_id : block -> Z.z **)
let rec block_id xxx =
  let yyy = xxx in yyy

(** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
let block_inv_rect_Type4 hterm h1 =
  let hcut = block_rect_Type4 h1 hterm in hcut __

(** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
let block_inv_rect_Type3 hterm h1 =
  let hcut = block_rect_Type3 h1 hterm in hcut __

(** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
let block_inv_rect_Type2 hterm h1 =
  let hcut = block_rect_Type2 h1 hterm in hcut __

(** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
let block_inv_rect_Type1 hterm h1 =
  let hcut = block_rect_Type1 h1 hterm in hcut __

(** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
let block_inv_rect_Type0 hterm h1 =
  let hcut = block_rect_Type0 h1 hterm in hcut __

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

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

(** val block_region : block -> AST.region **)
let block_region b =
  match Z.zleb (block_id b) Z.OZ with
  | Bool.True -> AST.Code
  | Bool.False -> AST.XData

(** val dummy_block_code : block **)
let dummy_block_code =
  Z.OZ

(** val eq_block : block -> block -> Bool.bool **)
let eq_block b1 b2 =
  Z.eqZb (block_id b1) (block_id b2)

(** val block_eq : Deqsets.deqSet **)
let block_eq =
  Obj.magic eq_block

(** val offset_size : Nat.nat **)
let offset_size =
  Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    Nat.O)))))))) AST.size_pointer

type offset =
  BitVector.bitVector
  (* singleton inductive, whose constructor was mk_offset *)

(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type4 h_mk_offset x_5054 =
  let offv = x_5054 in h_mk_offset offv

(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type5 h_mk_offset x_5056 =
  let offv = x_5056 in h_mk_offset offv

(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type3 h_mk_offset x_5058 =
  let offv = x_5058 in h_mk_offset offv

(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type2 h_mk_offset x_5060 =
  let offv = x_5060 in h_mk_offset offv

(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type1 h_mk_offset x_5062 =
  let offv = x_5062 in h_mk_offset offv

(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
let rec offset_rect_Type0 h_mk_offset x_5064 =
  let offv = x_5064 in h_mk_offset offv

(** val offv : offset -> BitVector.bitVector **)
let rec offv xxx =
  let yyy = xxx in yyy

(** val offset_inv_rect_Type4 :
    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let offset_inv_rect_Type4 hterm h1 =
  let hcut = offset_rect_Type4 h1 hterm in hcut __

(** val offset_inv_rect_Type3 :
    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let offset_inv_rect_Type3 hterm h1 =
  let hcut = offset_rect_Type3 h1 hterm in hcut __

(** val offset_inv_rect_Type2 :
    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let offset_inv_rect_Type2 hterm h1 =
  let hcut = offset_rect_Type2 h1 hterm in hcut __

(** val offset_inv_rect_Type1 :
    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let offset_inv_rect_Type1 hterm h1 =
  let hcut = offset_rect_Type1 h1 hterm in hcut __

(** val offset_inv_rect_Type0 :
    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
let offset_inv_rect_Type0 hterm h1 =
  let hcut = offset_rect_Type0 h1 hterm in hcut __

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

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

(** val eq_offset : offset -> offset -> Bool.bool **)
let eq_offset x y =
  BitVector.eq_bv offset_size (offv x) (offv y)

(** val offset_of_Z : Z.z -> offset **)
let offset_of_Z z =
  BitVectorZ.bitvector_of_Z offset_size z

(** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
let shift_offset n o i =
  Arithmetic.addition_n offset_size (offv o)
    (Arithmetic.sign_ext n offset_size i)

(** val shift_offset_n :
    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
    offset **)
let shift_offset_n n o i sg j =
  Arithmetic.addition_n offset_size (offv o)
    (Arithmetic.short_multiplication offset_size
      (Arithmetic.bitvector_of_nat offset_size i)
      (match sg with
       | AST.Signed -> Arithmetic.sign_ext n offset_size j
       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))

(** val neg_shift_offset :
    Nat.nat -> offset -> BitVector.bitVector -> offset **)
let neg_shift_offset n o i =
  Arithmetic.subtraction offset_size (offv o)
    (Arithmetic.sign_ext n offset_size i)

(** val neg_shift_offset_n :
    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
    offset **)
let neg_shift_offset_n n o i sg j =
  Arithmetic.subtraction offset_size (offv o)
    (Arithmetic.short_multiplication offset_size
      (Arithmetic.bitvector_of_nat offset_size i)
      (match sg with
       | AST.Signed -> Arithmetic.sign_ext n offset_size j
       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))

(** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
let sub_offset n x y =
  Arithmetic.sign_ext offset_size n
    (Arithmetic.subtraction offset_size (offv x) (offv y))

(** val zero_offset : offset **)
let zero_offset =
  BitVector.zero offset_size

(** val lt_offset : offset -> offset -> Bool.bool **)
let lt_offset x y =
  Arithmetic.lt_u offset_size (offv x) (offv y)

type pointer = { pblock : block; poff : offset }

(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type4 h_mk_pointer x_5080 =
  let { pblock = pblock0; poff = poff0 } = x_5080 in
  h_mk_pointer pblock0 poff0

(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type5 h_mk_pointer x_5082 =
  let { pblock = pblock0; poff = poff0 } = x_5082 in
  h_mk_pointer pblock0 poff0

(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type3 h_mk_pointer x_5084 =
  let { pblock = pblock0; poff = poff0 } = x_5084 in
  h_mk_pointer pblock0 poff0

(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type2 h_mk_pointer x_5086 =
  let { pblock = pblock0; poff = poff0 } = x_5086 in
  h_mk_pointer pblock0 poff0

(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type1 h_mk_pointer x_5088 =
  let { pblock = pblock0; poff = poff0 } = x_5088 in
  h_mk_pointer pblock0 poff0

(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
let rec pointer_rect_Type0 h_mk_pointer x_5090 =
  let { pblock = pblock0; poff = poff0 } = x_5090 in
  h_mk_pointer pblock0 poff0

(** val pblock : pointer -> block **)
let rec pblock xxx =
  xxx.pblock

(** val poff : pointer -> offset **)
let rec poff xxx =
  xxx.poff

(** val pointer_inv_rect_Type4 :
    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
let pointer_inv_rect_Type4 hterm h1 =
  let hcut = pointer_rect_Type4 h1 hterm in hcut __

(** val pointer_inv_rect_Type3 :
    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
let pointer_inv_rect_Type3 hterm h1 =
  let hcut = pointer_rect_Type3 h1 hterm in hcut __

(** val pointer_inv_rect_Type2 :
    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
let pointer_inv_rect_Type2 hterm h1 =
  let hcut = pointer_rect_Type2 h1 hterm in hcut __

(** val pointer_inv_rect_Type1 :
    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
let pointer_inv_rect_Type1 hterm h1 =
  let hcut = pointer_rect_Type1 h1 hterm in hcut __

(** val pointer_inv_rect_Type0 :
    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
let pointer_inv_rect_Type0 hterm h1 =
  let hcut = pointer_rect_Type0 h1 hterm in hcut __

(** val pointer_discr : pointer -> pointer -> __ **)
let pointer_discr x y =
  Logic.eq_rect_Type2 x
    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
    y

(** val pointer_jmdiscr : pointer -> pointer -> __ **)
let pointer_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
    y

(** val ptype : pointer -> AST.region **)
let ptype p =
  block_region p.pblock

(** val shift_pointer :
    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
let shift_pointer n p i =
  { pblock = p.pblock; poff = (shift_offset n p.poff i) }

(** val shift_pointer_n :
    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
    pointer **)
let shift_pointer_n n p i sg j =
  { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }

(** val neg_shift_pointer :
    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
let neg_shift_pointer n p i =
  { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }

(** val neg_shift_pointer_n :
    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
    pointer **)
let neg_shift_pointer_n n p i sg j =
  { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }

(** val eq_pointer : pointer -> pointer -> Bool.bool **)
let eq_pointer p1 p2 =
  Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)