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