Changeset 1193 for src/utilities
 Timestamp:
 Sep 6, 2011, 3:49:31 PM (9 years ago)
 Location:
 src/utilities
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Colouring.ma
r1192 r1193 1 1 include "ASM/I8051.ma". 2 2 include "utilities/Interference.ma". 3 include "utilities/RegisterSet.ma". 3 4 4 5 inductive decision: Type[0] ≝ … … 6 7  decision_colour: Register → decision. 7 8 8 definition colouring ≝ 9 definition colouring ≝ vertex_map decision. 10 11 (* XXX: was set data structure previously *) 12 definition colour_set ≝ rs_set. 13 14 definition 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 28 definition colours ≝ λrs. rs_from_list rs RegistersAllocatable. 29 30 definition k ≝ RegistersAllocatable. 31 32 definition 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 39 definition high ≝ 40 λgraph. 41 λv. 42 geb (ig_degree graph v) k. 43 44 definition high_neighbours ≝ 45 λgraph. 46 λv. 47 vs_filter (high graph) (ig_ipp graph v). 48 49 definition 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 8 8 (* vertex sets *) 9 9 axiom vertex_set: Type[0]. 10 axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A. 11 axiom vs_filter: (vertex → bool) → vertex_set → vertex_set. 12 axiom vs_subset: vertex_set → vertex_set → bool. 10 13 11 14 (* vertex maps *) 12 axiom vertex_map: Type[0]. 15 axiom vertex_map: Type[0] → Type[0]. 16 axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A. 13 17 14 18 definition interference_graph ≝ graph label. … … 35 39 interference_graph → option vertex. 36 40 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A. 37 axiom ig_ipp: interference_graph → vertex → list vertex.41 axiom ig_ipp: interference_graph → vertex → vertex_set. 38 42 axiom ig_iph: interference_graph → vertex → list Register. 39 axiom ig_ppp: interference_graph → vertex → list vertex.43 axiom ig_ppp: interference_graph → vertex → vertex_set. 40 44 axiom ig_pph: interference_graph → vertex → list Register. 41 45 definition ig_ppedge ≝ vertex × vertex. 
src/utilities/RegisterSet.ma
r1075 r1193 11 11 rs_exists: Register → rs_set → bool; 12 12 rs_union: rs_set → rs_set → rs_set; 13 rs_subset: rs_set → rs_set → bool; 13 14 rs_to_list: rs_set → list Register; 14 15 rs_from_list: list Register → rs_set … … 45 46 λs: list Register. 46 47 nub_by ? eq_Register (r @ s). 48 49 definition rs_list_set_subset ≝ 50 λr: list Register. 51 λs: list Register. 52 forall … (λx. member … eq_Register x s) r. 47 53 48 54 definition rs_list_set_from_list ≝ … … 55 61 rs_list_set_insert rs_list_set_exists 56 62 rs_list_set_union 63 rs_list_set_subset 57 64 (λx. x) rs_list_set_from_list.
Note: See TracChangeset
for help on using the changeset viewer.