--- a/src/Pure/General/graph.ML Wed Oct 05 18:38:28 2005 +0200
+++ b/src/Pure/General/graph.ML Wed Oct 05 18:38:43 2005 +0200
@@ -18,9 +18,11 @@
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val map_nodes: ('a -> 'b) -> 'a T -> 'b T
+ val fold_nodes: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
val fold_map_nodes: (key * 'b -> 'a -> 'c * 'a) -> 'b T -> 'a -> 'c T * 'a
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
+ val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
val imm_preds: 'a T -> key -> key list
val imm_succs: 'a T -> key -> key list
val all_preds: 'a T -> key list -> key list
@@ -92,12 +94,18 @@
| NONE => raise UNDEF x);
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
+fun map_entry_yield x f (G as Graph tab) =
+ let val (a, node') = f (get_entry G x)
+ in (a, Graph (Table.update (x, node') tab)) end;
(* nodes *)
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
+fun fold_nodes f (Graph tab) s =
+ Table.fold (fn (k, (i, ps)) => f (k, i)) tab s
+
fun fold_map_nodes f (Graph tab) s =
s
|> Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab
@@ -105,7 +113,8 @@
fun get_node G = #1 o get_entry G;
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
-
+fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
+ let val (a, i') = f i in (a, (i', ps)) end);
(* reachability *)