source: src/utilities/Colouring.ma @ 1219

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 
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.