include "RTL/RTL_paolo.ma".

definition simplify_stmt ≝
  λglobals.
  λexit: label.
  λlbl: label.
  λstmt: rtl_statement globals.
  λgraph: codeT rtlntc_params globals.
  match stmt with
  [ final fin ⇒
     match fin with
      [ tailcall ext ⇒
         match ext with
          [ rtl_tailcall_id f args ⇒
              add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
          | rtl_tailcall_ptr f1 f2 args ⇒
              add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
          ]
      | _ ⇒ 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.
  ∀exit: label.
  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
    
definition simplify_internal :
 ∀globals.
  joint_internal_function globals rtl_params →
   joint_internal_function globals rtlntc_params
≝
  λ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 (λvarnames. transf_fundef … (simplify_internal varnames)).