open Preamble

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

type 'f genv_t = { functions : 'f PositiveMap.positive_map;
                   nextfunction : Positive.pos;
                   symbols : Pointers.block Identifiers.identifier_map }

(** val genv_t_rect_Type4 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type4 h_mk_genv_t x_6621 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6621
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val genv_t_rect_Type5 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type5 h_mk_genv_t x_6623 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6623
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val genv_t_rect_Type3 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type3 h_mk_genv_t x_6625 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6625
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val genv_t_rect_Type2 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type2 h_mk_genv_t x_6627 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6627
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val genv_t_rect_Type1 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type1 h_mk_genv_t x_6629 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6629
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val genv_t_rect_Type0 :
    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
let rec genv_t_rect_Type0 h_mk_genv_t x_6631 =
  let { functions = functions0; nextfunction = nextfunction0; symbols =
    symbols0 } = x_6631
  in
  h_mk_genv_t functions0 nextfunction0 symbols0 __

(** val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map **)
let rec functions xxx =
  xxx.functions

(** val nextfunction : 'a1 genv_t -> Positive.pos **)
let rec nextfunction xxx =
  xxx.nextfunction

(** val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map **)
let rec symbols xxx =
  xxx.symbols

(** val genv_t_inv_rect_Type4 :
    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
let genv_t_inv_rect_Type4 hterm h1 =
  let hcut = genv_t_rect_Type4 h1 hterm in hcut __

(** val genv_t_inv_rect_Type3 :
    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
let genv_t_inv_rect_Type3 hterm h1 =
  let hcut = genv_t_rect_Type3 h1 hterm in hcut __

(** val genv_t_inv_rect_Type2 :
    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
let genv_t_inv_rect_Type2 hterm h1 =
  let hcut = genv_t_rect_Type2 h1 hterm in hcut __

(** val genv_t_inv_rect_Type1 :
    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
let genv_t_inv_rect_Type1 hterm h1 =
  let hcut = genv_t_rect_Type1 h1 hterm in hcut __

(** val genv_t_inv_rect_Type0 :
    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
let genv_t_inv_rect_Type0 hterm h1 =
  let hcut = genv_t_rect_Type0 h1 hterm in hcut __

(** val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __ **)
let genv_t_discr x y =
  Logic.eq_rect_Type2 x
    (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __ **)
let genv_t_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t **)
let drop_fn id g =
  let fns =
    match Identifiers.lookup PreIdentifiers.SymbolTag g.symbols id with
    | Types.None -> g.functions
    | Types.Some b' ->
      (match Pointers.block_id b' with
       | Z.OZ -> g.functions
       | Z.Pos x -> g.functions
       | Z.Neg p -> PositiveMap.pm_set p Types.None g.functions)
  in
  { functions = fns; nextfunction = g.nextfunction; symbols =
  (Identifiers.remove PreIdentifiers.SymbolTag g.symbols id) }

(** val add_funct :
    (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
let add_funct name_fun g =
  let blk_id = g.nextfunction in
  let b = Z.Neg blk_id in
  let g' = drop_fn name_fun.Types.fst g in
  { functions = (PositiveMap.insert blk_id name_fun.Types.snd g'.functions);
  nextfunction = (Positive.succ blk_id); symbols =
  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name_fun.Types.fst b) }

(** val add_symbol :
    AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t **)
let add_symbol name b g =
  let g' = drop_fn name g in
  { functions = g'.functions; nextfunction = g'.nextfunction; symbols =
  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name b) }

(** val empty_mem : GenMem.mem **)
let empty_mem =
  GenMem.empty

(** val empty : 'a1 genv_t **)
let empty =
  { functions = PositiveMap.Pm_leaf; nextfunction =
    (Positive.succ_pos_of_nat (Nat.S (Nat.S Nat.O))); symbols =
    (Identifiers.empty_map PreIdentifiers.SymbolTag) }

(** val add_functs :
    'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t **)
let add_functs init fns =
  List.foldr add_funct init fns

(** val find_symbol :
    'a1 genv_t -> AST.ident -> Pointers.block Types.option **)
let find_symbol ge =
  Identifiers.lookup PreIdentifiers.SymbolTag ge.symbols

(** val store_init_data :
    'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
    GenMem.mem Types.option **)
let store_init_data ge m b p id =
  let ptr = { Pointers.pblock = b; Pointers.poff =
    (BitVectorZ.bitvector_of_Z Pointers.offset_size p) }
  in
  (match id with
   | AST.Init_int8 n ->
     FrontEndMem.store (AST.ASTint (AST.I8, AST.Unsigned)) m ptr (Values.Vint
       (AST.I8, n))
   | AST.Init_int16 n ->
     FrontEndMem.store (AST.ASTint (AST.I16, AST.Unsigned)) m ptr
       (Values.Vint (AST.I16, n))
   | AST.Init_int32 n ->
     FrontEndMem.store (AST.ASTint (AST.I32, AST.Unsigned)) m ptr
       (Values.Vint (AST.I32, n))
   | AST.Init_space n -> Types.Some m
   | AST.Init_null -> FrontEndMem.store AST.ASTptr m ptr Values.Vnull
   | AST.Init_addrof (symb, ofs) ->
     (match find_symbol ge symb with
      | Types.None -> Types.None
      | Types.Some b' ->
        FrontEndMem.store AST.ASTptr m ptr (Values.Vptr { Pointers.pblock =
          b'; Pointers.poff =
          (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
            Pointers.zero_offset (AST.repr AST.I16 ofs)) })))

(** val size_init_data : AST.init_data -> Nat.nat **)
let size_init_data = function
| AST.Init_int8 x -> Nat.S Nat.O
| AST.Init_int16 x -> Nat.S (Nat.S Nat.O)
| AST.Init_int32 x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
| AST.Init_space n -> Nat.max n Nat.O
| AST.Init_null -> AST.size_pointer
| AST.Init_addrof (x, x0) -> AST.size_pointer

(** val store_init_data_list :
    'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
    List.list -> GenMem.mem Types.option **)
let rec store_init_data_list ge m b p = function
| List.Nil -> Types.Some m
| List.Cons (id, idl') ->
  (match store_init_data ge m b p id with
   | Types.None -> Types.None
   | Types.Some m' ->
     store_init_data_list ge m' b
       (Z.zplus p (Z.z_of_nat (size_init_data id))) idl')

(** val size_init_data_list : AST.init_data List.list -> Nat.nat **)
let size_init_data_list i_data =
  List.foldr (fun i_data0 sz -> Nat.plus (size_init_data i_data0) sz) Nat.O
    i_data

(** val add_globals :
    ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod
    -> ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
    genv_t, GenMem.mem) Types.prod **)
let add_globals extract_init init_env vars =
  Util.foldl (fun g_st id_init ->
    let { Types.fst = eta1367; Types.snd = init_info } = id_init in
    let { Types.fst = id; Types.snd = r } = eta1367 in
    let init = extract_init init_info in
    let { Types.fst = g; Types.snd = st } = g_st in
    let { Types.fst = st'; Types.snd = b } =
      GenMem.alloc st Z.OZ (Z.z_of_nat (size_init_data_list init))
    in
    let g' = add_symbol id b g in { Types.fst = g'; Types.snd = st' })
    init_env vars

(** val init_globals :
    ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
    ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
    GenMem.mem Errors.res **)
let init_globals extract_init g m vars =
  Util.foldl (fun st id_init ->
    let { Types.fst = eta1368; Types.snd = init_info } = id_init in
    let { Types.fst = id; Types.snd = r } = eta1368 in
    let init = extract_init init_info in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
        match find_symbol g id with
        | Types.None ->
          Obj.magic (Errors.Error
            (Errors.msg ErrorMessages.InitDataStoreFailed))
        | Types.Some b ->
          Obj.magic
            (Errors.opt_to_res (Errors.msg ErrorMessages.InitDataStoreFailed)
              (store_init_data_list g st0 b Z.OZ init))))) (Errors.OK m) vars

(** val globalenv_allocmem :
    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
    genv_t, GenMem.mem) Types.prod **)
let globalenv_allocmem init_info p =
  add_globals init_info { Types.fst = (add_functs empty p.AST.prog_funct);
    Types.snd = empty_mem } p.AST.prog_vars

(** val globalenv :
    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t **)
let globalenv i p =
  (globalenv_allocmem i p).Types.fst

(** val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t **)
let globalenv_noinit p =
  globalenv (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p

(** val init_mem :
    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
    Errors.res **)
let init_mem i p =
  let { Types.fst = g; Types.snd = m } = globalenv_allocmem i p in
  init_globals i g m p.AST.prog_vars

(** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem **)
let alloc_mem p =
  (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd

(** val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option **)
let find_funct_ptr ge b =
  match Pointers.block_region b with
  | AST.XData -> Types.None
  | AST.Code ->
    (match Pointers.block_id b with
     | Z.OZ -> Types.None
     | Z.Pos x -> Types.None
     | Z.Neg p -> PositiveMap.lookup_opt p ge.functions)

(** val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option **)
let find_funct ge = function
| Values.Vundef -> Types.None
| Values.Vint (x, x0) -> Types.None
| Values.Vnull -> Types.None
| Values.Vptr ptr ->
  (match Pointers.eq_offset ptr.Pointers.poff Pointers.zero_offset with
   | Bool.True -> find_funct_ptr ge ptr.Pointers.pblock
   | Bool.False -> Types.None)

(** val symbol_for_block :
    'a1 genv_t -> Pointers.block -> AST.ident Types.option **)
let symbol_for_block genv b =
  Types.option_map Types.fst
    (Identifiers.find PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
      Pointers.eq_block b b'))

(** val symbol_of_function_block :
    'a1 genv_t -> Pointers.block -> AST.ident **)
let symbol_of_function_block ge b =
  (match symbol_for_block ge b with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some id -> (fun _ -> id)) __

(** val symbol_of_function_block' :
    'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
let symbol_of_function_block' ge b f =
  symbol_of_function_block ge b

(** val find_funct_ptr_id :
    'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
let find_funct_ptr_id ge b =
  (match find_funct_ptr ge b with
   | Types.None -> (fun _ -> Types.None)
   | Types.Some f ->
     (fun _ -> Types.Some { Types.fst = f; Types.snd =
       (symbol_of_function_block' ge b f) })) __

(** val opt_eq_from_res__o__ffpi_drop__o__inject :
    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 **)
let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
  __

(** val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
    'a2) Types.dPair -> __ Types.sig0 **)
let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
  __

(** val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 -> __ Types.sig0 **)
let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
  __

(** val jmeq_to_eq__o__ffpi_drop__o__inject :
    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
  __

(** val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 **)
let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
  __

(** val dpi1__o__ffpi_drop__o__inject :
    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
    -> __ Types.sig0 **)
let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
  __

(** val eject__o__ffpi_drop__o__inject :
    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
  __

(** val ffpi_drop__o__inject :
    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
let ffpi_drop__o__inject x1 x2 x3 x4 =
  __

(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
let symbol_of_function_val ge v =
  (match v with
   | Values.Vundef -> (fun _ -> assert false (* absurd case *))
   | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
   | Values.Vnull -> (fun _ -> assert false (* absurd case *))
   | Values.Vptr p ->
     (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __

(** val symbol_of_function_val' :
    'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
let symbol_of_function_val' ge v f =
  symbol_of_function_val ge v

(** val find_funct_id :
    'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
let find_funct_id ge v =
  (match find_funct ge v with
   | Types.None -> (fun _ -> Types.None)
   | Types.Some f ->
     (fun _ -> Types.Some { Types.fst = f; Types.snd =
       (symbol_of_function_val' ge v f) })) __

(** val opt_eq_from_res__o__ffi_drop__o__inject :
    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 **)
let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
  __

(** val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
    'a2) Types.dPair -> __ Types.sig0 **)
let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
  __

(** val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 -> __ Types.sig0 **)
let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
  __

(** val jmeq_to_eq__o__ffi_drop__o__inject :
    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
  __

(** val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
    Types.sig0 **)
let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
  __

(** val dpi1__o__ffi_drop__o__inject :
    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
    __ Types.sig0 **)
let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
  __

(** val eject__o__ffi_drop__o__inject :
    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
    Types.sig0 **)
let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
  __

(** val ffi_drop__o__inject :
    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
let ffi_drop__o__inject x1 x2 x3 x4 =
  __

(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
let rec nat_plus_pos n p =
  match n with
  | Nat.O -> p
  | Nat.S m -> Positive.succ (nat_plus_pos m p)

(** val alloc_pair :
    GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
    GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1 **)
let alloc_pair clearme m' l h l' h' x =
  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
  (fun clearme0 ->
  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
  (fun l0 h0 l'0 h'0 _ _ ->
  Extralib.eq_rect_Type0_r nx' (fun _ h1 ->
    h1 { GenMem.blocks =
      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
        nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
        ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
      (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
        nx' }.GenMem.nextblock) } { GenMem.blocks =
      (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
        nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
        ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
      (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
        nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x

(** val prod_jmdiscr :
    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
let prod_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { Types.fst = a0; Types.snd = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val related_globals_rect_Type4 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_rect_Type5 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_rect_Type3 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_rect_Type2 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_rect_Type1 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_rect_Type0 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    -> 'a3 **)
let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
  h_mk_related_globals __ __ __ __

(** val related_globals_inv_rect_Type4 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
    -> 'a3) -> 'a3 **)
let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __

(** val related_globals_inv_rect_Type3 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
    -> 'a3) -> 'a3 **)
let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __

(** val related_globals_inv_rect_Type2 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
    -> 'a3) -> 'a3 **)
let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __

(** val related_globals_inv_rect_Type1 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
    -> 'a3) -> 'a3 **)
let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __

(** val related_globals_inv_rect_Type0 :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
    -> 'a3) -> 'a3 **)
let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __

(** val related_globals_discr :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
let related_globals_discr a3 a4 a5 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __

(** val related_globals_jmdiscr :
    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
let related_globals_jmdiscr a3 a4 a5 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __

(** val related_globals_gen_rect_Type4 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_rect_Type5 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_rect_Type3 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_rect_Type2 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_rect_Type1 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_rect_Type0 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> 'a3) -> 'a3 **)
let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
  h_mk_related_globals_gen __ __ __ __

(** val related_globals_gen_inv_rect_Type4 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __

(** val related_globals_gen_inv_rect_Type3 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __

(** val related_globals_gen_inv_rect_Type2 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __

(** val related_globals_gen_inv_rect_Type1 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __

(** val related_globals_gen_inv_rect_Type0 :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __

(** val related_globals_gen_discr :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
let related_globals_gen_discr a1 a4 a5 a6 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __

(** val related_globals_gen_jmdiscr :
    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
let related_globals_gen_jmdiscr a1 a4 a5 a6 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __

open Extra_bool