Ignore:
Timestamp:
Sep 6, 2011, 3:49:31 PM (8 years ago)
Author:
mulligan
Message:

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Colouring.ma

    r1192 r1193  
    11include "ASM/I8051.ma".
    22include "utilities/Interference.ma".
     3include "utilities/RegisterSet.ma".
    34
    45inductive decision: Type[0] ≝
     
    67  | decision_colour: Register → decision.
    78
    8 definition colouring ≝
     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 TracChangeset for help on using the changeset viewer.