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");
1 /*  Title:      Pure/General/graph.scala
2     Author:     Makarius
4 Directed graphs.
5 */
7 package isabelle
10 import scala.collection.immutable.{SortedMap, SortedSet}
11 import scala.annotation.tailrec
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
20   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
21     new Graph[Key, A](SortedMap.empty(ord))
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   }
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)
38   /* XML data representation */
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     }
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 }
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))
60   def ordering: Ordering[Key] = rep.ordering
61   def empty_keys: Keys = SortedSet.empty[Key](ordering)
64   /* graphs */
66   def is_empty: Boolean = rep.isEmpty
67   def defined(x: Key): Boolean = rep.isDefinedAt(x)
69   def iterator: Iterator[(Key, Entry)] = rep.iterator
71   def keys_iterator: Iterator[Key] = iterator.map(_._1)
72   def keys: List[Key] = keys_iterator.toList
73   def keys_set: Set[Key] = rep.keySet
75   def dest: List[((Key, A), List[Key])] =
76     (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
78   override def toString: String =
79     dest.map({ case ((x, _), ys) =>
80         x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
81       .mkString("Graph(", ", ", ")")
83   private def get_entry(x: Key): Entry =
84     rep.get(x) match {
85       case Some(entry) => entry
86       case None => throw new Graph.Undefined(x)
87     }
89   private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
90     new Graph[Key, A](rep + (x -> f(get_entry(x))))
93   /* nodes */
95   def get_node(x: Key): A = get_entry(x)._1
97   def map_node(x: Key, f: A => A): Graph[Key, A] =
98     map_entry(x, { case (i, ps) => (f(i), ps) })
101   /* reachability */
103   /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
104   def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
105   {
106     def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
107     {
108       val (rs, r_set) = reached
109       if (r_set(x)) reached
110       else {
111         val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
112         (x :: rs1, r_set1)
113       }
114     }
115     def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
116     {
117       val (rss, r_set) = reached
118       val (rs, r_set1) = reach(x, (Nil, r_set))
120     }
121     ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
122   }
124   /*immediate*/
125   def imm_preds(x: Key): Keys = get_entry(x)._2._1
126   def imm_succs(x: Key): Keys = get_entry(x)._2._2
128   /*transitive*/
129   def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
130   def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
132   /*strongly connected components; see: David King and John Launchbury,
133     "Structuring Depth First Search Algorithms in Haskell"*/
134   def strong_conn: List[List[Key]] =
135     reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
138   /* minimal and maximal elements */
140   def minimals: List[Key] =
141     (List.empty[Key] /: rep) {
142       case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
144   def maximals: List[Key] =
145     (List.empty[Key] /: rep) {
146       case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
148   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
149   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
151   def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
154   /* node operations */
156   def new_node(x: Key, info: A): Graph[Key, A] =
157   {
158     if (defined(x)) throw new Graph.Duplicate(x)
159     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
160   }
162   def default_node(x: Key, info: A): Graph[Key, A] =
163     if (defined(x)) this else new_node(x, info)
165   private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key)
166       : SortedMap[Key, Entry] =
167     map.get(y) match {
168       case None => map
169       case Some((i, (preds, succs))) =>
170         map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
171     }
173   def del_node(x: Key): Graph[Key, A] =
174   {
175     val (preds, succs) = get_entry(x)._2
176     new Graph[Key, A](
178   }
180   def restrict(pred: Key => Boolean): Graph[Key, A] =
181     (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
184   /* edge operations */
186   def edges_iterator: Iterator[(Key, Key)] =
187     for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y)
189   def is_edge(x: Key, y: Key): Boolean =
190     defined(x) && defined(y) && imm_succs(x)(y)
192   def add_edge(x: Key, y: Key): Graph[Key, A] =
193     if (is_edge(x, y)) this
194     else
195       map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
196       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
198   def del_edge(x: Key, y: Key): Graph[Key, A] =
199     if (is_edge(x, y))
200       map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
201       map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
202     else this
205   /* irreducible paths -- Hasse diagram */
207   private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] =
208   {
209     def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
210     @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
211       xs0 match {
212         case Nil => xs1
213         case x :: xs =>
214           if (!x_set(x) || x == z || path.contains(x) ||
215               xs.exists(red(x)) || xs1.exists(red(x)))
216             irreds(xs, xs1)
217           else irreds(xs, x :: xs1)
218       }
219     irreds(imm_preds(z).toList, Nil)
220   }
222   def irreducible_paths(x: Key, y: Key): List[List[Key]] =
223   {
224     val (_, x_set) = reachable(imm_succs, List(x))
225     def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
226       if (x == z) (z :: path) :: ps
227       else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
228     if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
229   }
232   /* transitive closure and reduction */
234   private def transitive_step(z: Key): Graph[Key, A] =
235   {
236     val (preds, succs) = get_entry(z)._2
237     var graph = this
238     for (x <- preds; y <- succs) graph = graph.add_edge(x, y)
239     graph
240   }
242   def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
244   def transitive_reduction_acyclic: Graph[Key, A] =
245   {
246     val trans = this.transitive_closure
247     if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
248       error("Cyclic graph")
250     var graph = this
251     for {
252       (x, (_, (_, succs))) <- iterator
253       y <- succs
254       if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
255     } graph = graph.del_edge(x, y)
256     graph
257   }
260   /* maintain acyclic graphs */
262   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
263     if (is_edge(x, y)) this
264     else {
265       irreducible_paths(y, x) match {
266         case Nil => add_edge(x, y)
267         case cycles => throw new Graph.Cycles(cycles.map(x :: _))
268       }
269     }
271   def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =