source: Deliverables/D3.3/id-lookup-branch/ERTL/build.ma @ 1153

Last change on this file since 1153 was 1153, checked in by campbell, 8 years ago

Merge trunk into branch.

File size: 1.3 KB
Line 
1include "ERTL/liveness.ma".
2include "utilities/Interference.ma".
3
4definition build ≝
5  λint_fun: ertl_internal_function.
6  let liveafter ≝ analyse int_fun in
7  let graph ≝ ig_create (ertl_if_locals int_fun) in
8  let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in
9  let graph ≝
10    foldi ? ? ? (λlabel. λstmt. λgraph.
11      let live ≝ liveafter label in
12      match eliminable live stmt with
13      [ Some _ ⇒ graph
14      | None   ⇒
15        let defined ≝ defined stmt in
16        let exceptions ≝
17          match stmt with
18          [ ertl_st_move _ sr _    ⇒ lattice_psingleton sr
19          | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr
20          | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr
21          | _                      ⇒ ?
22          ]
23        in
24        let graph ≝ ig_mki graph (lattice_diff live exceptions) defined in
25        let graph ≝
26          match stmt with
27          [ ertl_st_move r1 r2 _    ⇒ ig_mkppp graph r1 r2
28          | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr
29          | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr
30          | _                       ⇒ graph
31          ]
32        in graph
33      ]) (ertl_if_graph int_fun) graph
34  in
35    〈liveafter, graph〉.
36  [*: @lattice_bottom ] (* XXX: matita bug here! *)
37qed.
Note: See TracBrowser for help on using the repository browser.