src/Tools/Graphview/layout.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 67601 b34be3010273
permissions -rw-r--r--
tuned imports;
     1 /*  Title:      Tools/Graphview/layout.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 DAG 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 
    14 package isabelle.graphview
    15 
    16 
    17 import isabelle._
    18 
    19 
    20 object 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                   filter(inner_child => outer_child < inner_child).size).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) /: (0 until level.length)) {
   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 
   363 final 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