46611

1 
/* Title: Pure/General/graph.scala


2 
Module: PIDE


3 
Author: Makarius


4 


5 
Directed graphs.


6 
*/


7 


8 
package isabelle


9 


10 


11 
import scala.annotation.tailrec


12 


13 


14 
object Graph


15 
{


16 
class Duplicate[Key](x: Key) extends Exception


17 
class Undefined[Key](x: Key) extends Exception


18 
class Cycles[Key](cycles: List[List[Key]]) extends Exception


19 


20 
def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)


21 
}


22 


23 


24 
class Graph[Key, A] private(rep: Map[Key, (A, (Set[Key], Set[Key]))])


25 
extends Iterable[(Key, (A, (Set[Key], Set[Key])))]


26 
{


27 
type Keys = Set[Key]


28 
type Entry = (A, (Keys, Keys))


29 


30 
def iterator: Iterator[(Key, Entry)] = rep.iterator


31 


32 
def is_empty: Boolean = rep.isEmpty


33 


34 
def keys: Set[Key] = rep.keySet.toSet


35 


36 
def dest: List[(Key, List[Key])] =


37 
(for ((x, (_, (_, succs))) < iterator) yield (x, succs.toList)).toList


38 


39 


40 
/* entries */


41 


42 
private def get_entry(x: Key): Entry =


43 
rep.get(x) match {


44 
case Some(entry) => entry


45 
case None => throw new Graph.Undefined(x)


46 
}


47 


48 
private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =


49 
new Graph[Key, A](rep + (x > f(get_entry(x))))


50 


51 


52 
/* nodes */


53 


54 
def map_nodes[B](f: A => B): Graph[Key, B] =


55 
new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) })


56 


57 
def get_node(x: Key): A = get_entry(x)._1


58 


59 
def map_node(x: Key, f: A => A): Graph[Key, A] =


60 
map_entry(x, { case (i, ps) => (f(i), ps) })


61 


62 


63 
/* reachability */


64 


65 
/*nodes reachable from xs  topologically sorted for acyclic graphs*/


66 
def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =


67 
{


68 
def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =


69 
{


70 
val (rs, r_set) = reached


71 
if (r_set(x)) reached


72 
else {


73 
val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)


74 
(x :: rs1, r_set1)


75 
}


76 
}


77 
def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =


78 
{


79 
val (rss, r_set) = reached


80 
val (rs, r_set1) = reach((Nil, r_set), x)


81 
(rs :: rss, r_set1)


82 
}


83 
((List.empty[List[Key]], Set.empty[Key]) /: xs)(reachs)


84 
}


85 


86 
/*immediate*/


87 
def imm_preds(x: Key): Keys = get_entry(x)._2._1


88 
def imm_succs(x: Key): Keys = get_entry(x)._2._2


89 


90 
/*transitive*/


91 
def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten


92 
def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten


93 

46613

94 
/*strongly connected components; see: David King and John Launchbury,


95 
"Structuring Depth First Search Algorithms in Haskell"*/


96 
def strong_conn: List[List[Key]] =


97 
reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse


98 

46611

99 


100 
/* minimal and maximal elements */


101 


102 
def minimals: List[Key] =


103 
(List.empty[Key] /: rep) {


104 
case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }


105 


106 
def maximals: List[Key] =


107 
(List.empty[Key] /: rep) {


108 
case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }


109 


110 
def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty


111 
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty


112 


113 


114 
/* nodes */


115 


116 
def new_node(x: Key, info: A): Graph[Key, A] =


117 
{


118 
if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)


119 
else new Graph[Key, A](rep + (x > (info, (Set.empty, Set.empty))))


120 
}


121 

46613

122 
def default_node(x: Key, info: A): Graph[Key, A] =


123 
{


124 
if (rep.isDefinedAt(x)) this


125 
else new_node(x, info)


126 
}


127 

46611

128 
def del_nodes(xs: List[Key]): Graph[Key, A] =


129 
{


130 
xs.foreach(get_entry)


131 
new Graph[Key, A](


132 
(rep  xs) mapValues { case (i, (preds, succs)) => (i, (preds  xs, succs  xs)) })


133 
}


134 


135 
private def del_adjacent(fst: Boolean, x: Key)(map: Map[Key, Entry], y: Key): Map[Key, Entry] =


136 
map.get(y) match {


137 
case None => map


138 
case Some((i, (preds, succs))) =>


139 
map + (y > (i, if (fst) (preds  x, succs) else (preds, succs  x)))


140 
}


141 


142 
def del_node(x: Key): Graph[Key, A] =


143 
{


144 
val (preds, succs) = get_entry(x)._2


145 
new Graph[Key, A](


146 
(((rep  x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))


147 
}


148 


149 


150 
/* edges */


151 


152 
def is_edge(x: Key, y: Key): Boolean =


153 
try { imm_succs(x)(y) }


154 
catch { case _: Graph.Undefined[_] => false }


155 


156 
def add_edge(x: Key, y: Key): Graph[Key, A] =


157 
if (is_edge(x, y)) this


158 
else


159 
map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).


160 
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })


161 


162 
def del_edge(x: Key, y: Key): Graph[Key, A] =


163 
if (is_edge(x, y))


164 
map_entry(y, { case (i, (preds, succs)) => (i, (preds  x, succs)) }).


165 
map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs  y)) })


166 
else this


167 


168 


169 
/* irreducible paths  Hasse diagram */


170 


171 
def irreducible_preds(x_set: Set[Key], path: List[Key], z: Key): List[Key] =


172 
{


173 
def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z


174 
@tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =


175 
xs0 match {


176 
case Nil => xs1


177 
case x :: xs =>


178 
if (!(x_set(x))  x == z  path.contains(x) 


179 
xs.exists(red(x))  xs1.exists(red(x)))


180 
irreds(xs, xs1)


181 
else irreds(xs, x :: xs1)


182 
}


183 
irreds(imm_preds(z).toList, Nil)


184 
}


185 


186 
def irreducible_paths(x: Key, y: Key): List[List[Key]] =


187 
{


188 
val (_, x_set) = reachable(imm_succs, List(x))


189 
def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =


190 
if (x == z) (z :: path) :: ps


191 
else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))


192 
if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)


193 
}


194 


195 


196 
/* maintain acyclic graphs */


197 


198 
def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =


199 
if (is_edge(x, y)) this


200 
else {


201 
irreducible_paths(y, x) match {


202 
case Nil => add_edge(x, y)


203 
case cycles => throw new Graph.Cycles(cycles.map(x :: _))


204 
}


205 
}


206 


207 
def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] =


208 
(this /: xs)(_.add_edge_acyclic(_, y))


209 


210 
def topological_order: List[Key] = all_succs(minimals)


211 
}
