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