open Preamble

open ExtraGlobalenvs

open I8051bis

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open BackEndOps

open Joint

open BEMem

open CostLabel

open Events

open IOMonad

open IO

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

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 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 Globalenvs

open Joint_semantics

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open ExtraMonads

(** val reg_store :
    PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
    Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map **)
let reg_store reg v locals =
  Identifiers.add PreIdentifiers.RegisterTag locals reg v

(** val reg_retrieve :
    ByteValues.beval Registers.register_env -> Registers.register ->
    ByteValues.beval Errors.res **)
let reg_retrieve locals reg =
  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
    (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
    (Identifiers.lookup PreIdentifiers.RegisterTag locals reg)

type hw_register_env = { reg_env : ByteValues.beval
                                   BitVectorTrie.bitVectorTrie;
                         other_bit : ByteValues.bebit }

(** val hw_register_env_rect_Type4 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_25009 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25009 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val hw_register_env_rect_Type5 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_25011 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25011 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val hw_register_env_rect_Type3 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_25013 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25013 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val hw_register_env_rect_Type2 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_25015 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25015 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val hw_register_env_rect_Type1 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_25017 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25017 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val hw_register_env_rect_Type0 :
    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    -> hw_register_env -> 'a1 **)
let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_25019 =
  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25019 in
  h_mk_hw_register_env reg_env0 other_bit0

(** val reg_env :
    hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie **)
let rec reg_env xxx =
  xxx.reg_env

(** val other_bit : hw_register_env -> ByteValues.bebit **)
let rec other_bit xxx =
  xxx.other_bit

(** val hw_register_env_inv_rect_Type4 :
    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
let hw_register_env_inv_rect_Type4 hterm h1 =
  let hcut = hw_register_env_rect_Type4 h1 hterm in hcut __

(** val hw_register_env_inv_rect_Type3 :
    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
let hw_register_env_inv_rect_Type3 hterm h1 =
  let hcut = hw_register_env_rect_Type3 h1 hterm in hcut __

(** val hw_register_env_inv_rect_Type2 :
    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
let hw_register_env_inv_rect_Type2 hterm h1 =
  let hcut = hw_register_env_rect_Type2 h1 hterm in hcut __

(** val hw_register_env_inv_rect_Type1 :
    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
let hw_register_env_inv_rect_Type1 hterm h1 =
  let hcut = hw_register_env_rect_Type1 h1 hterm in hcut __

(** val hw_register_env_inv_rect_Type0 :
    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
let hw_register_env_inv_rect_Type0 hterm h1 =
  let hcut = hw_register_env_rect_Type0 h1 hterm in hcut __

(** val hw_register_env_discr : hw_register_env -> hw_register_env -> __ **)
let hw_register_env_discr x y =
  Logic.eq_rect_Type2 x
    (let { reg_env = a0; other_bit = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val hw_register_env_jmdiscr :
    hw_register_env -> hw_register_env -> __ **)
let hw_register_env_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { reg_env = a0; other_bit = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val hwreg_retrieve :
    hw_register_env -> I8051.register -> ByteValues.beval **)
let hwreg_retrieve env r =
  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
    (I8051.bitvector_of_register r) env.reg_env ByteValues.BVundef

(** val hwreg_store :
    I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env **)
let hwreg_store r v env =
  { reg_env =
    (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))) (I8051.bitvector_of_register r) v env.reg_env); other_bit =
    env.other_bit }

(** val hwreg_set_other :
    ByteValues.bebit -> hw_register_env -> hw_register_env **)
let hwreg_set_other v env =
  { reg_env = env.reg_env; other_bit = v }

(** val hwreg_retrieve_sp :
    hw_register_env -> ByteValues.xpointer Errors.res **)
let hwreg_retrieve_sp env =
  let spl = hwreg_retrieve env I8051.registerSPL in
  let sph = hwreg_retrieve env I8051.registerSPH in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (BEMem.pointer_of_address { Types.fst = spl; Types.snd = sph }))
      (fun ptr ->
      (match Pointers.ptype ptr with
       | AST.XData ->
         (fun _ -> Monad.m_return0 (Monad.max_def Errors.res0) ptr)
       | AST.Code ->
         (fun _ ->
           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
             ErrorMessages.BadPointer), List.Nil))))) __))

(** val hwreg_store_sp :
    hw_register_env -> ByteValues.xpointer -> hw_register_env **)
let hwreg_store_sp env sp =
  let { Types.fst = spl; Types.snd = sph } =
    ByteValues.beval_pair_of_pointer (Types.pi1 sp)
  in
  hwreg_store I8051.registerSPH sph (hwreg_store I8051.registerSPL spl env)

(** val init_hw_register_env : ByteValues.xpointer -> hw_register_env **)
let init_hw_register_env =
  hwreg_store_sp { reg_env = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S (Nat.S Nat.O))))))); other_bit = ByteValues.BBundef }

type sem_graph_params = { sgp_pars : Joint.uns_params;
                          sgp_sup : (__ -> __
                                    Joint_semantics.sem_unserialized_params);
                          graph_pre_main_generator : (Joint.joint_program ->
                                                     Joint.joint_closed_internal_function) }

(** val sem_graph_params_rect_Type4 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_25035 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25035
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sem_graph_params_rect_Type5 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_25037 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25037
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sem_graph_params_rect_Type3 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_25039 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25039
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sem_graph_params_rect_Type2 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_25041 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25041
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sem_graph_params_rect_Type1 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_25043 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25043
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sem_graph_params_rect_Type0 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_graph_params -> 'a1 **)
let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_25045 =
  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    graph_pre_main_generator0 } = x_25045
  in
  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0

(** val sgp_pars : sem_graph_params -> Joint.uns_params **)
let rec sgp_pars xxx =
  xxx.sgp_pars

(** val sgp_sup0 :
    sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params **)
let rec sgp_sup0 xxx =
  (let { sgp_pars = x; sgp_sup = yyy; graph_pre_main_generator = x0 } = xxx
   in
  Obj.magic yyy) __

(** val graph_pre_main_generator :
    sem_graph_params -> Joint.joint_program ->
    Joint.joint_closed_internal_function **)
let rec graph_pre_main_generator xxx =
  xxx.graph_pre_main_generator

(** val sem_graph_params_inv_rect_Type4 :
    sem_graph_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_graph_params_inv_rect_Type4 hterm h1 =
  let hcut = sem_graph_params_rect_Type4 h1 hterm in hcut __

(** val sem_graph_params_inv_rect_Type3 :
    sem_graph_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_graph_params_inv_rect_Type3 hterm h1 =
  let hcut = sem_graph_params_rect_Type3 h1 hterm in hcut __

(** val sem_graph_params_inv_rect_Type2 :
    sem_graph_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_graph_params_inv_rect_Type2 hterm h1 =
  let hcut = sem_graph_params_rect_Type2 h1 hterm in hcut __

(** val sem_graph_params_inv_rect_Type1 :
    sem_graph_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_graph_params_inv_rect_Type1 hterm h1 =
  let hcut = sem_graph_params_rect_Type1 h1 hterm in hcut __

(** val sem_graph_params_inv_rect_Type0 :
    sem_graph_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_graph_params_inv_rect_Type0 hterm h1 =
  let hcut = sem_graph_params_rect_Type0 h1 hterm in hcut __

(** val sem_graph_params_jmdiscr :
    sem_graph_params -> sem_graph_params -> __ **)
let sem_graph_params_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { sgp_pars = a0; sgp_sup = a1; graph_pre_main_generator = a2 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val sem_graph_params_to_graph_params :
    sem_graph_params -> Joint.graph_params **)
let sem_graph_params_to_graph_params pars =
  pars.sgp_pars

(** val sem_graph_params_to_sem_params :
    sem_graph_params -> Joint_semantics.sem_params **)
let sem_graph_params_to_sem_params pars =
  { Joint_semantics.spp' = { Joint_semantics.spp =
    (let x = sem_graph_params_to_graph_params pars in
    Joint.graph_params_to_params x); Joint_semantics.msu_pars =
    (sgp_sup0 pars); Joint_semantics.offset_of_point =
    (Obj.magic (Identifiers.word_of_identifier PreIdentifiers.LabelTag));
    Joint_semantics.point_of_offset = (Obj.magic (fun x -> x)) };
    Joint_semantics.pre_main_generator = pars.graph_pre_main_generator }

(** val sem_params_from_sem_graph_params__o__spp' :
    sem_graph_params -> Joint_semantics.serialized_params **)
let sem_params_from_sem_graph_params__o__spp' x0 =
  (sem_graph_params_to_sem_params x0).Joint_semantics.spp'

(** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
    sem_graph_params -> Joint.joint_closed_internal_function
    Joint_semantics.sem_unserialized_params **)
let sem_params_from_sem_graph_params__o__spp'__o__msu_pars x0 =
  Joint_semantics.spp'__o__msu_pars (sem_graph_params_to_sem_params x0)

(** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
    sem_graph_params -> Joint_semantics.sem_state_params **)
let sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars x0 =
  Joint_semantics.spp'__o__msu_pars__o__st_pars
    (sem_graph_params_to_sem_params x0)

(** val sem_params_from_sem_graph_params__o__spp'__o__spp :
    sem_graph_params -> Joint.params **)
let sem_params_from_sem_graph_params__o__spp'__o__spp x0 =
  Joint_semantics.spp'__o__spp (sem_graph_params_to_sem_params x0)

(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
    sem_graph_params -> Joint.stmt_params **)
let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars
    (sem_graph_params_to_sem_params x0)

(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    sem_graph_params -> Joint.uns_params **)
let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
    (sem_graph_params_to_sem_params x0)

(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    sem_graph_params -> Joint.unserialized_params **)
let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    (sem_graph_params_to_sem_params x0)

type sem_lin_params = { slp_pars : Joint.uns_params;
                        slp_sup : (__ -> __
                                  Joint_semantics.sem_unserialized_params);
                        lin_pre_main_generator : (Joint.joint_program ->
                                                 Joint.joint_closed_internal_function) }

(** val sem_lin_params_rect_Type4 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_25062 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25062
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val sem_lin_params_rect_Type5 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_25064 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25064
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val sem_lin_params_rect_Type3 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_25066 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25066
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val sem_lin_params_rect_Type2 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_25068 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25068
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val sem_lin_params_rect_Type1 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_25070 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25070
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val sem_lin_params_rect_Type0 :
    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    -> sem_lin_params -> 'a1 **)
let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_25072 =
  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    lin_pre_main_generator0 } = x_25072
  in
  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0

(** val slp_pars : sem_lin_params -> Joint.uns_params **)
let rec slp_pars xxx =
  xxx.slp_pars

(** val slp_sup0 :
    sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params **)
let rec slp_sup0 xxx =
  (let { slp_pars = x; slp_sup = yyy; lin_pre_main_generator = x0 } = xxx in
  Obj.magic yyy) __

(** val lin_pre_main_generator :
    sem_lin_params -> Joint.joint_program ->
    Joint.joint_closed_internal_function **)
let rec lin_pre_main_generator xxx =
  xxx.lin_pre_main_generator

(** val sem_lin_params_inv_rect_Type4 :
    sem_lin_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_lin_params_inv_rect_Type4 hterm h1 =
  let hcut = sem_lin_params_rect_Type4 h1 hterm in hcut __

(** val sem_lin_params_inv_rect_Type3 :
    sem_lin_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_lin_params_inv_rect_Type3 hterm h1 =
  let hcut = sem_lin_params_rect_Type3 h1 hterm in hcut __

(** val sem_lin_params_inv_rect_Type2 :
    sem_lin_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_lin_params_inv_rect_Type2 hterm h1 =
  let hcut = sem_lin_params_rect_Type2 h1 hterm in hcut __

(** val sem_lin_params_inv_rect_Type1 :
    sem_lin_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_lin_params_inv_rect_Type1 hterm h1 =
  let hcut = sem_lin_params_rect_Type1 h1 hterm in hcut __

(** val sem_lin_params_inv_rect_Type0 :
    sem_lin_params -> (Joint.uns_params -> (__ -> __
    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
let sem_lin_params_inv_rect_Type0 hterm h1 =
  let hcut = sem_lin_params_rect_Type0 h1 hterm in hcut __

(** val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __ **)
let sem_lin_params_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { slp_pars = a0; slp_sup = a1; lin_pre_main_generator = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params **)
let sem_lin_params_to_lin_params pars =
  pars.slp_pars

(** val sem_lin_params_to_sem_params :
    sem_lin_params -> Joint_semantics.sem_params **)
let sem_lin_params_to_sem_params pars =
  { Joint_semantics.spp' = { Joint_semantics.spp =
    (let x = sem_lin_params_to_lin_params pars in
    Joint.lin_params_to_params x); Joint_semantics.msu_pars =
    (slp_sup0 pars); Joint_semantics.offset_of_point =
    (Obj.magic Positive.succ_pos_of_nat); Joint_semantics.point_of_offset =
    (fun p -> Obj.magic (Nat.pred (Positive.nat_of_pos p))) };
    Joint_semantics.pre_main_generator = pars.lin_pre_main_generator }

(** val sem_params_from_sem_lin_params__o__spp' :
    sem_lin_params -> Joint_semantics.serialized_params **)
let sem_params_from_sem_lin_params__o__spp' x0 =
  (sem_lin_params_to_sem_params x0).Joint_semantics.spp'

(** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
    sem_lin_params -> Joint.joint_closed_internal_function
    Joint_semantics.sem_unserialized_params **)
let sem_params_from_sem_lin_params__o__spp'__o__msu_pars x0 =
  Joint_semantics.spp'__o__msu_pars (sem_lin_params_to_sem_params x0)

(** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
    sem_lin_params -> Joint_semantics.sem_state_params **)
let sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars x0 =
  Joint_semantics.spp'__o__msu_pars__o__st_pars
    (sem_lin_params_to_sem_params x0)

(** val sem_params_from_sem_lin_params__o__spp'__o__spp :
    sem_lin_params -> Joint.params **)
let sem_params_from_sem_lin_params__o__spp'__o__spp x0 =
  Joint_semantics.spp'__o__spp (sem_lin_params_to_sem_params x0)

(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
    sem_lin_params -> Joint.stmt_params **)
let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars
    (sem_lin_params_to_sem_params x0)

(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    sem_lin_params -> Joint.uns_params **)
let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
    (sem_lin_params_to_sem_params x0)

(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    sem_lin_params -> Joint.unserialized_params **)
let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    (sem_lin_params_to_sem_params x0)

(** val match_genv_t_rect_Type4 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type4 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_rect_Type5 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type5 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_rect_Type3 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type3 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_rect_Type2 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type2 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_rect_Type1 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type1 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_rect_Type0 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let rec match_genv_t_rect_Type0 m vars ge1 ge2 h_mk_match_genv_t =
  h_mk_match_genv_t __ __ __

(** val match_genv_t_inv_rect_Type4 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let match_genv_t_inv_rect_Type4 x1 x2 x3 x4 h1 =
  let hcut = match_genv_t_rect_Type4 x1 x2 x3 x4 h1 in hcut __

(** val match_genv_t_inv_rect_Type3 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let match_genv_t_inv_rect_Type3 x1 x2 x3 x4 h1 =
  let hcut = match_genv_t_rect_Type3 x1 x2 x3 x4 h1 in hcut __

(** val match_genv_t_inv_rect_Type2 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let match_genv_t_inv_rect_Type2 x1 x2 x3 x4 h1 =
  let hcut = match_genv_t_rect_Type2 x1 x2 x3 x4 h1 in hcut __

(** val match_genv_t_inv_rect_Type1 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let match_genv_t_inv_rect_Type1 x1 x2 x3 x4 h1 =
  let hcut = match_genv_t_rect_Type1 x1 x2 x3 x4 h1 in hcut __

(** val match_genv_t_inv_rect_Type0 :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let match_genv_t_inv_rect_Type0 x1 x2 x3 x4 h1 =
  let hcut = match_genv_t_rect_Type0 x1 x2 x3 x4 h1 in hcut __

(** val match_genv_t_discr :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> __ **)
let match_genv_t_discr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val match_genv_t_jmdiscr :
    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    Globalenvs.genv_t -> __ **)
let match_genv_t_jmdiscr a1 a2 a3 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __

(** val joint_globalenv :
    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> Joint_semantics.genv **)
let joint_globalenv p prog stacksizes =
  let genv = Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog in
  let pc_from_lbl = fun bl fn lbl ->
    Monad.m_bind0 (Monad.max_def Option.option)
      (Obj.magic
        ((Joint_semantics.spp'__o__spp p).Joint.point_of_label
          (Joint.prog_names (Joint_semantics.spp'__o__spp p) prog)
          (Types.pi1 fn).Joint.joint_if_code lbl)) (fun pt ->
      Monad.m_return0 (Monad.max_def Option.option) { ByteValues.pc_block =
        bl; ByteValues.pc_offset =
        (p.Joint_semantics.spp'.Joint_semantics.offset_of_point pt) })
  in
  { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = stacksizes;
  Joint_semantics.premain = (p.Joint_semantics.pre_main_generator prog);
  Joint_semantics.pc_from_label = (Obj.magic pc_from_lbl) }