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'.