include "RTL/RTL.ma".

(* dpm: this should not be option, fix *)
axiom map_fold:
  ∀A, B: Type[0].
  ∀f: label → A → B → option B.
  ∀m: rtl_statement_graph.
  ∀b: B.
    B.

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 lift_option3: ∀A, B, C, D. ∀f: A → B → C → D. A → B → C → option D ≝
  λA, B, C, D: Type[0].
  λf: A → B → C → D.
  λa: A.
  λb: B.
  λc: C.
    Some ? (f a b c).
  
definition simplify_graph ≝
  λexit.
  λgraph: rtl_statement_graph.
    map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph.
    
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_sig' ≝ rtl_if_sig 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_sig'
        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
        rtl_if_graph' rtl_if_entry' rtl_if_exit'.

definition simplify_funct ≝
  λid_def: ident × ?.
  let 〈id, def〉 ≝ id_def in
  let def' ≝
    match def with
    [ rtl_f_internal def ⇒ rtl_f_internal (simplify_internal def)
    | rtl_f_external def ⇒ rtl_f_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'.