Changeset 1270 for src/RTL/RTLTailcall.ma
 Timestamp:
 Sep 26, 2011, 3:59:28 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r1240 r1270 2 2 3 3 definition simplify_stmt ≝ 4 λglobals. 4 5 λexit: label. 5 6 λlbl: label. 6 λstmt .7 λgraph: rtl_statement_graph.7 λstmt: rtl_statement globals. 8 λgraph: codeT … (rtl_params globals). 8 9 match stmt with 9 [ rtl_st_tailcall_id f args ⇒ 10 add ? ? graph lbl (rtl_st_call_id f args [ ] exit) 11  rtl_st_tailcall_ptr f1 f2 args ⇒ 12 add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit) 13  _ ⇒ graph 14 ]. 10 [ joint_st_sequential seq DUMMY ⇒ 11 match seq with 12 [ joint_instr_extension ext ⇒ 13 match ext with 14 [ rtl_st_ext_tailcall_id f args ⇒ 15 add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit) 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) 18  _ ⇒ graph ] 19  _ ⇒ graph ] 20  _ ⇒ graph ]. 15 21 16 22 definition simplify_graph ≝ 23 λglobals. 17 24 λexit: label. 18 λgraph: rtl_statement_graph.19 foldi ? ? ? (simplify_stmt exit) graph graph.25 λgraph: codeT … (rtl_params globals). 26 foldi ? ? ? (simplify_stmt globals exit) graph graph. 20 27 21 28 axiom simplify_graph_preserves_labels: 22 ∀g: rtl_statement_graph. 29 ∀globals. 30 ∀g: codeT … (rtl_params globals). 23 31 ∀l: label. 24 32 ∀exit: label. 25 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.33 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?. 26 34 27 definition simplify_internal ≝ 28 λdef. 29 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 30 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 31 let rtl_if_result' ≝ rtl_if_result def in 32 let rtl_if_params' ≝ rtl_if_params def in 33 let rtl_if_locals' ≝ rtl_if_locals def in 34 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 35 let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in 36 let rtl_if_entry' ≝ rtl_if_entry def in 37 let rtl_if_exit' ≝ rtl_if_exit def in 38 mk_rtl_internal_function 39 rtl_if_luniverse' rtl_if_runiverse' 40 rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize' 41 rtl_if_graph' ? ?. 42 normalize nodelta 43 [1: cases rtl_if_entry' 44 #ENTRY #ENTRY_PRF 45 % 46 [1: @ENTRY 47 2: @simplify_graph_preserves_labels 48 @ENTRY_PRF 49 ] 50 2: cases rtl_if_exit' 51 #EXIT #EXIT_PRF 52 % 53 [1: @EXIT 54 2: @simplify_graph_preserves_labels 55 @EXIT_PRF 56 ] 57 ] 35 definition simplify_internal : 36 ∀globals. 37 joint_internal_function … (rtl_params globals) → 38 joint_internal_function … (rtl_params globals) 39 ≝ 40 λglobals,def. 41 let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in 42 mk_joint_internal_function … 43 (joint_if_luniverse … def) (joint_if_runiverse … def) 44 (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def) 45 (joint_if_stacksize … def) graph 46 (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)). 47 [ cases (joint_if_entry … def)  cases (joint_if_exit … def) ] 48 #l #IH @simplify_graph_preserves_labels @IH 58 49 qed. 59 50 60 51 definition tailcall_simplify : rtl_program → rtl_program ≝ 61 λp. transform_program … p (transf_fundef … simplify_internal).52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracChangeset
for help on using the changeset viewer.