--- 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;