open Preamble

open BitVectorTrie

open Graphs

open Order

open Registers

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open FrontEndOps

open CostLabel

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Types

open AST

open Hints_declaration

open Core_notation

open Pts

open Logic

open RTLabs_syntax

open Extra_bool

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open I8051

open BackEndOps

open Joint

open RTL

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

(** val size_of_sig_type : AST.typ -> Nat.nat **)
let size_of_sig_type = function
| AST.ASTint (isize, sign) ->
  (match isize with
   | AST.I8 -> Nat.S Nat.O
   | AST.I16 -> Nat.S (Nat.S Nat.O)
   | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
| AST.ASTptr -> Nat.S (Nat.S Nat.O)

(** val sign_of_sig_type : AST.typ -> AST.signedness **)
let sign_of_sig_type = function
| AST.ASTint (x, sign) -> sign
| AST.ASTptr -> AST.Unsigned

type register_type =
| Register_int of Registers.register
| Register_ptr of Registers.register * Registers.register

(** val register_type_rect_Type4 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type4 h_register_int h_register_ptr = function
| Register_int x_18380 -> h_register_int x_18380
| Register_ptr (x_18382, x_18381) -> h_register_ptr x_18382 x_18381

(** val register_type_rect_Type5 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type5 h_register_int h_register_ptr = function
| Register_int x_18386 -> h_register_int x_18386
| Register_ptr (x_18388, x_18387) -> h_register_ptr x_18388 x_18387

(** val register_type_rect_Type3 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type3 h_register_int h_register_ptr = function
| Register_int x_18392 -> h_register_int x_18392
| Register_ptr (x_18394, x_18393) -> h_register_ptr x_18394 x_18393

(** val register_type_rect_Type2 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type2 h_register_int h_register_ptr = function
| Register_int x_18398 -> h_register_int x_18398
| Register_ptr (x_18400, x_18399) -> h_register_ptr x_18400 x_18399

(** val register_type_rect_Type1 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type1 h_register_int h_register_ptr = function
| Register_int x_18404 -> h_register_int x_18404
| Register_ptr (x_18406, x_18405) -> h_register_ptr x_18406 x_18405

(** val register_type_rect_Type0 :
    (Registers.register -> 'a1) -> (Registers.register -> Registers.register
    -> 'a1) -> register_type -> 'a1 **)
let rec register_type_rect_Type0 h_register_int h_register_ptr = function
| Register_int x_18410 -> h_register_int x_18410
| Register_ptr (x_18412, x_18411) -> h_register_ptr x_18412 x_18411

(** val register_type_inv_rect_Type4 :
    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
    -> Registers.register -> __ -> 'a1) -> 'a1 **)
let register_type_inv_rect_Type4 hterm h1 h2 =
  let hcut = register_type_rect_Type4 h1 h2 hterm in hcut __

(** val register_type_inv_rect_Type3 :
    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
    -> Registers.register -> __ -> 'a1) -> 'a1 **)
let register_type_inv_rect_Type3 hterm h1 h2 =
  let hcut = register_type_rect_Type3 h1 h2 hterm in hcut __

(** val register_type_inv_rect_Type2 :
    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
    -> Registers.register -> __ -> 'a1) -> 'a1 **)
let register_type_inv_rect_Type2 hterm h1 h2 =
  let hcut = register_type_rect_Type2 h1 h2 hterm in hcut __

(** val register_type_inv_rect_Type1 :
    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
    -> Registers.register -> __ -> 'a1) -> 'a1 **)
let register_type_inv_rect_Type1 hterm h1 h2 =
  let hcut = register_type_rect_Type1 h1 h2 hterm in hcut __

(** val register_type_inv_rect_Type0 :
    register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
    -> Registers.register -> __ -> 'a1) -> 'a1 **)
let register_type_inv_rect_Type0 hterm h1 h2 =
  let hcut = register_type_rect_Type0 h1 h2 hterm in hcut __

(** val register_type_discr : register_type -> register_type -> __ **)
let register_type_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
     | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

(** val register_type_jmdiscr : register_type -> register_type -> __ **)
let register_type_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Register_int a0 -> Obj.magic (fun _ dH -> dH __)
     | Register_ptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y

type local_env = Registers.register List.list Identifiers.identifier_map

(** val find_local_env :
    PreIdentifiers.identifier -> local_env -> Registers.register List.list **)
let find_local_env r lenv =
  Option.opt_safe (Identifiers.lookup PreIdentifiers.RegisterTag lenv r)

(** val find_local_env_arg :
    Registers.register -> local_env -> Joint.psd_argument List.list **)
let find_local_env_arg r lenv =
  List.map (fun x -> Joint.Reg x) (find_local_env r lenv)

(** val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __ **)
let rec m_iter m f n m0 =
  match n with
  | Nat.O -> m0
  | Nat.S k -> Monad.m_bind0 m m0 (fun v -> m_iter m f k (f v))

(** val fresh_registers :
    Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
    List.list Monad.smax_def__o__monad **)
let fresh_registers p g n =
  let f = fun acc ->
    Monad.m_bind0 (Monad.smax_def State.state_monad)
      (TranslateUtils.fresh_register p g) (fun m ->
      Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc)))
  in
  m_iter (Monad.smax_def State.state_monad) f n
    (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)

(** val map_list_local_env :
    Registers.register List.list Identifiers.identifier_map ->
    (Registers.register, AST.typ) Types.prod List.list -> Registers.register
    List.list **)
let rec map_list_local_env lenv regs =
  (match regs with
   | List.Nil -> (fun _ -> List.Nil)
   | List.Cons (hd, tl) ->
     (fun _ ->
       List.append (find_local_env hd.Types.fst lenv)
         (map_list_local_env lenv tl))) __

(** val initialize_local_env :
    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
    -> local_env Monad.smax_def__o__monad **)
let initialize_local_env globals registers =
  let f = fun r_sig lenv ->
    let { Types.fst = r; Types.snd = sig0 } = r_sig in
    let size = size_of_sig_type sig0 in
    Monad.m_bind0 (Monad.smax_def State.state_monad)
      (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size)
      (fun regs ->
      Monad.m_return0 (Monad.smax_def State.state_monad)
        (Identifiers.add PreIdentifiers.RegisterTag lenv r regs))
  in
  Monad.m_fold (Monad.smax_def State.state_monad) f registers
    (Identifiers.empty_map PreIdentifiers.RegisterTag)

(** val initialize_locals_params_ret :
    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
    -> (Registers.register, AST.typ) Types.prod List.list ->
    (Registers.register, AST.typ) Types.prod Types.option -> local_env
    Monad.smax_def__o__monad **)
let initialize_locals_params_ret globals locals params ret =
  Obj.magic (fun def ->
    (let { Types.fst = def'; Types.snd = lenv } =
       Obj.magic initialize_local_env globals
         (List.append
           (match ret with
            | Types.None -> List.Nil
            | Types.Some r_sig -> List.Cons (r_sig, List.Nil))
           (List.append locals params)) def
     in
    (fun _ ->
    let params' = map_list_local_env lenv params in
    let ret' =
      (match ret with
       | Types.None -> (fun _ -> List.Nil)
       | Types.Some r_sig -> (fun _ -> find_local_env r_sig.Types.fst lenv))
        __
    in
    let def'' = { Joint.joint_if_luniverse = def'.Joint.joint_if_luniverse;
      Joint.joint_if_runiverse = def'.Joint.joint_if_runiverse;
      Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
      (Obj.magic params'); Joint.joint_if_stacksize =
      def'.Joint.joint_if_stacksize; Joint.joint_if_local_stacksize =
      def'.Joint.joint_if_local_stacksize; Joint.joint_if_code =
      def'.Joint.joint_if_code; Joint.joint_if_entry =
      def'.Joint.joint_if_entry }
    in
    { Types.fst = def''; Types.snd = lenv })) __)

(** val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod **)
let make_addr lst =
  { Types.fst = (Util.nth_safe Nat.O lst); Types.snd =
    (Util.nth_safe (Nat.S Nat.O) lst) }

(** val find_and_addr :
    PreIdentifiers.identifier -> local_env -> (Registers.register,
    Registers.register) Types.prod **)
let find_and_addr r lenv =
  make_addr (find_local_env r lenv)

(** val find_and_addr_arg :
    Registers.register -> local_env -> (Joint.psd_argument,
    Joint.psd_argument) Types.prod **)
let find_and_addr_arg r lenv =
  make_addr (find_local_env_arg r lenv)

(** val rtl_args :
    Registers.register List.list -> local_env -> Joint.psd_argument List.list **)
let rec rtl_args args env =
  (match args with
   | List.Nil -> (fun _ -> List.Nil)
   | List.Cons (hd, tl) ->
     (fun _ -> List.append (find_local_env_arg hd env) (rtl_args tl env))) __

(** val vrsplit :
    Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
    Types.sig0 **)
let rec vrsplit m n =
  match m with
  | Nat.O -> (fun v -> List.Nil)
  | Nat.S k ->
    (fun v ->
      let spl = Vector.vsplit n (Nat.times k n) v in
      List.Cons (spl.Types.fst, (Types.pi1 (vrsplit k n spl.Types.snd))))

(** val split_into_bytes :
    AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0 **)
let split_into_bytes size int =
  List.reverse
    (Types.pi1
      (vrsplit (AST.size_intsize size) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S (Nat.S Nat.O)))))))) int))

(** val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list **)
let rec list_inject_All_aux l =
  (match l with
   | List.Nil -> (fun _ -> List.Nil)
   | List.Cons (hd, tl) ->
     (fun _ -> List.Cons (hd, (list_inject_All_aux tl)))) __

(** val translate_op_aux :
    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    Joint.joint_seq List.list **)
let translate_op_aux globals op destrs srcrs1 srcrs2 =
  Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1)) (Obj.magic destrs)
    (Obj.magic srcrs1) (Obj.magic srcrs2)

(** val translate_op :
    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    Joint.joint_seq List.list **)
let translate_op globals op destrs srcrs1 srcrs2 =
  (match op with
   | BackEndOps.Add ->
     (match destrs with
      | List.Nil -> (fun _ _ -> List.Nil)
      | List.Cons (destr, destrs') ->
        (match srcrs1 with
         | List.Nil -> (fun _ -> assert false (* absurd case *))
         | List.Cons (srcr1, srcrs1') ->
           (fun _ ->
             match srcrs2 with
             | List.Nil -> (fun _ -> assert false (* absurd case *))
             | List.Cons (srcr2, srcrs2') ->
               (fun _ -> List.Cons ((Joint.OP2 (BackEndOps.Add,
                 (Obj.magic destr), (Obj.magic srcr1), (Obj.magic srcr2))),
                 (translate_op_aux globals BackEndOps.Addc destrs' srcrs1'
                   srcrs2'))))))
   | BackEndOps.Addc ->
     (fun _ _ ->
       List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
         (translate_op_aux globals BackEndOps.Addc destrs srcrs1 srcrs2))
   | BackEndOps.Sub ->
     (fun _ _ ->
       List.append (List.Cons (Joint.CLEAR_CARRY, List.Nil))
         (translate_op_aux globals BackEndOps.Sub destrs srcrs1 srcrs2))
   | BackEndOps.And ->
     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
   | BackEndOps.Or ->
     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)
   | BackEndOps.Xor ->
     (fun _ _ -> translate_op_aux globals op destrs srcrs1 srcrs2)) __ __

(** val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list **)
let cast_list deflt new_length l =
  match Nat.leb (List.length l) new_length with
  | Bool.True ->
    List.append l
      (List.make_list deflt (Nat.minus new_length (List.length l)))
  | Bool.False -> List.lhd l new_length

(** val translate_op_asym_unsigned :
    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    Joint.joint_seq List.list **)
let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
  let l = List.length destrs in
  let srcrs1' =
    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
      srcrs1
  in
  let srcrs2' =
    cast_list (let x = Joint.psd_argument_from_byte Joint.zero_byte in x) l
      srcrs2
  in
  translate_op globals op destrs srcrs1' srcrs2'

(** val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
let zero_args size =
  List.make_list (Joint.psd_argument_from_byte Joint.zero_byte) size

(** val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0 **)
let one_args = function
| Nat.O -> List.Nil
| Nat.S k ->
  List.Cons
    ((let x = Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O))
      in
     x), (Types.pi1 (zero_args k)))

(** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
let size_of_cst typ = function
| FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
| FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
| FrontEndOps.Oaddrstack x -> Nat.S (Nat.S Nat.O)

(** val translate_cst :
    AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
    Registers.register List.list -> (Registers.register, Joint.joint_seq
    List.list) Bind_new.bind_new **)
let translate_cst ty globals cst_sig destrs =
  let l =
    (match Types.pi1 cst_sig with
     | FrontEndOps.Ointconst (size, sign, const) ->
       (fun _ _ ->
         Util.map2 (fun r b -> Joint.MOVE
           (Obj.magic { Types.fst = r; Types.snd =
             (Joint.psd_argument_from_byte b) })) destrs
           (Types.pi1 (split_into_bytes size const)))
     | FrontEndOps.Oaddrsymbol (id, offset) ->
       (fun _ _ ->
         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
         let off =
           Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
             (Nat.S (Nat.S Nat.O)))))))))))))))) offset
         in
         List.Cons ((Joint.ADDRESS (id, off, (Obj.magic r1),
         (Obj.magic r2))), List.Nil))
     | FrontEndOps.Oaddrstack offset ->
       (fun _ _ ->
         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
         List.Cons
         ((let x = Joint.Extension_seq
             (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
           in
          x),
         (match Nat.eqb offset Nat.O with
          | Bool.True -> List.Nil
          | Bool.False ->
            translate_op globals BackEndOps.Add (List.Cons (r1, (List.Cons
              (r2, List.Nil)))) (List.Cons ((Joint.psd_argument_from_reg r1),
              (List.Cons ((Joint.psd_argument_from_reg r2), List.Nil))))
              (List.Cons
              ((Joint.psd_argument_from_byte (Joint.byte_of_nat offset)),
              (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
              List.Nil)))))))) __ __
  in
  Bind_new.Bret l

(** val translate_move :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    List.list -> Joint.joint_seq List.list **)
let translate_move globals destrs srcrs =
  Util.map2 (fun dst src -> Joint.MOVE
    (Obj.magic { Types.fst = dst; Types.snd = src })) destrs srcrs

(** val sign_mask :
    AST.ident List.list -> Registers.register -> Joint.psd_argument ->
    Joint.joint_seq List.list **)
let sign_mask globals destr = function
| Joint.Reg srcr ->
  let byte_127 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O))))))), Bool.False,
    (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))
  in
  List.Cons ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
  (Obj.magic (Joint.psd_argument_from_reg srcr)),
  (Obj.magic (Joint.psd_argument_from_byte byte_127)))), (List.Cons
  ((Joint.OP1 (BackEndOps.Rl, (Obj.magic destr), (Obj.magic destr))),
  (List.Cons ((Joint.OP1 (BackEndOps.Inc, (Obj.magic destr),
  (Obj.magic destr))), (List.Cons ((Joint.OP1 (BackEndOps.Cmpl,
  (Obj.magic destr), (Obj.magic destr))), List.Nil)))))))
| Joint.Imm b ->
  (match Arithmetic.sign_bit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
           (Nat.S Nat.O)))))))) b with
   | Bool.True ->
     List.Cons ((Joint.MOVE
       (Obj.magic { Types.fst = destr; Types.snd =
         (let x =
            BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S Nat.O))))))))
          in
         Joint.psd_argument_from_byte x) })), List.Nil)
   | Bool.False ->
     List.Cons ((Joint.MOVE
       (Obj.magic { Types.fst = destr; Types.snd =
         (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil))

(** val translate_cast_signed :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_cast_signed globals destrs srca =
  Bind_new.Bnew (fun tmp ->
    let l =
      List.append (sign_mask globals tmp srca)
        (translate_move globals destrs
          (List.make_list (Joint.Reg tmp) (List.length destrs)))
    in
    Bind_new.Bret l)

(** val translate_fill_with_zero :
    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
    List.list **)
let translate_fill_with_zero globals destrs =
  translate_move globals destrs (Types.pi1 (zero_args (List.length destrs)))

(** val last : 'a1 List.list -> 'a1 Types.option **)
let rec last = function
| List.Nil -> Types.None
| List.Cons (hd, tl) ->
  (match tl with
   | List.Nil -> Types.Some hd
   | List.Cons (x, x0) -> last tl)

(** val translate_op_asym_signed :
    AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_op_asym_signed globals op destrs srcrs1 srcrs2 =
  Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
    let l = List.length destrs in
    let cast_srcrs = fun srcrs tmp ->
      let srcrs_l = List.length srcrs in
      (match Nat.leb (Nat.S srcrs_l) l with
       | Bool.True ->
         (match last srcrs with
          | Types.None ->
            { Types.fst =
              (List.make_list
                (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
                l); Types.snd = List.Nil }
          | Types.Some last0 ->
            { Types.fst =
              (List.append srcrs
                (List.make_list (Joint.Reg tmp) (Nat.minus l srcrs_l)));
              Types.snd = (sign_mask globals tmp last0) })
       | Bool.False ->
         { Types.fst = (List.lhd srcrs l); Types.snd = List.Nil })
    in
    let srcrs1init = cast_srcrs srcrs1 tmp1 in
    let srcrs2init = cast_srcrs srcrs2 tmp2 in
    BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
      (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
        (let l0 =
           translate_op globals op destrs srcrs1init.Types.fst
             srcrs2init.Types.fst
         in
        Bind_new.Bret l0))))

(** val translate_cast :
    AST.ident List.list -> AST.signedness -> Registers.register List.list ->
    Registers.register List.list -> (Registers.register, Joint.joint_seq
    List.list) Bind_new.bind_new **)
let translate_cast globals src_sign destrs srcrs =
  let t = Util.reduce_strong srcrs destrs in
  let src_common = t.Types.fst.Types.fst in
  let src_rest = t.Types.fst.Types.snd in
  let dst_common = t.Types.snd.Types.fst in
  let dst_rest = t.Types.snd.Types.snd in
  BindLists.bappend
    (let l =
       translate_move globals dst_common
         (List.map (fun x -> Joint.Reg x) src_common)
     in
    Bind_new.Bret l)
    (match src_rest with
     | List.Nil ->
       (match src_sign with
        | AST.Signed ->
          (match last srcrs with
           | Types.None ->
             let l = translate_fill_with_zero globals dst_rest in
             Bind_new.Bret l
           | Types.Some src_last ->
             translate_cast_signed globals dst_rest
               (Joint.psd_argument_from_reg src_last))
        | AST.Unsigned ->
          let l = translate_fill_with_zero globals dst_rest in
          Bind_new.Bret l)
     | List.Cons (x, x0) -> let l = List.Nil in Bind_new.Bret l)

(** val translate_notint :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    List.list -> Joint.joint_seq List.list **)
let translate_notint globals destrs srcrs =
  Util.map2 (fun x x0 -> Joint.OP1 (BackEndOps.Cmpl, x, x0))
    (Obj.magic destrs) (Obj.magic srcrs)

(** val translate_negint :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    List.list -> Joint.joint_seq List.list **)
let translate_negint globals destrs srcrs =
  List.append (translate_notint globals destrs srcrs)
    (translate_op globals BackEndOps.Add destrs
      (List.map (fun x -> Joint.Reg x) destrs)
      (Types.pi1 (one_args (List.length destrs))))

(** val translate_notbool :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    List.list -> (Registers.register, Joint.joint_seq List.list)
    Bind_new.bind_new **)
let translate_notbool globals destrs srcrs =
  match destrs with
  | List.Nil -> let l = List.Nil in Bind_new.Bret l
  | List.Cons (destr, destrs') ->
    BindLists.bappend
      (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
      (match srcrs with
       | List.Nil ->
         let l = List.Cons ((Joint.MOVE
           (Obj.magic { Types.fst = destr; Types.snd =
             (Joint.psd_argument_from_byte Joint.zero_byte) })), List.Nil)
         in
         Bind_new.Bret l
       | List.Cons (srcr, srcrs') ->
         BindLists.bappend
           (BindLists.bcons (Joint.MOVE
             (Obj.magic { Types.fst = destr; Types.snd =
               (Joint.psd_argument_from_reg srcr) }))
             (let l =
                List.map (fun r -> Joint.OP2 (BackEndOps.Or,
                  (Obj.magic destr),
                  (Obj.magic (Joint.psd_argument_from_reg destr)),
                  (Obj.magic (Joint.psd_argument_from_reg r)))) srcrs'
              in
             Bind_new.Bret l))
           (BindLists.bcons Joint.CLEAR_CARRY (Bind_new.Bnew (fun tmp ->
             let l = List.Cons ((Joint.MOVE
               (Obj.magic { Types.fst = tmp; Types.snd =
                 (Joint.psd_argument_from_byte Joint.zero_byte) })),
               (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic destr),
               (Obj.magic (Joint.psd_argument_from_reg tmp)),
               (Obj.magic (Joint.psd_argument_from_reg tmp)))), (List.Cons
               ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
               (Obj.magic (Joint.psd_argument_from_reg tmp)),
               (Obj.magic (Joint.psd_argument_from_reg tmp)))), List.Nil)))))
             in
             Bind_new.Bret l))))

(** val translate_op1 :
    AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation
    -> Registers.register List.list -> Registers.register List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_op1 globals ty ty' op1 destrs srcrs =
  (match op1 with
   | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
     (fun _ _ -> translate_cast globals src_sign destrs srcrs)
   | FrontEndOps.Onegint (sz, sg) ->
     (fun _ _ ->
       let l = translate_negint globals destrs srcrs in Bind_new.Bret l)
   | FrontEndOps.Onotbool (x, x0, x1) ->
     (fun _ _ -> translate_notbool globals destrs srcrs)
   | FrontEndOps.Onotint (sz, sg) ->
     (fun _ _ ->
       let l = translate_notint globals destrs srcrs in Bind_new.Bret l)
   | FrontEndOps.Oid t ->
     (fun _ _ ->
       let l =
         translate_move globals destrs
           (List.map (fun x -> Joint.Reg x) srcrs)
       in
       Bind_new.Bret l)
   | FrontEndOps.Optrofint (sz, sg) ->
     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)
   | FrontEndOps.Ointofptr (sz, sg) ->
     (fun _ _ -> translate_cast globals AST.Unsigned destrs srcrs)) __ __

(** val translate_mul_i :
    AST.ident List.list -> Registers.register -> Registers.register ->
    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
    -> Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
    Joint.joint_seq List.list -> Joint.joint_seq List.list **)
let translate_mul_i globals a b n tmp_destrs_dummy srcrs1 srcrs2 k i_sig acc =
  let i = i_sig in
  let args =
    List.append (List.Cons ((Joint.Reg a), (List.Cons ((Joint.Reg b),
      List.Nil))))
      (List.make_list
        (let x = Joint.psd_argument_from_byte Joint.zero_byte in x)
        (Nat.minus (Nat.minus n (Nat.S Nat.O)) k))
  in
  let tmp_destrs_view = List.ltl tmp_destrs_dummy k in
  List.append (List.Cons ((Joint.OPACCS (BackEndOps.Mul, (Obj.magic a),
    (Obj.magic b), (Util.nth_safe i (Obj.magic srcrs1)),
    (Util.nth_safe (Nat.minus k i) (Obj.magic srcrs2)))), List.Nil))
    (List.append
      (translate_op globals BackEndOps.Add tmp_destrs_view
        (List.map (fun x -> Joint.Reg x) tmp_destrs_view) args) acc)

(** val translate_mul :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    List.list -> Joint.psd_argument List.list -> (Registers.register,
    Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_mul globals destrs srcrs1 srcrs2 =
  Bind_new.Bnew (fun a -> Bind_new.Bnew (fun b ->
    Bind_new.bnews_strong (List.length destrs) (fun tmp_destrs _ ->
      Bind_new.Bnew (fun dummy ->
      BindLists.bcons (Joint.MOVE
        (Obj.magic { Types.fst = dummy; Types.snd =
          (Joint.psd_argument_from_byte (Joint.byte_of_nat Nat.O)) }))
        (let translate_mul_k = fun k_sig acc ->
           let k = k_sig in
           List.foldr
             (translate_mul_i globals a b (List.length destrs)
               (List.append tmp_destrs (List.Cons (dummy, List.Nil))) srcrs1
               srcrs2 k) acc (Lists.range_strong (Nat.S k))
         in
        let l =
          List.append (translate_fill_with_zero globals tmp_destrs)
            (List.append
              (List.foldr translate_mul_k List.Nil
                (Lists.range_strong (List.length destrs)))
              (translate_move globals destrs
                (List.map (fun x -> Joint.Reg x) tmp_destrs)))
        in
        Bind_new.Bret l)))))

(** val translate_divumodu8 :
    AST.ident List.list -> Bool.bool -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_divumodu8 globals div_not_mod destrs srcrs1 srcrs2 =
  (match destrs with
   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
   | List.Cons (destr, destrs') ->
     (fun _ ->
       match destrs' with
       | List.Nil ->
         (match srcrs1 with
          | List.Nil -> (fun _ -> assert false (* absurd case *))
          | List.Cons (srcr1, srcrs1') ->
            (fun _ ->
              (match srcrs2 with
               | List.Nil -> (fun _ -> assert false (* absurd case *))
               | List.Cons (srcr2, srcrs2') ->
                 (fun _ -> Bind_new.Bnew (fun dummy ->
                   let l =
                     let { Types.fst = destr1; Types.snd = destr2 } =
                       match div_not_mod with
                       | Bool.True ->
                         { Types.fst = destr; Types.snd = dummy }
                       | Bool.False ->
                         { Types.fst = dummy; Types.snd = destr }
                     in
                     List.Cons ((Joint.OPACCS (BackEndOps.DivuModu,
                     (Obj.magic destr1), (Obj.magic destr2),
                     (Obj.magic srcr1), (Obj.magic srcr2))), List.Nil)
                   in
                   Bind_new.Bret l))) __)) __
       | List.Cons (x, x0) -> Logic.false_rect_Type0 __)) __

(** val foldr2 :
    ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list ->
    'a3 **)
let rec foldr2 f init l1 l2 =
  (match l1 with
   | List.Nil -> (fun _ -> init)
   | List.Cons (a, l1') ->
     (fun _ ->
       (match l2 with
        | List.Nil -> (fun _ -> assert false (* absurd case *))
        | List.Cons (b, l2') -> (fun _ -> f a b (foldr2 f init l1' l2'))) __))
    __

(** val translate_ne :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    List.list -> Joint.psd_argument List.list -> (Registers.register,
    Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_ne globals destrs srcrs1 srcrs2 =
  (match destrs with
   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
   | List.Cons (destr, destrs') ->
     (fun _ ->
       BindLists.bappend
         (let l = translate_fill_with_zero globals destrs' in
         Bind_new.Bret l)
         ((match srcrs1 with
           | List.Nil ->
             (fun _ ->
               let l = List.Cons ((Joint.MOVE
                 (Obj.magic { Types.fst = destr; Types.snd =
                   (Joint.psd_argument_from_byte Joint.zero_byte) })),
                 List.Nil)
               in
               Bind_new.Bret l)
           | List.Cons (srcr1, srcrs1') ->
             (match srcrs2 with
              | List.Nil -> (fun _ -> assert false (* absurd case *))
              | List.Cons (srcr2, srcrs2') ->
                (fun _ -> Bind_new.Bnew (fun tmpr ->
                  let f = fun s1 s2 acc -> List.Cons ((Joint.OP2
                    (BackEndOps.Xor, (Obj.magic tmpr), s1, s2)), (List.Cons
                    ((Joint.OP2 (BackEndOps.Or, (Obj.magic destr),
                    (Obj.magic (Joint.psd_argument_from_reg destr)),
                    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), acc)))
                  in
                  let epilogue = List.Cons (Joint.CLEAR_CARRY, (List.Cons
                    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic tmpr),
                    (Obj.magic
                      (Joint.psd_argument_from_byte Joint.zero_byte)),
                    (Obj.magic (Joint.psd_argument_from_reg destr)))),
                    (List.Cons ((Joint.OP2 (BackEndOps.Addc,
                    (Obj.magic destr),
                    (Obj.magic
                      (Joint.psd_argument_from_byte Joint.zero_byte)),
                    (Obj.magic
                      (Joint.psd_argument_from_byte Joint.zero_byte)))),
                    List.Nil)))))
                  in
                  let l = List.Cons ((Joint.OP2 (BackEndOps.Xor,
                    (Obj.magic destr), (Obj.magic srcr1),
                    (Obj.magic srcr2))),
                    (foldr2 f epilogue (Obj.magic srcrs1')
                      (Obj.magic srcrs2')))
                  in
                  Bind_new.Bret l)))) __))) __

(** val translate_toggle_bool :
    AST.ident List.list -> Registers.register List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_toggle_bool globals destrs =
  (match destrs with
   | List.Nil -> (fun _ -> let l = List.Nil in Bind_new.Bret l)
   | List.Cons (destr, x) ->
     (fun _ ->
       let l = List.Cons ((Joint.OP2 (BackEndOps.Xor, (Obj.magic destr),
         (Obj.magic (Joint.psd_argument_from_reg destr)),
         (Obj.magic
           (Joint.psd_argument_from_byte (Joint.byte_of_nat (Nat.S Nat.O)))))),
         List.Nil)
       in
       Bind_new.Bret l)) __

(** val translate_lt_unsigned :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    List.list -> Joint.psd_argument List.list -> (Registers.register,
    Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_lt_unsigned globals destrs srcrs1 srcrs2 =
  match destrs with
  | List.Nil -> let l = List.Nil in Bind_new.Bret l
  | List.Cons (destr, destrs') ->
    Bind_new.Bnew (fun tmpr ->
      BindLists.bappend
        (let l = translate_fill_with_zero globals destrs' in Bind_new.Bret l)
        (BindLists.bappend
          (let l =
             translate_op globals BackEndOps.Sub
               (List.make_list tmpr (List.length srcrs1)) srcrs1 srcrs2
           in
          Bind_new.Bret l)
          (let l = List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic destr),
             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)),
             (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
             List.Nil)
           in
          Bind_new.Bret l)))

(** val shift_signed :
    AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
    -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
    Types.sig0 **)
let rec shift_signed globals tmp srcrs =
  let byte_128 = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    (Nat.S Nat.O))))))), Bool.True,
    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      Nat.O)))))))))
  in
  (match srcrs with
   | List.Nil -> (fun _ -> { Types.fst = List.Nil; Types.snd = List.Nil })
   | List.Cons (srcr, srcrs') ->
     (fun _ ->
       (match srcrs' with
        | List.Nil ->
          (fun _ -> { Types.fst = (List.Cons ((Joint.Reg tmp), List.Nil));
            Types.snd = (List.Cons ((Joint.OP2 (BackEndOps.Add,
            (Obj.magic tmp), (Obj.magic srcr),
            (Obj.magic (Joint.psd_argument_from_byte byte_128)))),
            List.Nil)) })
        | List.Cons (x, x0) ->
          (fun _ ->
            let re = shift_signed globals tmp srcrs' in
            { Types.fst = (List.Cons (srcr, (Types.pi1 re).Types.fst));
            Types.snd = (Types.pi1 re).Types.snd })) __)) __

(** val translate_lt_signed :
    AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
    List.list -> Joint.psd_argument List.list -> (Registers.register,
    Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_lt_signed globals destrs srcrs1 srcrs2 =
  Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
    let p1 = shift_signed globals tmp_last_s1 srcrs1 in
    let new_srcrs1 = (Types.pi1 p1).Types.fst in
    let shift_srcrs1 = (Types.pi1 p1).Types.snd in
    let p2 = shift_signed globals tmp_last_s2 srcrs2 in
    let new_srcrs2 = (Types.pi1 p2).Types.fst in
    let shift_srcrs2 = (Types.pi1 p2).Types.snd in
    BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
      (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
        (translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2))))

(** val translate_lt :
    Bool.bool -> AST.ident List.list -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_lt is_unsigned globals destrs srcrs1 srcrs2 =
  match is_unsigned with
  | Bool.True -> translate_lt_unsigned globals destrs srcrs1 srcrs2
  | Bool.False -> translate_lt_signed globals destrs srcrs1 srcrs2

(** val translate_cmp :
    Bool.bool -> AST.ident List.list -> Integers.comparison ->
    Registers.register List.list -> Joint.psd_argument List.list ->
    Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
    BindLists.bind_list **)
let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 =
  match cmp with
  | Integers.Ceq ->
    BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
      (translate_toggle_bool globals destrs)
  | Integers.Cne -> translate_ne globals destrs srcrs1 srcrs2
  | Integers.Clt -> translate_lt is_unsigned globals destrs srcrs1 srcrs2
  | Integers.Cle ->
    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs2 srcrs1)
      (translate_toggle_bool globals destrs)
  | Integers.Cgt -> translate_lt is_unsigned globals destrs srcrs2 srcrs1
  | Integers.Cge ->
    BindLists.bappend (translate_lt is_unsigned globals destrs srcrs1 srcrs2)
      (translate_toggle_bool globals destrs)

(** val translate_op2 :
    AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
    FrontEndOps.binary_operation -> Registers.register List.list ->
    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 =
  (match op2 with
   | FrontEndOps.Oadd (sz, sg) ->
     (fun _ _ _ ->
       let l = translate_op globals BackEndOps.Add destrs srcrs1 srcrs2 in
       Bind_new.Bret l)
   | FrontEndOps.Osub (sz, sg) ->
     (fun _ _ _ ->
       let l = translate_op globals BackEndOps.Sub destrs srcrs1 srcrs2 in
       Bind_new.Bret l)
   | FrontEndOps.Omul (sz, sg) ->
     (fun _ _ _ -> translate_mul globals destrs srcrs1 srcrs2)
   | FrontEndOps.Odiv x -> assert false (* absurd case *)
   | FrontEndOps.Odivu sz ->
     (fun _ _ _ ->
       translate_divumodu8 globals Bool.True destrs srcrs1 srcrs2)
   | FrontEndOps.Omod x -> assert false (* absurd case *)
   | FrontEndOps.Omodu sz ->
     (fun _ _ _ ->
       translate_divumodu8 globals Bool.False destrs srcrs1 srcrs2)
   | FrontEndOps.Oand (sz, sg) ->
     (fun _ _ _ ->
       let l = translate_op globals BackEndOps.And destrs srcrs1 srcrs2 in
       Bind_new.Bret l)
   | FrontEndOps.Oor (sz, sg) ->
     (fun _ _ _ ->
       let l = translate_op globals BackEndOps.Or destrs srcrs1 srcrs2 in
       Bind_new.Bret l)
   | FrontEndOps.Oxor (sz, sg) ->
     (fun _ _ _ ->
       let l = translate_op globals BackEndOps.Xor destrs srcrs1 srcrs2 in
       Bind_new.Bret l)
   | FrontEndOps.Oshl (x, x0) -> assert false (* absurd case *)
   | FrontEndOps.Oshr (x, x0) -> assert false (* absurd case *)
   | FrontEndOps.Oshru (x, x0) -> assert false (* absurd case *)
   | FrontEndOps.Ocmp (sz, sg1, sg2, c) ->
     (fun _ _ _ -> translate_cmp Bool.False globals c destrs srcrs1 srcrs2)
   | FrontEndOps.Ocmpu (sz, sg, c) ->
     (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2)
   | FrontEndOps.Oaddpi sz ->
     (fun _ _ _ ->
       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
   | FrontEndOps.Oaddip sz ->
     (fun _ _ _ ->
       translate_op_asym_signed globals BackEndOps.Add destrs srcrs2 srcrs1)
   | FrontEndOps.Osubpi sz ->
     (fun _ _ _ ->
       translate_op_asym_signed globals BackEndOps.Add destrs srcrs1 srcrs2)
   | FrontEndOps.Osubpp sz ->
     (fun _ _ _ ->
       let l =
         translate_op_asym_unsigned globals BackEndOps.Sub destrs srcrs1
           srcrs2
       in
       Bind_new.Bret l)
   | FrontEndOps.Ocmpp (sg, c) ->
     (fun _ _ _ -> translate_cmp Bool.True globals c destrs srcrs1 srcrs2))
    __ __ __

(** val translate_cond :
    AST.ident List.list -> Registers.register List.list -> Graphs.label ->
    Blocks.bind_step_block **)
let translate_cond globals srcrs lbl_true =
  match srcrs with
  | List.Nil ->
    Bind_new.Bret
      (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
        globals List.Nil)
  | List.Cons (srcr, srcrs') ->
    Bind_new.Bnew (fun tmpr ->
      let f = fun r x -> Joint.OP2 (BackEndOps.Or, (Obj.magic tmpr),
        (Obj.magic (Joint.psd_argument_from_reg tmpr)),
        (Obj.magic (Joint.psd_argument_from_reg r)))
      in
      Bind_new.Bret { Types.fst = { Types.fst = (List.Cons ((fun x ->
      Joint.MOVE
      (Obj.magic { Types.fst = tmpr; Types.snd =
        (Joint.psd_argument_from_reg srcr) })), (List.map f srcrs')));
      Types.snd = (fun x -> Joint.COND ((Obj.magic tmpr), lbl_true)) };
      Types.snd = List.Nil })

(** val translate_load :
    AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
    List.list -> (Registers.register, Joint.joint_seq List.list)
    Bind_new.bind_new **)
let translate_load globals addr destrs =
  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
    BindLists.bappend
      (let l =
         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
           (tmp_addr_h, List.Nil)))) addr
       in
      Bind_new.Bret l)
      (let f = fun destr acc ->
         BindLists.bappend
           (let l = List.Cons ((Joint.LOAD (destr,
              (Obj.magic (Joint.Reg tmp_addr_l)),
              (Obj.magic (Joint.Reg tmp_addr_h)))), List.Nil)
            in
           Bind_new.Bret l)
           (BindLists.bappend
             (let l =
                translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
                  (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
                  ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
                  ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
                  (List.Cons
                  ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
                  (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
                  List.Nil))))
              in
             Bind_new.Bret l) acc)
       in
      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic destrs))))

(** val translate_store :
    AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
    List.list -> (Registers.register, Joint.joint_seq List.list)
    Bind_new.bind_new **)
let translate_store globals addr srcrs =
  Bind_new.Bnew (fun tmp_addr_l -> Bind_new.Bnew (fun tmp_addr_h ->
    BindLists.bappend
      (let l =
         translate_move globals (List.Cons (tmp_addr_l, (List.Cons
           (tmp_addr_h, List.Nil)))) addr
       in
      Bind_new.Bret l)
      (let f = fun srcr acc ->
         BindLists.bappend
           (let l = List.Cons ((Joint.STORE
              ((Obj.magic (Joint.Reg tmp_addr_l)),
              (Obj.magic (Joint.Reg tmp_addr_h)), srcr)), List.Nil)
            in
           Bind_new.Bret l)
           (BindLists.bappend
             (let l =
                translate_op globals BackEndOps.Add (List.Cons (tmp_addr_l,
                  (List.Cons (tmp_addr_h, List.Nil)))) (List.Cons
                  ((Joint.psd_argument_from_reg tmp_addr_l), (List.Cons
                  ((Joint.psd_argument_from_reg tmp_addr_h), List.Nil))))
                  (List.Cons
                  ((let x = I8051.int_size in Joint.psd_argument_from_byte x),
                  (List.Cons ((Joint.psd_argument_from_byte Joint.zero_byte),
                  List.Nil))))
              in
             Bind_new.Bret l) acc)
       in
      List.foldr f (let l = List.Nil in Bind_new.Bret l) (Obj.magic srcrs))))

(** val ensure_bind_step_block :
    Joint.params -> AST.ident List.list -> (Registers.register,
    Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
let ensure_bind_step_block p g b =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
      Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l))))

(** val translate_statement :
    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
    -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
    Blocks.bind_fin_block) Types.sum, __) Types.dPair **)
let translate_statement globals locals lenv stmt =
  (match stmt with
   | RTLabs_syntax.St_skip lbl' ->
     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret
       (Blocks.ensure_step_block (Joint.graph_params_to_params RTL.rTL)
         globals List.Nil))); Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_cost (cost_lbl, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.COST_LABEL
       cost_lbl) }; Types.snd = List.Nil })); Types.dpi2 =
       (Obj.magic lbl') })
   | RTLabs_syntax.St_const (ty, destr, cst, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
         (translate_cst ty globals cst (find_local_env destr lenv))));
       Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
         (translate_op1 globals ty' ty op1 (find_local_env destr lenv)
           (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
         (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv)
           (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
       Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_load (ignore, addr, destr, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
         (translate_load globals (find_local_env_arg addr lenv)
           (find_local_env destr lenv)))); Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_store (ignore, addr, srcr, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
         (translate_store globals (find_local_env_arg addr lenv)
           (find_local_env_arg srcr lenv)))); Types.dpi2 =
       (Obj.magic lbl') })
   | RTLabs_syntax.St_call_id (f, args, retr, lbl') ->
     (fun _ -> { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst =
       { Types.fst = List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inl
       f), (Obj.magic (rtl_args args lenv)),
       (match retr with
        | Types.None -> Obj.magic List.Nil
        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_call_ptr (f, args, retr, lbl') ->
     (fun _ ->
       let fs = find_and_addr_arg f lenv in
       { Types.dpi1 = (Types.Inl (Bind_new.Bret { Types.fst = { Types.fst =
       List.Nil; Types.snd = (fun x -> Joint.CALL ((Types.Inr
       (Obj.magic fs)), (Obj.magic (rtl_args args lenv)),
       (match retr with
        | Types.None -> Obj.magic List.Nil
        | Types.Some retr0 -> Obj.magic (find_local_env retr0 lenv)))) };
       Types.snd = List.Nil })); Types.dpi2 = (Obj.magic lbl') })
   | RTLabs_syntax.St_cond (r, lbl_true, lbl_false) ->
     (fun _ -> { Types.dpi1 = (Types.Inl
       (translate_cond globals (find_local_env r lenv) lbl_true));
       Types.dpi2 = (Obj.magic lbl_false) })
   | RTLabs_syntax.St_return ->
     (fun _ -> { Types.dpi1 = (Types.Inr (Bind_new.Bret { Types.fst =
       List.Nil; Types.snd = Joint.RETURN })); Types.dpi2 =
       (Obj.magic Types.It) })) __

(** val translate_internal :
    AST.ident List.list -> RTLabs_syntax.internal_function ->
    Joint.joint_closed_internal_function **)
let translate_internal globals def =
  let runiverse' = def.RTLabs_syntax.f_reggen in
  let luniverse' = def.RTLabs_syntax.f_labgen in
  let stack_size' = def.RTLabs_syntax.f_stacksize in
  let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
  let init = { Joint.joint_if_luniverse = luniverse';
    Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
    (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
    stack_size'; Joint.joint_if_code =
    (Obj.magic
      (Identifiers.add PreIdentifiers.LabelTag
        (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
        Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
  in
  (let { Types.fst = init'; Types.snd = lenv } =
     Obj.magic initialize_locals_params_ret globals
       def.RTLabs_syntax.f_locals def.RTLabs_syntax.f_params
       def.RTLabs_syntax.f_result init
   in
  (fun _ ->
  let vars =
    List.append def.RTLabs_syntax.f_locals
      (List.append def.RTLabs_syntax.f_params
        (match def.RTLabs_syntax.f_result with
         | Types.None -> List.Nil
         | Types.Some x -> List.Cons (x, List.Nil)))
  in
  let f_trans = fun lbl stmt def0 ->
    let pr = translate_statement globals vars lenv stmt in
    (match pr.Types.dpi1 with
     | Types.Inl instrs ->
       (fun lbl' ->
         TranslateUtils.b_adds_graph RTL.rTL globals instrs lbl
           (Obj.magic lbl') def0)
     | Types.Inr instrs ->
       (fun x ->
         TranslateUtils.b_fin_adds_graph RTL.rTL globals instrs lbl def0))
      pr.Types.dpi2
  in
  Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph
    init')) __

(** val rtlabs_to_rtl :
    CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
let rtlabs_to_rtl init_cost p =
  { Joint.jp_functions = (AST.prog_funct_names p); Joint.joint_prog =
    (AST.transform_program p (fun varnames ->
      AST.transf_fundef
        (translate_internal (List.append varnames (AST.prog_funct_names p)))));
    Joint.init_cost_label = init_cost }