# HG changeset patch
# User bulwahn
# Date 1244548588 -7200
# Node ID 9801a92d52d700208e7d7c85be29879fe82b90cd
# Parent  62fc203eed8840332a3057162ba5f1057e7be281
added graph builders

diff -r 62fc203eed88 -r 9801a92d52d7 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Jun 09 13:40:57 2009 +0200
+++ b/src/Pure/General/graph.ML	Tue Jun 09 13:56:28 2009 +0200
@@ -48,6 +48,8 @@
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
+  val extend: (key -> 'a * key list) -> key list -> 'a T -> 'a T
+  val make: (key -> 'a * key list) -> key list -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
@@ -275,6 +277,25 @@
   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
+  
+(* constructing graphs *)
+
+fun extend explore =
+  let
+    fun contains_node gr key = member eq_key (keys gr) key
+    fun extend' key gr =
+      let
+        val (node, preds) = explore key
+      in
+        gr |> (not (contains_node gr key)) ?
+          (new_node (key, node)
+          #> fold extend' preds
+          #> fold (add_edge o (pair key)) preds)
+      end
+  in fold extend' end
+
+fun make explore keys = extend explore keys empty
+
 
 (*final declarations of this structure!*)
 val fold = fold_graph;