source: src/utilities/Colouring.ma @ 1193

Last change on this file since 1193 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 
1include "ASM/I8051.ma".
2include "utilities/Interference.ma".
3include "utilities/RegisterSet.ma".
4
5inductive decision: Type[0] ≝
6  | decision_spill: decision
7  | decision_colour: Register → decision.
8
9definition colouring ≝ vertex_map decision.
10
11(* XXX: was set data structure previously *)
12definition colour_set ≝ rs_set.
13
14definition 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
28definition colours ≝ λrs. rs_from_list rs RegistersAllocatable.
29
30definition k ≝ |RegistersAllocatable|.
31
32definition 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   
39definition high ≝
40  λgraph.
41  λv.
42    geb (ig_degree graph v) k.
43
44definition high_neighbours ≝
45  λgraph.
46  λv.
47    vs_filter (high graph) (ig_ipp graph v).
48
49definition 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.