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