src/Pure/General/graph.ML
author wenzelm
Fri Feb 03 23:12:28 2006 +0100 (2006-02-03 ago)
changeset 18921 f47c46d7d654
parent 18133 1d403623dabc
child 18970 d055a29ddd23
permissions -rw-r--r--
canonical member/insert/merge;
     1 (*  Title:      Pure/General/graph.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4 
     5 Directed graphs.
     6 *)
     7 
     8 signature GRAPH =
     9 sig
    10   type key
    11   type 'a T
    12   exception UNDEF of key
    13   exception DUP of key
    14   exception DUPS of key list
    15   val empty: 'a T
    16   val keys: 'a T -> key list
    17   val dest: 'a T -> (key * key list) list
    18   val minimals: 'a T -> key list
    19   val maximals: 'a T -> key list
    20   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
    21   val fold_nodes: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
    22   val fold_map_nodes: (key * 'b -> 'a -> 'c * 'a) -> 'b T -> 'a -> 'c T * 'a
    23   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    24   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    25   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    26   val imm_preds: 'a T -> key -> key list
    27   val imm_succs: 'a T -> key -> key list
    28   val all_preds: 'a T -> key list -> key list
    29   val all_succs: 'a T -> key list -> key list
    30   val strong_conn: 'a T -> key list list
    31   val subgraph: key list -> 'a T -> 'a T
    32   val find_paths: 'a T -> key * key -> key list list
    33   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    34   val default_node: key * 'a -> 'a T -> 'a T
    35   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    36   val is_edge: 'a T -> key * key -> bool
    37   val add_edge: key * key -> 'a T -> 'a T
    38   val del_edge: key * key -> 'a T -> 'a T
    39   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
    40   val join: (key -> 'a * 'a -> 'a option) -> 'a T * 'a T -> 'a T      (*exception DUPS*)
    41   exception CYCLES of key list list
    42   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    43   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    44   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    45   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    46   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    47 end;
    48 
    49 functor GraphFun(Key: KEY): GRAPH =
    50 struct
    51 
    52 (* keys *)
    53 
    54 type key = Key.key;
    55 
    56 val eq_key = equal EQUAL o Key.ord;
    57 
    58 val member_key = member eq_key;
    59 val remove_key = remove eq_key;
    60 
    61 
    62 (* tables and sets of keys *)
    63 
    64 structure Table = TableFun(Key);
    65 type keys = unit Table.table;
    66 
    67 val empty_keys = Table.empty: keys;
    68 
    69 fun member_keys tab = Table.defined (tab: keys);
    70 fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    71 
    72 
    73 (* graphs *)
    74 
    75 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    76 
    77 exception UNDEF of key;
    78 exception DUP = Table.DUP;
    79 exception DUPS = Table.DUPS;
    80 
    81 val empty = Graph Table.empty;
    82 fun keys (Graph tab) = Table.keys tab;
    83 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
    84 
    85 fun minimals (Graph tab) = Table.fold (fn (m, (_, ([], _))) => cons m | _ => I) tab [];
    86 fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab [];
    87 
    88 fun get_entry (Graph tab) x =
    89   (case Table.lookup tab x of
    90     SOME entry => entry
    91   | NONE => raise UNDEF x);
    92 
    93 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
    94 fun map_entry_yield x f (G as Graph tab) =
    95   let val (a, node') = f (get_entry G x)
    96   in (a, Graph (Table.update (x, node') tab)) end;
    97 
    98 
    99 (* nodes *)
   100 
   101 fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
   102 
   103 fun fold_nodes f (Graph tab) s =
   104   Table.fold (fn (k, (i, ps)) => f (k, i)) tab s
   105 
   106 fun fold_map_nodes f (Graph tab) s =
   107   s
   108   |> Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab
   109   |> apfst Graph;
   110 
   111 fun get_node G = #1 o get_entry G;
   112 
   113 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
   114 fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
   115   let val (a, i') = f i in (a, (i', ps)) end);
   116 
   117 
   118 (* reachability *)
   119 
   120 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   121 fun reachable next xs =
   122   let
   123     fun reach x (rs, R) =
   124       if member_keys R x then (rs, R)
   125       else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
   126   in fold_map (fn x => reach x o pair []) xs empty_keys end;
   127 
   128 (*immediate*)
   129 fun imm_preds G = #1 o #2 o get_entry G;
   130 fun imm_succs G = #2 o #2 o get_entry G;
   131 
   132 (*transitive*)
   133 fun all_preds G = List.concat o fst o reachable (imm_preds G);
   134 fun all_succs G = List.concat o fst o reachable (imm_succs G);
   135 
   136 (*strongly connected components; see: David King and John Launchbury,
   137   "Structuring Depth First Search Algorithms in Haskell"*)
   138 fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
   139   (List.concat (rev (fst (reachable (imm_succs G) (keys G)))))));
   140 
   141 (*subgraph induced by node subset*)
   142 fun subgraph keys (Graph tab) =
   143   let
   144     val select = member eq_key keys;
   145     fun subg (k, (i, (preds, succs))) tab' =
   146       if select k
   147       then tab' |> Table.update (k, (i, (filter select preds, filter select succs)))
   148       else tab'
   149   in Table.empty |> Table.fold subg tab |> Graph end;
   150 
   151 
   152 (* paths *)
   153 
   154 fun find_paths G (x, y) =
   155   let
   156     val (_, X) = reachable (imm_succs G) [x];
   157     fun paths ps p =
   158       if not (null ps) andalso eq_key (p, x) then [p :: ps]
   159       else if member_keys X p andalso not (member_key ps p)
   160       then List.concat (map (paths (p :: ps)) (imm_preds G p))
   161       else [];
   162   in paths [] y end;
   163 
   164 
   165 (* nodes *)
   166 
   167 fun new_node (x, info) (Graph tab) =
   168   Graph (Table.update_new (x, (info, ([], []))) tab);
   169 
   170 fun default_node (x, info) (Graph tab) =
   171   Graph (Table.default (x, (info, ([], []))) tab);
   172 
   173 fun del_nodes xs (Graph tab) =
   174   Graph (tab
   175     |> fold Table.delete xs
   176     |> Table.map (fn (i, (preds, succs)) =>
   177       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   178 
   179 
   180 (* edges *)
   181 
   182 fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   183 
   184 fun add_edge (x, y) G =
   185   if is_edge G (x, y) then G
   186   else
   187     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   188       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
   189 
   190 fun del_edge (x, y) G =
   191   if is_edge G (x, y) then
   192     G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
   193       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   194   else G;
   195 
   196 fun diff_edges G1 G2 =
   197   List.concat (dest G1 |> map (fn (x, ys) => ys |> List.mapPartial (fn y =>
   198     if is_edge G2 (x, y) then NONE else SOME (x, y))));
   199 
   200 fun edges G = diff_edges G empty;
   201 
   202 
   203 (* join and merge *)
   204 
   205 fun no_edges (i, _) = (i, ([], []));
   206 
   207 fun join f (Graph tab1, G2 as Graph tab2) =
   208   let
   209     fun join_node key ((i1, edges1), (i2, _)) =
   210       (Option.map (rpair edges1) o f key) (i1, i2);
   211   in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
   212 
   213 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   214   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
   215   in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
   216 
   217 fun merge eq GG = gen_merge add_edge eq GG;
   218 
   219 
   220 (* maintain acyclic graphs *)
   221 
   222 exception CYCLES of key list list;
   223 
   224 fun add_edge_acyclic (x, y) G =
   225   if is_edge G (x, y) then G
   226   else
   227     (case find_paths G (y, x) of
   228       [] => add_edge (x, y) G
   229     | cycles => raise CYCLES (map (cons x) cycles));
   230 
   231 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   232 
   233 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   234 
   235 
   236 (* maintain transitive acyclic graphs *)
   237 
   238 fun add_edge_trans_acyclic (x, y) G =
   239   add_edge_acyclic (x, y) G |>
   240   fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
   241 
   242 fun merge_trans_acyclic eq (G1, G2) =
   243   merge_acyclic eq (G1, G2) |>
   244   fold add_edge_trans_acyclic (diff_edges G1 G2 @ diff_edges G2 G1);
   245 
   246 end;
   247 
   248 
   249 (*graphs indexed by strings*)
   250 structure Graph = GraphFun(type key = string val ord = fast_string_ord);