added graph builders
authorbulwahn
Tue, 09 Jun 2009 13:56:28 +0200
changeset 31516 9801a92d52d7
parent 31515 62fc203eed88
child 31517 e8a64ab9fe99
added graph builders
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;