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

definition change_exit_label ≝
  λl: label.
  λp: ertl_internal_function.
  λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
  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'.
  @prf
qed.

definition change_entry_label ≝
  λl: label.
  λp: ertl_internal_function.
  λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
  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'.
  @prf
qed.
                             
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' ? ?.
  normalize nodelta;
  [1: generalize in match ertl_if_entry';
      #HYP
      cases HYP
      #LBL #LBL_PRF
      %
      [1: @LBL
      |2: @graph_add_lookup
          @LBL_PRF
      ]
  |2: generalize in match ertl_if_exit';
      #HYP
      cases HYP
      #LBL #LBL_PRF
      %
      [1: @LBL
      |2: @graph_add_lookup
          @LBL_PRF
      ]
  ]
qed.
                             
definition fresh_label ≝
  λdef.
    fresh LabelTag (ertl_if_luniverse def).
    
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 r1 r2 x _ ⇒ ertl_st_addr r1 r2 x 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 d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 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_set_carry _ ⇒ ertl_st_set_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 a i1 i2 ⇒ ertl_st_cond a i1 i2
  | ertl_st_return ⇒ ertl_st_return
  ].
  
let rec adds_graph
  (stmt_list: list ertl_statement) (start_lbl: label)
  (dest_lbl: label) (def: ertl_internal_function)
    on stmt_list ≝
  match stmt_list with
  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
  | cons stmt stmt_list ⇒
    match stmt_list with
    [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
    | _ ⇒
      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
      let stmt ≝ change_label tmp_lbl stmt in
      let def ≝ add_graph start_lbl stmt def in
        adds_graph stmt_list tmp_lbl dest_lbl def
    ]
  ].

let rec add_translates
  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
  (def: ertl_internal_function)
    on translate_list ≝
  match translate_list with
  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
  | cons trans translate_list ⇒
    match translate_list with
    [ nil ⇒ trans start_lbl dest_lbl def
    | _ ⇒
      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
      let def ≝ trans start_lbl tmp_lbl def in
        add_translates translate_list tmp_lbl dest_lbl def
    ]
  ].

axiom register_fresh: universe RegisterTag → register.

definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
  λdef.
    let r ≝ register_fresh (ertl_if_runiverse def) in
    let locals ≝ r :: ertl_if_locals def in
    let ertl_if_luniverse' ≝ ertl_if_luniverse def in
    let ertl_if_runiverse' ≝ ertl_if_runiverse def in
    let ertl_if_params' ≝ ertl_if_params def in
    let ertl_if_locals' ≝ locals in
    let ertl_if_stacksize' ≝ ertl_if_stacksize def in
    let ertl_if_graph' ≝ ertl_if_graph def in
    let ertl_if_entry' ≝ ertl_if_entry def in
    let ertl_if_exit' ≝ ertl_if_exit def 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', r〉.

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'〉
  ].
  
axiom fresh_regs_length:
  ∀def: ertl_internal_function.
  ∀n: nat.
    |(\snd (fresh_regs def n))| = n.

definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
  λdef: ertl_internal_function.
  λn: nat.
    fresh_regs def n.
  @fresh_regs_length
qed.
  
definition save_hdws_internal ≝
  λdestr_srcr: register × 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: 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 params with
  [ nil ⇒ [get_params_hdw_internal]
  | _ ⇒
    let l ≝ zip_pottier ? ? params RegisterParams in
      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 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size 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 ≝
  λparams.
  match params with
  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
  | _ ⇒
    let f ≝ λi. λr. get_param_stack i r in
      mapi ? ? f params
  ].

definition get_params ≝
  λparams.
  let n ≝ min (length ? params) (length ? RegisterParams) in
  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
  let hdw_params ≝ get_params_hdw hdw_params in
    hdw_params @ (get_params_stack stack_params).
  
definition add_prologue ≝
  λparams: list register.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ ertl_if_entry def in
  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
  match lookup ? ? (ertl_if_graph def) start_lbl
    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
  [ None ⇒ λnone_absrd. ?
  | Some last_stmt ⇒ λsome_prf.
    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) @
         (get_params params))
        start_lbl tmp_lbl def
    in
      add_graph tmp_lbl last_stmt def
  ] ?.
  cases not_implemented (* dep. types here *)
qed.

definition save_return ≝
  λret_regs.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: ertl_internal_function.
  let 〈def, tmpr〉 ≝ fresh_reg def in
  match reduce_strong ? ? RegisterSTS ret_regs with
  [ dp crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let restl ≝ \snd (\fst crl) in
    let restr ≝ \snd (\snd crl) in
    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
    let defaults ≝ map ? ? f_default restl in
      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
  ].

definition assign_result ≝
  λstart_lbl: label.
  match reduce_strong ? ? RegisterRets RegisterSTS with
  [ dp crl crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
      adds_graph insts start_lbl
  ].

definition add_epilogue ≝
  λret_regs.
  λsral.
  λsrah.
  λsregs.
  λdef.
  let start_lbl ≝ ertl_if_exit def in
  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
  match lookup ? ? (ertl_if_graph def) start_lbl
    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
  [ None ⇒ λnone_absd. ?
  | Some last_stmt ⇒ λsome_prf.
    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
        ]] @
        [assign_result]
      ) start_lbl tmp_lbl def
    in
    let def ≝ add_graph tmp_lbl last_stmt def in
      change_exit_label tmp_lbl def ?
  ] ?.
  cases not_implemented (* dep types here, bug in matita too! *)
qed.
  
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.
  λsaved: rs_set rs.
  λdef.
    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
   
definition add_pro_and_epilogue ≝
  λparams.
  λret_regs.
  λdef.
  match fresh_regs_strong def 2 with
  [ dp def_sra def_sra_proof ⇒
    let def ≝ \fst def_sra in
    let sra ≝ \snd def_sra in
    let sral ≝ nth_safe ? 0 sra ? in
    let srah ≝ nth_safe ? 1 sra ? in
    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
    let def ≝ add_prologue params sral srah sregs def in
    let def ≝ add_epilogue ret_regs sral srah sregs def in
      def
  ].
  [1: >def_sra_proof //
  |2: >def_sra_proof //
  ]
qed.

definition set_params_hdw ≝
  λparams.
  match params with
  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
  | _ ⇒
    let l ≝ zip_pottier ? ? params RegisterParams in
      restore_hdws l
  ].

definition set_param_stack ≝
  λoff.
  λsrcr.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef: ertl_internal_function.
  let 〈def, addr1〉 ≝ fresh_reg def in
  let 〈def, addr2〉 ≝ fresh_reg def in
  let 〈def, tmpr〉 ≝ fresh_reg def in
  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    adds_graph [
      ertl_st_int addr1 int_off 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 (zero ?) 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 params with
  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
  | _ ⇒
    let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
      mapi ? ? f params
  ].

axiom min_fst:
  ∀m, n: nat.
    min m n ≤ m.

definition set_params ≝
  λparams.
  let n ≝ min (|params|) (|RegisterParams|) in
  let hdw_stack_params ≝ split ? params n ? in
  let hdw_params ≝ \fst hdw_stack_params in
  let stack_params ≝ \snd hdw_stack_params in
    set_params_hdw hdw_params @ set_params_stack stack_params.
  @min_fst
qed.

definition fetch_result ≝
  λret_regs.
  λstart_lbl: label.
  match reduce_strong ? ? RegisterSTS RegisterRets with
  [ dp crl first_crl_proof ⇒
    let commonl ≝ \fst (\fst crl) in
    let commonr ≝ \fst (\snd crl) in
    let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    match reduce_strong ? ? ret_regs RegisterSTS with
    [ dp crl second_crl_proof ⇒
      let commonl ≝ \fst (\fst crl) in
      let commonr ≝ \fst (\snd crl) in
      let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
        adds_graph (saves @ restores) start_lbl
    ]
  ].
  [ normalize nodelta; @second_crl_proof
  | @first_crl_proof
  ]
qed.

definition translate_call_id ≝
  λf.
  λargs.
  λret_regs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  let nb_args ≝ |args| in
    add_translates (
      set_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.
  λstmt.
  λdef.
  match stmt with
  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x 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' ⇒  add_graph lbl (ertl_st_int r i lbl') def
  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
      add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
(* XXX: change from o'caml
    adds_graph [
      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
      ] lbl lbl' def
*)
  | rtl_st_op1 op1 destr srcr lbl' ⇒
    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
    add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
  | rtl_st_clear_carry lbl' ⇒
    add_graph lbl (ertl_st_clear_carry lbl') def
  | rtl_st_set_carry lbl' ⇒
    add_graph lbl (ertl_st_set_carry lbl') def
  | rtl_st_load destr addr1 addr2 lbl' ⇒
    add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
  | rtl_st_store addr1 addr2 srcr lbl' ⇒
    add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
  | rtl_st_call_id f args ret_regs lbl' ⇒
    translate_call_id f args ret_regs lbl lbl' def
  | rtl_st_cond srcr lbl_true lbl_false ⇒
    add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
  | rtl_st_return ⇒
    add_graph lbl ertl_st_return def
  | _ ⇒ ? (* assert false: not implemented or should not happen *)
  ].
  cases not_implemented
qed.    

(* hack with empty graphs used here *)
definition translate_funct_internal ≝
  λdef.
  let nb_params ≝ |rtl_if_params def| in
  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
  let entry' ≝ rtl_if_entry def in
  let exit' ≝ rtl_if_exit def in
  let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
  let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') 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)
      graph' ? ? in
  let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
    def'.
  [1: %
      [1: @entry'
      |2: normalize nodelta
          @graph_add_lookup
          @graph_add
      ]
  |2: %
      [1: @exit'
      |2: normalize nodelta
          @graph_add
      ]
  ]
qed.
    
definition translate_funct ≝
  λid_def: ident × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with
    [ Internal def ⇒ Internal ? (translate_funct_internal def)
    | External def ⇒ External ? def
    ] in
  〈id, def'〉.

definition generate ≝
  λstmt.
  λdef.
  let 〈entry, nuniv〉 ≝ fresh_label def in
  let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
    mk_ertl_internal_function
      nuniv (ertl_if_runiverse def) (ertl_if_params def)
      (ertl_if_locals def) (ertl_if_stacksize def) graph
      ? ?.
  [1: %
    [1: @entry
    |2: normalize nodelta;
        @graph_add
    ]
  |2: generalize in match (ertl_if_exit def)
      #HYP
      cases HYP
      #LBL #LBL_PRF
      %
      [1: @LBL
      |2: normalize nodelta;
          @graph_add_lookup
          @LBL_PRF
      ]
  ]
qed.
    
let rec find_and_remove_first_cost_label_internal
  (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
    on num_nodes ≝
  match num_nodes with
  [ O ⇒ 〈None ?, def〉
  | S num_nodes' ⇒
    match lookup ? ? (ertl_if_graph def) lbl with
    [ None ⇒ 〈None ?, def〉
    | Some stmt ⇒
      match stmt with
      [ ertl_st_cost cost_lbl next_lbl ⇒
          〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
      | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
      | ertl_st_return ⇒ 〈None ?, def〉
      | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 
      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
      ]
    ]
  ].
    
definition find_and_remove_first_cost_label ≝
  λdef.  
    find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (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 with
  [ None ⇒ def
  | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
  ].

definition move_first_cost_label_up ≝
  λA: Type[0].
  λid_def: A × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with
    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
    | External ext ⇒ def
    ]
  in
    〈id, def'〉.

definition translate ≝
  λp.
  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
  let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
  let vars ≝ map ? ? f (rtl_pr_functs p) in
    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).