open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

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 ByteValues

open BackEndOps

open Joint

type move_dst =
| PSD of Registers.register
| HDW of I8051.register

(** val move_dst_rect_Type4 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type4 h_PSD h_HDW = function
| PSD x_18499 -> h_PSD x_18499
| HDW x_18500 -> h_HDW x_18500

(** val move_dst_rect_Type5 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type5 h_PSD h_HDW = function
| PSD x_18504 -> h_PSD x_18504
| HDW x_18505 -> h_HDW x_18505

(** val move_dst_rect_Type3 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type3 h_PSD h_HDW = function
| PSD x_18509 -> h_PSD x_18509
| HDW x_18510 -> h_HDW x_18510

(** val move_dst_rect_Type2 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type2 h_PSD h_HDW = function
| PSD x_18514 -> h_PSD x_18514
| HDW x_18515 -> h_HDW x_18515

(** val move_dst_rect_Type1 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type1 h_PSD h_HDW = function
| PSD x_18519 -> h_PSD x_18519
| HDW x_18520 -> h_HDW x_18520

(** val move_dst_rect_Type0 :
    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
let rec move_dst_rect_Type0 h_PSD h_HDW = function
| PSD x_18524 -> h_PSD x_18524
| HDW x_18525 -> h_HDW x_18525

(** val move_dst_inv_rect_Type4 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type4 hterm h1 h2 =
  let hcut = move_dst_rect_Type4 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type3 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type3 hterm h1 h2 =
  let hcut = move_dst_rect_Type3 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type2 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type2 hterm h1 h2 =
  let hcut = move_dst_rect_Type2 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type1 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type1 hterm h1 h2 =
  let hcut = move_dst_rect_Type1 h1 h2 hterm in hcut __

(** val move_dst_inv_rect_Type0 :
    move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
    'a1) -> 'a1 **)
let move_dst_inv_rect_Type0 hterm h1 h2 =
  let hcut = move_dst_rect_Type0 h1 h2 hterm in hcut __

(** val move_dst_discr : move_dst -> move_dst -> __ **)
let move_dst_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val move_dst_jmdiscr : move_dst -> move_dst -> __ **)
let move_dst_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | PSD a0 -> Obj.magic (fun _ dH -> dH __)
     | HDW a0 -> Obj.magic (fun _ dH -> dH __)) y

type move_src = move_dst Joint.argument

(** val move_src_from_dst : move_dst -> move_src **)
let move_src_from_dst x =
  Joint.Reg x

(** val dpi1__o__move_dst_to_src__o__inject :
    (move_dst, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__move_dst_to_src__o__inject x2 =
  move_src_from_dst x2.Types.dpi1

(** val eject__o__move_dst_to_src__o__inject :
    move_dst Types.sig0 -> move_src Types.sig0 **)
let eject__o__move_dst_to_src__o__inject x2 =
  move_src_from_dst (Types.pi1 x2)

(** val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0 **)
let move_dst_to_src__o__inject x1 =
  move_src_from_dst x1

(** val dpi1__o__move_dst_to_src :
    (move_dst, 'a1) Types.dPair -> move_src **)
let dpi1__o__move_dst_to_src x1 =
  move_src_from_dst x1.Types.dpi1

(** val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src **)
let eject__o__move_dst_to_src x1 =
  move_src_from_dst (Types.pi1 x1)

(** val psd_argument_move_src : Joint.psd_argument -> move_src **)
let psd_argument_move_src = function
| Joint.Reg r -> Joint.Reg (PSD r)
| Joint.Imm b -> Joint.Imm b

(** val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    BitVector.byte -> move_src Types.sig0 **)
let byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
  psd_argument_move_src (Joint.psd_argument_from_byte x0)

(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x2)

(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x2)

(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x2)

(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x2)

(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x2)

(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    Registers.register Types.sig0 -> move_src Types.sig0 **)
let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x2)

(** val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
    Registers.register -> move_src Types.sig0 **)
let reg_to_psd_argument__o__psd_argument_to_move_src__o__inject x0 =
  psd_argument_move_src (Joint.psd_argument_from_reg x0)

(** val dpi1__o__psd_argument_to_move_src__o__inject :
    (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src x2.Types.dpi1

(** val eject__o__psd_argument_to_move_src__o__inject :
    Joint.psd_argument Types.sig0 -> move_src Types.sig0 **)
let eject__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_move_src (Types.pi1 x2)

(** val psd_argument_to_move_src__o__inject :
    Joint.psd_argument -> move_src Types.sig0 **)
let psd_argument_to_move_src__o__inject x1 =
  psd_argument_move_src x1

(** val byte_to_psd_argument__o__psd_argument_to_move_src :
    BitVector.byte -> move_src **)
let byte_to_psd_argument__o__psd_argument_to_move_src x0 =
  psd_argument_move_src (Joint.psd_argument_from_byte x0)

(** val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
    (BitVector.byte, 'a1) Types.dPair -> move_src **)
let dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.dpi1__o__byte_to_hdw_argument x1)

(** val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
    (BitVector.byte, 'a1) Types.dPair -> move_src **)
let dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.dpi1__o__byte_to_psd_argument x1)

(** val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
    (Registers.register, 'a1) Types.dPair -> move_src **)
let dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.dpi1__o__reg_to_psd_argument x1)

(** val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
    BitVector.byte Types.sig0 -> move_src **)
let eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.eject__o__byte_to_hdw_argument x1)

(** val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
    BitVector.byte Types.sig0 -> move_src **)
let eject__o__byte_to_psd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.eject__o__byte_to_psd_argument x1)

(** val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
    Registers.register Types.sig0 -> move_src **)
let eject__o__reg_to_psd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.eject__o__reg_to_psd_argument x1)

(** val reg_to_psd_argument__o__psd_argument_to_move_src :
    Registers.register -> move_src **)
let reg_to_psd_argument__o__psd_argument_to_move_src x0 =
  psd_argument_move_src (Joint.psd_argument_from_reg x0)

(** val dpi1__o__psd_argument_to_move_src :
    (Joint.psd_argument, 'a1) Types.dPair -> move_src **)
let dpi1__o__psd_argument_to_move_src x1 =
  psd_argument_move_src x1.Types.dpi1

(** val eject__o__psd_argument_to_move_src :
    Joint.psd_argument Types.sig0 -> move_src **)
let eject__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Types.pi1 x1)

type ertl_seq =
| Ertl_new_frame
| Ertl_del_frame
| Ertl_frame_size of Registers.register

(** val ertl_seq_rect_Type4 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type4 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18564 -> h_ertl_frame_size x_18564

(** val ertl_seq_rect_Type5 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type5 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18569 -> h_ertl_frame_size x_18569

(** val ertl_seq_rect_Type3 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type3 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18574 -> h_ertl_frame_size x_18574

(** val ertl_seq_rect_Type2 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type2 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18579 -> h_ertl_frame_size x_18579

(** val ertl_seq_rect_Type1 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type1 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18584 -> h_ertl_frame_size x_18584

(** val ertl_seq_rect_Type0 :
    'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1 **)
let rec ertl_seq_rect_Type0 h_ertl_new_frame h_ertl_del_frame h_ertl_frame_size = function
| Ertl_new_frame -> h_ertl_new_frame
| Ertl_del_frame -> h_ertl_del_frame
| Ertl_frame_size x_18589 -> h_ertl_frame_size x_18589

(** val ertl_seq_inv_rect_Type4 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type4 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type4 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type3 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type3 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type3 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type2 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type2 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type2 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type1 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type1 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type1 h1 h2 h3 hterm in hcut __

(** val ertl_seq_inv_rect_Type0 :
    ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ ->
    'a1) -> 'a1 **)
let ertl_seq_inv_rect_Type0 hterm h1 h2 h3 =
  let hcut = ertl_seq_rect_Type0 h1 h2 h3 hterm in hcut __

(** val ertl_seq_discr : ertl_seq -> ertl_seq -> __ **)
let ertl_seq_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __ **)
let ertl_seq_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Ertl_new_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_del_frame -> Obj.magic (fun _ dH -> dH)
     | Ertl_frame_size a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val eRTL_uns : Joint.unserialized_params **)
let eRTL_uns =
  { Joint.ext_seq_labels = (fun x -> List.Nil); Joint.has_tailcalls =
    Bool.False }

(** val regs_from_move_dst : move_dst -> Registers.register List.list **)
let regs_from_move_dst = function
| PSD r -> List.Cons (r, List.Nil)
| HDW x -> List.Nil

(** val regs_from_move_src : move_src -> Registers.register List.list **)
let regs_from_move_src = function
| Joint.Reg r ->
  (match r with
   | PSD r1 -> List.Cons (r1, List.Nil)
   | HDW x -> List.Nil)
| Joint.Imm x -> List.Nil

(** val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list **)
let ertl_ext_seq_regs = function
| Ertl_new_frame -> List.Nil
| Ertl_del_frame -> List.Nil
| Ertl_frame_size r -> List.Cons (r, List.Nil)

(** val eRTL_functs : Joint.get_pseudo_reg_functs **)
let eRTL_functs =
  { Joint.acc_a_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
    Joint.acc_b_regs = (fun r -> List.Cons ((Obj.magic r), List.Nil));
    Joint.acc_a_args = (fun arg ->
    match Obj.magic arg with
    | Joint.Reg r -> List.Cons (r, List.Nil)
    | Joint.Imm x -> List.Nil); Joint.acc_b_args = (fun arg ->
    match Obj.magic arg with
    | Joint.Reg r -> List.Cons (r, List.Nil)
    | Joint.Imm x -> List.Nil); Joint.dpl_regs = (fun r -> List.Cons
    ((Obj.magic r), List.Nil)); Joint.dph_regs = (fun r -> List.Cons
    ((Obj.magic r), List.Nil)); Joint.dpl_args = (fun arg ->
    match Obj.magic arg with
    | Joint.Reg r -> List.Cons (r, List.Nil)
    | Joint.Imm x -> List.Nil); Joint.dph_args = (fun arg ->
    match Obj.magic arg with
    | Joint.Reg r -> List.Cons (r, List.Nil)
    | Joint.Imm x -> List.Nil); Joint.snd_args = (fun arg ->
    match Obj.magic arg with
    | Joint.Reg r -> List.Cons (r, List.Nil)
    | Joint.Imm x -> List.Nil); Joint.pair_move_regs = (fun x ->
    List.append (regs_from_move_dst (Obj.magic x).Types.fst)
      (regs_from_move_src (Obj.magic x).Types.snd)); Joint.f_call_args =
    (fun x -> List.Nil); Joint.f_call_dest = (fun x -> List.Nil);
    Joint.ext_seq_regs = (Obj.magic ertl_ext_seq_regs); Joint.params_regs =
    (fun x -> List.Nil) }

(** val eRTL : Joint.graph_params **)
let eRTL =
  { Joint.u_pars = eRTL_uns; Joint.functs = eRTL_functs }

type ertl_program = Joint.joint_program

(** val dpi1__o__reg_to_ertl_snd_argument__o__inject :
    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
let dpi1__o__reg_to_ertl_snd_argument__o__inject x2 =
  Joint.psd_argument_from_reg x2.Types.dpi1

(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    (Registers.register, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_to_move_src__o__inject
    (Joint.psd_argument_from_reg x2.Types.dpi1)

(** val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
    (Registers.register, 'a1) Types.dPair -> move_src **)
let dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.psd_argument_from_reg x1.Types.dpi1)

(** val eject__o__reg_to_ertl_snd_argument__o__inject :
    Registers.register Types.sig0 -> Joint.psd_argument Types.sig0 **)
let eject__o__reg_to_ertl_snd_argument__o__inject x2 =
  Joint.psd_argument_from_reg (Types.pi1 x2)

(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    Registers.register Types.sig0 -> move_src Types.sig0 **)
let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_to_move_src__o__inject
    (Joint.psd_argument_from_reg (Types.pi1 x2))

(** val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
    Registers.register Types.sig0 -> move_src **)
let eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.psd_argument_from_reg (Types.pi1 x1))

(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
    Registers.register -> move_src **)
let reg_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
  psd_argument_move_src (Joint.psd_argument_from_reg x0)

(** val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    Registers.register -> move_src Types.sig0 **)
let reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_reg x1)

(** val reg_to_ertl_snd_argument__o__inject :
    Registers.register -> Joint.psd_argument Types.sig0 **)
let reg_to_ertl_snd_argument__o__inject x1 =
  Joint.psd_argument_from_reg x1

(** val dpi1__o__reg_to_ertl_snd_argument :
    (Registers.register, 'a1) Types.dPair -> Joint.psd_argument **)
let dpi1__o__reg_to_ertl_snd_argument x1 =
  Joint.psd_argument_from_reg x1.Types.dpi1

(** val eject__o__reg_to_ertl_snd_argument :
    Registers.register Types.sig0 -> Joint.psd_argument **)
let eject__o__reg_to_ertl_snd_argument x1 =
  Joint.psd_argument_from_reg (Types.pi1 x1)

(** val dpi1__o__byte_to_ertl_snd_argument__o__inject :
    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0 **)
let dpi1__o__byte_to_ertl_snd_argument__o__inject x2 =
  Joint.psd_argument_from_byte x2.Types.dpi1

(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0 **)
let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_to_move_src__o__inject
    (Joint.psd_argument_from_byte x2.Types.dpi1)

(** val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
    (BitVector.byte, 'a1) Types.dPair -> move_src **)
let dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.psd_argument_from_byte x1.Types.dpi1)

(** val eject__o__byte_to_ertl_snd_argument__o__inject :
    BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0 **)
let eject__o__byte_to_ertl_snd_argument__o__inject x2 =
  Joint.psd_argument_from_byte (Types.pi1 x2)

(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    BitVector.byte Types.sig0 -> move_src Types.sig0 **)
let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x2 =
  psd_argument_to_move_src__o__inject
    (Joint.psd_argument_from_byte (Types.pi1 x2))

(** val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
    BitVector.byte Types.sig0 -> move_src **)
let eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src x1 =
  psd_argument_move_src (Joint.psd_argument_from_byte (Types.pi1 x1))

(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
    BitVector.byte -> move_src **)
let byte_to_ertl_snd_argument__o__psd_argument_to_move_src x0 =
  psd_argument_move_src (Joint.psd_argument_from_byte x0)

(** val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
    BitVector.byte -> move_src Types.sig0 **)
let byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject x1 =
  psd_argument_to_move_src__o__inject (Joint.psd_argument_from_byte x1)

(** val byte_to_ertl_snd_argument__o__inject :
    BitVector.byte -> Joint.psd_argument Types.sig0 **)
let byte_to_ertl_snd_argument__o__inject x1 =
  Joint.psd_argument_from_byte x1

(** val dpi1__o__byte_to_ertl_snd_argument :
    (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument **)
let dpi1__o__byte_to_ertl_snd_argument x1 =
  Joint.psd_argument_from_byte x1.Types.dpi1

(** val eject__o__byte_to_ertl_snd_argument :
    BitVector.byte Types.sig0 -> Joint.psd_argument **)
let eject__o__byte_to_ertl_snd_argument x1 =
  Joint.psd_argument_from_byte (Types.pi1 x1)

(** val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq **)
let ertl_seq_joint =
  Obj.magic (fun _ x -> Joint.Extension_seq x)

(** val dpi1__o__ertl_seq_to_joint_seq__o__inject :
    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
    Types.sig0 **)
let dpi1__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
  ertl_seq_joint x1 x2.Types.dpi1

(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
    Types.sig0 **)
let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
  Joint.seq_to_step__o__inject
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
    (ertl_seq_joint x1 x2.Types.dpi1)

(** val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
let dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
  Joint.Step_seq (ertl_seq_joint x1 x2.Types.dpi1)

(** val eject__o__ertl_seq_to_joint_seq__o__inject :
    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
let eject__o__ertl_seq_to_joint_seq__o__inject x1 x2 =
  ertl_seq_joint x1 (Types.pi1 x2)

(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
let eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
  Joint.seq_to_step__o__inject
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x1
    (ertl_seq_joint x1 (Types.pi1 x2))

(** val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
let eject__o__ertl_seq_to_joint_seq__o__seq_to_step x1 x2 =
  Joint.Step_seq (ertl_seq_joint x1 (Types.pi1 x2))

(** val ertl_seq_to_joint_seq__o__seq_to_step :
    AST.ident List.list -> __ -> Joint.joint_step **)
let ertl_seq_to_joint_seq__o__seq_to_step x0 x1 =
  Joint.Step_seq (ertl_seq_joint x0 x1)

(** val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
let ertl_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
  Joint.seq_to_step__o__inject
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars eRTL) x0
    (ertl_seq_joint x0 x1)

(** val ertl_seq_to_joint_seq__o__inject :
    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
let ertl_seq_to_joint_seq__o__inject x0 x1 =
  ertl_seq_joint x0 x1

(** val dpi1__o__ertl_seq_to_joint_seq :
    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
let dpi1__o__ertl_seq_to_joint_seq x1 x2 =
  ertl_seq_joint x1 x2.Types.dpi1

(** val eject__o__ertl_seq_to_joint_seq :
    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
let eject__o__ertl_seq_to_joint_seq x1 x2 =
  ertl_seq_joint x1 (Types.pi1 x2)

(** val eRTL_premain :
    ertl_program -> Joint.joint_closed_internal_function **)
let eRTL_premain p =
  let l1 = Positive.One in
  let l2 = Positive.P0 Positive.One in
  let l3 = Positive.P1 Positive.One in
  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
    Positive.One)); Joint.joint_if_runiverse = Positive.One;
    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
    Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
    Joint.joint_if_code =
    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
    Joint.joint_if_entry = (Obj.magic l1) }
  in
  let res0 =
    Joint.add_graph eRTL
      (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l1
      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
      (Obj.magic l2))) res
  in
  let res1 =
    Joint.add_graph eRTL
      (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l2
      (Joint.Sequential ((Joint.CALL ((Types.Inl
      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
      (Obj.magic Types.It))), (Obj.magic l3))) res0
  in
  let res2 =
    Joint.add_graph eRTL
      (Joint.prog_names (Joint.graph_params_to_params eRTL) p) l3
      (Joint.Final (Joint.GOTO l3)) res1
  in
  res2