27 def apply(graph: Model.Graph): Layout = |
28 def apply(graph: Model.Graph): Layout = |
28 { |
29 { |
29 if (graph.is_empty) |
30 if (graph.is_empty) |
30 (Map[Key, Point](), Map[(Key, Key), List[Point]]()) |
31 (Map[Key, Point](), Map[(Key, Key), List[Point]]()) |
31 else { |
32 else { |
|
33 val initial_levels = level_map(graph) |
|
34 |
32 val (dummy_graph, dummies, dummy_levels) = |
35 val (dummy_graph, dummies, dummy_levels) = |
33 { |
|
34 val initial_levels = level_map(graph) |
|
35 |
|
36 def add_dummies(graph: Model.Graph, from: Key, to: Key, |
|
37 levels: Map[Key, Int]): Dummies = { |
|
38 val ds = |
|
39 ((levels(from) + 1) until levels(to)) |
|
40 .map("%s$%s$%d" format (from, to, _)).toList |
|
41 |
|
42 val ls = |
|
43 (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { |
|
44 case (ls, (l, d)) => ls + (d -> l) |
|
45 } |
|
46 |
|
47 val next_nodes = |
|
48 (graph /: ds) { |
|
49 (graph, d) => graph.new_node(d, Model.empty_info) |
|
50 } |
|
51 |
|
52 val next = |
|
53 (next_nodes.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { |
|
54 case (graph, List(f, t)) => graph.add_edge(f, t) |
|
55 } |
|
56 (next, ds, ls) |
|
57 } |
|
58 |
|
59 ((graph, Map[(Key, Key), List[Key]](), initial_levels) /: graph.keys) { |
36 ((graph, Map[(Key, Key), List[Key]](), initial_levels) /: graph.keys) { |
60 case ((graph, dummies, levels), from) => { |
37 case ((graph, dummies, levels), from) => |
61 ((graph, dummies, levels) /: graph.imm_succs(from)) { |
38 ((graph, dummies, levels) /: graph.imm_succs(from)) { |
62 case ((graph, dummies, levels), to) => { |
39 case ((graph, dummies, levels), to) => |
63 if (levels(to) - levels(from) <= 1) (graph, dummies, levels) |
40 if (levels(to) - levels(from) <= 1) (graph, dummies, levels) |
64 else add_dummies(graph, from, to, levels) match { |
41 else |
|
42 add_dummies(graph, from, to, levels) match { |
65 case (next, ds, ls) => (next, dummies + ((from, to) -> ds), ls) |
43 case (next, ds, ls) => (next, dummies + ((from, to) -> ds), ls) |
66 } |
44 } |
67 } |
|
68 } |
45 } |
69 } |
46 } |
70 } |
|
71 } |
|
72 |
47 |
73 val levels = |
48 val levels = |
74 minimize_crossings( |
49 minimize_crossings( |
75 dummy_graph, |
50 dummy_graph, |
76 level_list(dummy_levels) |
51 level_list(dummy_levels) |
87 case (map, key) => map + (key -> dummies(key).map(coords(_))) |
62 case (map, key) => map + (key -> dummies(key).map(coords(_))) |
88 } |
63 } |
89 |
64 |
90 (coords, dummy_coords) |
65 (coords, dummy_coords) |
91 } |
66 } |
|
67 } |
|
68 |
|
69 |
|
70 def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = |
|
71 { |
|
72 val ds = |
|
73 ((levels(from) + 1) until levels(to)) |
|
74 .map("%s$%s$%d" format (from, to, _)).toList |
|
75 |
|
76 val ls = |
|
77 (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { |
|
78 case (ls, (l, d)) => ls + (d -> l) |
|
79 } |
|
80 |
|
81 val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) |
|
82 val graph2 = |
|
83 (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { |
|
84 case (g, List(x, y)) => g.add_edge(x, y) |
|
85 } |
|
86 (graph2, ds, ls) |
92 } |
87 } |
93 |
88 |
94 def level_map(graph: Model.Graph): Map[Key, Int] = |
89 def level_map(graph: Model.Graph): Map[Key, Int] = |
95 (Map[Key, Int]() /: graph.topological_order) { |
90 (Map[Key, Int]() /: graph.topological_order) { |
96 (levels, key) => { |
91 (levels, key) => { |