include "RTL/RTL.ma".

definition simplify_stmt ≝
  λexit: label.
  λlbl: label.
  λstmt.
  λgraph: rtl_statement_graph.
  match stmt with
  [ rtl_st_tailcall_id f args ⇒
      add ? ? graph lbl (rtl_st_call_id f args [ ] exit) 
  | rtl_st_tailcall_ptr f1 f2 args ⇒
      add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit)
  | _ ⇒ graph
  ].

definition simplify_graph ≝
  λexit: label.
  λgraph: rtl_statement_graph.
    foldi ? ? ? (simplify_stmt exit) graph graph.

axiom simplify_graph_preserves_labels:
  ∀g: rtl_statement_graph.
  ∀l: label.
  ∀exit: label.
    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
    
definition simplify_internal ≝
  λdef.
    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    let rtl_if_result' ≝ rtl_if_result def in
    let rtl_if_params' ≝ rtl_if_params def in
    let rtl_if_locals' ≝ rtl_if_locals def in
    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in
    let rtl_if_entry' ≝ rtl_if_entry def in
    let rtl_if_exit' ≝ rtl_if_exit def in
      mk_rtl_internal_function
        rtl_if_luniverse' rtl_if_runiverse'
        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
        rtl_if_graph' ? ?.
  normalize nodelta
  [1: cases rtl_if_entry'
      #ENTRY #ENTRY_PRF
      %
      [1: @ENTRY
      |2: @simplify_graph_preserves_labels
          @ENTRY_PRF
      ]
  |2: cases rtl_if_exit'
      #EXIT #EXIT_PRF
      %
      [1: @EXIT
      |2: @simplify_graph_preserves_labels
          @EXIT_PRF
      ]
  ]
qed.

definition simplify_funct ≝
  λid_def: ident × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with
    [ Internal def ⇒ Internal ? (simplify_internal def)
    | External def ⇒ External ? def
    ]
  in
    〈id, def'〉.
  
definition tailcall_simplify ≝
  λp.
  let rtl_pr_vars' ≝ rtl_pr_vars p in
  let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in
  let rtl_pr_main' ≝ rtl_pr_main p in
    mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'.