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