source: src/ERTL/ERTLToLTL.ma @ 1167

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

(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)

inductive decision: Type[0] ≝
  | decision_spill: Byte → decision
  | decision_colour: Register → decision.
  
axiom lookup: register → decision.

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

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 ≝
  λglobals.
  λint_fun.
    colour_locals + (ertl_if_stacksize globals int_fun).

definition stacksize ≝
  λglobals.
  λint_fun.
    colour_locals + (ertl_if_stacksize globals int_fun).

definition adjust_off ≝
  λ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 globals int_fun)) int_off false in
    sub.

definition get_stack ≝
  λglobals: list ident.
  λint_fun.
  λgraph: graph (ltl_statement (globals)).
  λr.
  λoff.
  λl.
    let off ≝ adjust_off globals int_fun off in
    let luniv ≝ ertl_if_luniverse globals int_fun in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in
    ?.
    
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.

definition set_stack ≝
  λint_fun.
  λglobals.
  λgraph: graph (ltl_statement (globals)).
  λoff.
  λr.
  λl.
  let off ≝ adjust_off int_fun off in
  let luniv ≝ ertl_if_luniverse int_fun in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.

definition write ≝
  λint_fun.
  λglobals.
  λgraph: graph (ltl_statement (globals)).
  λr: register.
  λl: label.
  match lookup r with
  [ decision_spill off ⇒
    let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in
    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
      〈RegisterSST, 〈l, 〈graph, luniv〉〉〉
  | decision_colour hwr ⇒
    let luniv ≝ ertl_if_luniverse int_fun in
      〈hwr, 〈l, 〈graph, luniv〉〉〉
  ].

definition read ≝
  λint_fun.
  λglobals.
  λgraph: graph (ltl_statement (globals)).
  λr: register.
  λstmt: Register → ltl_statement globals.
  match lookup r with
  [ decision_colour hwr ⇒ generate globals graph (stmt hwr)
  | decision_spill off ⇒
    let temphwr ≝ RegisterSST in
    let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in
    let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in
      generate globals graph stmt
  ].

definition move ≝
  λint_fun.
  λglobals: list ident.
  λgraph: graph (ltl_statement globals).
  λdest: decision.
  λsrc: decision.
  λl: label.
  match dest with
  [ decision_colour dest_hwr ⇒
    match src with
    [ decision_colour src_hwr ⇒
      if eq_Register dest_hwr src_hwr then
        〈joint_st_goto ? globals l, graph〉
      else
        let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
          〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉
    | decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l
    ]
  | decision_spill dest_off ⇒
    match src with
    [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l
    | decision_spill src_off ⇒
      if eq_bv ? dest_off src_off then
        〈joint_st_goto ? globals l, graph〉
      else
        let temp_hwr ≝ RegisterSST in
        let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in
        let 〈l, graph〉 ≝ generate globals graph stmt in
          get_stack int_fun globals graph temp_hwr src_off l
    ]
  ].

definition newframe ≝
  λint_fun.
  λglobals.
  λgraph: graph (ltl_statement globals).
  λl.
  if eq_nat (stacksize int_fun) 0 then
    〈joint_st_goto ? globals l, graph〉
  else
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
      〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉.

definition delframe ≝
  λint_fun.
  λglobals.
  λgraph: graph (ltl_statement globals).
  λl.
  if eq_nat (stacksize int_fun) 0 then
    〈joint_st_goto ? globals l, graph〉
  else
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.

definition translate_statement ≝
  λint_fun.
  λglobals: list ident.
  λgraph: graph (ltl_statement globals).
  λstmt: ertl_statement.
  match stmt with
  [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
  | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
  | ertl_st_hdw_to_hdw r1 r2 l ⇒
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
  | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
  | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
  | ertl_st_frame_size r l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    let 〈l, graph〉 ≝ l in
      〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
  | ertl_st_pop r l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
      〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
  | ertl_st_push r l ⇒
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_addr rl rh x l ⇒
    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
(*  | ertl_st_addr_h r x l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
  | ertl_st_addr_l r x l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
*)
  | ertl_st_int r i l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    let 〈l, graph〉 ≝ l in
      〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
    let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
(*
  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      joint_st_goto ? globals l
  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      joint_st_goto ? globals l
*)
  | ertl_st_op1 op1 destr srcr l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
  | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
  | ertl_st_load destr addr1 addr2 l ⇒
    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    let 〈l, graph〉 ≝ l in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_store addr1 addr2 srcr l ⇒
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
  | ertl_st_cond srcr lbl_true lbl_false ⇒
    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
      〈joint_st_goto ? globals l, graph〉
  | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
  ].
  cases daemon (* XXX: todo -- proofs regarding gvars *)
qed.

(* **** *)

definition translate_internal ≝
  λglobals: list ident.
  λf.
  λint_fun: ertl_internal_function.
  let lookup ≝ λr.
    match lookup r with
    | colour_spill ->
        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    | colour_colour color ->
        ERTLToLTLI.Color color
  in
  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
  let stacksize ≝ (ertl_if_params int_fun) + locals in
    mk_ltl_internal_function
      globals
      (ertl_if_luniverse int_fun)
      (ertl_if_runiverse int_fun)
      stacksize.

  let () =
    Label.Map.iter (fun label stmt ->
      let stmt =
        match Liveness.eliminable (G.liveafter label) stmt with
        | Some successor ->
            LTL.St_skip successor
        | None ->
            I.translate_statement stmt
      in
      graph := Label.Map.add label stmt !graph
    ) int_fun.ERTL.f_graph
  in

definition translate_funct ≝
  λname_def.
  let 〈name, def〉 ≝ name_def in
  let def' ≝
    match def with
    [ Internal def ⇒ Internal ? (translate_internal name def)
    | External def ⇒ External ? def
    ]
  in
    〈name, def'〉.

definition translate ≝
  λp.
  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).