--- a/src/Pure/General/graph.ML Tue Jul 24 19:44:35 2007 +0200
+++ b/src/Pure/General/graph.ML Tue Jul 24 19:44:36 2007 +0200
@@ -44,6 +44,7 @@
val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*)
val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*)
val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
+ 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*)
end;
@@ -130,7 +131,7 @@
fun reach x (rs, R) =
if member_keys R x then (rs, R)
else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
- in fold_map (fn x => reach x o pair []) xs empty_keys end;
+ in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end;
(*immediate*)
fun imm_preds G = #1 o #2 o get_entry G;
@@ -249,6 +250,8 @@
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
+fun topological_order G = minimals G |> all_succs G;
+
(* maintain transitive acyclic graphs *)