Changeset 1275 for src/RTL/RTLTailcall.ma
 Timestamp:
 Sep 26, 2011, 6:07:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r1270 r1275 6 6 λlbl: label. 7 7 λstmt: rtl_statement globals. 8 λgraph: codeT … (rtl _params globals).8 λgraph: codeT … (rtlntc_params globals). 9 9 match stmt with 10 10 [ joint_st_sequential seq DUMMY ⇒ … … 15 15 add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit) 16 16  rtl_st_ext_tailcall_ptr f1 f2 args ⇒ 17 add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtl _st_ext_call_ptr f1 f2 args [ ])) exit)17 add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit) 18 18  _ ⇒ graph ] 19 19  _ ⇒ graph ] … … 24 24 λexit: label. 25 25 λgraph: codeT … (rtl_params globals). 26 foldi ? ? ? (simplify_stmt globals exit) graph graph.26 foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …). 27 27 28 28 axiom simplify_graph_preserves_labels: … … 36 36 ∀globals. 37 37 joint_internal_function … (rtl_params globals) → 38 joint_internal_function … (rtl _params globals)38 joint_internal_function … (rtlntc_params globals) 39 39 ≝ 40 40 λglobals,def. … … 49 49 qed. 50 50 51 definition tailcall_simplify : rtl_program → rtl _program ≝51 definition tailcall_simplify : rtl_program → rtlntc_program ≝ 52 52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracChangeset
for help on using the changeset viewer.