1/* Title: Tools/Graphview/layout.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5DAG layout according to: 6 7 Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing, 8 DIMACS International Workshop (GD'94), Springer LNCS 894, 1995. 9 10 https://doi.org/10.1007/3-540-58950-3_371 11 ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz 12*/ 13 14package isabelle.graphview 15 16 17import isabelle._ 18 19 20object Layout 21{ 22 /* graph structure */ 23 24 object Vertex 25 { 26 object Ordering extends scala.math.Ordering[Vertex] 27 { 28 def compare(v1: Vertex, v2: Vertex): Int = 29 (v1, v2) match { 30 case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) 31 case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => 32 Graph_Display.Node.Ordering.compare(a1, b1) match { 33 case 0 => 34 Graph_Display.Node.Ordering.compare(a2, b2) match { 35 case 0 => i compare j 36 case ord => ord 37 } 38 case ord => ord 39 } 40 case (Node(a), Dummy(b, _, _)) => 41 Graph_Display.Node.Ordering.compare(a, b) match { 42 case 0 => -1 43 case ord => ord 44 } 45 case (Dummy(a, _, _), Node(b)) => 46 Graph_Display.Node.Ordering.compare(a, b) match { 47 case 0 => 1 48 case ord => ord 49 } 50 } 51 } 52 } 53 54 sealed abstract class Vertex 55 case class Node(node: Graph_Display.Node) extends Vertex 56 case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex 57 58 sealed case class Info( 59 x: Double, y: Double, width2: Double, height2: Double, lines: List[String]) 60 { 61 def left: Double = x - width2 62 def right: Double = x + width2 63 def width: Double = 2 * width2 64 def height: Double = 2 * height2 65 } 66 67 type Graph = isabelle.Graph[Vertex, Info] 68 69 def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph = 70 isabelle.Graph.make(entries)(Vertex.Ordering) 71 72 val empty_graph: Graph = make_graph(Nil) 73 74 75 /* vertex x coordinate */ 76 77 private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left 78 private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right 79 80 private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph = 81 if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx)) 82 83 84 /* layout */ 85 86 val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) 87 88 89 private type Levels = Map[Vertex, Int] 90 private val empty_levels: Levels = Map.empty 91 92 def make(options: Options, metrics: Metrics, 93 node_text: (Graph_Display.Node, XML.Body) => String, 94 input_graph: Graph_Display.Graph): Layout = 95 { 96 if (input_graph.is_empty) empty 97 else { 98 /* initial graph */ 99 100 val initial_graph = 101 make_graph( 102 input_graph.iterator.map( 103 { case (a, (content, (_, bs))) => 104 val lines = split_lines(node_text(a, content)) 105 val w2 = metrics.node_width2(lines) 106 val h2 = metrics.node_height2(lines.length) 107 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_))) 108 }).toList) 109 110 val initial_levels: Levels = 111 (empty_levels /: initial_graph.topological_order) { 112 case (levels, vertex) => 113 val level = 114 1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) } 115 levels + (vertex -> level) 116 } 117 118 119 /* graph with dummies */ 120 121 val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil) 122 123 val (dummy_graph, dummy_levels) = 124 ((initial_graph, initial_levels) /: input_graph.edges_iterator) { 125 case ((graph, levels), (node1, node2)) => 126 val v1 = Node(node1); val l1 = levels(v1) 127 val v2 = Node(node2); val l2 = levels(v2) 128 if (l2 - l1 <= 1) (graph, levels) 129 else { 130 val dummies_levels = 131 (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } 132 yield (Dummy(node1, node2, i), l)).toList 133 val dummies = dummies_levels.map(_._1) 134 135 val levels1 = (levels /: dummies_levels)(_ + _) 136 val graph1 = 137 ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /: 138 (v1 :: dummies ::: List(v2)).sliding(2)) { 139 case (g, List(a, b)) => g.add_edge(a, b) } 140 (graph1, levels1) 141 } 142 } 143 144 145 /* minimize edge crossings and initial coordinates */ 146 147 val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels)) 148 149 val levels_graph: Graph = 150 (((dummy_graph, 0.0) /: levels) { 151 case ((graph, y), level) => 152 val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length } 153 val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size } 154 155 val y1 = y + metrics.node_height2(num_lines) 156 157 val graph1 = 158 (((graph, 0.0) /: level) { case ((g, x), v) => 159 val info = g.get_node(v) 160 val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1)) 161 val x1 = x + info.width + metrics.gap 162 (g1, x1) 163 })._1 164 165 val y2 = y1 + metrics.level_height2(num_lines, num_edges) 166 167 (graph1, y2) 168 })._1 169 170 171 /* pendulum/rubberband layout */ 172 173 val output_graph = 174 rubberband(options, metrics, levels, 175 pendulum(options, metrics, levels, levels_graph)) 176 177 new Layout(metrics, input_graph, output_graph) 178 } 179 } 180 181 182 183 /** edge crossings **/ 184 185 private type Level = List[Vertex] 186 187 private def minimize_crossings( 188 options: Options, graph: Graph, levels: List[Level]): List[Level] = 189 { 190 def resort(parent: Level, child: Level, top_down: Boolean): Level = 191 child.map(v => { 192 val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) 193 val weight = 194 (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) 195 (v, weight) 196 }).sortBy(_._2).map(_._1) 197 198 ((levels, count_crossings(graph, levels)) /: 199 (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) { 200 case ((old_levels, old_crossings), iteration) => 201 val top_down = (iteration % 2 == 1) 202 val new_levels = 203 if (top_down) 204 (List(old_levels.head) /: old_levels.tail)((tops, bot) => 205 resort(tops.head, bot, top_down) :: tops).reverse 206 else { 207 val rev_old_levels = old_levels.reverse 208 (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) => 209 resort(bots.head, top, top_down) :: bots) 210 } 211 val new_crossings = count_crossings(graph, new_levels) 212 if (new_crossings < old_crossings) 213 (new_levels, new_crossings) 214 else 215 (old_levels, old_crossings) 216 }._1 217 } 218 219 private def level_list(levels: Levels): List[Level] = 220 { 221 val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l } 222 val buckets = new Array[Level](max_lev + 1) 223 for (l <- 0 to max_lev) { buckets(l) = Nil } 224 for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } 225 buckets.iterator.map(_.sorted(Vertex.Ordering)).toList 226 } 227 228 private def count_crossings(graph: Graph, levels: List[Level]): Int = 229 levels.iterator.sliding(2).map { 230 case List(top, bot) => 231 top.iterator.zipWithIndex.map { 232 case (outer_parent, outer_parent_index) => 233 graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child => 234 (0 until outer_parent_index).iterator.map(inner_parent => 235 graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) 236 .count(inner_child => outer_child < inner_child)).sum).sum 237 }.sum 238 case _ => 0 239 }.sum 240 241 242 243 /** pendulum method **/ 244 245 /*This is an auxiliary class which is used by the layout algorithm when 246 calculating coordinates with the "pendulum method". A "region" is a 247 group of vertices which "stick together".*/ 248 private class Region(val content: List[Vertex]) 249 { 250 def distance(metrics: Metrics, graph: Graph, that: Region): Double = 251 vertex_left(graph, that.content.head) - 252 vertex_right(graph, this.content.last) - 253 metrics.gap 254 255 def deflection(graph: Graph, top_down: Boolean): Double = 256 ((for (a <- content.iterator) yield { 257 val x = graph.get_node(a).x 258 val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) 259 bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1) 260 }).sum / content.length).round.toDouble 261 262 def move(graph: Graph, dx: Double): Graph = 263 if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx)) 264 265 def combine(that: Region): Region = new Region(content ::: that.content) 266 } 267 268 private def pendulum( 269 options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph = 270 { 271 def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] = 272 level match { 273 case r1 :: rest => 274 val rest1 = combine_regions(graph, top_down, rest) 275 rest1 match { 276 case r2 :: rest2 => 277 val d1 = r1.deflection(graph, top_down) 278 val d2 = r2.deflection(graph, top_down) 279 if (// Do regions touch? 280 r1.distance(metrics, graph, r2) <= 0.0 && 281 // Do they influence each other? 282 (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0)) 283 r1.combine(r2) :: rest2 284 else r1 :: rest1 285 case _ => r1 :: rest1 286 } 287 case _ => level 288 } 289 290 def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) = 291 { 292 ((graph, false) /: level.indices) { 293 case ((graph, moved), i) => 294 val r = level(i) 295 val d = r.deflection(graph, top_down) 296 val dx = 297 if (d < 0.0 && i > 0) 298 - (level(i - 1).distance(metrics, graph, r) min (- d)) 299 else if (d >= 0.0 && i < level.length - 1) 300 r.distance(metrics, graph, level(i + 1)) min d 301 else d 302 (r.move(graph, dx), moved || d != 0.0) 303 } 304 } 305 306 val initial_regions = levels.map(level => level.map(l => new Region(List(l)))) 307 308 ((levels_graph, initial_regions, true) /: 309 (1 to (2 * options.int("graphview_iterations_pendulum")))) { 310 case ((graph, regions, moved), iteration) => 311 val top_down = (iteration % 2 == 1) 312 if (moved) { 313 val (graph1, regions1, moved1) = 314 ((graph, List.empty[List[Region]], false) /: 315 (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) => 316 val bot1 = combine_regions(graph, top_down, bot) 317 val (graph1, moved1) = deflect(bot1, top_down, graph) 318 (graph1, bot1 :: tops, moved || moved1) 319 } 320 (graph1, regions1.reverse, moved1) 321 } 322 else (graph, regions, moved) 323 }._1 324 } 325 326 327 328 /** rubberband method **/ 329 330 private def force_weight(graph: Graph, v: Vertex): Double = 331 { 332 val preds = graph.imm_preds(v) 333 val succs = graph.imm_succs(v) 334 val n = preds.size + succs.size 335 if (n == 0) 0.0 336 else { 337 val x = graph.get_node(v).x 338 ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n 339 } 340 } 341 342 private def rubberband( 343 options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph = 344 { 345 val gap = metrics.gap 346 347 (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) => 348 (graph /: levels) { case (graph, level) => 349 val m = level.length - 1 350 (graph /: level.iterator.zipWithIndex) { 351 case (g, (v, i)) => 352 val d = force_weight(g, v) 353 if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) || 354 d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d)) 355 move_vertex(g, v, d.round.toDouble) 356 else g 357 } 358 } 359 } 360 } 361} 362 363final class Layout private( 364 val metrics: Metrics, 365 val input_graph: Graph_Display.Graph, 366 val output_graph: Layout.Graph) 367{ 368 /* vertex coordinates */ 369 370 def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout = 371 { 372 if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this 373 else { 374 val output_graph1 = 375 output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy)) 376 new Layout(metrics, input_graph, output_graph1) 377 } 378 } 379 380 381 /* regular nodes */ 382 383 def get_node(node: Graph_Display.Node): Layout.Info = 384 output_graph.get_node(Layout.Node(node)) 385 386 def nodes_iterator: Iterator[Layout.Info] = 387 for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info 388 389 390 /* dummies */ 391 392 def dummies_iterator: Iterator[Layout.Info] = 393 for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info 394 395 def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] = 396 new Iterator[Layout.Info] { 397 private var index = 0 398 def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index)) 399 def next: Layout.Info = 400 { 401 val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index)) 402 index += 1 403 info 404 } 405 } 406} 407 408