# HG changeset patch # User wenzelm # Date 1420142478 -3600 # Node ID 07a7dfd6d694cab8cb32d163f6d5d7fd42484994 # Parent 6dea47cf6c6b895be06d34ec434bf3f8afe4226e tuned signature; diff -r 6dea47cf6c6b -r 07a7dfd6d694 src/Pure/build-jars --- a/src/Pure/build-jars Thu Jan 01 20:50:20 2015 +0100 +++ b/src/Pure/build-jars Thu Jan 01 21:01:18 2015 +0100 @@ -103,7 +103,7 @@ term.scala term_xml.scala "../Tools/Graphview/graph_panel.scala" - "../Tools/Graphview/layout_pendulum.scala" + "../Tools/Graphview/layout.scala" "../Tools/Graphview/main_panel.scala" "../Tools/Graphview/model.scala" "../Tools/Graphview/mutator_dialog.scala" diff -r 6dea47cf6c6b -r 07a7dfd6d694 src/Tools/Graphview/layout.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/layout.scala Thu Jan 01 21:01:18 2015 +0100 @@ -0,0 +1,278 @@ +/* Title: Tools/Graphview/layout.scala + Author: Markus Kaiser, TU Muenchen + +Pendulum DAG layout algorithm. +*/ + +package isabelle.graphview + + +import isabelle._ + + +final case class Layout( + nodes: Layout.Coordinates, + dummies: Map[(Layout.Key, Layout.Key), List[Layout.Point]]) + +object Layout +{ + type Key = String + type Point = (Double, Double) + type Coordinates = Map[Key, Point] + type Level = List[Key] + type Levels = List[Level] + type Dummies = (Model.Graph, List[Key], Map[Key, Int]) + + val empty = Layout(Map.empty, Map.empty) + + val pendulum_iterations = 10 + val minimize_crossings_iterations = 40 + + def make(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = + { + if (graph.is_empty) empty + else { + val initial_levels = level_map(graph) + + val (dummy_graph, dummies, dummy_levels) = + ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { + case ((graph, dummies, levels), from) => + ((graph, dummies, levels) /: graph.imm_succs(from)) { + case ((graph, dummies, levels), to) => + if (levels(to) - levels(from) <= 1) (graph, dummies, levels) + else { + val (next, ds, ls) = add_dummies(graph, from, to, levels) + (next, dummies + ((from, to) -> ds), ls) + } + } + } + + val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) + + val initial_coordinates: Coordinates = + (((Map.empty[Key, Point], 0.0) /: levels) { + case ((coords1, y), level) => + ((((coords1, 0.0) /: level) { + case ((coords2, x), key) => + val s = if (graph.defined(key)) graph.get_node(key).name else "X" + (coords2 + (key -> (x, y)), x + box_distance) + })._1, y + box_height(level.length)) + })._1 + + val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) + + val dummy_coords = + (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { + case (map, key) => map + (key -> dummies(key).map(coords(_))) + } + + Layout(coords, dummy_coords) + } + } + + + def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = + { + val ds = + ((levels(from) + 1) until levels(to)) + .map("%s$%s$%d" format (from, to, _)).toList + + val ls = + (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { + case (ls, (l, d)) => ls + (d -> l) + } + + val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) + val graph2 = + (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { + case (g, List(x, y)) => g.add_edge(x, y) + } + (graph2, ds, ls) + } + + def level_map(graph: Model.Graph): Map[Key, Int] = + (Map.empty[Key, Int] /: graph.topological_order) { + (levels, key) => { + 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 = + { + 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.iterator.zipWithIndex.map { + case (outer_parent, outer_parent_index) => + graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) + .map(outer_child => + (0 until outer_parent_index) + .map(inner_parent => + graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) + .filter(inner_child => outer_child < inner_child) + .size + ).sum + ).sum + }.sum + + case _ => 0 + } + + levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum + } + + def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = + { + def resort_level(parent: Level, child: Level, top_down: Boolean): Level = + child.map(k => { + val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) + val weight = + (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) + (k, weight) + }).sortBy(_._2).map(_._1) + + def resort(levels: Levels, top_down: Boolean) = top_down match { + case true => + (List[Level](levels.head) /: levels.tail) { + (tops, bot) => resort_level(tops.head, bot, top_down) :: tops + }.reverse + + case false => + (List[Level](levels.reverse.head) /: levels.reverse.tail) { + (bots, top) => resort_level(bots.head, top, top_down) :: bots + } + } + + ((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) + (new_levels, new_crossings, !top_down) + else + (old_levels, old_crossings, !top_down) + } + }._1 + } + + def pendulum(graph: Model.Graph, box_distance: Double, + levels: Levels, coords: Map[Key, Point]): Coordinates = + { + type Regions = List[List[Region]] + + def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) + : (Regions, Coordinates, Boolean) = + { + val (nextr, nextc, moved) = + ((List.empty[List[Region]], coords, false) /: + (if (top_down) regions else regions.reverse)) { + case ((tops, coords, prev_moved), bot) => { + val nextb = collapse(coords, bot, top_down) + val (nextc, this_moved) = deflect(coords, nextb, top_down) + (nextb :: tops, nextc, prev_moved || this_moved) + } + } + + (nextr.reverse, nextc, moved) + } + + def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = + { + if (level.size <= 1) level + else { + var next = level + var regions_changed = true + while (regions_changed) { + regions_changed = false + for (i <- (next.length to 1)) { + val (r1, r2) = (next(i-1), next(i)) + val d1 = r1.deflection(coords, top_down) + val d2 = r2.deflection(coords, top_down) + + if (// Do regions touch? + r1.distance(coords, r2) <= box_distance && + // Do they influence each other? + (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) + { + regions_changed = true + r1.nodes = r1.nodes ::: r2.nodes + next = next.filter(next.indexOf(_) != i) + } + } + } + next + } + } + + def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) + : (Coordinates, Boolean) = + { + ((coords, false) /: (0 until level.length)) { + case ((coords, moved), i) => { + val r = level(i) + val d = r.deflection(coords, top_down) + val offset = { + if (i == 0 && d <= 0) d + else if (i == level.length - 1 && d >= 0) d + else if (d < 0) { + val prev = level(i-1) + (-(r.distance(coords, prev) - box_distance)) max d + } + else { + val next = level(i+1) + (r.distance(coords, next) - box_distance) min d + } + } + + (r.move(coords, offset), moved || (d != 0)) + } + } + } + + val regions = levels.map(level => level.map(new Region(graph, _))) + + ((regions, coords, true, true) /: (1 to pendulum_iterations)) { + case ((regions, coords, top_down, moved), _) => + if (moved) { + val (nextr, nextc, m) = iteration(regions, coords, top_down) + (nextr, nextc, !top_down, m) + } + else (regions, coords, !top_down, moved) + }._2 + } + + private class Region(val graph: Model.Graph, node: Key) + { + var nodes: List[Key] = List(node) + + def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min + def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max + + def distance(coords: Coordinates, to: Region): Double = + math.abs(left(coords) - to.left(coords)) min + math.abs(right(coords) - to.right(coords)) + + def deflection(coords: Coordinates, use_preds: Boolean) = + nodes.map(k => (coords(k)._1, + 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 / (as.length max 1) }) + .sum / nodes.length + + def move(coords: Coordinates, by: Double): Coordinates = + (coords /: nodes) { + case (cs, node) => + val (x, y) = cs(node) + cs + (node -> (x + by, y)) + } + } +} diff -r 6dea47cf6c6b -r 07a7dfd6d694 src/Tools/Graphview/layout_pendulum.scala --- a/src/Tools/Graphview/layout_pendulum.scala Thu Jan 01 20:50:20 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,275 +0,0 @@ -/* Title: Tools/Graphview/layout_pendulum.scala - Author: Markus Kaiser, TU Muenchen - -Pendulum DAG layout algorithm. -*/ - -package isabelle.graphview - - -import isabelle._ - - -object Layout_Pendulum -{ - type Key = String - type Point = (Double, Double) - type Coordinates = Map[Key, Point] - type Level = List[Key] - type Levels = List[Level] - type Dummies = (Model.Graph, List[Key], Map[Key, Int]) - - case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]]) - val empty_layout = Layout(Map.empty, Map.empty) - - val pendulum_iterations = 10 - val minimize_crossings_iterations = 40 - - def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = - { - if (graph.is_empty) empty_layout - else { - val initial_levels = level_map(graph) - - val (dummy_graph, dummies, dummy_levels) = - ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { - case ((graph, dummies, levels), from) => - ((graph, dummies, levels) /: graph.imm_succs(from)) { - case ((graph, dummies, levels), to) => - if (levels(to) - levels(from) <= 1) (graph, dummies, levels) - else { - val (next, ds, ls) = add_dummies(graph, from, to, levels) - (next, dummies + ((from, to) -> ds), ls) - } - } - } - - val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) - - val initial_coordinates: Coordinates = - (((Map.empty[Key, Point], 0.0) /: levels) { - case ((coords1, y), level) => - ((((coords1, 0.0) /: level) { - case ((coords2, x), key) => - val s = if (graph.defined(key)) graph.get_node(key).name else "X" - (coords2 + (key -> (x, y)), x + box_distance) - })._1, y + box_height(level.length)) - })._1 - - val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) - - val dummy_coords = - (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { - case (map, key) => map + (key -> dummies(key).map(coords(_))) - } - - Layout(coords, dummy_coords) - } - } - - - def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = - { - val ds = - ((levels(from) + 1) until levels(to)) - .map("%s$%s$%d" format (from, to, _)).toList - - val ls = - (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { - case (ls, (l, d)) => ls + (d -> l) - } - - val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) - val graph2 = - (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { - case (g, List(x, y)) => g.add_edge(x, y) - } - (graph2, ds, ls) - } - - def level_map(graph: Model.Graph): Map[Key, Int] = - (Map.empty[Key, Int] /: graph.topological_order) { - (levels, key) => { - 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 = - { - 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.iterator.zipWithIndex.map { - case (outer_parent, outer_parent_index) => - graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) - .map(outer_child => - (0 until outer_parent_index) - .map(inner_parent => - graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) - .filter(inner_child => outer_child < inner_child) - .size - ).sum - ).sum - }.sum - - case _ => 0 - } - - levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum - } - - def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = - { - def resort_level(parent: Level, child: Level, top_down: Boolean): Level = - child.map(k => { - val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) - val weight = - (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) - (k, weight) - }).sortBy(_._2).map(_._1) - - def resort(levels: Levels, top_down: Boolean) = top_down match { - case true => - (List[Level](levels.head) /: levels.tail) { - (tops, bot) => resort_level(tops.head, bot, top_down) :: tops - }.reverse - - case false => - (List[Level](levels.reverse.head) /: levels.reverse.tail) { - (bots, top) => resort_level(bots.head, top, top_down) :: bots - } - } - - ((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) - (new_levels, new_crossings, !top_down) - else - (old_levels, old_crossings, !top_down) - } - }._1 - } - - def pendulum(graph: Model.Graph, box_distance: Double, - levels: Levels, coords: Map[Key, Point]): Coordinates = - { - type Regions = List[List[Region]] - - def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) - : (Regions, Coordinates, Boolean) = - { - val (nextr, nextc, moved) = - ((List.empty[List[Region]], coords, false) /: - (if (top_down) regions else regions.reverse)) { - case ((tops, coords, prev_moved), bot) => { - val nextb = collapse(coords, bot, top_down) - val (nextc, this_moved) = deflect(coords, nextb, top_down) - (nextb :: tops, nextc, prev_moved || this_moved) - } - } - - (nextr.reverse, nextc, moved) - } - - def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = - { - if (level.size <= 1) level - else { - var next = level - var regions_changed = true - while (regions_changed) { - regions_changed = false - for (i <- (next.length to 1)) { - val (r1, r2) = (next(i-1), next(i)) - val d1 = r1.deflection(coords, top_down) - val d2 = r2.deflection(coords, top_down) - - if (// Do regions touch? - r1.distance(coords, r2) <= box_distance && - // Do they influence each other? - (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) - { - regions_changed = true - r1.nodes = r1.nodes ::: r2.nodes - next = next.filter(next.indexOf(_) != i) - } - } - } - next - } - } - - def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) - : (Coordinates, Boolean) = - { - ((coords, false) /: (0 until level.length)) { - case ((coords, moved), i) => { - val r = level(i) - val d = r.deflection(coords, top_down) - val offset = { - if (i == 0 && d <= 0) d - else if (i == level.length - 1 && d >= 0) d - else if (d < 0) { - val prev = level(i-1) - (-(r.distance(coords, prev) - box_distance)) max d - } - else { - val next = level(i+1) - (r.distance(coords, next) - box_distance) min d - } - } - - (r.move(coords, offset), moved || (d != 0)) - } - } - } - - val regions = levels.map(level => level.map(new Region(graph, _))) - - ((regions, coords, true, true) /: (1 to pendulum_iterations)) { - case ((regions, coords, top_down, moved), _) => - if (moved) { - val (nextr, nextc, m) = iteration(regions, coords, top_down) - (nextr, nextc, !top_down, m) - } - else (regions, coords, !top_down, moved) - }._2 - } - - private class Region(val graph: Model.Graph, node: Key) - { - var nodes: List[Key] = List(node) - - def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min - def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max - - def distance(coords: Coordinates, to: Region): Double = - math.abs(left(coords) - to.left(coords)) min - math.abs(right(coords) - to.right(coords)) - - def deflection(coords: Coordinates, use_preds: Boolean) = - nodes.map(k => (coords(k)._1, - 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 / (as.length max 1) }) - .sum / nodes.length - - def move(coords: Coordinates, by: Double): Coordinates = - (coords /: nodes) { - case (cs, node) => - val (x, y) = cs(node) - cs + (node -> (x + by, y)) - } - } -} diff -r 6dea47cf6c6b -r 07a7dfd6d694 src/Tools/Graphview/visualizer.scala --- a/src/Tools/Graphview/visualizer.scala Thu Jan 01 20:50:20 2015 +0100 +++ b/src/Tools/Graphview/visualizer.scala Thu Jan 01 21:01:18 2015 +0100 @@ -91,7 +91,7 @@ object Coordinates { - private var layout = Layout_Pendulum.empty_layout + private var layout = Layout.empty def apply(k: String): (Double, Double) = layout.nodes.get(k) match { @@ -140,7 +140,7 @@ def update_layout() { layout = - if (model.current_graph.is_empty) Layout_Pendulum.empty_layout + if (model.current_graph.is_empty) Layout.empty else { val m = metrics() @@ -150,7 +150,7 @@ val box_distance = max_width + m.pad_x + m.gap_x def box_height(n: Int): Double = (m.line_height + m.pad_y) * (5 max n) - Layout_Pendulum(model.current_graph, box_distance, box_height _) + Layout.make(model.current_graph, box_distance, box_height _) } }