src/Pure/General/graph.scala
author wenzelm
Tue Nov 07 11:11:37 2017 +0100 (17 months ago)
changeset 67018 f6aa133f9b16
parent 67012 671decd2e627
child 67935 61888dd27f73
permissions -rw-r--r--
backed out odd "bug fix" 671decd2e627;
     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 
    74   def dest: List[((Key, A), List[Key])] =
    75     (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
    76 
    77   override def toString: String =
    78     dest.map({ case ((x, _), ys) =>
    79         x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
    80       .mkString("Graph(", ", ", ")")
    81 
    82   private def get_entry(x: Key): Entry =
    83     rep.get(x) match {
    84       case Some(entry) => entry
    85       case None => throw new Graph.Undefined(x)
    86     }
    87 
    88   private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
    89     new Graph[Key, A](rep + (x -> f(get_entry(x))))
    90 
    91 
    92   /* nodes */
    93 
    94   def get_node(x: Key): A = get_entry(x)._1
    95 
    96   def map_node(x: Key, f: A => A): Graph[Key, A] =
    97     map_entry(x, { case (i, ps) => (f(i), ps) })
    98 
    99 
   100   /* reachability */
   101 
   102   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
   103   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
   104   {
   105     def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
   106     {
   107       val (rs, r_set) = reached
   108       if (r_set(x)) reached
   109       else {
   110         val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
   111         (x :: rs1, r_set1)
   112       }
   113     }
   114     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
   115     {
   116       val (rss, r_set) = reached
   117       val (rs, r_set1) = reach(x, (Nil, r_set))
   118       (rs :: rss, r_set1)
   119     }
   120     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
   121   }
   122 
   123   /*immediate*/
   124   def imm_preds(x: Key): Keys = get_entry(x)._2._1
   125   def imm_succs(x: Key): Keys = get_entry(x)._2._2
   126 
   127   /*transitive*/
   128   def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
   129   def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
   130 
   131   /*strongly connected components; see: David King and John Launchbury,
   132     "Structuring Depth First Search Algorithms in Haskell"*/
   133   def strong_conn: List[List[Key]] =
   134     reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
   135 
   136 
   137   /* minimal and maximal elements */
   138 
   139   def minimals: List[Key] =
   140     (List.empty[Key] /: rep) {
   141       case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
   142 
   143   def maximals: List[Key] =
   144     (List.empty[Key] /: rep) {
   145       case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
   146 
   147   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   148   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
   149 
   150   def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
   151 
   152 
   153   /* node operations */
   154 
   155   def new_node(x: Key, info: A): Graph[Key, A] =
   156   {
   157     if (defined(x)) throw new Graph.Duplicate(x)
   158     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
   159   }
   160 
   161   def default_node(x: Key, info: A): Graph[Key, A] =
   162     if (defined(x)) this else new_node(x, info)
   163 
   164   private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key)
   165       : SortedMap[Key, Entry] =
   166     map.get(y) match {
   167       case None => map
   168       case Some((i, (preds, succs))) =>
   169         map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
   170     }
   171 
   172   def del_node(x: Key): Graph[Key, A] =
   173   {
   174     val (preds, succs) = get_entry(x)._2
   175     new Graph[Key, A](
   176       (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
   177   }
   178 
   179   def restrict(pred: Key => Boolean): Graph[Key, A] =
   180     (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
   181 
   182 
   183   /* edge operations */
   184 
   185   def edges_iterator: Iterator[(Key, Key)] =
   186     for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y)
   187 
   188   def is_edge(x: Key, y: Key): Boolean =
   189     defined(x) && defined(y) && imm_succs(x)(y)
   190 
   191   def add_edge(x: Key, y: Key): Graph[Key, A] =
   192     if (is_edge(x, y)) this
   193     else
   194       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
   195       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
   196 
   197   def del_edge(x: Key, y: Key): Graph[Key, A] =
   198     if (is_edge(x, y))
   199       map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
   200       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
   201     else this
   202 
   203 
   204   /* irreducible paths -- Hasse diagram */
   205 
   206   private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] =
   207   {
   208     def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
   209     @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
   210       xs0 match {
   211         case Nil => xs1
   212         case x :: xs =>
   213           if (!x_set(x) || x == z || path.contains(x) ||
   214               xs.exists(red(x)) || xs1.exists(red(x)))
   215             irreds(xs, xs1)
   216           else irreds(xs, x :: xs1)
   217       }
   218     irreds(imm_preds(z).toList, Nil)
   219   }
   220 
   221   def irreducible_paths(x: Key, y: Key): List[List[Key]] =
   222   {
   223     val (_, x_set) = reachable(imm_succs, List(x))
   224     def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
   225       if (x == z) (z :: path) :: ps
   226       else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
   227     if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
   228   }
   229 
   230 
   231   /* transitive closure and reduction */
   232 
   233   private def transitive_step(z: Key): Graph[Key, A] =
   234   {
   235     val (preds, succs) = get_entry(z)._2
   236     var graph = this
   237     for (x <- preds; y <- succs) graph = graph.add_edge(x, y)
   238     graph
   239   }
   240 
   241   def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
   242 
   243   def transitive_reduction_acyclic: Graph[Key, A] =
   244   {
   245     val trans = this.transitive_closure
   246     if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
   247       error("Cyclic graph")
   248 
   249     var graph = this
   250     for {
   251       (x, (_, (_, succs))) <- iterator
   252       y <- succs
   253       if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
   254     } graph = graph.del_edge(x, y)
   255     graph
   256   }
   257 
   258 
   259   /* maintain acyclic graphs */
   260 
   261   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
   262     if (is_edge(x, y)) this
   263     else {
   264       irreducible_paths(y, x) match {
   265         case Nil => add_edge(x, y)
   266         case cycles => throw new Graph.Cycles(cycles.map(x :: _))
   267       }
   268     }
   269 
   270   def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =
   271     (this /: xs)(_.add_edge_acyclic(_, y))
   272 
   273   def topological_order: List[Key] = all_succs(minimals)
   274 }