Changeset 1211
 Timestamp:
 Sep 14, 2011, 4:14:59 PM (9 years ago)
 Location:
 src/utilities
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1210 r1211 9 9 include "utilities/adt/register_table.ma". 10 10 11 definition vertex_set ≝ set _adt vertex vertex_ordered.12 definition vertex_priority_set ≝ priority_set _adt vertex vertex_ordered.13 definition Register_set ≝ set _adt Register Register_ordered.11 definition vertex_set ≝ set vertex. 12 definition vertex_priority_set ≝ priority_set vertex. 13 definition Register_set ≝ set Register. 14 14 15 record graph 16 (set_impl: set_adt … Register Register_ordered): Type[1] ≝ 15 record graph: Type[1] ≝ 17 16 { 18 ig_reg_table : register_table_adt set_impl; 19 ig_vertex_set : vertex_set; 20 ig_vertex_pset: vertex_priority_set; 21 ig_Reg_set : Register_set; 22 ig_regmap : register_table set_impl ig_reg_table; 23 ig_ivv : set … ig_vertex_set vertex; 24 ig_ivh : set … ig_Reg_set Register; 25 ig_pvv : set … ig_vertex_set vertex; 26 ig_pvh : set … ig_Reg_set Register; 27 ig_degree : priority_set … ig_vertex_pset vertex; 28 ig_nmr : priority_set … ig_vertex_pset vertex 17 ig_regmap : register_table; 18 ig_ivv : vertex_set; 19 ig_ivh : Register_set; 20 ig_pvv : vertex_set; 21 ig_pvh : Register_set; 22 ig_degree : vertex_priority_set; 23 ig_nmr : vertex_priority_set 29 24 }. 30 25 31 26 definition ig_create ≝ 32 λReg_set_impl: set_adt … Register Register_ordered.33 λvertex_set_impl: set_adt … vertex vertex_ordered.34 λvertex_priority_set_impl: priority_set_adt … vertex vertex_ordered.35 λReg_table_impl: register_table_adt Reg_set_impl.36 27 λregs. 37 28 let 〈ignore_int, table'', priority''〉 ≝ 38 29 foldr … (λr. λv_table_priority'. 39 30 let 〈v, table', priority'〉 ≝ v_table_priority' in 40 let table'' ≝ rt_add ? Reg_table_implr v table' in41 let priority'' ≝ ps_insert ? ? vertex_priority_set_implv 0 priority' in31 let table'' ≝ rt_add r v table' in 32 let priority'' ≝ ps_insert ? v 0 priority' in 42 33 〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs 43 34 in 44 mk_graph Reg_set_impl 45 Reg_table_impl vertex_set_impl vertex_priority_set_impl 46 Reg_set_impl table'' (set_empty …) (set_empty …) (set_empty …) 35 mk_graph table'' (set_empty …) (set_empty …) (set_empty …) 47 36 (set_empty …) priority'' priority''. 48 37 
src/utilities/adt/register_table.ma
r1210 r1211 20 20 axiom rt_remove: vertex → register_table → register_table. 21 21 22 axiom rt_fold: ∀a: Type[0]. (vertex → set … set_implRegister → a → a) →23 register_table → a → a ;22 axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) → 23 register_table → a → a. 24 24 25 25 axiom rt_coalesce: vertex → vertex → register_table → register_table.
Note: See TracChangeset
for help on using the changeset viewer.