Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma

    r1153 r1197  
    33include "common/Graphs.ma".
    44include "common/Registers.ma".
     5include "utilities/RegisterSet.ma".
     6
     7definition vertex ≝ nat. (* XXX: int in o'caml *)
     8
     9(* vertex sets *)
     10axiom vertex_set: Type[0].
     11axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     12axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     13axiom vs_subset: vertex_set → vertex_set → bool.
     14
     15(* vertex maps *)
     16axiom vertex_map: Type[0] → Type[0].
     17axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    518
    619definition interference_graph ≝ graph label.
    7 axiom vertex: Type[0].
    8 axiom vertex_set: Type[0].
    9 axiom vertex_map: Type[0].
    1020
    11 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
    1249axiom ig_mki: interference_graph → (list register) × (list Register) →
    1350  (list register) × (list Register) → interference_graph.
     
    3067  interference_graph → option vertex.
    3168axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    32 axiom ig_ipp: interference_graph → vertex → list vertex.
     69axiom ig_ipp: interference_graph → vertex → vertex_set.
    3370axiom ig_iph: interference_graph → vertex → list Register.
    34 axiom ig_ppp: interference_graph → vertex → list vertex.
     71axiom ig_ppp: interference_graph → vertex → vertex_set.
    3572axiom ig_pph: interference_graph → vertex → list Register.
    3673definition ig_ppedge ≝ vertex × vertex.
Note: See TracChangeset for help on using the changeset viewer.