 Timestamp:
 Sep 13, 2011, 4:33:10 PM (9 years ago)
 Location:
 src/utilities
 Files:

 6 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1196 r1208 3 3 include "common/Graphs.ma". 4 4 include "common/Registers.ma". 5 include "utilities/RegisterSet.ma". 5 6 include "utilities/adt/table_adt.ma". 7 include "utilities/adt/priority_set_adt.ma". 8 include "utilities/adt/set_adt.ma". 6 9 7 10 definition vertex ≝ nat. (* XXX: int in o'caml *) … … 17 20 axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A. 18 21 19 definition interference_graph ≝ graph label. 22 axiom ordered_vertex: ordered vertex. 23 axiom ordered_register: ordered register. 24 axiom ordered_Register: ordered Register. 20 25 21 definition ig_create: ∀rs. rs_set rs → interference_graph ≝ 22 let 〈ignore_int, regmap, degree〉 ≝ 23 rs_fold rs (λr. λv_regmap_degree. 24 let 〈v, regmap, degree〉 ≝ v_regmap_degree in 25 〈v + 1, (r, v)::regmap, 26 record interference_graph: Type[1] ≝ 27 { 28 ig_reg_table : table_adt register vertex ordered_register; 29 ig_vertex_set : set_adt vertex ordered_vertex; 30 ig_vertex_pset: priority_set_adt vertex ordered_vertex; 31 ig_Reg_set : set_adt Register ordered_Register; 32 ig_regmap : table … ig_reg_table register vertex; 33 ig_ivv : set … ig_vertex_set vertex; 34 ig_ivh : set … ig_Reg_set Register; 35 ig_pvv : set … ig_vertex_set vertex; 36 ig_pvh : set … ig_Reg_set Register; 37 ig_degree : priority_set … ig_vertex_pset vertex; 38 ig_nmr : priority_set … ig_vertex_pset vertex 39 }. 26 40 41 definition ig_create ≝ 42 λreg_table : table_adt register vertex ordered_register. 43 λvertex_set : set_adt vertex ordered_vertex. 44 λvertex_pset: priority_set_adt vertex ordered_vertex. 45 λReg_set : set_adt Register ordered_Register. 46 λregs. 47 let 〈ignore_int, table'', priority''〉 ≝ 48 foldr … (λr. λv_table_priority'. 49 let 〈v, table', priority'〉 ≝ v_table_priority' in 50 let table'' ≝ insert … reg_table r v table' in 51 let priority'' ≝ insert … vertex_pset v 0 priority' in 52 〈v + 1, table'', priority''〉) 〈0, empty …, empty …〉 regs 53 in 54 mk_interference_graph 55 reg_table vertex_set vertex_pset Reg_set 56 table'' [ ] [ ] [ ] [ ] priority'' priority''. 27 57 58 definition ig_mkipp: interference_graph → list register → list register → 59 interference_graph ≝ 60 λgraph. 61 λregs1. 62 λregs2. 63 foldr … (λr. λgraph. 64 let v1 ≝ lookup 28 65 66 let mkipp graph regs1 regs2 = 67 Register.Set.fold (fun r1 graph > 68 let v1 = lookup graph r1 in 69 Register.Set.fold (fun r2 graph > 70 interference#mkvv graph v1 (lookup graph r2) 71 ) regs2 graph 72 ) regs1 graph 29 73 30 let create regs =31 let (_ : int), regmap, degree =32 Register.Set.fold (fun r (v, regmap, degree) >33 v+1,34 RegMap.add r v regmap,35 PrioritySet.add v 0 degree36 ) regs (0, RegMap.empty, PrioritySet.empty)37 in38 {39 regmap = regmap;40 ivv = Vertex.Map.empty;41 ivh = Vertex.Map.empty;42 pvv = Vertex.Map.empty;43 pvh = Vertex.Map.empty;44 degree = degree;45 nmr = degree46 }47 48 49 axiom ig_mki: interference_graph → (list register) × (list Register) →50 (list register) × (list Register) → interference_graph.51 74 axiom ig_mkiph: interference_graph → list register → list Register → 52 75 interference_graph. 76 77 definition ig_mki: interference_graph → (list register) × (list Register) → 78 (list register) × (list Register) → interference_graph ≝ 79 λgraph. 80 λregs1_hwregs1. 81 λregs2_hwregs2. 82 let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in 83 let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in 84 let graph ≝ ig_mkipp graph regs1 regs2 in 85 let graph ≝ ig_mkiph graph regs1 hwregs2 in 86 let graph ≝ ig_mkiph graph regs2 hwregs1 in 87 graph. 88 53 89 axiom ig_mkppp: interference_graph → register → register → interference_graph. 54 90 axiom ig_mkpph: interference_graph → register → Register → interference_graph.
Note: See TracChangeset
for help on using the changeset viewer.