Last change
on this file since 1219 was
1193,
checked in by mulligan, 10 years ago

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

File size:
1.3 KB

Line  

1  include "ASM/I8051.ma". 

2  include "utilities/Interference.ma". 

3  include "utilities/RegisterSet.ma". 

4  

5  inductive decision: Type[0] ≝ 

6   decision_spill: decision 

7   decision_colour: Register → decision. 

8  

9  definition colouring ≝ vertex_map decision. 

10  

11  (* XXX: was set data structure previously *) 

12  definition colour_set ≝ rs_set. 

13  

14  definition add_colour ≝ 

15  λrs: register_set. 

16  λc: colouring. 

17  λr: vertex. 

18  λcs: colour_set rs. 

19  match vm_find … r c with 

20  [ None ⇒ cs (* XXX: correct, or should we assert false? *) 

21   Some decision ⇒ 

22  match decision with 

23  [ decision_spill ⇒ cs 

24   decision_colour colour ⇒ rs_insert rs colour cs 

25  ] 

26  ]. 

27  

28  definition colours ≝ λrs. rs_from_list rs RegistersAllocatable. 

29  

30  definition k ≝ RegistersAllocatable. 

31  

32  definition forbidden_colours ≝ 

33  λrs. 

34  λgraph. 

35  λcolouring. 

36  λv. 

37  vs_fold ? (add_colour rs colouring) (ig_ipp graph v) (rs_from_list rs (ig_iph graph v)). 

38  

39  definition high ≝ 

40  λgraph. 

41  λv. 

42  geb (ig_degree graph v) k. 

43  

44  definition high_neighbours ≝ 

45  λgraph. 

46  λv. 

47  vs_filter (high graph) (ig_ipp graph v). 

48  

49  definition georgepp ≝ 

50  λrs. 

51  λgraph. 

52  λab. 

53  let 〈a, b〉 ≝ ab in 

54  vs_subset … (high_neighbours graph a) (ig_ipp graph b) ∧ 

55  rs_subset rs (rs_from_list rs (ig_iph graph a)) (rs_from_list rs (ig_iph graph b)). 

56  

57  

58  

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