 Timestamp:
 Sep 6, 2011, 6:15:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1193 r1196 3 3 include "common/Graphs.ma". 4 4 include "common/Registers.ma". 5 include "utilities/RegisterSet.ma". 5 6 6 7 definition vertex ≝ nat. (* XXX: int in o'caml *) … … 18 19 definition interference_graph ≝ graph label. 19 20 20 axiom ig_create: list register → interference_graph. 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 27 28 29 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 degree 36 ) regs (0, RegMap.empty, PrioritySet.empty) 37 in 38 { 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 = degree 46 } 47 48 21 49 axiom ig_mki: interference_graph → (list register) × (list Register) → 22 50 (list register) × (list Register) → interference_graph.
Note: See TracChangeset
for help on using the changeset viewer.