--- 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"
--- /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))
+ }
+ }
+}
--- 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))
- }
- }
-}
--- 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 _)
}
}