Changeset 1196


Ignore:
Timestamp:
Sep 6, 2011, 6:15:11 PM (8 years ago)
Author:
mulligan
Message:

some more changes, need some additional datastructures

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1193 r1196  
    33include "common/Graphs.ma".
    44include "common/Registers.ma".
     5include "utilities/RegisterSet.ma".
    56
    67definition vertex ≝ nat. (* XXX: int in o'caml *)
     
    1819definition interference_graph ≝ graph label.
    1920
    20 axiom ig_create: list register → interference_graph.
     21definition 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
     30let 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
    2149axiom ig_mki: interference_graph → (list register) × (list Register) →
    2250  (list register) × (list Register) → interference_graph.
Note: See TracChangeset for help on using the changeset viewer.