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                  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
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