1 /* Title: Tools/Graphview/src/mutator.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Filters and add-operations on graphs. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.Color |
|
13 import scala.collection.immutable.SortedSet |
|
14 |
|
15 |
|
16 trait Mutator |
|
17 { |
|
18 val name: String |
|
19 val description: String |
|
20 def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph |
|
21 |
|
22 override def toString: String = name |
|
23 } |
|
24 |
|
25 trait Filter extends Mutator |
|
26 { |
|
27 def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub) |
|
28 def filter(sub: Model.Graph) : Model.Graph |
|
29 } |
|
30 |
|
31 object Mutators { |
|
32 type Mutator_Markup = (Boolean, Color, Mutator) |
|
33 |
|
34 val Enabled = true |
|
35 val Disabled = false |
|
36 |
|
37 def create(visualizer: Visualizer, m: Mutator): Mutator_Markup = |
|
38 (Mutators.Enabled, visualizer.Colors.next, m) |
|
39 |
|
40 class Graph_Filter(val name: String, val description: String, |
|
41 pred: Model.Graph => Model.Graph) |
|
42 extends Filter |
|
43 { |
|
44 def filter(sub: Model.Graph) : Model.Graph = pred(sub) |
|
45 } |
|
46 |
|
47 class Graph_Mutator(val name: String, val description: String, |
|
48 pred: (Model.Graph, Model.Graph) => Model.Graph) |
|
49 extends Mutator |
|
50 { |
|
51 def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph = |
|
52 pred(complete, sub) |
|
53 } |
|
54 |
|
55 class Node_Filter(name: String, description: String, |
|
56 pred: (Model.Graph, String) => Boolean) |
|
57 extends Graph_Filter ( |
|
58 |
|
59 name, |
|
60 description, |
|
61 g => g.restrict(pred(g, _)) |
|
62 ) |
|
63 |
|
64 class Edge_Filter(name: String, description: String, |
|
65 pred: (Model.Graph, String, String) => Boolean) |
|
66 extends Graph_Filter ( |
|
67 |
|
68 name, |
|
69 description, |
|
70 g => (g /: g.dest) { |
|
71 case (graph, ((from, _), tos)) => { |
|
72 (graph /: tos) { |
|
73 (gr, to) => if (pred(gr, from, to)) gr |
|
74 else gr.del_edge(from, to) |
|
75 } |
|
76 } |
|
77 } |
|
78 ) |
|
79 |
|
80 class Node_Family_Filter(name: String, description: String, |
|
81 reverse: Boolean, parents: Boolean, children: Boolean, |
|
82 pred: (Model.Graph, String) => Boolean) |
|
83 extends Node_Filter( |
|
84 |
|
85 name, |
|
86 description, |
|
87 (g, k) => reverse != ( |
|
88 pred(g, k) || |
|
89 (parents && g.all_preds(List(k)).exists(pred(g, _))) || |
|
90 (children && g.all_succs(List(k)).exists(pred(g, _))) |
|
91 ) |
|
92 ) |
|
93 |
|
94 case class Identity() |
|
95 extends Graph_Filter( |
|
96 |
|
97 "Identity", |
|
98 "Does not change the graph.", |
|
99 g => g |
|
100 ) |
|
101 |
|
102 case class Node_Expression(regex: String, |
|
103 reverse: Boolean, parents: Boolean, children: Boolean) |
|
104 extends Node_Family_Filter( |
|
105 |
|
106 "Filter by Name", |
|
107 "Only shows or hides all nodes with any family member's name matching " + |
|
108 "a regex.", |
|
109 reverse, |
|
110 parents, |
|
111 children, |
|
112 (g, k) => (regex.r findFirstIn k).isDefined |
|
113 ) |
|
114 |
|
115 case class Node_List(list: List[String], |
|
116 reverse: Boolean, parents: Boolean, children: Boolean) |
|
117 extends Node_Family_Filter( |
|
118 |
|
119 "Filter by Name List", |
|
120 "Only shows or hides all nodes with any family member's name matching " + |
|
121 "any string in a comma separated list.", |
|
122 reverse, |
|
123 parents, |
|
124 children, |
|
125 (g, k) => list.exists(_ == k) |
|
126 ) |
|
127 |
|
128 case class Edge_Endpoints(source: String, dest: String) |
|
129 extends Edge_Filter( |
|
130 |
|
131 "Hide edge", |
|
132 "Hides the edge whose endpoints match strings.", |
|
133 (g, s, d) => !(s == source && d == dest) |
|
134 ) |
|
135 |
|
136 private def add_node_group(from: Model.Graph, to: Model.Graph, |
|
137 keys: List[String]) = { |
|
138 |
|
139 // Add Nodes |
|
140 val with_nodes = |
|
141 (to /: keys) { |
|
142 (graph, key) => graph.default_node(key, from.get_node(key)) |
|
143 } |
|
144 |
|
145 // Add Edges |
|
146 (with_nodes /: keys) { |
|
147 (gv, key) => { |
|
148 def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) = |
|
149 (g /: keys) { |
|
150 (graph, end) => { |
|
151 if (!graph.keys_iterator.contains(end)) graph |
|
152 else { |
|
153 if (succs) graph.add_edge(key, end) |
|
154 else graph.add_edge(end, key) |
|
155 } |
|
156 } |
|
157 } |
|
158 |
|
159 |
|
160 add_edges( |
|
161 add_edges(gv, from.imm_preds(key), false), |
|
162 from.imm_succs(key), true |
|
163 ) |
|
164 } |
|
165 } |
|
166 } |
|
167 |
|
168 case class Add_Node_Expression(regex: String) |
|
169 extends Graph_Mutator( |
|
170 |
|
171 "Add by name", |
|
172 "Adds every node whose name matches the regex. " + |
|
173 "Adds all relevant edges.", |
|
174 (complete, sub) => { |
|
175 add_node_group(complete, sub, complete.keys.filter( |
|
176 k => (regex.r findFirstIn k).isDefined |
|
177 ).toList) |
|
178 } |
|
179 ) |
|
180 |
|
181 case class Add_Transitive_Closure(parents: Boolean, children: Boolean) |
|
182 extends Graph_Mutator( |
|
183 |
|
184 "Add transitive closure", |
|
185 "Adds all family members of all current nodes.", |
|
186 (complete, sub) => { |
|
187 val withparents = |
|
188 if (parents) |
|
189 add_node_group(complete, sub, complete.all_preds(sub.keys)) |
|
190 else |
|
191 sub |
|
192 |
|
193 if (children) |
|
194 add_node_group(complete, withparents, complete.all_succs(sub.keys)) |
|
195 else |
|
196 withparents |
|
197 } |
|
198 ) |
|
199 } |
|