source: src/ERTL/build.ma @ 1187

Last change on this file since 1187 was 1187, checked in by mulligan, 9 years ago

fixed build.ma

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