include "RTL/RTL.ma".

definition simplify_stmt ≝
  λglobals.
  λexit: label.
  λlbl: label.
  λstmt: rtl_statement globals.
  λgraph: codeT … (rtlntc_params globals).
  match stmt with
  [ sequential seq DUMMY ⇒
     match seq with
      [ extension ext ⇒
         match ext with
          [ rtl_st_ext_tailcall_id f args ⇒
              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit) 
          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
          | _ ⇒ graph ]
      | _ ⇒ graph ]
  | _ ⇒ graph ].

definition simplify_graph ≝
  λglobals.
  λexit: label.
  λgraph: codeT … (rtl_params globals).
    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).

axiom simplify_graph_preserves_labels:
  ∀globals.
  ∀g: codeT … (rtl_params globals).
  ∀l: label.
  ∀exit: label.
    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
    
definition simplify_internal :
 ∀globals.
  joint_internal_function … (rtl_params globals) →
   joint_internal_function … (rtlntc_params 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)).
 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
 #l #IH @simplify_graph_preserves_labels @IH
qed.

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