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