source: src/ERTL/build.ma @ 1227

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

changes

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