# HG changeset patch # User wenzelm # Date 1349731747 -7200 # Node ID dd6fc7c9504a7269186e521c374008ffc5282ea8 # Parent dfa100466d2e801fd1bf3094e17abde37cb0f4eb 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; diff -r dfa100466d2e -r dd6fc7c9504a src/Tools/Graphview/src/layout_pendulum.scala --- 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 diff -r dfa100466d2e -r dd6fc7c9504a src/Tools/Graphview/src/model.scala --- 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 = diff -r dfa100466d2e -r dd6fc7c9504a src/Tools/Graphview/src/mutator.scala --- 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)) } ) diff -r dfa100466d2e -r dd6fc7c9504a src/Tools/Graphview/src/popups.scala --- 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) {