source: src/ERTL/build.ma @ 1246

Last change on this file since 1246 was 1229, checked in by mulligan, 8 years ago

changes

File size: 2.0 KB
Line 
1include "ERTL/liveness.ma".
2(* include "utilities/Interference.ma". *)
3
4(*
5definition build ≝
6  λglobals: list ident.
7  λint_fun: ertl_internal_function globals.
8  let liveafter ≝ analyse globals int_fun in
9  let graph ≝ ig_create (ertl_if_locals globals int_fun) in
10  let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in
11  let graph ≝
12    foldi ? ? ? (λlabel. λstmt. λgraph.
13      let live ≝ liveafter label in
14      match eliminable globals live stmt with
15      [ Some _ ⇒ graph
16      | None   ⇒
17        let defined ≝ defined globals stmt in
18        let exceptions ≝
19          match stmt with
20          [ joint_st_sequential seq l ⇒
21            match seq with
22            [ joint_instr_move pair_reg ⇒
23              let reg_r ≝ \snd pair_reg in
24              match reg_r with
25              [ hardware hw ⇒ lattice_hsingleton hw
26              | pseudo   ps ⇒ lattice_psingleton ps
27              ]
28            | _                         ⇒ ?
29            ]
30          | _ ⇒ ?
31          ]
32        in
33        let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in
34        let graph ≝
35          match stmt with
36          [ joint_st_sequential seq l ⇒
37            match seq with
38            [ joint_instr_move pair_reg ⇒
39              let reg_l ≝ \fst pair_reg in
40              let reg_r ≝ \snd pair_reg in
41              match reg_l with
42              [ pseudo ps1 ⇒
43                match reg_r with
44                [ pseudo ps2  ⇒ ig_mkppp graph ps1 ps2
45                | hardware hw ⇒ ig_mkpph graph ps1 hw
46                ]
47              | hardware hw1 ⇒
48                match reg_r with
49                [ pseudo ps    ⇒ ig_mkpph graph ps hw1
50                | hardware hw2 ⇒ graph
51                ]
52              ]
53            | _ ⇒ graph
54            ]
55          | _ ⇒ graph
56          ]
57        in graph
58      ]) (ertl_if_graph globals int_fun) graph
59  in
60    〈liveafter, graph〉.
61  [*: @lattice_bottom ] (* XXX: matita bug here! *)
62qed. *)
Note: See TracBrowser for help on using the repository browser.