--- a/src/Tools/Graphview/layout.scala Tue Jan 06 11:58:57 2015 +0100
+++ b/src/Tools/Graphview/layout.scala Tue Jan 06 16:33:30 2015 +0100
@@ -19,136 +19,140 @@
object Layout
{
+ /* graph structure */
+
+ object Vertex
+ {
+ object Ordering extends scala.math.Ordering[Vertex]
+ {
+ def compare(v1: Vertex, v2: Vertex): Int =
+ (v1, v2) match {
+ case (_: Node, _: Dummy) => -1
+ case (_: Dummy, _: Node) => 1
+ case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
+ case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
+ Graph_Display.Node.Ordering.compare(a1, b1) match {
+ case 0 =>
+ Graph_Display.Node.Ordering.compare(a2, b2) match {
+ case 0 => i compare j
+ case ord => ord
+ }
+ case ord => ord
+ }
+ }
+ }
+ }
+
+ sealed abstract class Vertex
+ case class Node(node: Graph_Display.Node) extends Vertex
+ case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
+
object Point { val zero: Point = Point(0.0, 0.0) }
case class Point(x: Double, y: Double)
- private type Key = Graph_Display.Node
- private type Coordinates = Map[Key, Point]
- private type Level = List[Key]
- private type Levels = List[Level]
+ type Graph = isabelle.Graph[Vertex, Point]
+
+ def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph =
+ isabelle.Graph.make(entries)(Vertex.Ordering)
- val empty: Layout =
- new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty)
+ val empty_graph: Graph = make_graph(Nil)
+
+
+ /* layout */
+
+ val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
val pendulum_iterations = 10
val minimize_crossings_iterations = 40
- def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout =
+
+ private type Levels = Map[Vertex, Int]
+ private val empty_levels: Levels = Map.empty
+
+ def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout =
{
- if (visible_graph.is_empty) empty
+ if (input_graph.is_empty) empty
else {
- val initial_levels = level_map(visible_graph)
+ /* initial graph */
+
+ val initial_graph =
+ make_graph(
+ input_graph.iterator.map(
+ { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList)
- val (dummy_graph, dummies, dummy_levels) =
- ((visible_graph, Map.empty[(Key, Key), List[Key]], initial_levels) /:
- visible_graph.edges_iterator) {
- case ((graph, dummies, levels), (from, to)) =>
- if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
+ val initial_levels: Levels =
+ (empty_levels /: initial_graph.topological_order) {
+ case (levels, vertex) =>
+ val level =
+ 1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
+ levels + (vertex -> level)
+ }
+
+
+ /* graph with dummies */
+
+ val (dummy_graph, dummy_levels) =
+ ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
+ case ((graph, levels), (node1, node2)) =>
+ val v1 = Node(node1); val l1 = levels(v1)
+ val v2 = Node(node2); val l2 = levels(v2)
+ if (l2 - l1 <= 1) (graph, levels)
else {
- val (graph1, ds, levels1) = add_dummies(graph, from, to, levels)
- (graph1, dummies + ((from, to) -> ds), levels1)
+ val dummies_levels =
+ (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
+ yield (Dummy(node1, node2, i), l)).toList
+ val dummies = dummies_levels.map(_._1)
+
+ val levels1 = (levels /: dummies_levels)(_ + _)
+ val graph1 =
+ ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /:
+ (v1 :: dummies ::: List(v2)).sliding(2)) {
+ case (g, List(a, b)) => g.add_edge(a, b) }
+ (graph1, levels1)
}
}
+
+ /* minimize edge crossings and initial coordinates */
+
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 w2 = metrics.box_width2(key)
- (coords2 + (key -> Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
+ val levels_graph: Graph =
+ (((dummy_graph, 0.0) /: levels) {
+ case ((graph, y), level) =>
+ ((((graph, 0.0) /: level) {
+ case ((g, x), v) =>
+ val w2 = metrics.box_width2(v)
+ (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
})._1, y + metrics.box_height(level.length))
})._1
- val coords = pendulum(metrics, dummy_graph, levels, initial_coordinates)
+ /* pendulum layout */
- val dummy_coords =
- (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
- case (map, key) => map + (key -> dummies(key).map(coords(_)))
- }
+ val output_graph = pendulum(metrics, levels_graph, levels)
- new Layout(metrics, visible_graph, coords, dummy_coords)
+ new Layout(metrics, input_graph, output_graph)
}
}
- def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int])
- : (Graph_Display.Graph, List[Key], Map[Key, Int]) =
- {
- val ds =
- ((levels(from) + 1) until levels(to)).map(l => {
- // FIXME !?
- val ident = "%s$%s$%d".format(from.ident, to.ident, l)
- Graph_Display.Node(" ", ident)
- }).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(_, Nil))
- 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: Graph_Display.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)
- }
- }
+ /** edge crossings **/
- 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(Graph_Display.Node.Ordering)).toList
- }
+ private type Level = List[Vertex]
- def count_crossings(graph: Graph_Display.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: Graph_Display.Graph, levels: Levels): Levels =
+ def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
{
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)
+ child.map(v => {
+ val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
val weight =
(0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
- (k, weight)
+ (v, weight)
}).sortBy(_._2).map(_._1)
- def resort(levels: Levels, top_down: Boolean) =
+ def resort(levels: List[Level], top_down: Boolean) =
if (top_down)
(List(levels.head) /: levels.tail)((tops, bot) =>
resort_level(tops.head, bot, top_down) :: tops).reverse
@@ -170,26 +174,85 @@
}._1
}
- def pendulum(
- metrics: Metrics, graph: Graph_Display.Graph,
- levels: Levels, coords: Map[Key, Point]): Coordinates =
+ def level_list(levels: Levels): List[Level] =
{
- type Regions = List[List[Region]]
+ val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
+ val buckets = new Array[Level](max_lev + 1)
+ for (l <- 0 to max_lev) { buckets(l) = Nil }
+ for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
+ buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
+ }
- def iteration(
- coords: Coordinates, regions: Regions, top_down: Boolean): (Coordinates, Regions, Boolean) =
- {
- val (coords1, regions1, moved) =
- ((coords, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
- case ((coords, tops, moved), bot) =>
- val bot1 = collapse(coords, bot, top_down)
- val (coords1, moved1) = deflect(coords, bot1, top_down)
- (coords1, bot1 :: tops, moved || moved1)
- }
- (coords1, regions1.reverse, moved)
+ def count_crossings(graph: Graph, levels: List[Level]): Int =
+ {
+ def in_level(ls: List[Level]): 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
}
- def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] =
+ levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
+ }
+
+
+
+ /** pendulum method **/
+
+ /*This is an auxiliary class which is used by the layout algorithm when
+ calculating coordinates with the "pendulum method". A "region" is a
+ group of vertices which "stick together".*/
+ private class Region(init: Vertex)
+ {
+ var content: List[Vertex] = List(init)
+
+ def distance(metrics: Metrics, graph: Graph, that: Region): Double =
+ {
+ val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1)
+ val v2 = that.content.head; val x2 = graph.get_node(v2).x - metrics.box_width2(v2)
+ x2 - x1 - metrics.box_gap
+ }
+
+ def deflection(graph: Graph, top_down: Boolean): Double =
+ ((for (a <- content.iterator) yield {
+ val x = graph.get_node(a).x
+ val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
+ bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
+ }).sum / content.length).round.toDouble
+
+ def move(graph: Graph, dx: Double): Graph =
+ if (dx == 0.0) graph
+ else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) }
+ }
+
+ private type Regions = List[List[Region]]
+
+ def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
+ {
+ def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
+ {
+ val (graph1, regions1, moved) =
+ ((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
+ case ((graph, tops, moved), bot) =>
+ val bot1 = collapse(graph, bot, top_down)
+ val (graph1, moved1) = deflect(graph, bot1, top_down)
+ (graph1, bot1 :: tops, moved || moved1)
+ }
+ (graph1, regions1.reverse, moved)
+ }
+
+ def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] =
{
if (level.size <= 1) level
else {
@@ -199,16 +262,16 @@
regions_changed = false
for (i <- Range(next.length - 1, 0, -1)) {
val (r1, r2) = (next(i - 1), next(i))
- val d1 = r1.deflection(graph, coords, top_down)
- val d2 = r2.deflection(graph, coords, top_down)
+ val d1 = r1.deflection(graph, top_down)
+ val d2 = r2.deflection(graph, top_down)
if (// Do regions touch?
- r1.distance(metrics, coords, r2) <= 0.0 &&
+ r1.distance(metrics, graph, r2) <= 0.0 &&
// Do they influence each other?
(d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
{
regions_changed = true
- r1.nodes = r1.nodes ::: r2.nodes
+ r1.content = r1.content ::: r2.content
next = next.filter(next.indexOf(_) != i)
}
}
@@ -217,101 +280,74 @@
}
}
- def deflect(
- coords: Coordinates, level: List[Region], top_down: Boolean): (Coordinates, Boolean) =
+ def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) =
{
- ((coords, false) /: (0 until level.length)) {
- case ((coords, moved), i) =>
+ ((graph, false) /: (0 until level.length)) {
+ case ((graph, moved), i) =>
val r = level(i)
- val d = r.deflection(graph, coords, top_down)
+ val d = r.deflection(graph, top_down)
val offset =
if (d < 0 && i > 0)
- - (level(i - 1).distance(metrics, coords, r) min (- d))
+ - (level(i - 1).distance(metrics, graph, r) min (- d))
else if (d >= 0 && i < level.length - 1)
- r.distance(metrics, coords, level(i + 1)) min d
+ r.distance(metrics, graph, level(i + 1)) min d
else d
- (r.move(coords, offset), moved || d != 0)
+ (r.move(graph, offset), moved || d != 0)
}
}
- val regions = levels.map(level => level.map(new Region(_)))
-
- ((coords, regions, true, true) /: (1 to pendulum_iterations)) {
- case ((coords, regions, top_down, moved), _) =>
- if (moved) {
- val (coords1, regions1, m) = iteration(coords, regions, top_down)
- (coords1, regions1, !top_down, m)
- }
- else (coords, regions, !top_down, moved)
- }._1
- }
-
- /*This is an auxiliary class which is used by the layout algorithm when
- calculating coordinates with the "pendulum method". A "region" is a
- group of nodes which "stick together".*/
- private class Region(node: Key)
- {
- var nodes: List[Key] = List(node)
+ val initial_regions = levels.map(level => level.map(new Region(_)))
- def distance(metrics: Metrics, coords: Coordinates, that: Region): Double =
- {
- val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1)
- val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2)
- x2 - x1 - metrics.box_gap
- }
-
- def deflection(graph: Graph_Display.Graph, coords: Coordinates, top_down: Boolean): Double =
- ((for (a <- nodes.iterator) yield {
- val x = coords(a).x
- val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
- bs.iterator.map(coords(_).x - x).sum / (bs.size max 1)
- }).sum / nodes.length).round.toDouble
-
- def move(coords: Coordinates, dx: Double): Coordinates =
- if (dx == 0.0) coords
- else
- (coords /: nodes) {
- case (cs, node) =>
- val p = cs(node)
- cs + (node -> Point(p.x + dx, p.y))
+ ((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) {
+ case ((graph, regions, top_down, moved), _) =>
+ if (moved) {
+ val (graph1, regions1, moved1) = iteration(graph, regions, top_down)
+ (graph1, regions1, !top_down, moved1)
}
+ else (graph, regions, !top_down, moved)
+ }._1
}
}
final class Layout private(
val metrics: Metrics,
- val visible_graph: Graph_Display.Graph,
- nodes: Map[Graph_Display.Node, Layout.Point],
- dummies: Map[Graph_Display.Edge, List[Layout.Point]])
+ val input_graph: Graph_Display.Graph,
+ val output_graph: Layout.Graph)
{
- /* nodes */
+ /* vertex coordinates */
+
+ def get_vertex(v: Layout.Vertex): Layout.Point =
+ if (output_graph.defined(v)) output_graph.get_node(v)
+ else Layout.Point.zero
- def get_node(node: Graph_Display.Node): Layout.Point =
- nodes.getOrElse(node, Layout.Point.zero)
-
- def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
- nodes.get(node) match {
- case None => this
- case Some(p) =>
- val nodes1 = nodes + (node -> f(p))
- new Layout(metrics, visible_graph, nodes1, dummies)
+ def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
+ {
+ if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
+ else {
+ val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dy, p.y + dy))
+ new Layout(metrics, input_graph, output_graph1)
}
+ }
/* dummies */
- def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
- dummies.getOrElse(edge, Nil)
-
- def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
- dummies.get(edge) match {
- case None => this
- case Some(ds) =>
- val dummies1 = dummies + (edge -> f(ds))
- new Layout(metrics, visible_graph, nodes, dummies1)
- }
+ def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
+ output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
def dummies_iterator: Iterator[Layout.Point] =
- for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
+ for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
+
+ def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
+ new Iterator[Layout.Point] {
+ private var index = 0
+ def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
+ def next: Layout.Point =
+ {
+ val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
+ index += 1
+ p
+ }
+ }
}