1 /* Title: Tools/Graphview/layout_pendulum.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Pendulum DAG layout algorithm. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 |
|
13 object Layout_Pendulum |
|
14 { |
|
15 type Key = String |
|
16 type Point = (Double, Double) |
|
17 type Coordinates = Map[Key, Point] |
|
18 type Level = List[Key] |
|
19 type Levels = List[Level] |
|
20 type Dummies = (Model.Graph, List[Key], Map[Key, Int]) |
|
21 |
|
22 case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]]) |
|
23 val empty_layout = Layout(Map.empty, Map.empty) |
|
24 |
|
25 val pendulum_iterations = 10 |
|
26 val minimize_crossings_iterations = 40 |
|
27 |
|
28 def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = |
|
29 { |
|
30 if (graph.is_empty) empty_layout |
|
31 else { |
|
32 val initial_levels = level_map(graph) |
|
33 |
|
34 val (dummy_graph, dummies, dummy_levels) = |
|
35 ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { |
|
36 case ((graph, dummies, levels), from) => |
|
37 ((graph, dummies, levels) /: graph.imm_succs(from)) { |
|
38 case ((graph, dummies, levels), to) => |
|
39 if (levels(to) - levels(from) <= 1) (graph, dummies, levels) |
|
40 else { |
|
41 val (next, ds, ls) = add_dummies(graph, from, to, levels) |
|
42 (next, dummies + ((from, to) -> ds), ls) |
|
43 } |
|
44 } |
|
45 } |
|
46 |
|
47 val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) |
|
48 |
|
49 val initial_coordinates: Coordinates = |
|
50 (((Map.empty[Key, Point], 0.0) /: levels) { |
|
51 case ((coords1, y), level) => |
|
52 ((((coords1, 0.0) /: level) { |
|
53 case ((coords2, x), key) => |
|
54 val s = if (graph.defined(key)) graph.get_node(key).name else "X" |
|
55 (coords2 + (key -> (x, y)), x + box_distance) |
|
56 })._1, y + box_height(level.length)) |
|
57 })._1 |
|
58 |
|
59 val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) |
|
60 |
|
61 val dummy_coords = |
|
62 (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { |
|
63 case (map, key) => map + (key -> dummies(key).map(coords(_))) |
|
64 } |
|
65 |
|
66 Layout(coords, dummy_coords) |
|
67 } |
|
68 } |
|
69 |
|
70 |
|
71 def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = |
|
72 { |
|
73 val ds = |
|
74 ((levels(from) + 1) until levels(to)) |
|
75 .map("%s$%s$%d" format (from, to, _)).toList |
|
76 |
|
77 val ls = |
|
78 (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { |
|
79 case (ls, (l, d)) => ls + (d -> l) |
|
80 } |
|
81 |
|
82 val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) |
|
83 val graph2 = |
|
84 (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { |
|
85 case (g, List(x, y)) => g.add_edge(x, y) |
|
86 } |
|
87 (graph2, ds, ls) |
|
88 } |
|
89 |
|
90 def level_map(graph: Model.Graph): Map[Key, Int] = |
|
91 (Map.empty[Key, Int] /: graph.topological_order) { |
|
92 (levels, key) => { |
|
93 val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) } |
|
94 levels + (key -> lev) |
|
95 } |
|
96 } |
|
97 |
|
98 def level_list(map: Map[Key, Int]): Levels = |
|
99 { |
|
100 val max_lev = (-1 /: map) { case (m, (_, l)) => m max l } |
|
101 val buckets = new Array[Level](max_lev + 1) |
|
102 for (l <- 0 to max_lev) { buckets(l) = Nil } |
|
103 for ((key, l) <- map) { buckets(l) = key :: buckets(l) } |
|
104 buckets.iterator.map(_.sorted).toList |
|
105 } |
|
106 |
|
107 def count_crossings(graph: Model.Graph, levels: Levels): Int = |
|
108 { |
|
109 def in_level(ls: Levels): Int = ls match { |
|
110 case List(top, bot) => |
|
111 top.iterator.zipWithIndex.map { |
|
112 case (outer_parent, outer_parent_index) => |
|
113 graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) |
|
114 .map(outer_child => |
|
115 (0 until outer_parent_index) |
|
116 .map(inner_parent => |
|
117 graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) |
|
118 .filter(inner_child => outer_child < inner_child) |
|
119 .size |
|
120 ).sum |
|
121 ).sum |
|
122 }.sum |
|
123 |
|
124 case _ => 0 |
|
125 } |
|
126 |
|
127 levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum |
|
128 } |
|
129 |
|
130 def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = |
|
131 { |
|
132 def resort_level(parent: Level, child: Level, top_down: Boolean): Level = |
|
133 child.map(k => { |
|
134 val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) |
|
135 val weight = |
|
136 (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) |
|
137 (k, weight) |
|
138 }).sortBy(_._2).map(_._1) |
|
139 |
|
140 def resort(levels: Levels, top_down: Boolean) = top_down match { |
|
141 case true => |
|
142 (List[Level](levels.head) /: levels.tail) { |
|
143 (tops, bot) => resort_level(tops.head, bot, top_down) :: tops |
|
144 }.reverse |
|
145 |
|
146 case false => |
|
147 (List[Level](levels.reverse.head) /: levels.reverse.tail) { |
|
148 (bots, top) => resort_level(bots.head, top, top_down) :: bots |
|
149 } |
|
150 } |
|
151 |
|
152 ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { |
|
153 case ((old_levels, old_crossings, top_down), _) => { |
|
154 val new_levels = resort(old_levels, top_down) |
|
155 val new_crossings = count_crossings(graph, new_levels) |
|
156 if (new_crossings < old_crossings) |
|
157 (new_levels, new_crossings, !top_down) |
|
158 else |
|
159 (old_levels, old_crossings, !top_down) |
|
160 } |
|
161 }._1 |
|
162 } |
|
163 |
|
164 def pendulum(graph: Model.Graph, box_distance: Double, |
|
165 levels: Levels, coords: Map[Key, Point]): Coordinates = |
|
166 { |
|
167 type Regions = List[List[Region]] |
|
168 |
|
169 def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) |
|
170 : (Regions, Coordinates, Boolean) = |
|
171 { |
|
172 val (nextr, nextc, moved) = |
|
173 ((List.empty[List[Region]], coords, false) /: |
|
174 (if (top_down) regions else regions.reverse)) { |
|
175 case ((tops, coords, prev_moved), bot) => { |
|
176 val nextb = collapse(coords, bot, top_down) |
|
177 val (nextc, this_moved) = deflect(coords, nextb, top_down) |
|
178 (nextb :: tops, nextc, prev_moved || this_moved) |
|
179 } |
|
180 } |
|
181 |
|
182 (nextr.reverse, nextc, moved) |
|
183 } |
|
184 |
|
185 def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = |
|
186 { |
|
187 if (level.size <= 1) level |
|
188 else { |
|
189 var next = level |
|
190 var regions_changed = true |
|
191 while (regions_changed) { |
|
192 regions_changed = false |
|
193 for (i <- (next.length to 1)) { |
|
194 val (r1, r2) = (next(i-1), next(i)) |
|
195 val d1 = r1.deflection(coords, top_down) |
|
196 val d2 = r2.deflection(coords, top_down) |
|
197 |
|
198 if (// Do regions touch? |
|
199 r1.distance(coords, r2) <= box_distance && |
|
200 // Do they influence each other? |
|
201 (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) |
|
202 { |
|
203 regions_changed = true |
|
204 r1.nodes = r1.nodes ::: r2.nodes |
|
205 next = next.filter(next.indexOf(_) != i) |
|
206 } |
|
207 } |
|
208 } |
|
209 next |
|
210 } |
|
211 } |
|
212 |
|
213 def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) |
|
214 : (Coordinates, Boolean) = |
|
215 { |
|
216 ((coords, false) /: (0 until level.length)) { |
|
217 case ((coords, moved), i) => { |
|
218 val r = level(i) |
|
219 val d = r.deflection(coords, top_down) |
|
220 val offset = { |
|
221 if (i == 0 && d <= 0) d |
|
222 else if (i == level.length - 1 && d >= 0) d |
|
223 else if (d < 0) { |
|
224 val prev = level(i-1) |
|
225 (-(r.distance(coords, prev) - box_distance)) max d |
|
226 } |
|
227 else { |
|
228 val next = level(i+1) |
|
229 (r.distance(coords, next) - box_distance) min d |
|
230 } |
|
231 } |
|
232 |
|
233 (r.move(coords, offset), moved || (d != 0)) |
|
234 } |
|
235 } |
|
236 } |
|
237 |
|
238 val regions = levels.map(level => level.map(new Region(graph, _))) |
|
239 |
|
240 ((regions, coords, true, true) /: (1 to pendulum_iterations)) { |
|
241 case ((regions, coords, top_down, moved), _) => |
|
242 if (moved) { |
|
243 val (nextr, nextc, m) = iteration(regions, coords, top_down) |
|
244 (nextr, nextc, !top_down, m) |
|
245 } |
|
246 else (regions, coords, !top_down, moved) |
|
247 }._2 |
|
248 } |
|
249 |
|
250 private class Region(val graph: Model.Graph, node: Key) |
|
251 { |
|
252 var nodes: List[Key] = List(node) |
|
253 |
|
254 def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min |
|
255 def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max |
|
256 |
|
257 def distance(coords: Coordinates, to: Region): Double = |
|
258 math.abs(left(coords) - to.left(coords)) min |
|
259 math.abs(right(coords) - to.right(coords)) |
|
260 |
|
261 def deflection(coords: Coordinates, use_preds: Boolean) = |
|
262 nodes.map(k => (coords(k)._1, |
|
263 if (use_preds) graph.imm_preds(k).toList // FIXME iterator |
|
264 else graph.imm_succs(k).toList)) |
|
265 .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) }) |
|
266 .sum / nodes.length |
|
267 |
|
268 def move(coords: Coordinates, by: Double): Coordinates = |
|
269 (coords /: nodes) { |
|
270 case (cs, node) => |
|
271 val (x, y) = cs(node) |
|
272 cs + (node -> (x + by, y)) |
|
273 } |
|
274 } |
|
275 } |
|