Last change
on this file since 1219 was
1193,
checked in by mulligan, 9 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.