src/Tools/Graphview/mutator.scala
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 59459 985fc55e9f27
permissions -rw-r--r--
more strict AFP properties;
     1 /*  Title:      Tools/Graphview/mutator.scala
     2     Author:     Markus Kaiser, TU Muenchen
     3     Author:     Makarius
     4 
     5 Filters and add-operations on graphs.
     6 */
     7 
     8 package isabelle.graphview
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.Color
    14 import scala.collection.immutable.SortedSet
    15 
    16 
    17 object 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 
   165 trait 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 
   174 trait 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 }