source: src/ERTL/build.ma @ 1223

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

changes

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