author wenzelm Mon, 08 Oct 2012 23:29:07 +0200 changeset 49737 dd6fc7c9504a parent 49736 dfa100466d2e child 49741 fb88f0e4c710
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient; more elementary level_list: avoid stack overflow; prefer elementary graph operations; tuned;
```--- a/src/Tools/Graphview/src/layout_pendulum.scala	Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Mon Oct 08 23:29:07 2012 +0200
@@ -22,12 +22,15 @@
val x_distance = 350
val y_distance = 350
val pendulum_iterations = 10
+  val minimize_crossings_iterations = 40

-  def apply(graph: Model.Graph): Layout = {
-    if (graph.entries.isEmpty)
+  def apply(graph: Model.Graph): Layout =
+  {
+    if (graph.is_empty)
(Map[Key, Point](), Map[(Key, Key), List[Point]]())
else {
-      val (dummy_graph, dummies, dummy_levels) = {
+      val (dummy_graph, dummies, dummy_levels) =
+      {
val initial_levels = level_map(graph)

def add_dummies(graph: Model.Graph, from: Key, to: Key,
@@ -79,7 +82,7 @@
initial_coordinates(levels)
)

-      val dummy_coords =
+      val dummy_coords =
(Map[(Key, Key), List[Point]]() /: dummies.keys) {
case (map, key) => map + (key -> dummies(key).map(coords(_)))
}
@@ -87,32 +90,30 @@
(coords, dummy_coords)
}
}
-
+
def level_map(graph: Model.Graph): Map[Key, Int] =
-    (Map[Key, Int]() /: graph.topological_order){
+    (Map[Key, Int]() /: graph.topological_order) {
(levels, key) => {
-        val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
-        levels + (key -> (pred_levels.max + 1))
-      }}
+        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
+        levels + (key -> lev)
+      }
+    }

def level_list(map: Map[Key, Int]): Levels =
-    (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
-        case ((key, i), list) => {
-            if (list.isEmpty) (i, List(key)) :: list
-            else {
-              val (j, l) = list.head
-              if (i == j) (i, key :: l) :: list.tail
-              else (i, List(key)) :: list
-            }
-        }
-    }.map(_._2)
-
+  {
+    val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
+    val buckets = new Array[Level](max_lev + 1)
+    for (l <- 0 to max_lev) { buckets(l) = Nil }
+    for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
+    buckets.iterator.map(_.sorted).toList
+  }
+
def count_crossings(graph: Model.Graph, levels: Levels): Int = {
def in_level(ls: Levels): Int = ls match {
case List(top, bot) =>
top.zipWithIndex.map{
case (outer_parent, outer_parent_index) =>
-            graph.imm_succs(outer_parent).map(bot.indexOf(_))
+            graph.imm_succs(outer_parent).map(bot.indexOf(_))  // FIXME iterator
.map(outer_child => {
(0 until outer_parent_index)
.map(inner_parent =>
@@ -153,11 +154,11 @@
}
}

-    ((levels, count_crossings(graph, levels), true) /: (1 to 40)) {
+    ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
case ((old_levels, old_crossings, top_down), _) => {
val new_levels = resort(old_levels, top_down)
val new_crossings = count_crossings(graph, new_levels)
-          if ( new_crossings < old_crossings)
+          if (new_crossings < old_crossings)
(new_levels, new_crossings, !top_down)
else
(old_levels, old_crossings, !top_down)
@@ -250,7 +251,7 @@
val regions = levels.map(level => level.map(new Region(graph, _)))

((regions, coords, true, true) /: (1 to pendulum_iterations)) {
-      case ((regions, coords, top_down, moved), _) =>
+      case ((regions, coords, top_down, moved), i) =>
if (moved) {
val (nextr, nextc, m) = iteration(regions, coords, top_down)
(nextr, nextc, !top_down, m)
@@ -272,7 +273,7 @@

def deflection(coords: Coordinates, use_preds: Boolean) =
nodes.map(k => (coords(k)._1,
-                      if (use_preds) graph.imm_preds(k).toList
+                      if (use_preds) graph.imm_preds(k).toList  // FIXME iterator
else graph.imm_succs(k).toList))
.map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
.sum / nodes.length```
```--- a/src/Tools/Graphview/src/model.scala	Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/model.scala	Mon Oct 08 23:29:07 2012 +0200
@@ -78,7 +78,7 @@
def visible_nodes(): Iterator[String] = current.keys

def visible_edges(): Iterator[(String, String)] =
-    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
+    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator

def complete = graph
def current: Model.Graph =```
```--- a/src/Tools/Graphview/src/mutator.scala	Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/mutator.scala	Mon Oct 08 23:29:07 2012 +0200
@@ -139,7 +139,7 @@
"Hide transitive edges",
"Hides all transitive edges.",
(g, s, d) => {
-      !g.imm_succs(s).filter(_ != d)
+      !g.imm_succs(s).filter(_ != d)  // FIXME iterator
.exists(p => !(g.irreducible_paths(p, d).isEmpty))
}
)```
```--- a/src/Tools/Graphview/src/popups.scala	Mon Oct 08 21:17:20 2012 +0200
+++ b/src/Tools/Graphview/src/popups.scala	Mon Oct 08 23:29:07 2012 +0200
@@ -61,9 +61,9 @@

if (edges) {
-          val outs = ls.map(l => (l, curr.imm_succs(l)))
+          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
.filter(_._2.size > 0).sortBy(_._1)
-          val ins = ls.map(l => (l, curr.imm_preds(l)))
+          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
.filter(_._2.size > 0).sortBy(_._1)

if (outs.nonEmpty || ins.nonEmpty) {```