author wenzelm Thu, 23 Feb 2012 15:15:59 +0100 changeset 46613 74331911375d parent 46612 0a881b8c066e child 46614 165886a4fe64
further graph operations from ML;
 src/Pure/General/graph.ML file | annotate | diff | comparison | revisions src/Pure/General/graph.scala file | annotate | diff | comparison | revisions
```--- a/src/Pure/General/graph.ML	Thu Feb 23 14:46:38 2012 +0100
+++ b/src/Pure/General/graph.ML	Thu Feb 23 15:15:59 2012 +0100
@@ -37,11 +37,11 @@
val immediate_succs: 'a T -> key -> key list
val all_preds: 'a T -> key list -> key list
val all_succs: 'a T -> key list -> key list
+  val strong_conn: 'a T -> key list list
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val is_minimal: 'a T -> key -> bool
val is_maximal: 'a T -> key -> bool
-  val strong_conn: 'a T -> key list list
val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
val default_node: key * 'a -> 'a T -> 'a T
val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
@@ -169,17 +169,19 @@
fun all_preds G = flat o #1 o reachable (imm_preds G);
fun all_succs G = flat o #1 o reachable (imm_succs G);

-(*minimal and maximal elements*)
+(*strongly connected components; see: David King and John Launchbury,
+  "Structuring Depth First Search Algorithms in Haskell"*)
+fun strong_conn G =
+  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
+
+
+(* minimal and maximal elements *)
+
fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
fun is_minimal G x = Keys.is_empty (imm_preds G x);
fun is_maximal G x = Keys.is_empty (imm_succs G x);

-(*strongly connected components; see: David King and John Launchbury,
-  "Structuring Depth First Search Algorithms in Haskell"*)
-fun strong_conn G =
-  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
-

(* nodes *)
```
```--- a/src/Pure/General/graph.scala	Thu Feb 23 14:46:38 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 15:15:59 2012 +0100
@@ -91,6 +91,11 @@
def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten

+  /*strongly connected components; see: David King and John Launchbury,
+    "Structuring Depth First Search Algorithms in Haskell"*/
+  def strong_conn: List[List[Key]] =
+    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
+

/* minimal and maximal elements */

@@ -114,6 +119,12 @@
else new Graph[Key, A](rep + (x -> (info, (Set.empty, Set.empty))))
}

+  def default_node(x: Key, info: A): Graph[Key, A] =
+  {
+    if (rep.isDefinedAt(x)) this
+    else new_node(x, info)
+  }
+
def del_nodes(xs: List[Key]): Graph[Key, A] =
{
xs.foreach(get_entry)```