include "LTL/LTL.ma".
include "ERTL/Interference.ma".
include "ASM/Arithmetic.ma".

definition fresh_label ≝
  λglobals: list ident.
  λluniv.
    fresh LabelTag luniv.

definition ltl_statement_graph ≝
  λglobals.
    graph … (ltl_statement globals).

definition add_graph ≝
  λglobals.
  λlabel.
  λstmt: ltl_statement globals.
  λgraph: ltl_statement_graph globals.
    add LabelTag ? graph label stmt.

definition generate ≝
  λglobals: list ident.
  λluniv.
  λgraph: ltl_statement_graph globals.
  λstmt: ltl_statement globals.
  let 〈l, luniv〉 ≝ fresh_label globals luniv in
  let graph ≝ add_graph globals l stmt graph in
    〈l, graph, luniv〉.

definition num_locals ≝
  λspilled_no.
  λglobals.
  λint_fun.
    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).

definition stacksize ≝
  λspilled_no.
  λglobals.
  λint_fun.
    spilled_no + (joint_if_stacksize globals (ertl_params globals) int_fun).

definition adjust_off ≝
  λspilled_no.
  λglobals.
  λint_fun.
  λoff.
  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals spilled_no globals int_fun)) int_off false in
    sub.

definition get_stack:
 nat → ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
  λspilled_no.
  λglobals: list ident.
  λint_fun.
  λgraph: graph (ltl_statement (globals)).
  λr.
  λoff.
  λl.
  λoriginal_label.
    let off ≝ adjust_off spilled_no globals int_fun off in
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.

definition set_stack:
  nat → ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    → Register → label → ? ≝
  λspilled_no.
  λglobals: list ident.
  λint_fun.
  λgraph: graph (ltl_statement (globals)).
  λoff.
  λr.
  λl.
  λoriginal_label.
  let off ≝ adjust_off spilled_no globals int_fun off in
  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.


definition write ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  λvaluation.
  λcoloured_graph.
  λgraph.
  λr.
  λl.
  λoriginal_label: label.
  match colouring valuation coloured_graph (inl … r) with
  [ decision_spill off ⇒
    let luniv ≝ joint_if_luniverse … int_fun in
    let 〈graph, luniv〉 ≝ set_stack (spilled_no … coloured_graph) globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
      〈RegisterSST, l, graph, luniv〉
  | decision_colour hwr ⇒
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
      〈hwr, l, graph, luniv〉
  ].

definition read ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  λvaluation.
  λcoloured_graph.
  λgraph.
  λr.
  λstmt.
  λoriginal_label: label.
  match colouring valuation coloured_graph (inl … r) with
  [ decision_colour hwr ⇒
    let luniv ≝ joint_if_luniverse … int_fun in
      〈add_graph globals original_label (stmt hwr) graph, luniv〉
  | decision_spill off ⇒
    let temphwr ≝ RegisterSST in
    let luniv ≝ joint_if_luniverse … int_fun in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
      get_stack (spilled_no … coloured_graph) globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
  ].

definition move ≝
  λspilled_no.
  λglobals: list ident.
  λint_fun.
  λgraph: graph (ltl_statement globals).
  λdest: decision.
  λsrc: decision.
  λl: label.
  λoriginal_label: label.
  match dest with
  [ decision_colour dest_hwr ⇒
    match src with
    [ decision_colour src_hwr ⇒
      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
      if eq_Register dest_hwr src_hwr then
        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
      else
        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
    | decision_spill src_off ⇒ get_stack spilled_no globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    ]
  | decision_spill dest_off ⇒
    match src with
    [ decision_colour src_hwr ⇒ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    | decision_spill src_off ⇒
      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
      if eq_nat dest_off src_off then
        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
      else
        let temp_hwr ≝ RegisterSST in
        let 〈graph, luniv〉 ≝ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
          get_stack spilled_no globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    ]
  ].

definition newframe ≝
  λspilled_no.
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  λgraph: ltl_statement_graph globals.
  λl: label.
  λoriginal_label: label.
  if eq_nat (stacksize spilled_no globals int_fun) 0 then
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
  else
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) in
      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.

definition delframe ≝
  λspilled_no.
  λglobals.
  λint_fun.
  λgraph: graph (ltl_statement globals).
  λl.
  λoriginal_label: label.
  if eq_nat (stacksize spilled_no globals int_fun) 0 then
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
  else
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) graph, luniv〉.

definition translate_statement:
  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
  λglobals: list ident.
  λint_fun.
  λvaluation.
  λcoloured_graph: coloured_graph valuation.
  λgraph: ltl_statement_graph globals.
  λstmt: ertl_statement globals.
  λoriginal_label: label.
  match stmt with
  [ sequential seq l ⇒
    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    match seq with
    [ COMMENT c ⇒
      〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
    | COST_LABEL cost_lbl ⇒
      〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
    | POP r ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
        〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
    | PUSH r ⇒
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    | COND srcr lbl_true ⇒
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
    | STORE addr1 addr2 srcr ⇒
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … l) graph, luniv〉
    | LOAD destr addr1 addr2 ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals ? int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
    | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
    | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
    | OP2 op2 destr srcr1 srcr2 ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … l) graph, luniv〉
    | OP1 op1 destr srcr ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … l) graph, luniv〉
    | INT r i ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
    | MOVE pair_regs ⇒
      let regl ≝ \fst pair_regs in
      let regr ≝ \snd pair_regs in
      match regl with
      [ pseudo p1  ⇒
        match regr with 
        [ pseudo p2  ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
        | hardware h ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
        ]
      | hardware h1 ⇒
        match regr with
        [ pseudo p    ⇒ move (spilled_no … coloured_graph) globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
        | hardware h2 ⇒
          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
            〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
        ]
      ]
    | ADDRESS lbl prf dpl dph ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
        〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
    | extension ext ⇒
      match ext with
      [ ertl_st_ext_new_frame ⇒ newframe (spilled_no … coloured_graph)globals int_fun graph l original_label
      | ertl_st_ext_del_frame ⇒ delframe (spilled_no … coloured_graph) globals int_fun graph l original_label
      | ertl_st_ext_frame_size r ⇒
        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize (spilled_no … coloured_graph) … int_fun))) l) graph, luniv〉
      ]
    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
        〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
    ]
  | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
  ].

definition graph_fold ≝
  λglobals.
  λb : Type[0].
  λf    : label → ertl_statement globals → b → b.
  λgraph: graph (ertl_statement globals).
  λseed : b.
    foldi (ertl_statement globals) b ? f graph seed.

definition translate_internal: ∀globals: list ident.
  ertl_internal_function globals → ltl_internal_function globals ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  let graph ≝ (empty_map … : ltl_statement_graph globals) in
  let valuation ≝ analyse globals int_fun in
  let coloured_graph ≝ build valuation in
  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
    let 〈graph, luniv〉 ≝ graph_luniv in
      match eliminable globals (valuation label) stmt with
      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
      | None           ⇒
        translate_statement globals int_fun valuation coloured_graph graph stmt label
      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
  in
    match joint_if_entry … int_fun with
    [ mk_Sig entry_label entry_label_prf ⇒
      match joint_if_exit … int_fun with
      [ mk_Sig exit_label exit_label_prf ⇒
          mk_joint_internal_function globals (ltl_params globals)
            luniv (joint_if_runiverse … int_fun)
              it it it (joint_if_stacksize … int_fun)
                graph ? ?
      ]
    ].
  [1: %
    [1: @entry_label
    |2: cases daemon (* XXX *)
    ]
  |2: %
    [1: @exit_label
    |2: cases daemon (* XXX *)
    ]
  ]
qed.

definition ertl_to_ltl: ertl_program → ltl_program ≝
  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).