src/Pure/General/graph.scala
author wenzelm
Sun Nov 05 16:57:03 2017 +0100 (17 months ago)
changeset 67012 671decd2e627
parent 66830 3b50269b90c2
child 67018 f6aa133f9b16
permissions -rw-r--r--
uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");
     1 /*  Title:      Pure/General/graph.scala
     2     Author:     Makarius
     3 
     4 Directed graphs.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.immutable.{SortedMap, SortedSet}
    11 import scala.annotation.tailrec
    12 
    13 
    14 object Graph
    15 {
    16   class Duplicate[Key](val key: Key) extends Exception
    17   class Undefined[Key](val key: Key) extends Exception
    18   class Cycles[Key](val cycles: List[List[Key]]) extends Exception
    19 
    20   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    21     new Graph[Key, A](SortedMap.empty(ord))
    22 
    23   def make[Key, A](entries: List[((Key, A), List[Key])])(
    24     implicit ord: Ordering[Key]): Graph[Key, A] =
    25   {
    26     val graph1 =
    27       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
    28     val graph2 =
    29       (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
    30     graph2
    31   }
    32 
    33   def string[A]: Graph[String, A] = empty(Ordering.String)
    34   def int[A]: Graph[Int, A] = empty(Ordering.Int)
    35   def long[A]: Graph[Long, A] = empty(Ordering.Long)
    36 
    37 
    38   /* XML data representation */
    39 
    40   def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
    41     (graph: Graph[Key, A]) => {
    42       import XML.Encode._
    43       list(pair(pair(key, info), list(key)))(graph.dest)
    44     }
    45 
    46   def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
    47     implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
    48     (body: XML.Body) => {
    49       import XML.Decode._
    50       make(list(pair(pair(key, info), list(key)))(body))(ord)
    51     }
    52 }
    53 
    54 
    55 final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
    56 {
    57   type Keys = SortedSet[Key]
    58   type Entry = (A, (Keys, Keys))
    59 
    60   def ordering: Ordering[Key] = rep.ordering
    61   def empty_keys: Keys = SortedSet.empty[Key](ordering)
    62 
    63 
    64   /* graphs */
    65 
    66   def is_empty: Boolean = rep.isEmpty
    67   def defined(x: Key): Boolean = rep.isDefinedAt(x)
    68 
    69   def iterator: Iterator[(Key, Entry)] = rep.iterator
    70 
    71   def keys_iterator: Iterator[Key] = iterator.map(_._1)
    72   def keys: List[Key] = keys_iterator.toList
    73   def keys_set: Set[Key] = rep.keySet
    74 
    75   def dest: List[((Key, A), List[Key])] =
    76     (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
    77 
    78   override def toString: String =
    79     dest.map({ case ((x, _), ys) =>
    80         x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
    81       .mkString("Graph(", ", ", ")")
    82 
    83   private def get_entry(x: Key): Entry =
    84     rep.get(x) match {
    85       case Some(entry) => entry
    86       case None => throw new Graph.Undefined(x)
    87     }
    88 
    89   private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
    90     new Graph[Key, A](rep + (x -> f(get_entry(x))))
    91 
    92 
    93   /* nodes */
    94 
    95   def get_node(x: Key): A = get_entry(x)._1
    96 
    97   def map_node(x: Key, f: A => A): Graph[Key, A] =
    98     map_entry(x, { case (i, ps) => (f(i), ps) })
    99 
   100 
   101   /* reachability */
   102 
   103   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
   104   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
   105   {
   106     def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
   107     {
   108       val (rs, r_set) = reached
   109       if (r_set(x)) reached
   110       else {
   111         val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
   112         (x :: rs1, r_set1)
   113       }
   114     }
   115     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
   116     {
   117       val (rss, r_set) = reached
   118       val (rs, r_set1) = reach(x, (Nil, r_set))
   119       (rs :: rss, r_set1)
   120     }
   121     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
   122   }
   123 
   124   /*immediate*/
   125   def imm_preds(x: Key): Keys = get_entry(x)._2._1
   126   def imm_succs(x: Key): Keys = get_entry(x)._2._2
   127 
   128   /*transitive*/
   129   def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
   130   def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
   131 
   132   /*strongly connected components; see: David King and John Launchbury,
   133     "Structuring Depth First Search Algorithms in Haskell"*/
   134   def strong_conn: List[List[Key]] =
   135     reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
   136 
   137 
   138   /* minimal and maximal elements */
   139 
   140   def minimals: List[Key] =
   141     (List.empty[Key] /: rep) {
   142       case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
   143 
   144   def maximals: List[Key] =
   145     (List.empty[Key] /: rep) {
   146       case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
   147 
   148   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   149   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
   150 
   151   def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
   152 
   153 
   154   /* node operations */
   155 
   156   def new_node(x: Key, info: A): Graph[Key, A] =
   157   {
   158     if (defined(x)) throw new Graph.Duplicate(x)
   159     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
   160   }
   161 
   162   def default_node(x: Key, info: A): Graph[Key, A] =
   163     if (defined(x)) this else new_node(x, info)
   164 
   165   private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key)
   166       : SortedMap[Key, Entry] =
   167     map.get(y) match {
   168       case None => map
   169       case Some((i, (preds, succs))) =>
   170         map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
   171     }
   172 
   173   def del_node(x: Key): Graph[Key, A] =
   174   {
   175     val (preds, succs) = get_entry(x)._2
   176     new Graph[Key, A](
   177       (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
   178   }
   179 
   180   def restrict(pred: Key => Boolean): Graph[Key, A] =
   181     (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
   182 
   183 
   184   /* edge operations */
   185 
   186   def edges_iterator: Iterator[(Key, Key)] =
   187     for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y)
   188 
   189   def is_edge(x: Key, y: Key): Boolean =
   190     defined(x) && defined(y) && imm_succs(x)(y)
   191 
   192   def add_edge(x: Key, y: Key): Graph[Key, A] =
   193     if (is_edge(x, y)) this
   194     else
   195       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
   196       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
   197 
   198   def del_edge(x: Key, y: Key): Graph[Key, A] =
   199     if (is_edge(x, y))
   200       map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
   201       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
   202     else this
   203 
   204 
   205   /* irreducible paths -- Hasse diagram */
   206 
   207   private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] =
   208   {
   209     def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
   210     @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
   211       xs0 match {
   212         case Nil => xs1
   213         case x :: xs =>
   214           if (!x_set(x) || x == z || path.contains(x) ||
   215               xs.exists(red(x)) || xs1.exists(red(x)))
   216             irreds(xs, xs1)
   217           else irreds(xs, x :: xs1)
   218       }
   219     irreds(imm_preds(z).toList, Nil)
   220   }
   221 
   222   def irreducible_paths(x: Key, y: Key): List[List[Key]] =
   223   {
   224     val (_, x_set) = reachable(imm_succs, List(x))
   225     def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
   226       if (x == z) (z :: path) :: ps
   227       else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
   228     if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
   229   }
   230 
   231 
   232   /* transitive closure and reduction */
   233 
   234   private def transitive_step(z: Key): Graph[Key, A] =
   235   {
   236     val (preds, succs) = get_entry(z)._2
   237     var graph = this
   238     for (x <- preds; y <- succs) graph = graph.add_edge(x, y)
   239     graph
   240   }
   241 
   242   def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
   243 
   244   def transitive_reduction_acyclic: Graph[Key, A] =
   245   {
   246     val trans = this.transitive_closure
   247     if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
   248       error("Cyclic graph")
   249 
   250     var graph = this
   251     for {
   252       (x, (_, (_, succs))) <- iterator
   253       y <- succs
   254       if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
   255     } graph = graph.del_edge(x, y)
   256     graph
   257   }
   258 
   259 
   260   /* maintain acyclic graphs */
   261 
   262   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
   263     if (is_edge(x, y)) this
   264     else {
   265       irreducible_paths(y, x) match {
   266         case Nil => add_edge(x, y)
   267         case cycles => throw new Graph.Cycles(cycles.map(x :: _))
   268       }
   269     }
   270 
   271   def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =
   272     (this /: xs)(_.add_edge_acyclic(_, y))
   273 
   274   def topological_order: List[Key] = all_succs(minimals)
   275 }