include "RTL/RTL.ma".

definition simplify_stmt ≝
  λglobals.
  λexit: label.
  λstmt: joint_statement RTL globals.
  match stmt with
  [ final fin ⇒
     match fin with
      [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit
      | RETURN ⇒ RETURN RTL_ntc
      | GOTO l ⇒ GOTO RTL_ntc l
      ]
  | sequential s next ⇒
    sequential RTL_ntc ?
    (match s return λ_.joint_step RTL_ntc globals with
    [ step_seq s ⇒
      match s return λ_.joint_seq RTL_ntc globals with
      [ COMMENT s ⇒ COMMENT … s
      | COST_LABEL l ⇒ COST_LABEL … l
      | MOVE m ⇒ MOVE … m
      | POP a ⇒ POP … a
      | PUSH a ⇒ PUSH … a
      | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph
      | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2
      | OP1 op a arg ⇒ OP1 … op a arg
      | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2
      | CLEAR_CARRY ⇒ CLEAR_CARRY ??
      | SET_CARRY ⇒ SET_CARRY ??
      | LOAD a dpl dph ⇒ LOAD … a dpl dph
      | STORE dpl dph a ⇒ STORE … dpl dph a
      | CALL f args dest ⇒ CALL … f args dest
      | extension_seq s ⇒ extension_seq … s
      ]
    | COND a ltrue ⇒ COND … a ltrue
    ]) next
  ].

definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
λtag,A,B,f,m.
match m with
[ an_id_map m ⇒ an_id_map … (map … f m)
].

definition simplify_graph ≝
  λglobals.
  λexit: label.
  λgraph: codeT RTL globals.
  id_map_map … (simplify_stmt globals exit) graph.

axiom simplify_graph_preserves_labels:
  ∀globals.
  ∀g: codeT RTL globals.
  ∀exit: label.
  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
    
definition simplify_internal :
 ∀globals.
  joint_closed_internal_function RTL globals →
   joint_closed_internal_function RTL_ntc globals
≝
  λglobals,def.
    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
    «mk_joint_internal_function …
       (joint_if_luniverse … def) (joint_if_runiverse … def)
       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
       (joint_if_stacksize … def) graph
       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?».
 [3: cases daemon (* TODO *)
 | cases (joint_if_exit … def) | cases (joint_if_entry … def) ]
 #l #IH @simplify_graph_preserves_labels @IH
qed.

definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).