src/Pure/General/graph.scala
author wenzelm
Mon Feb 27 17:13:25 2012 +0100 (2012-02-27)
changeset 46712 8650d9a95736
parent 46668 9034b44844bd
child 48348 cbb25adad26f
permissions -rw-r--r--
prefer final ADTs -- prevent ooddities;
     1 /*  Title:      Pure/General/graph.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Directed graphs.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.immutable.{SortedMap, SortedSet}
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Graph
    16 {
    17   class Duplicate[Key](x: Key) extends Exception
    18   class Undefined[Key](x: Key) extends Exception
    19   class Cycles[Key](cycles: List[List[Key]]) extends Exception
    20 
    21   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
    22     new Graph[Key, A](SortedMap.empty(ord))
    23 
    24   def string[A]: Graph[String, A] = empty(Ordering.String)
    25   def int[A]: Graph[Int, A] = empty(Ordering.Int)
    26   def long[A]: Graph[Long, A] = empty(Ordering.Long)
    27 }
    28 
    29 
    30 final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
    31 {
    32   type Keys = SortedSet[Key]
    33   type Entry = (A, (Keys, Keys))
    34 
    35   def ordering: Ordering[Key] = rep.ordering
    36   def empty_keys: Keys = SortedSet.empty[Key](ordering)
    37 
    38 
    39   /* graphs */
    40 
    41   def is_empty: Boolean = rep.isEmpty
    42 
    43   def entries: Iterator[(Key, Entry)] = rep.iterator
    44   def keys: Iterator[Key] = entries.map(_._1)
    45 
    46   def dest: List[(Key, List[Key])] =
    47     (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
    48 
    49   override def toString: String =
    50     dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
    51       .mkString("Graph(", ", ", ")")
    52 
    53   private def get_entry(x: Key): Entry =
    54     rep.get(x) match {
    55       case Some(entry) => entry
    56       case None => throw new Graph.Undefined(x)
    57     }
    58 
    59   private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
    60     new Graph[Key, A](rep + (x -> f(get_entry(x))))
    61 
    62 
    63   /* nodes */
    64 
    65   def get_node(x: Key): A = get_entry(x)._1
    66 
    67   def map_node(x: Key, f: A => A): Graph[Key, A] =
    68     map_entry(x, { case (i, ps) => (f(i), ps) })
    69 
    70 
    71   /* reachability */
    72 
    73   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
    74   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
    75   {
    76     def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
    77     {
    78       val (rs, r_set) = reached
    79       if (r_set(x)) reached
    80       else {
    81         val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
    82         (x :: rs1, r_set1)
    83       }
    84     }
    85     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
    86     {
    87       val (rss, r_set) = reached
    88       val (rs, r_set1) = reach((Nil, r_set), x)
    89       (rs :: rss, r_set1)
    90     }
    91     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
    92   }
    93 
    94   /*immediate*/
    95   def imm_preds(x: Key): Keys = get_entry(x)._2._1
    96   def imm_succs(x: Key): Keys = get_entry(x)._2._2
    97 
    98   /*transitive*/
    99   def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
   100   def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
   101 
   102   /*strongly connected components; see: David King and John Launchbury,
   103     "Structuring Depth First Search Algorithms in Haskell"*/
   104   def strong_conn: List[List[Key]] =
   105     reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
   106 
   107 
   108   /* minimal and maximal elements */
   109 
   110   def minimals: List[Key] =
   111     (List.empty[Key] /: rep) {
   112       case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
   113 
   114   def maximals: List[Key] =
   115     (List.empty[Key] /: rep) {
   116       case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
   117 
   118   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   119   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
   120 
   121 
   122   /* node operations */
   123 
   124   def new_node(x: Key, info: A): Graph[Key, A] =
   125   {
   126     if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)
   127     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
   128   }
   129 
   130   def default_node(x: Key, info: A): Graph[Key, A] =
   131   {
   132     if (rep.isDefinedAt(x)) this
   133     else new_node(x, info)
   134   }
   135 
   136   private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key)
   137       : SortedMap[Key, Entry] =
   138     map.get(y) match {
   139       case None => map
   140       case Some((i, (preds, succs))) =>
   141         map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
   142     }
   143 
   144   def del_node(x: Key): Graph[Key, A] =
   145   {
   146     val (preds, succs) = get_entry(x)._2
   147     new Graph[Key, A](
   148       (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
   149   }
   150 
   151   def restrict(pred: Key => Boolean): Graph[Key, A] =
   152     (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
   153 
   154 
   155   /* edge operations */
   156 
   157   def is_edge(x: Key, y: Key): Boolean =
   158     try { imm_succs(x)(y) }
   159     catch { case _: Graph.Undefined[_] => false }
   160 
   161   def add_edge(x: Key, y: Key): Graph[Key, A] =
   162     if (is_edge(x, y)) this
   163     else
   164       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
   165       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
   166 
   167   def del_edge(x: Key, y: Key): Graph[Key, A] =
   168     if (is_edge(x, y))
   169       map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
   170       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
   171     else this
   172 
   173 
   174   /* irreducible paths -- Hasse diagram */
   175 
   176   private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] =
   177   {
   178     def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
   179     @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
   180       xs0 match {
   181         case Nil => xs1
   182         case x :: xs =>
   183           if (!(x_set(x)) || x == z || path.contains(x) ||
   184               xs.exists(red(x)) || xs1.exists(red(x)))
   185             irreds(xs, xs1)
   186           else irreds(xs, x :: xs1)
   187       }
   188     irreds(imm_preds(z).toList, Nil)
   189   }
   190 
   191   def irreducible_paths(x: Key, y: Key): List[List[Key]] =
   192   {
   193     val (_, x_set) = reachable(imm_succs, List(x))
   194     def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
   195       if (x == z) (z :: path) :: ps
   196       else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
   197     if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
   198   }
   199 
   200 
   201   /* maintain acyclic graphs */
   202 
   203   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
   204     if (is_edge(x, y)) this
   205     else {
   206       irreducible_paths(y, x) match {
   207         case Nil => add_edge(x, y)
   208         case cycles => throw new Graph.Cycles(cycles.map(x :: _))
   209       }
   210     }
   211 
   212   def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] =
   213     (this /: xs)(_.add_edge_acyclic(_, y))
   214 
   215   def topological_order: List[Key] = all_succs(minimals)
   216 }