Changeset 1218 for src/utilities/Interference.ma

Timestamp:

Sep 15, 2011, 4:56:30 PM (8 years ago)

Author:

mulligan

Message:

a lot added to interference graph calculation

File:

• src/utilities/Interference.ma (modified) (3 diffs)

src/utilities/Interference.ma

@@ -12 +12 @@
 definition vertex_set ≝ set vertex.
 definition vertex_priority_set ≝ priority_set vertex.
+definition vertex_set_table ≝ set_table vertex (set vertex).
+definition Register_set_table ≝ set_table vertex (set Register).
 definition Register_set ≝ set Register.
 
-record graph: Type[1] ≝
+record graph: Type[0] ≝
 {
   ig_regmap     : register_table;
-  ig_ivv        : vertex_set;
-  ig_ivh        : Register_set;
+  ig_ivv        : vertex_set_table;
+  ig_ivh        : Register_set_table;
   ig_pvv        : vertex_set;
   ig_pvh        : Register_set;
@@ -24 +26 @@
   ig_nmr        : vertex_priority_set
 }.
+
+definition set_ivv ≝
+  λgraph.
+  λivv: vertex_set_table.
+    let regmap ≝ ig_regmap graph in
+    let ivh    ≝ ig_ivh graph in
+    let pvv    ≝ ig_pvv graph in
+    let pvh    ≝ ig_pvh graph in
+    let degree ≝ ig_degree graph in
+    let nmr    ≝ ig_nmr graph in
+      mk_graph
+        regmap ivv ivh pvv pvh degree nmr.
+
+definition set_ivh ≝
+  λgraph.
+  λivh: Register_set_table.
+    let regmap ≝ ig_regmap graph in
+    let ivv    ≝ ig_ivv graph in
+    let pvv    ≝ ig_pvv graph in
+    let pvh    ≝ ig_pvh graph in
+    let degree ≝ ig_degree graph in
+    let nmr    ≝ ig_nmr graph in
+      mk_graph
+        regmap ivv ivh pvv pvh degree nmr.
+
+definition set_degree ≝
+  λgraph.
+  λdegree: vertex_priority_set.
+    let regmap ≝ ig_regmap graph in
+    let ivv    ≝ ig_ivv graph in
+    let ivh    ≝ ig_ivh graph in
+    let pvv    ≝ ig_pvv graph in
+    let pvh    ≝ ig_pvh graph in
+    let nmr    ≝ ig_nmr graph in
+      mk_graph
+        regmap ivv ivh pvv pvh degree nmr.
+
+definition set_nmr ≝
+  λgraph.
+  λnmr: vertex_priority_set.
+    let regmap ≝ ig_regmap graph in
+    let ivv    ≝ ig_ivv graph in
+    let ivh    ≝ ig_ivh graph in
+    let pvv    ≝ ig_pvv graph in
+    let pvh    ≝ ig_pvh graph in
+    let degree ≝ ig_degree graph in
+      mk_graph
+        regmap ivv ivh pvv pvh degree nmr.
+
+definition sg_neighboursv ≝
+  λgraph: graph.
+  λv: vertex.
+    set_tbl_find … v (ig_ivv graph).
+
+definition sg_existsvv ≝
+  λgraph.
+  λv1.
+  λv2.
+  match sg_neighboursv graph v2 with
+  [ None       ⇒ false (* XXX: ok? *)
+  | Some neigh ⇒ set_member ? v1 neigh
+  ].
+
+definition sg_neighboursh ≝
+  λgraph.
+  λv.
+    set_tbl_find ? ? v (ig_ivh graph). 
+
+definition sg_existsvh ≝
+  λgraph.
+  λv.
+  λh.
+  match sg_neighboursh graph v with
+  [ None       ⇒ false (* XXX: ok? *)
+  | Some neigh ⇒ set_member ? h neigh
+  ].
+
+definition sg_degree ≝
+  λgraph.
+  λv.
+  match sg_neighboursv graph v with
+  [ None ⇒ None ?
+  | Some neigh ⇒
+    match sg_neighboursh graph v with
+    [ None ⇒ None ?
+    | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
+    ]
+  ].
+    
+definition sg_hwregs ≝
+  λgraph: graph.
+    let union ≝ λkey: vertex. set_union ? in
+    set_tbl_fold vertex ? ? union (ig_ivh graph) (set_empty Register).
+
+axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
+
+definition sg_mkvvi ≝
+  λgraph.
+  λv1.
+  λv2.
+    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (ig_ivv graph)).
+
+definition sg_mkvv ≝
+  λgraph.
+  λv1.
+  λv2.
+    if eq_nat v1 v2 then
+      graph
+    else if sg_existsvv graph v1 v2 then
+      graph
+    else
+      sg_mkvvi graph v1 v2.
+
+definition sg_rmvv ≝
+  λgraph.
+  λv1.
+  λv2.
+    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (ig_ivv graph)).
+
+definition sg_rmvvifx ≝
+  λgraph.
+  λv1.
+  λv2.
+  if sg_existsvv graph v1 v2 then
+    sg_rmvv graph v1 v2
+  else
+    graph.
+
+definition sg_mkvhi ≝
+  λgraph.
+  λv.
+  λh.
+    set_ivh graph (set_tbl_update … v (set_insert … h) (ig_ivh graph)). 
+
+definition sg_mkvh ≝
+  λgraph.
+  λv.
+  λh.
+  if sg_existsvh graph v h then
+    graph
+  else
+    sg_mkvhi graph v h.
+
+definition sg_rmvh ≝
+  λgraph.
+  λv.
+  λh.
+    set_ivh graph (set_tbl_update … v (set_remove … h) (ig_ivh graph)).
+
+definition sg_rmvhifx ≝
+  λgraph.
+  λv.
+  λh.
+    if sg_existsvh graph v h then
+      sg_rmvh graph v h
+    else
+      graph.
+
+definition sg_coalesce ≝
+  λg.
+  λx.
+  λy.
+  match sg_neighboursv g x with
+  [ None       ⇒ None ?
+  | Some neigh ⇒
+    let graph ≝ set_fold ? graph (λw. λg.
+      sg_mkvv (sg_rmvv g x w) y w) neigh g
+    in
+    match sg_neighboursh g x with
+    [ None ⇒ None ?
+    | Some neigh ⇒
+      let graph ≝ set_fold ? ? (λh. λg.
+        sg_mkvh (sg_rmvh g x h) y h) neigh g
+      in
+        Some … graph
+    ]
+  ].
+
+definition sg_coalesceh ≝
+  λg.
+  λx.
+  λh.
+  match sg_neighboursv g x with
+  [ None       ⇒ None ?
+  | Some neigh ⇒
+    let graph ≝ set_fold ? graph (λw. λg.
+      sg_mkvh (sg_rmvv g x w) w h) neigh g
+    in
+    match sg_neighboursh g x with
+    [ None ⇒ None ?
+    | Some neigh ⇒
+      let graph ≝ set_fold ? ? (λk. λg.
+        sg_rmvh graph x k) neigh g
+      in
+        Some … graph
+    ]
+  ].
+
+definition sg_remove ≝
+  λg.
+  λx.
+  match sg_neighboursv g x with
+  [ None ⇒ None ?
+  | Some neigh ⇒
+    let graph ≝
+      set_fold … (λw. λgraph.
+        sg_rmvv graph x w) neigh g
+    in
+    match sg_neighboursh graph x with
+    [ None ⇒ None ?
+    | Some neigh ⇒
+      let graph ≝ set_fold … (λh. λg.
+        sg_rmvh g x h) neigh graph
+      in
+        Some ? graph
+    ]
+  ].
+
+definition ig_mkvvi ≝
+  λgraph.
+  λv1.
+  λv2.
+  let graph ≝ sg_mkvvi graph v1 v2 in
+  let graph ≝ sg_rmvvifx graph v1 v2 in
+  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (ig_degree graph)) in
+  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (ig_nmr graph)) in
+    set_degree (set_nmr graph nmr') degree'.
+
+definition ig_rmvv ≝
+  λgraph.
+  λv1.
+  λv2.
+  let graph ≝ sg_rmvv graph v1 v2 in
+  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (ig_degree graph)) in
+  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (ig_nmr graph)) in
+    set_degree (set_nmr graph nmr') degree'.
+
+definition ig_mkvhi ≝
+  λgraph.
+  λv.
+  λh.
+  let graph ≝ sg_mkvhi graph v h in
+  let graph ≝ sg_rmvhifx graph v h in
+  let degree ≝ pset_increment ? v (repr 1) (ig_degree graph) in
+  let nmr ≝ pset_incrementifx ? v (repr 1) (ig_nmr graph) in
+    set_degree (set_nmr graph nmr) degree.
+
+definition ig_rmvh ≝
+  λgraph.
+  λv.
+  λh.
+  let graph ≝ sg_rmvh graph v h in
+  let degree ≝ pset_increment ? v (neg (repr 1)) (ig_degree graph) in
+  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (ig_nmr graph) in
+    set_degree (set_nmr graph nmr) degree.
+
+definition pref_nmr ≝
+  λgraph.
+  λv.
+  match sg_neighboursv graph v with
+  [ None       ⇒ false (* XXX: ok? *)
+  | Some neigh ⇒
+    match sg_neighboursh graph v with
+    [ None        ⇒ false
+    | Some neigh' ⇒
+      andb (set_is_empty ? neigh) (set_is_empty ? neigh')
+    ]
+  ].
+
+definition pref_mkcheck ≝
+  λgraph.
+  λv.
+    if pref_nmr graph v then
+      let nmr' ≝ pset_remove ? v (ig_nmr graph) in
+        set_nmr graph nmr'
+    else
+      graph.
+
+definition pref_mkvvi ≝
+  λgraph.
+  λv1.
+  λv2.
+    if sg_existsvv graph v1 v2 then
+      graph
+    else
+      let graph ≝ pref_mkcheck graph v1 in
+      let graph ≝ pref_mkcheck graph v2 in
+        sg_mkvvi graph v1 v2.
+
+definition pref_mkvhi ≝
+  λgraph.
+  λv.
+  λh.
+  if sg_existsvh graph v h then
+    graph
+  else
+    let graph ≝ pref_mkcheck graph v in
+      sg_mkvhi graph v h.
+
+(* XXX: look at this carefully *)
+definition pref_rmcheck ≝
+  λgraph.
+  λv.
+  if pref_nmr graph v then
+    match pset_lookup ? v (ig_degree graph) with
+    [ None ⇒ graph (* XXX: ok? *)
+    | Some pref ⇒
+      let nmr ≝ pset_insert ? v pref (ig_nmr graph) in
+        set_nmr graph nmr
+    ]
+  else
+    graph.
+
+definition pref_rmvv ≝
+  λgraph.
+  λv1.
+  λv2.
+  let graph ≝ sg_rmvv graph v1 v2 in
+  let graph ≝ pref_rmcheck graph v1 in
+  let graph ≝ pref_rmcheck graph v2 in
+    graph.
+
+definition pref_rmvh ≝
+  λgraph.
+  λv.
+  λh.
+  let graph ≝ sg_rmvh graph v h in
+  let graph ≝ pref_rmcheck graph v in
+    graph.
+
+
 
 definition ig_create ≝
@@ -34 +367 @@
         〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
   in
-      mk_graph table'' (set_empty …) (set_empty …) (set_empty …)
+      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …)
       (set_empty …) priority'' priority''.
 
-definition neighboursv ≝
-  λgraph: graph.
-  λv: vertex.
-    set_tbl_find … v (ig_ivv graph).
-
-  method neighborsv graph v =
-    VertexSetMap.find v (self#getvv graph)
+
 
 definition ig_mkipp ≝