include "RTL/RTL.ma".
include "RTL/RTLTailcall.ma".
include "ERTL/ERTL.ma".
include "utilities/RegisterSet.ma".

definition change_exit_label ≝
  λl: label.
  λp: ertl_internal_function.
  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
  let ertl_if_params' ≝ ertl_if_params p in
  let ertl_if_locals' ≝ ertl_if_locals p in
  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
  let ertl_if_graph' ≝ ertl_if_graph p in
  let ertl_if_entry' ≝ ertl_if_entry p in
  let ertl_if_exit' ≝ l in
    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.

definition change_entry_label ≝
  λl: label.
  λp: ertl_internal_function.
  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
  let ertl_if_params' ≝ ertl_if_params p in
  let ertl_if_locals' ≝ ertl_if_locals p in
  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
  let ertl_if_graph' ≝ ertl_if_graph p in
  let ertl_if_entry' ≝ l in
  let ertl_if_exit' ≝ ertl_if_exit p in
    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
                             
definition add_graph ≝
  λl: label.
  λstmt.
  λp.
  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
  let ertl_if_params' ≝ ertl_if_params p in
  let ertl_if_locals' ≝ ertl_if_locals p in
  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
  let ertl_if_entry' ≝ ertl_if_entry p in
  let ertl_if_exit' ≝ ertl_if_exit p in
    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
                             
definition fresh_label ≝
  λdef.
    match fresh LabelTag (ertl_if_luniverse def) with
    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    | Error ⇒ None ?
    ].
    
definition change_label ≝
  λl.
  λe: ertl_statement.
  match e with
  [ ertl_st_skip _ ⇒ ertl_st_skip l
  | ertl_st_comment s _ ⇒ ertl_st_comment s l
  | ertl_st_cost c _ ⇒ ertl_st_cost c l
  | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
  | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
  | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
  | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
  | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
  | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
  | ertl_st_pop r _ ⇒ ertl_st_pop r l
  | ertl_st_push r _ ⇒ ertl_st_push r l
  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
  | ertl_st_int r i _ ⇒ ertl_st_int r i l
  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
  | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
  | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
  | ertl_st_return a ⇒ ertl_st_return a
  ].
  
let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
  match stmt_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
    | _ ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ Some tmp_lbl ⇒
        let stmt ≝ change_label tmp_lbl hd in
        let def ≝ add_graph start_lbl hd def in
          adds_graph tl tmp_lbl dest_lbl def
      | None ⇒ None ?
      ]
    ]
  ].

let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
                       (start_lbl: label) (dest_lbl: label)
                       (def: ertl_internal_function): option ertl_internal_function ≝
  match translate_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ hd start_lbl dest_lbl def
    | _ ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ Some tmp_lbl ⇒
        match hd start_lbl tmp_lbl def with
        [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
        | None ⇒ None ?
        ]
      | None ⇒ None ?
      ]
    ]
  ].
  
axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.

let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
  match n with
  [ O ⇒ 〈def, [ ]〉
  | S n' ⇒
    let 〈def', regs'〉 ≝ fresh_regs def n' in
    let 〈def', reg〉 ≝ fresh_reg def' in
      〈def', reg :: regs'〉
  ].
  
definition save_hdws_internal ≝
  λdestr_srcr: register × hardware_register.
  λstart_lbl: label.
    let 〈destr, srcr〉 ≝ destr_srcr in
      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
  
definition save_hdws ≝
  λl.
    map ? ? save_hdws_internal l.
    
definition restore_hdws_internal ≝
  λdestr_srcr: hardware_register × register.
  λstart_lbl: label.
    let 〈destr, srcr〉 ≝ destr_srcr in
    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
    
definition swap_components ≝
  λA, B: Type[0].
  λp: A × B.
  let 〈l, r〉 ≝ p in
  〈r, l〉.
    
definition restore_hdws ≝
  λl.
    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).

definition get_params_hdw_internal ≝
  λstart_lbl: label.
    adds_graph [ ertl_st_skip start_lbl ] start_lbl.

definition get_params_hdw ≝
  λparams: list register.
  match length ? params with
  [ O ⇒ Some ? [ get_params_hdw_internal ]
  | _ ⇒
    match zip ? ? params parameters with
    [ None ⇒ None ?
    | Some l ⇒ Some ? (save_hdws l)
    ]
  ].

definition get_param_stack ≝
  λoff: nat.
  λdestr.
  λstart_lbl, dest_lbl: label.
  λdef.
  let 〈def, addr1〉 ≝ fresh_reg def in
  let 〈def, addr2〉 ≝ fresh_reg def in
  let 〈def, tmpr〉 ≝ fresh_reg def in
  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
  adds_graph [
    ertl_st_frame_size addr1 start_lbl;
    ertl_st_int tmpr int_offset start_lbl;
    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
    ertl_st_load destr addr1 addr2 start_lbl
  ] start_lbl dest_lbl def.
  
definition get_params_stack_internal ≝
  λi.
  λr.
    get_param_stack i r.
  
definition get_params_stack ≝
  λparams.
  match length ? params with
  [ O ⇒ [ get_params_hdw_internal ]
  | _ ⇒ mapi ? ? get_params_stack_internal params
  ].

definition get_params ≝
  λparams.
  let n ≝ min (length ? params) (length ? parameters) in
  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
  match get_params_hdw hdw_params with
  [ None ⇒ None ?
  | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
  ].
  
definition add_prologue ≝
  λparams.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ ertl_if_entry def in
  let tmp_lbl ≝ fresh_label def in
  match tmp_lbl with
  [ None ⇒ None ?
  | Some tmp_lbl ⇒
    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
    let params ≝
      match get_params params with
      [ Some params ⇒ params
      | None ⇒ [ ] (* dpm: is this ok? *)
      ] in
    let def ≝
      add_translates (
        adds_graph [ ertl_st_new_frame start_lbl ] ::
        adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
        save_hdws sregs @
        params) start_lbl tmp_lbl def in
    match def with
    [ Some def ⇒
      match last_stmt with
      [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
      | None ⇒ None ?
      ]
    | None ⇒ None ?
    ]
  ].
  
definition allocate_regs_internal ≝
  λr: register.
  λdef_sregs.
  let 〈def, sregs〉 ≝ def_sregs in
  let 〈def, r'〉 ≝ fresh_reg def in
    〈def, 〈r', r〉 :: sregs〉.
  
definition allocate_regs ≝
  λrs: register_set.
  λsaved: rs_set rs.
  λdef.
    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    
definition save_return_internal ≝
  λr.
  λstart_lbl.
  λdest_lbl.
  λdef.
  let 〈def, r_tmp〉 ≝ fresh_reg def in
  adds_graph [
    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
    ertl_st_set_hdw RegisterST0 r start_lbl;
    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
   
definition save_return_internal' ≝
  λr1, r2.
  λstart_lbl.
  adds_graph [
    ertl_st_set_hdw RegisterST0 r1 start_lbl;
    ertl_st_set_hdw RegisterST1 r2 start_lbl
  ] start_lbl.
    
definition save_return ≝
  λret_regs.
  match ret_regs with
  [ nil ⇒ [ get_params_hdw_internal ]
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ [ save_return_internal hd ]
    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
    ]
  ].
   
definition add_epilogue ≝
  λret_regs.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ ertl_if_exit def in
  let tmp_lbl ≝ fresh_label def in
  match tmp_lbl with
  [ None ⇒ None ?
  | Some tmp_lbl ⇒
    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
    match last_stmt with
    [ None ⇒ None ?
    | Some last_stmt ⇒
      let def ≝
        add_translates (
          save_return ret_regs @
          restore_hdws sregs @
          [adds_graph [
            ertl_st_push srah start_lbl;
            ertl_st_push sral start_lbl
          ]] @
          [adds_graph [
            ertl_st_del_frame start_lbl
          ]] @
          [adds_graph [
            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
          ]]) start_lbl tmp_lbl def in
      match def with
      [ None ⇒ None ?
      | Some def ⇒ 
        let def ≝ add_graph tmp_lbl last_stmt def in
          Some ? (change_exit_label tmp_lbl def)
      ]
    ]
  ].
  
axiom add_pro_and_epilogue:
  ∀rs: register_set.
  ∀params: list register.
  ∀ret_args: list register.
  ∀def: ertl_internal_function.
    option ertl_internal_function.
    
(*
  dpm: address callee_saved problem   
definition add_pro_and_epilogue ≝
  λrs: register_set.
  λparams.
  λret_args.
  λdef.
  let 〈def, sra〉 ≝ fresh_regs def 2 in
  let sral ≝ safe_nth ? 0 sra ? in
  let srah ≝ safe_nth ? 1 sra ? in
  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
  let def ≝ add_prologue params sral srah sregs def in
  let def ≝ add_epilogue ret_args sral srah sregs def in
    def.  
*)

definition set_params_hdw ≝
  λparams.
  match length ? params with
  [ O ⇒ Some ? [ get_params_hdw_internal ]
  | _ ⇒
    match zip ? ? params parameters with
    [ None ⇒ None ?
    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
    ]
  ].
  
definition set_param_stack ≝
  λoff: nat.
  λsrcr.
  λstart_lbl, dest_lbl: label.
  λdef.
  let 〈def, addr1〉 ≝ fresh_reg def in
  let 〈def, addr2〉 ≝ fresh_reg def in
  let 〈def, tmpr〉 ≝ fresh_reg def in
  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
    adds_graph [
      ertl_st_int addr2 int_offset start_lbl;
      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
      ertl_st_clear_carry start_lbl;
      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
      ertl_st_store addr1 addr2 srcr start_lbl
    ] start_lbl dest_lbl def.

definition set_params_stack ≝
  λparams.
  match length ? params with
  [ O ⇒ [ get_params_hdw_internal ]
  | _ ⇒ mapi ? ? set_param_stack params
  
  ].
  
definition set_params ≝
  λparams.
  let n ≝ min (length ? params) (length ? parameters) in
  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    match set_params_hdw hdw_params with
    [ None ⇒ None ?
    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
    ].
    
definition fetch_result ≝
  λret_regs.
  λstart_lbl.
  match ret_regs with
  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
  | cons hd tl ⇒
    match tl with
    [ nil ⇒
      adds_graph [
        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
        ertl_st_get_hdw hd RegisterST0 start_lbl
      ] start_lbl
    | cons hd' tl' ⇒
      adds_graph [
        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
        ertl_st_get_hdw hd RegisterST0 start_lbl;
        ertl_st_get_hdw hd' RegisterST1 start_lbl
      ] start_lbl
    ]
  ].
  
definition translate_call_id ≝
  λf.
  λargs.
  λret_regs.
  λstart_lbl, dest_lbl: label.
  λdef.
  let nb_args ≝ bitvector_of_nat ? (length ? args) in
  match set_params args with
  [ None ⇒ None ?
  | Some params_args ⇒
    add_translates (
      params_args @ [
        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
        fetch_result ret_regs
      ]) start_lbl dest_lbl def
  ].
  
definition translate_stmt ≝
  λlbl: label.
  λstmt: rtl_statement.
  λdef: ertl_internal_function.
  match stmt with
  [ rtl_st_skip lbl' ⇒
    Some ? (add_graph lbl (ertl_st_skip lbl') def)
  | rtl_st_cost cost_lbl lbl' ⇒
    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
  | rtl_st_addr r1 r2 x lbl' ⇒
    adds_graph [
      ertl_st_addr_l r1 x lbl;
      ertl_st_addr_h r2 x lbl
    ] lbl lbl' def
  | rtl_st_stack_addr r1 r2 lbl' ⇒
    adds_graph [
      ertl_st_get_hdw r1 RegisterSPL lbl;
      ertl_st_get_hdw r2 RegisterSPH lbl
    ] lbl lbl' def
  | rtl_st_int r i lbl' ⇒
    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
  | rtl_st_move r1 r2 lbl' ⇒
    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
  | rtl_st_op1 op1 d s lbl' ⇒
    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
  | rtl_st_clear_carry lbl' ⇒
    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
  | rtl_st_load d a1 a2 lbl' ⇒
    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
  | rtl_st_store a1 a2 s lbl' ⇒
    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
  | rtl_st_call_id f args ret_regs lbl' ⇒
    translate_call_id f args ret_regs lbl lbl' def
  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
  | rtl_st_cond_acc src lbl_true lbl_false ⇒
    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
  | rtl_st_return ret_regs ⇒
    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
  ].
    
definition translate_funct_internal ≝
  λdef.
  let nb_params ≝ length ? (rtl_if_params def) in
  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
  let def' ≝
    mk_ertl_internal_function
      (rtl_if_luniverse def) (rtl_if_runiverse def)
      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
    def'.
    
definition translate_funct ≝
  λid_def: ident × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with
    [ rtl_f_internal def ⇒
      match translate_funct_internal def with
      [ None ⇒ None ?
      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
      ]
    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
    ] in
  〈id, def'〉.

definition generate ≝
  λstmt.
  λdef.
  let entry ≝ fresh_label def in
  match entry with
  [ None ⇒ None ?
  | Some entry ⇒
    let def ≝ add_graph entry stmt def in
      Some ? (change_entry_label entry def)
  ].
  
let rec find_and_remove_first_cost_label_internal (def: ertl_internal_function)
                                                  (lbl: label) (n: nat) on n ≝
  match n with
  [ O ⇒ None ?
  | S n' ⇒
    let statement_at_label ≝ lookup ? ? (ertl_if_graph def) lbl in
    match statement_at_label with
    [ None ⇒ None ?
    | Some statement ⇒
      match statement with
      [ ertl_st_cost cost_lbl next_lbl ⇒
        let def' ≝ add_graph lbl (ertl_st_skip next_lbl) def in
          Some ? 〈Some ? cost_lbl, def'〉
      | ertl_st_cond_acc _ _ _ ⇒ Some ? 〈None ?, def〉
      | ertl_st_return _⇒ Some ? 〈None ?, def〉
      | ertl_st_skip lbl' ⇒ find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_comment _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_get_hdw _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_set_hdw _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_hdw_to_hdw _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_pop _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_push _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_addr_h _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_addr_l _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_int _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_move _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_opaccs _ _ _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_op2 _ _ _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_op1 _ _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_clear_carry lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_load _ _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_store _ _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_call_id _ _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_new_frame lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_del_frame lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      | ertl_st_frame_size _ lbl' ⇒
        find_and_remove_first_cost_label_internal def lbl' n'
      ]
    ]
  ].
  
axiom num_entries:
  ∀A: Type[0].
  ∀g: graph A.
    nat.
  
definition find_and_remove_first_cost_label ≝
  λdef.
    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (num_entries ? (ertl_if_graph def)).

definition move_first_cost_label_up_internal ≝
  λdef.
  let cost_label_def ≝ find_and_remove_first_cost_label def in
  match cost_label_def with
  [ None ⇒ None ?
  | Some cost_label_def ⇒
    let 〈cost_label, def〉 ≝ cost_label_def in
    match cost_label with
    [ None ⇒ Some ? def
    | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
    ]
  ].
  
definition move_first_cost_label_up ≝
  λid_def: ident × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with  
    [ ertl_f_internal int_fun ⇒
      let cost_label_def ≝ move_first_cost_label_up_internal int_fun in
      match cost_label_def with
      [ None ⇒ None ?
      | Some cost_label_def ⇒
          Some ? (ertl_f_internal cost_label_def)
      ]
    | ertl_f_external _ ⇒ Some ? def
    ] in
  match def' with
  [ None ⇒ None ?
  | Some def' ⇒ Some ? 〈id, def'〉
  ].
  
definition translate_internal ≝
  λfunct.
    let 〈id, funct〉 ≝ translate_funct funct in
    match funct with
    [ None ⇒ None ?
    | Some funct ⇒ move_first_cost_label_up 〈id, funct〉
    ].

let rec strip_none (A: Type[0]) (l: list (option A)) on l: list A ≝
  match l with
  [ nil ⇒ nil ?
  | cons hd tl ⇒
    match hd with
    [ None ⇒ strip_none A tl
    | Some hd ⇒ hd :: strip_none A tl
    ]
  ].
  
definition translate: rtl_program → ertl_program ≝
  λp.
  let p ≝ tailcall_simplify p in
  let rtl_pr_vars' ≝ rtl_pr_vars p in
  let rtl_pr_functs' ≝ map … translate_internal (rtl_pr_functs p) in
  let rtl_pr_functs_filtered ≝ strip_none ? rtl_pr_functs' in
  let rtl_pr_main' ≝ rtl_pr_main p in
    mk_ertl_program rtl_pr_vars' rtl_pr_functs_filtered rtl_pr_main'.