source: src/utilities/Colouring.ma @ 1227

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

changes

File size: 1.3 KB
Line 
1include "ASM/I8051.ma".
2include "utilities/Interference.ma".
3
4inductive decision: Type[0] ≝
5  | decision_spill: decision
6  | decision_colour: Register → decision.
7
8definition colouring ≝ table vertex decision.
9
10(* XXX: was set data structure previously *)
11definition colour_set ≝ set register.
12
13definition add_colour ≝
14  λc: colouring.
15  λr: vertex.
16  λcs: colour_set.
17  match tbl_lookup … r c with
18  [ None ⇒ cs (* XXX: correct, or should we assert false? *)
19  | Some decision ⇒
20    match decision with
21    [ decision_spill ⇒ cs
22    | decision_colour colour ⇒ rs_insert rs colour cs
23    ]
24  ].
25
26definition colours ≝ λrs. rs_from_list rs RegistersAllocatable.
27
28definition k ≝ |RegistersAllocatable|.
29
30definition forbidden_colours ≝
31  λrs.
32  λgraph.
33  λcolouring.
34  λv.
35    vs_fold ? (add_colour rs colouring) (ig_ipp graph v) (rs_from_list rs (ig_iph graph v)).
36   
37definition high ≝
38  λgraph.
39  λv.
40    geb (ig_degree graph v) k.
41
42definition high_neighbours ≝
43  λgraph.
44  λv.
45    vs_filter (high graph) (ig_ipp graph v).
46
47definition georgepp ≝
48  λrs.
49  λgraph.
50  λab.
51  let 〈a, b〉 ≝ ab in
52    vs_subset … (high_neighbours graph a) (ig_ipp graph b) ∧
53      rs_subset rs (rs_from_list rs (ig_iph graph a)) (rs_from_list rs (ig_iph graph b)).
54
55
56
Note: See TracBrowser for help on using the repository browser.