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

open State

open Bind_new

open BindLists

open Blocks

open Deqsets_extra

(** val fresh_label :
    Joint.params -> AST.ident List.list -> Graphs.label
    Monad.smax_def__o__monad **)
let fresh_label g_pars globals =
  Obj.magic (fun def ->
    let { Types.fst = r; Types.snd = luniverse } =
      Identifiers.fresh PreIdentifiers.LabelTag def.Joint.joint_if_luniverse
    in
    { Types.fst = (Joint.set_luniverse g_pars globals def luniverse);
    Types.snd = r })

(** val fresh_register :
    Joint.params -> AST.ident List.list -> Registers.register
    Monad.smax_def__o__monad **)
let fresh_register g_pars globals =
  Obj.magic (fun def ->
    let { Types.fst = r; Types.snd = runiverse } =
      Identifiers.fresh PreIdentifiers.RegisterTag
        def.Joint.joint_if_runiverse
    in
    { Types.fst = (Joint.set_runiverse g_pars globals def runiverse);
    Types.snd = r })

(** val adds_graph_pre :
    Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
    Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
    Monad.smax_def__o__monad **)
let rec adds_graph_pre g_pars globals pre_process insts src =
  match insts with
  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) src
  | List.Cons (i, rest) ->
    Monad.m_bind0 (Monad.smax_def State.state_monad)
      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun mid ->
      Monad.m_bind0 (Monad.smax_def State.state_monad)
        (adds_graph_pre g_pars globals pre_process rest mid) (fun dst ->
        Monad.m_bind0 (Monad.smax_def State.state_monad)
          (State.state_update
            (Joint.add_graph g_pars globals src (Joint.Sequential
              ((Joint.Step_seq (pre_process dst i)), (Obj.magic mid)))))
          (fun x -> Monad.m_return0 (Monad.smax_def State.state_monad) dst)))

(** val adds_graph_post :
    Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
    Graphs.label -> Graphs.label Monad.smax_def__o__monad **)
let rec adds_graph_post g_pars globals insts dst =
  match insts with
  | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) dst
  | List.Cons (i, rest) ->
    Monad.m_bind0 (Monad.smax_def State.state_monad)
      (fresh_label (Joint.graph_params_to_params g_pars) globals) (fun src ->
      Monad.m_bind0 (Monad.smax_def State.state_monad)
        (adds_graph_post g_pars globals rest dst) (fun mid ->
        Monad.m_bind0 (Monad.smax_def State.state_monad)
          (State.state_update
            (Joint.add_graph g_pars globals src (Joint.Sequential
              ((Joint.Step_seq i), mid)))) (fun x ->
          Monad.m_return0 (Monad.smax_def State.state_monad) src)))

(** val adds_graph :
    Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
    Joint.joint_internal_function **)
let adds_graph g_pars globals insts src dst def =
  let pref = insts.Types.fst.Types.fst in
  let op = insts.Types.fst.Types.snd in
  let post = insts.Types.snd in
  let { Types.fst = def0; Types.snd = mid } =
    Obj.magic adds_graph_pre g_pars globals (fun lbl inst -> inst lbl)
      (Obj.magic pref) src def
  in
  let { Types.fst = def1; Types.snd = mid' } =
    Obj.magic adds_graph_post g_pars globals post dst def0
  in
  Joint.add_graph g_pars globals mid (Joint.Sequential ((Obj.magic op mid),
    mid')) def1

(** val fin_adds_graph :
    Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
    Graphs.label -> Joint.joint_internal_function ->
    Joint.joint_internal_function **)
let fin_adds_graph g_pars globals insts src def =
  let pref = insts.Types.fst in
  let last = insts.Types.snd in
  let { Types.fst = def0; Types.snd = mid } =
    Obj.magic adds_graph_pre g_pars globals (fun x i -> i) pref src def
  in
  Joint.add_graph g_pars globals mid (Joint.Final last) def0

(** val b_adds_graph :
    Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
    Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
    Joint.joint_internal_function **)
let b_adds_graph g_pars globals insts src dst def =
  let { Types.fst = def0; Types.snd = stmts } =
    Obj.magic Bind_new.bcompile
      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
      def
  in
  adds_graph g_pars globals stmts src dst def0

(** val b_fin_adds_graph :
    Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
    Graphs.label -> Joint.joint_internal_function ->
    Joint.joint_internal_function **)
let b_fin_adds_graph g_pars globals insts src def =
  let { Types.fst = def0; Types.snd = stmts } =
    Obj.magic Bind_new.bcompile
      (fresh_register (Joint.graph_params_to_params g_pars) globals) insts
      def
  in
  fin_adds_graph g_pars globals stmts src def0

(** val step_registers :
    Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
    Registers.register List.list **)
let step_registers p globals s =
  Joint.get_used_registers_from_step p.Joint.u_pars globals p.Joint.functs s

(** val fin_step_registers :
    Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list **)
let fin_step_registers p = function
| Joint.GOTO x -> List.Nil
| Joint.RETURN -> List.Nil
| Joint.TAILCALL (x0, r) -> p.Joint.functs.Joint.f_call_args r

type b_graph_translate_data = { init_ret : __; init_params : __;
                                init_stack_size : Nat.nat;
                                added_prologue : Joint.joint_seq List.list;
                                new_regs : Registers.register List.list;
                                f_step : (Graphs.label -> Joint.joint_step ->
                                         Blocks.bind_step_block);
                                f_fin : (Graphs.label -> Joint.joint_fin_step
                                        -> Blocks.bind_fin_block) }

(** val b_graph_translate_data_rect_Type4 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18277 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18277
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val b_graph_translate_data_rect_Type5 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18279 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18279
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val b_graph_translate_data_rect_Type3 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18281 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18281
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val b_graph_translate_data_rect_Type2 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18283 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18283
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val b_graph_translate_data_rect_Type1 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18285 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18285
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val b_graph_translate_data_rect_Type0 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
    __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register
    List.list -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block)
    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18287 =
  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    f_step = f_step0; f_fin = f_fin0 } = x_18287
  in
  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
    added_prologue0 new_regs0 f_step0 f_fin0 __ __ __ __

(** val init_ret :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> __ **)
let rec init_ret src dst globals xxx =
  xxx.init_ret

(** val init_params :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> __ **)
let rec init_params src dst globals xxx =
  xxx.init_params

(** val init_stack_size :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Nat.nat **)
let rec init_stack_size src dst globals xxx =
  xxx.init_stack_size

(** val added_prologue :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_seq List.list **)
let rec added_prologue src dst globals xxx =
  xxx.added_prologue

(** val new_regs :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Registers.register List.list **)
let rec new_regs src dst globals xxx =
  xxx.new_regs

(** val f_step :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
    Blocks.bind_step_block **)
let rec f_step src dst globals xxx =
  xxx.f_step

(** val f_fin :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
    Blocks.bind_fin_block **)
let rec f_fin src dst globals xxx =
  xxx.f_fin

(** val b_graph_translate_data_inv_rect_Type4 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
    List.list -> Registers.register List.list -> (Graphs.label ->
    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let b_graph_translate_data_inv_rect_Type4 x1 x2 x3 hterm h1 =
  let hcut = b_graph_translate_data_rect_Type4 x1 x2 x3 h1 hterm in hcut __

(** val b_graph_translate_data_inv_rect_Type3 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
    List.list -> Registers.register List.list -> (Graphs.label ->
    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let b_graph_translate_data_inv_rect_Type3 x1 x2 x3 hterm h1 =
  let hcut = b_graph_translate_data_rect_Type3 x1 x2 x3 h1 hterm in hcut __

(** val b_graph_translate_data_inv_rect_Type2 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
    List.list -> Registers.register List.list -> (Graphs.label ->
    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let b_graph_translate_data_inv_rect_Type2 x1 x2 x3 hterm h1 =
  let hcut = b_graph_translate_data_rect_Type2 x1 x2 x3 h1 hterm in hcut __

(** val b_graph_translate_data_inv_rect_Type1 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
    List.list -> Registers.register List.list -> (Graphs.label ->
    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let b_graph_translate_data_inv_rect_Type1 x1 x2 x3 hterm h1 =
  let hcut = b_graph_translate_data_rect_Type1 x1 x2 x3 h1 hterm in hcut __

(** val b_graph_translate_data_inv_rect_Type0 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq
    List.list -> Registers.register List.list -> (Graphs.label ->
    Joint.joint_step -> Blocks.bind_step_block) -> (Graphs.label ->
    Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __ -> __ -> __ ->
    __ -> 'a1) -> 'a1 **)
let b_graph_translate_data_inv_rect_Type0 x1 x2 x3 hterm h1 =
  let hcut = b_graph_translate_data_rect_Type0 x1 x2 x3 h1 hterm in hcut __

(** val b_graph_translate_data_jmdiscr :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> b_graph_translate_data -> __ **)
let b_graph_translate_data_jmdiscr a1 a2 a3 x y =
  Logic.eq_rect_Type2 x
    (let { init_ret = a0; init_params = a10; init_stack_size = a20;
       added_prologue = a30; new_regs = a4; f_step = a5; f_fin = a6 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y

type bound_b_graph_translate_data =
  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0

(** val get_first_costlabel_next :
    Joint.params -> AST.ident List.list ->
    Joint.joint_closed_internal_function -> (CostLabel.costlabel, __)
    Types.prod **)
let get_first_costlabel_next p g def =
  (match p.Joint.stmt_at g (Types.pi1 def).Joint.joint_if_code
           (Types.pi1 def).Joint.joint_if_entry with
   | Types.None -> (fun _ -> assert false (* absurd case *))
   | Types.Some s ->
     (match s with
      | Joint.Sequential (s', nxt) ->
        (match s' with
         | Joint.COST_LABEL c ->
           (fun _ -> { Types.fst = c; Types.snd = nxt })
         | Joint.CALL (x, x0, x1) ->
           (fun _ -> assert false (* absurd case *))
         | Joint.COND (x, x0) -> (fun _ -> assert false (* absurd case *))
         | Joint.Step_seq x -> (fun _ -> assert false (* absurd case *)))
      | Joint.Final x -> (fun _ -> assert false (* absurd case *))
      | Joint.FCOND (x0, x1, x2) -> (fun _ -> assert false (* absurd case *))))
    __

(** val get_first_costlabel :
    Joint.params -> AST.ident List.list ->
    Joint.joint_closed_internal_function -> CostLabel.costlabel **)
let get_first_costlabel p g f =
  (get_first_costlabel_next p g f).Types.fst

(** val not_emptyb : 'a1 List.list -> Bool.bool **)
let not_emptyb = function
| List.Nil -> Bool.False
| List.Cons (x, x0) -> Bool.True

(** val b_graph_translate_props_rect_Type4 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type4 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_rect_Type5 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type5 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_rect_Type3 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type3 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_rect_Type2 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type2 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_rect_Type1 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type1 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_rect_Type0 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let rec b_graph_translate_props_rect_Type0 src_g_pars dst_g_pars globals data def_in def_out f_lbls f_regs h_mk_b_graph_translate_props =
  h_mk_b_graph_translate_props __ __ __ __ __ __ __ __ __ __ __

(** val b_graph_translate_props_inv_rect_Type4 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let b_graph_translate_props_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
  let hcut = b_graph_translate_props_rect_Type4 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
  hcut __

(** val b_graph_translate_props_inv_rect_Type3 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let b_graph_translate_props_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
  let hcut = b_graph_translate_props_rect_Type3 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
  hcut __

(** val b_graph_translate_props_inv_rect_Type2 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let b_graph_translate_props_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
  let hcut = b_graph_translate_props_rect_Type2 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
  hcut __

(** val b_graph_translate_props_inv_rect_Type1 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let b_graph_translate_props_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
  let hcut = b_graph_translate_props_rect_Type1 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
  hcut __

(** val b_graph_translate_props_inv_rect_Type0 :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
    -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    'a1 **)
let b_graph_translate_props_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 =
  let hcut = b_graph_translate_props_rect_Type0 x1 x2 x3 x4 x5 x6 x7 x8 h1 in
  hcut __

(** val b_graph_translate_props_jmdiscr :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
    List.list) -> (Graphs.label -> Registers.register List.list) -> __ **)
let b_graph_translate_props_jmdiscr a1 a2 a3 a4 a5 a6 a7 a8 =
  Logic.eq_rect_Type2 __
    (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) __

(** val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod **)
let pair_swap pr =
  { Types.fst = pr.Types.snd; Types.snd = pr.Types.fst }

(** val set_entry :
    AST.ident List.list -> Joint.params -> Joint.joint_internal_function ->
    __ -> Joint.joint_internal_function **)
let set_entry globals pars int_fun entry =
  { Joint.joint_if_luniverse = int_fun.Joint.joint_if_luniverse;
    Joint.joint_if_runiverse = int_fun.Joint.joint_if_runiverse;
    Joint.joint_if_result = int_fun.Joint.joint_if_result;
    Joint.joint_if_params = int_fun.Joint.joint_if_params;
    Joint.joint_if_stacksize = int_fun.Joint.joint_if_stacksize;
    Joint.joint_if_local_stacksize = int_fun.Joint.joint_if_local_stacksize;
    Joint.joint_if_code = int_fun.Joint.joint_if_code; Joint.joint_if_entry =
    entry }

(** val b_graph_translate :
    Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
    bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
    Joint.joint_closed_internal_function Types.sig0 **)
let b_graph_translate src_g_pars dst_g_pars globals data def =
  let runiv_data =
    Obj.magic Bind_new.bcompile
      (Obj.magic
        (Relations.compose pair_swap
          (Identifiers.fresh PreIdentifiers.RegisterTag))) (Types.pi1 data)
      (Types.pi1 def).Joint.joint_if_runiverse
  in
  let runiv = runiv_data.Types.fst in
  let data0 = runiv_data.Types.snd in
  let entry = (Types.pi1 def).Joint.joint_if_entry in
  let init = { Joint.joint_if_luniverse =
    (Types.pi1 def).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
    runiv; Joint.joint_if_result = data0.init_ret; Joint.joint_if_params =
    data0.init_params; Joint.joint_if_stacksize = data0.init_stack_size;
    Joint.joint_if_local_stacksize =
    (Types.pi1 def).Joint.joint_if_local_stacksize; Joint.joint_if_code =
    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
    Joint.joint_if_entry = entry }
  in
  let f = fun lbl stmt def0 ->
    match stmt with
    | Joint.Sequential (inst, next) ->
      b_adds_graph dst_g_pars globals (data0.f_step lbl inst) lbl
        (Obj.magic next) def0
    | Joint.Final inst ->
      b_fin_adds_graph dst_g_pars globals (data0.f_fin lbl inst) lbl def0
    | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
  in
  let def_out =
    Identifiers.foldi PreIdentifiers.LabelTag f
      (Obj.magic (Types.pi1 def).Joint.joint_if_code) init
  in
  let prologue = data0.added_prologue in
  let def_out0 =
    match not_emptyb prologue with
    | Bool.True ->
      let { Types.fst = init_c; Types.snd = nxt } =
        get_first_costlabel_next (Joint.graph_params_to_params src_g_pars)
          globals def
      in
      let def_out0 =
        Joint.add_graph dst_g_pars globals (Obj.magic entry)
          (Joint.Sequential ((Joint.Step_seq
          (Joint.nOOP
            (Joint.uns_pars__o__u_pars
              (Joint.gp_to_p__o__stmt_pars dst_g_pars)) globals)), nxt))
          def_out
      in
      let { Types.fst = def_out1; Types.snd = entry' } =
        Obj.magic fresh_label (Joint.graph_params_to_params dst_g_pars)
          globals def_out0
      in
      let def_out2 =
        adds_graph dst_g_pars globals { Types.fst = { Types.fst = List.Nil;
          Types.snd = (fun x -> Joint.COST_LABEL init_c) }; Types.snd =
          prologue } entry' (Obj.magic entry) def_out1
      in
      set_entry globals (Joint.graph_params_to_params dst_g_pars) def_out2
        (Obj.magic entry')
    | Bool.False -> def_out
  in
  def_out0

(** val b_graph_transform_program :
    Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
    Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
    Joint.joint_program -> Joint.joint_program **)
let b_graph_transform_program src dst init =
  Joint.transform_joint_program (Joint.graph_params_to_params src)
    (Joint.graph_params_to_params dst) (fun varnames def_in ->
    Types.pi1
      (b_graph_translate src dst varnames (init varnames def_in) def_in))

(** val added_registers :
    Joint.graph_params -> AST.ident List.list ->
    Joint.joint_internal_function -> (Graphs.label -> Registers.register
    List.list) -> Registers.register List.list **)
let added_registers p g def f_regs =
  let f = fun lbl x acc -> List.append (f_regs lbl) acc in
  Identifiers.foldi PreIdentifiers.LabelTag f
    (Obj.magic def.Joint.joint_if_code) List.Nil