Line | |
---|
1 | include "ASM/I8051.ma". |
---|
2 | include "utilities/Interference.ma". |
---|
3 | |
---|
4 | inductive decision: Type[0] ≝ |
---|
5 | | decision_spill: decision |
---|
6 | | decision_colour: Register → decision. |
---|
7 | |
---|
8 | definition colouring ≝ table vertex decision. |
---|
9 | |
---|
10 | (* XXX: was set data structure previously *) |
---|
11 | definition colour_set ≝ set register. |
---|
12 | |
---|
13 | definition 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 | |
---|
26 | definition colours ≝ λrs. rs_from_list rs RegistersAllocatable. |
---|
27 | |
---|
28 | definition k ≝ |RegistersAllocatable|. |
---|
29 | |
---|
30 | definition 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 | |
---|
37 | definition high ≝ |
---|
38 | λgraph. |
---|
39 | λv. |
---|
40 | geb (ig_degree graph v) k. |
---|
41 | |
---|
42 | definition high_neighbours ≝ |
---|
43 | λgraph. |
---|
44 | λv. |
---|
45 | vs_filter (high graph) (ig_ipp graph v). |
---|
46 | |
---|
47 | definition 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.