# HG changeset patch
# User wenzelm
# Date 1355058069 -3600
# Node ID 68c9a6538c0ec8bd21bd8d6a6dc26010cfe6a41f
# Parent  f2241b8d0db588bedd8e1e9b39ad8ad1970c89ff
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

diff -r f2241b8d0db5 -r 68c9a6538c0e src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/Pure/General/graph.scala	Sun Dec 09 14:01:09 2012 +0100
@@ -222,6 +222,34 @@
   }
 
 
+  /* transitive closure and reduction */
+
+  def transitive_closure: Graph[Key, A] =
+  {
+    var graph = this
+    for {
+      (_, (_, (preds, succs))) <- this.entries
+      x <- preds
+      y <- succs
+    } graph = graph.add_edge(x, y)
+    graph
+  }
+
+  def transitive_reduction_acyclic: Graph[Key, A] =
+  {
+    val trans = this.transitive_closure
+    assert(!trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+
+    var graph = this
+    for {
+      (x, (_, (_, succs))) <- this.entries
+      y <- succs
+      if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
+    } graph = graph.del_edge(x, y)
+    graph
+  }
+
+
   /* maintain acyclic graphs */
 
   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =