source: src/RTL/RTLTailcall.ma @ 2497

Last change on this file since 2497 was 2490, checked in by tranquil, 8 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 2.5 KB
RevLine 
[784]1include "RTL/RTL.ma".
2
3definition simplify_stmt ≝
[1270]4  λglobals.
[784]5  λexit: label.
[2286]6  λstmt: joint_statement RTL globals.
[784]7  match stmt with
[2286]8  [ final fin ⇒
9     match fin with
[2490]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  ].
[1081]38
[2490]39definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
40λtag,A,B,f,m.
41match m with
42[ an_id_map m ⇒ an_id_map … (map … f m)
43].
44
[784]45definition simplify_graph ≝
[1270]46  λglobals.
[1081]47  λexit: label.
[2286]48  λgraph: codeT RTL globals.
[2490]49  id_map_map … (simplify_stmt globals exit) graph.
[1081]50
51axiom simplify_graph_preserves_labels:
[1270]52  ∀globals.
[2286]53  ∀g: codeT RTL globals.
[1081]54  ∀exit: label.
[2286]55  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
[784]56   
[1270]57definition simplify_internal :
58 ∀globals.
[2490]59  joint_closed_internal_function RTL globals →
60   joint_closed_internal_function RTL_ntc globals
[1270]61
62  λglobals,def.
63    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
[2490]64    «mk_joint_internal_function …
[1270]65       (joint_if_luniverse … def) (joint_if_runiverse … def)
66       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
67       (joint_if_stacksize … def) graph
[2490]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) ]
[1270]71 #l #IH @simplify_graph_preserves_labels @IH
[1081]72qed.
[784]73
[2286]74definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
[2103]75 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracBrowser for help on using the repository browser.