src/Pure/General/graph.ML

 
 signature GRAPH =
 sig
   type key
   type 'a T
-  exception UNDEFINED of key
+  exception UNDEF of key
+  exception DUP of key
+  exception DUPS of key list
   val empty: 'a T
   val keys: '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
   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
   val all_succs: 'a T -> key list -> key list
   val find_paths: 'a T -> key * key -> key list list
-  exception DUPLICATE of key
   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 add_edge: key * key -> 'a T -> 'a T
   val del_edge: key * key -> '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
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
 struct
 

 
 (* graphs *)
 
 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
 
-exception UNDEFINED of key;
+exception UNDEF of key;
+exception DUP = Table.DUP;
+exception DUPS = Table.DUPS;
 
 val empty = Graph Table.empty;
 fun keys (Graph tab) = Table.keys tab;
 
 fun get_entry (Graph tab) x =
   (case Table.lookup (tab, x) of
     Some entry => entry
-  | None => raise UNDEFINED x);
+  | None => raise UNDEF x);
 
 fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab));
 
 
 (* nodes *)

       else flat (map (paths (p :: ps))
         (filter (fn pp => pp mem_keys X andalso not (pp mem_key ps)) (imm_preds G p)));
   in get_entry G y; if y mem_keys X then (paths [] y) else [] end;
 
 
-(* build graphs *)
+(* nodes *)
 
 exception DUPLICATE of key;
 
 fun new_node (x, info) (Graph tab) =
-  Graph (Table.update_new ((x, (info, ([], []))), tab)
-    handle Table.DUP key => raise DUPLICATE key);
+  Graph (Table.update_new ((x, (info, ([], []))), tab));
 
 fun del_nodes xs (Graph tab) =
   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)));
   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 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 add_edge_acyclic (x, y) G =
   (case find_paths G (y, x) of
     [] => add_edge (x, y) G
   | cycles => raise CYCLES (map (cons x) cycles));
 
+fun add_deps_acyclic (y, xs) G =
+  foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
+
+
+(* merge_acyclic *)
+
+fun merge_acyclic eq (Graph tab1, G2 as Graph tab2) =
+  foldl (fn (G, xy) => add_edge_acyclic xy G)
+    (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
+
 
 end;
 
 
 (*graphs indexed by strings*)