Last change
on this file since 1167 was
1144,
checked in by mulligan, 10 years ago

added build.ma file. matita bug found

File size:
1.3 KB

Line  

1  include "ERTL/liveness.ma". 

2  include "utilities/Interference.ma". 

3  

4  definition 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! *) 

37  qed. 

Note: See
TracBrowser
for help on using the repository browser.