Changeset 2286 for src/RTL/RTLTailcall.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r2103 r2286 5 5 λexit: label. 6 6 λlbl: label. 7 λstmt: rtl_statementglobals.8 λgraph: codeT … (rtlntc_params globals).7 λstmt: joint_statement RTL globals. 8 λgraph: codeT RTL_ntc globals. 9 9 match stmt with 10 [ sequential seq DUMMY⇒11 match seqwith12 [ extensionext ⇒10 [ final fin ⇒ 11 match fin with 12 [ tailcall ext ⇒ 13 13 match ext with 14 [ rtl_ st_ext_tailcall_id f args ⇒15 add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)16  rtl_ st_ext_tailcall_ptr f1 f2 args ⇒17 add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)18  _ ⇒ graph]14 [ rtl_tailcall_id f args ⇒ 15 add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit) 16  rtl_tailcall_ptr f1 f2 args ⇒ 17 add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit) 18 ] 19 19  _ ⇒ graph ] 20 20  _ ⇒ graph ]. … … 23 23 λglobals. 24 24 λexit: label. 25 λgraph: codeT … (rtl_params globals).25 λgraph: codeT RTL globals. 26 26 foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …). 27 27 28 28 axiom simplify_graph_preserves_labels: 29 29 ∀globals. 30 ∀g: codeT … (rtl_params globals). 31 ∀l: label. 30 ∀g: codeT RTL globals. 32 31 ∀exit: label. 33 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.32 ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g. 34 33 35 34 definition simplify_internal : 36 35 ∀globals. 37 joint_internal_function … (rtl_params globals)→38 joint_internal_function … (rtlntc_params globals)36 joint_internal_function RTL globals → 37 joint_internal_function RTL_ntc globals 39 38 ≝ 40 39 λglobals,def. … … 49 48 qed. 50 49 51 definition tailcall_simplify : rtl_program → rtl ntc_program ≝50 definition tailcall_simplify : rtl_program → rtl_ntc_program ≝ 52 51 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracChangeset
for help on using the changeset viewer.