directed graphs (in Scala);
authorwenzelm
Thu Feb 23 14:17:51 2012 +0100 (2012-02-23)
changeset 46611669601fa1a62
parent 46601 be67deaea760
child 46612 0a881b8c066e
directed graphs (in Scala);
src/Pure/General/graph.ML
src/Pure/General/graph.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/graph.ML	Thu Feb 23 12:08:59 2012 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Thu Feb 23 14:17:51 2012 +0100
     1.3 @@ -27,10 +27,10 @@
     1.4    val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
     1.5    val subgraph: (key -> bool) -> 'a T -> 'a T
     1.6    val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
     1.7 -  val map: (key -> 'a -> 'b) -> 'a T -> 'b T
     1.8    val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
     1.9    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    1.10    val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    1.11 +  val map: (key -> 'a -> 'b) -> 'a T -> 'b T
    1.12    val imm_preds: 'a T -> key -> Keys.T
    1.13    val imm_succs: 'a T -> key -> Keys.T
    1.14    val immediate_preds: 'a T -> key -> key list
    1.15 @@ -137,8 +137,6 @@
    1.16  
    1.17  (* nodes *)
    1.18  
    1.19 -fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
    1.20 -
    1.21  fun get_node G = #1 o #2 o get_entry G;
    1.22  
    1.23  fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
    1.24 @@ -146,6 +144,8 @@
    1.25  fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
    1.26    let val (a, i') = f i in (a, (i', ps)) end);
    1.27  
    1.28 +fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
    1.29 +
    1.30  
    1.31  (* reachability *)
    1.32  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/graph.scala	Thu Feb 23 14:17:51 2012 +0100
     2.3 @@ -0,0 +1,200 @@
     2.4 +/*  Title:      Pure/General/graph.scala
     2.5 +    Module:     PIDE
     2.6 +    Author:     Makarius
     2.7 +
     2.8 +Directed graphs.
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +import scala.annotation.tailrec
    2.15 +
    2.16 +
    2.17 +object Graph
    2.18 +{
    2.19 +  class Duplicate[Key](x: Key) extends Exception
    2.20 +  class Undefined[Key](x: Key) extends Exception
    2.21 +  class Cycles[Key](cycles: List[List[Key]]) extends Exception
    2.22 +
    2.23 +  def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)
    2.24 +}
    2.25 +
    2.26 +
    2.27 +class Graph[Key, A] private(rep: Map[Key, (A, (Set[Key], Set[Key]))])
    2.28 +  extends Iterable[(Key, (A, (Set[Key], Set[Key])))]
    2.29 +{
    2.30 +  type Keys = Set[Key]
    2.31 +  type Entry = (A, (Keys, Keys))
    2.32 +
    2.33 +  def iterator: Iterator[(Key, Entry)] = rep.iterator
    2.34 +
    2.35 +  def is_empty: Boolean = rep.isEmpty
    2.36 +
    2.37 +  def keys: Set[Key] = rep.keySet.toSet
    2.38 +
    2.39 +  def dest: List[(Key, List[Key])] =
    2.40 +    (for ((x, (_, (_, succs))) <- iterator) yield (x, succs.toList)).toList
    2.41 +
    2.42 +
    2.43 +  /* entries */
    2.44 +
    2.45 +  private def get_entry(x: Key): Entry =
    2.46 +    rep.get(x) match {
    2.47 +      case Some(entry) => entry
    2.48 +      case None => throw new Graph.Undefined(x)
    2.49 +    }
    2.50 +
    2.51 +  private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] =
    2.52 +    new Graph[Key, A](rep + (x -> f(get_entry(x))))
    2.53 +
    2.54 +
    2.55 +  /* nodes */
    2.56 +
    2.57 +  def map_nodes[B](f: A => B): Graph[Key, B] =
    2.58 +    new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) })
    2.59 +
    2.60 +  def get_node(x: Key): A = get_entry(x)._1
    2.61 +
    2.62 +  def map_node(x: Key, f: A => A): Graph[Key, A] =
    2.63 +    map_entry(x, { case (i, ps) => (f(i), ps) })
    2.64 +
    2.65 +
    2.66 +  /* reachability */
    2.67 +
    2.68 +  /*nodes reachable from xs -- topologically sorted for acyclic graphs*/
    2.69 +  def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
    2.70 +  {
    2.71 +    def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
    2.72 +    {
    2.73 +      val (rs, r_set) = reached
    2.74 +      if (r_set(x)) reached
    2.75 +      else {
    2.76 +        val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
    2.77 +        (x :: rs1, r_set1)
    2.78 +      }
    2.79 +    }
    2.80 +    def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
    2.81 +    {
    2.82 +      val (rss, r_set) = reached
    2.83 +      val (rs, r_set1) = reach((Nil, r_set), x)
    2.84 +      (rs :: rss, r_set1)
    2.85 +    }
    2.86 +    ((List.empty[List[Key]], Set.empty[Key]) /: xs)(reachs)
    2.87 +  }
    2.88 +
    2.89 +  /*immediate*/
    2.90 +  def imm_preds(x: Key): Keys = get_entry(x)._2._1
    2.91 +  def imm_succs(x: Key): Keys = get_entry(x)._2._2
    2.92 +
    2.93 +  /*transitive*/
    2.94 +  def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
    2.95 +  def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
    2.96 +
    2.97 +
    2.98 +  /* minimal and maximal elements */
    2.99 +
   2.100 +  def minimals: List[Key] =
   2.101 +    (List.empty[Key] /: rep) {
   2.102 +      case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
   2.103 +
   2.104 +  def maximals: List[Key] =
   2.105 +    (List.empty[Key] /: rep) {
   2.106 +      case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
   2.107 +
   2.108 +  def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   2.109 +  def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
   2.110 +
   2.111 +
   2.112 +  /* nodes */
   2.113 +
   2.114 +  def new_node(x: Key, info: A): Graph[Key, A] =
   2.115 +  {
   2.116 +    if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)
   2.117 +    else new Graph[Key, A](rep + (x -> (info, (Set.empty, Set.empty))))
   2.118 +  }
   2.119 +
   2.120 +  def del_nodes(xs: List[Key]): Graph[Key, A] =
   2.121 +  {
   2.122 +    xs.foreach(get_entry)
   2.123 +    new Graph[Key, A](
   2.124 +      (rep -- xs) mapValues { case (i, (preds, succs)) => (i, (preds -- xs, succs -- xs)) })
   2.125 +  }
   2.126 +
   2.127 +  private def del_adjacent(fst: Boolean, x: Key)(map: Map[Key, Entry], y: Key): Map[Key, Entry] =
   2.128 +    map.get(y) match {
   2.129 +      case None => map
   2.130 +      case Some((i, (preds, succs))) =>
   2.131 +        map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x)))
   2.132 +    }
   2.133 +
   2.134 +  def del_node(x: Key): Graph[Key, A] =
   2.135 +  {
   2.136 +    val (preds, succs) = get_entry(x)._2
   2.137 +    new Graph[Key, A](
   2.138 +      (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
   2.139 +  }
   2.140 +
   2.141 +
   2.142 +  /* edges */
   2.143 +
   2.144 +  def is_edge(x: Key, y: Key): Boolean =
   2.145 +    try { imm_succs(x)(y) }
   2.146 +    catch { case _: Graph.Undefined[_] => false }
   2.147 +
   2.148 +  def add_edge(x: Key, y: Key): Graph[Key, A] =
   2.149 +    if (is_edge(x, y)) this
   2.150 +    else
   2.151 +      map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }).
   2.152 +      map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) })
   2.153 +
   2.154 +  def del_edge(x: Key, y: Key): Graph[Key, A] =
   2.155 +    if (is_edge(x, y))
   2.156 +      map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }).
   2.157 +      map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) })
   2.158 +    else this
   2.159 +
   2.160 +
   2.161 +  /* irreducible paths -- Hasse diagram */
   2.162 +
   2.163 +  def irreducible_preds(x_set: Set[Key], path: List[Key], z: Key): List[Key] =
   2.164 +  {
   2.165 +    def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z
   2.166 +    @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] =
   2.167 +      xs0 match {
   2.168 +        case Nil => xs1
   2.169 +        case x :: xs =>
   2.170 +          if (!(x_set(x)) || x == z || path.contains(x) ||
   2.171 +              xs.exists(red(x)) || xs1.exists(red(x)))
   2.172 +            irreds(xs, xs1)
   2.173 +          else irreds(xs, x :: xs1)
   2.174 +      }
   2.175 +    irreds(imm_preds(z).toList, Nil)
   2.176 +  }
   2.177 +
   2.178 +  def irreducible_paths(x: Key, y: Key): List[List[Key]] =
   2.179 +  {
   2.180 +    val (_, x_set) = reachable(imm_succs, List(x))
   2.181 +    def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
   2.182 +      if (x == z) (z :: path) :: ps
   2.183 +      else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
   2.184 +    if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
   2.185 +  }
   2.186 +
   2.187 +
   2.188 +  /* maintain acyclic graphs */
   2.189 +
   2.190 +  def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =
   2.191 +    if (is_edge(x, y)) this
   2.192 +    else {
   2.193 +      irreducible_paths(y, x) match {
   2.194 +        case Nil => add_edge(x, y)
   2.195 +        case cycles => throw new Graph.Cycles(cycles.map(x :: _))
   2.196 +      }
   2.197 +    }
   2.198 +
   2.199 +  def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] =
   2.200 +    (this /: xs)(_.add_edge_acyclic(_, y))
   2.201 +
   2.202 +  def topological_order: List[Key] = all_succs(minimals)
   2.203 +}
     3.1 --- a/src/Pure/build-jars	Thu Feb 23 12:08:59 2012 +0100
     3.2 +++ b/src/Pure/build-jars	Thu Feb 23 14:17:51 2012 +0100
     3.3 @@ -14,6 +14,7 @@
     3.4    Concurrent/simple_thread.scala
     3.5    Concurrent/volatile.scala
     3.6    General/exn.scala
     3.7 +  General/graph.scala
     3.8    General/linear_set.scala
     3.9    General/path.scala
    3.10    General/position.scala