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