added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;

--- a/src/Pure/General/graph.ML	Fri May 21 21:27:42 2004 +0200
+++ b/src/Pure/General/graph.ML	Fri May 21 21:28:01 2004 +0200
@@ -15,6 +15,9 @@
   exception DUPS of key list
   val empty: 'a T
   val keys: 'a T -> key list
+  val dest: 'a T -> (key * key list) list
+  val minimals: 'a T -> key list
+  val maximals: 'a T -> key list
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
   val get_node: 'a T -> key -> 'a
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -26,20 +29,21 @@
   val find_paths: 'a T -> key * key -> key list list
   val new_node: key * 'a -> 'a T -> 'a T
   val del_nodes: key list -> 'a T -> 'a T
-  val edges: 'a T -> (key * key) list
+  val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T
   val del_edge: key * key -> 'a T -> 'a T
+  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T
   val add_deps_acyclic: key * key list -> 'a T -> 'a T
   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
-  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
+  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T
+  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
 struct
 
-
 (* keys *)
 
 type key = Key.key;
@@ -55,9 +59,6 @@
 infix del_key;
 fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
 
-infix del_keys;
-val op del_keys = foldl (op del_key);
-
 
 (* tables and sets of keys *)
 
@@ -83,6 +84,12 @@
 
 val empty = Graph Table.empty;
 fun keys (Graph tab) = Table.keys tab;
+fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
+
+fun minimals (Graph tab) =
+  Table.foldl (fn (ms, (m, (_, ([], _)))) => m :: ms | (ms, _) => ms) ([], tab);
+fun maximals (Graph tab) =
+  Table.foldl (fn (ms, (m, (_, (_, [])))) => m :: ms | (ms, _) => ms) ([], tab);
 
 fun get_entry (Graph tab) x =
   (case Table.lookup (tab, x) of
@@ -119,9 +126,8 @@
 fun all_preds G = flat o snd o reachable (imm_preds G);
 fun all_succs G = flat o snd o reachable (imm_succs G);
 
-(* strongly connected components; see: David King and John Launchbury, *)
-(* "Structuring Depth First Search Algorithms in Haskell"              *)
-
+(*strongly connected components; see: David King and John Launchbury,
+  "Structuring Depth First Search Algorithms in Haskell"*)
 fun strong_conn G = filter_out null (snd (reachable (imm_preds G)
   (flat (rev (snd (reachable (imm_succs G) (keys G)))))));
 
@@ -150,28 +156,50 @@
   let
     fun del (x, (i, (preds, succs))) =
       if x mem_key xs then None
-      else Some (x, (i, (preds del_keys xs, succs del_keys xs)));
+      else Some (x, (i, (foldl op del_key (preds, xs), foldl op del_key (succs, xs))));
   in Graph (Table.make (mapfilter del (Table.dest tab))) end;
 
 
 (* edges *)
 
-fun edges (Graph tab) =
-  flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab));
+fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
+
+fun add_edge (x, y) G =
+  if is_edge G (x, y) then G
+  else
+    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
+      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
+
+fun del_edge (x, y) G =
+  if is_edge G (x, y) then
+    G |> map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)))
+      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y)))
+  else G;
 
-fun add_edge (x, y) =
-  map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o
-   map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
+fun diff_edges G1 G2 =
+  flat (dest G1 |> map (fn (x, ys) => ys |> mapfilter (fn y =>
+    if is_edge G2 (x, y) then None else Some (x, y))));
+
+fun edges G = diff_edges G empty;
+
+
+(* merge *)
 
-fun del_edge (x, y) =
-  map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o
-   map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));
+fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
+  let
+    fun eq_node ((i1, _), (i2, _)) = eq (i1, i2);
+    fun no_edges (i, _) = (i, ([], []));
+  in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
 
+fun merge eq GG = gen_merge add_edge eq GG;
+
+
+(* maintain acyclic graphs *)
 
 exception CYCLES of key list list;
 
 fun add_edge_acyclic (x, y) G =
-  if y mem_key imm_succs G x then G
+  if is_edge G (x, y) then G
   else
     (case find_paths G (y, x) of
       [] => add_edge (x, y) G
@@ -180,16 +208,18 @@
 fun add_deps_acyclic (y, xs) G =
   foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
 
+fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
 
-(* merge_acyclic *)
+
+(* maintain transitive acyclic graphs *)
 
-fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
-  foldl (fn (G, xy) => add xy G)
-    (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
+fun add_edge_trans_acyclic (x, y) G =
+  add_edge_acyclic (x, y) G |>
+  fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
 
-fun merge_acyclic eq p = gen_merge add_edge_acyclic eq p;
-fun merge eq p = gen_merge add_edge eq p;
-
+fun merge_trans_acyclic eq (G1, G2) =
+  merge_acyclic eq (G1, G2) |>
+  fold add_edge_trans_acyclic (diff_edges G1 G2 @ diff_edges G2 G1);
 
 end;