Changeset 2490 for src/RTL/RTLTailcall.ma
- Timestamp:
- Nov 25, 2012, 1:33:09 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLTailcall.ma
r2286 r2490 4 4 λglobals. 5 5 λexit: label. 6 λlbl: label.7 6 λstmt: joint_statement RTL globals. 8 λgraph: codeT RTL_ntc globals.9 7 match stmt with 10 8 [ final fin ⇒ 11 9 match fin with 12 [ tailcall ext ⇒ 13 match ext with 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 | _ ⇒ graph ] 20 | _ ⇒ graph ]. 10 [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit 11 | RETURN ⇒ RETURN RTL_ntc 12 | GOTO l ⇒ GOTO RTL_ntc l 13 ] 14 | sequential s next ⇒ 15 sequential RTL_ntc ? 16 (match s return λ_.joint_step RTL_ntc globals with 17 [ step_seq s ⇒ 18 match s return λ_.joint_seq RTL_ntc globals with 19 [ COMMENT s ⇒ COMMENT … s 20 | COST_LABEL l ⇒ COST_LABEL … l 21 | MOVE m ⇒ MOVE … m 22 | POP a ⇒ POP … a 23 | PUSH a ⇒ PUSH … a 24 | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph 25 | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2 26 | OP1 op a arg ⇒ OP1 … op a arg 27 | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2 28 | CLEAR_CARRY ⇒ CLEAR_CARRY ?? 29 | SET_CARRY ⇒ SET_CARRY ?? 30 | LOAD a dpl dph ⇒ LOAD … a dpl dph 31 | STORE dpl dph a ⇒ STORE … dpl dph a 32 | CALL f args dest ⇒ CALL … f args dest 33 | extension_seq s ⇒ extension_seq … s 34 ] 35 | COND a ltrue ⇒ COND … a ltrue 36 ]) next 37 ]. 38 39 definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝ 40 λtag,A,B,f,m. 41 match m with 42 [ an_id_map m ⇒ an_id_map … (map … f m) 43 ]. 21 44 22 45 definition simplify_graph ≝ … … 24 47 λexit: label. 25 48 λgraph: codeT RTL globals. 26 foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).49 id_map_map … (simplify_stmt globals exit) graph. 27 50 28 51 axiom simplify_graph_preserves_labels: … … 34 57 definition simplify_internal : 35 58 ∀globals. 36 joint_ internal_function RTL globals →37 joint_ internal_function RTL_ntc globals59 joint_closed_internal_function RTL globals → 60 joint_closed_internal_function RTL_ntc globals 38 61 ≝ 39 62 λglobals,def. 40 63 let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in 41 64 «mk_joint_internal_function … 42 65 (joint_if_luniverse … def) (joint_if_runiverse … def) 43 66 (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def) 44 67 (joint_if_stacksize … def) graph 45 (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)). 46 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ] 68 (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?». 69 [3: cases daemon (* TODO *) 70 | cases (joint_if_exit … def) | cases (joint_if_entry … def) ] 47 71 #l #IH @simplify_graph_preserves_labels @IH 48 72 qed.
Note: See TracChangeset
for help on using the changeset viewer.