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