Changeset 1193 for src/utilities


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!)

Location:
src/utilities
Files:
3 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
  • src/utilities/Interference.ma

    r1192 r1193  
    88(* vertex sets *)
    99axiom vertex_set: Type[0].
     10axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     11axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     12axiom vs_subset: vertex_set → vertex_set → bool.
    1013
    1114(* vertex maps *)
    12 axiom vertex_map: Type[0].
     15axiom vertex_map: Type[0] → Type[0].
     16axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    1317
    1418definition interference_graph ≝ graph label.
     
    3539  interference_graph → option vertex.
    3640axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    37 axiom ig_ipp: interference_graph → vertex → list vertex.
     41axiom ig_ipp: interference_graph → vertex → vertex_set.
    3842axiom ig_iph: interference_graph → vertex → list Register.
    39 axiom ig_ppp: interference_graph → vertex → list vertex.
     43axiom ig_ppp: interference_graph → vertex → vertex_set.
    4044axiom ig_pph: interference_graph → vertex → list Register.
    4145definition ig_ppedge ≝ vertex × vertex.
  • src/utilities/RegisterSet.ma

    r1075 r1193  
    1111  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
     13  rs_subset: rs_set → rs_set → bool;
    1314  rs_to_list: rs_set → list Register;
    1415  rs_from_list: list Register → rs_set
     
    4546  λs: list Register.
    4647    nub_by ? eq_Register (r @ s).
     48
     49definition rs_list_set_subset ≝
     50  λr: list Register.
     51  λs: list Register.
     52    forall … (λx. member … eq_Register x s) r.
    4753 
    4854definition rs_list_set_from_list ≝
     
    5561                  rs_list_set_insert rs_list_set_exists
    5662                  rs_list_set_union
     63                  rs_list_set_subset
    5764                  (λx. x) rs_list_set_from_list.
Note: See TracChangeset for help on using the changeset viewer.