src/Pure/General/graph.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23655 d2d1138e0ddc
child 23964 d2df2797519b
permissions -rw-r--r--
tuned signature;
     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 DUP of key
    13   exception SAME
    14   exception UNDEF of key
    15   val empty: 'a T
    16   val keys: 'a T -> key list
    17   val dest: 'a T -> (key * key list) list
    18   val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    19   val minimals: 'a T -> key list
    20   val maximals: 'a T -> key list
    21   val subgraph: (key -> bool) -> 'a T -> 'a T
    22   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
    23   val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b
    24   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    25   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    26   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    27   val imm_preds: 'a T -> key -> key list
    28   val imm_succs: 'a T -> key -> key list
    29   val all_preds: 'a T -> key list -> key list
    30   val all_succs: 'a T -> key list -> key list
    31   val strong_conn: 'a T -> key list list
    32   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    33   val default_node: key * 'a -> 'a T -> 'a T
    34   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    35   val is_edge: 'a T -> key * key -> bool
    36   val add_edge: key * key -> 'a T -> 'a T
    37   val del_edge: key * key -> 'a T -> 'a T
    38   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    39   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    40     'a T * 'a T -> 'a T                                               (*exception DUP*)
    41   val irreducible_paths: 'a T -> key * key -> key list list
    42   val all_paths: 'a T -> key * key -> key list list
    43   exception CYCLES of key list list
    44   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    45   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    46   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    47   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    48   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    49 end;
    50 
    51 functor GraphFun(Key: KEY): GRAPH =
    52 struct
    53 
    54 (* keys *)
    55 
    56 type key = Key.key;
    57 
    58 val eq_key = is_equal o Key.ord;
    59 
    60 val member_key = member eq_key;
    61 val remove_key = remove eq_key;
    62 
    63 
    64 (* tables and sets of keys *)
    65 
    66 structure Table = TableFun(Key);
    67 type keys = unit Table.table;
    68 
    69 val empty_keys = Table.empty: keys;
    70 
    71 fun member_keys tab = Table.defined (tab: keys);
    72 fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    73 
    74 
    75 (* graphs *)
    76 
    77 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    78 
    79 exception DUP = Table.DUP;
    80 exception UNDEF = Table.UNDEF;
    81 exception SAME = Table.SAME;
    82 
    83 val empty = Graph Table.empty;
    84 fun keys (Graph tab) = Table.keys tab;
    85 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
    86 
    87 fun fold_graph f (Graph tab) = Table.fold f tab;
    88 
    89 fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
    90 fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
    91 
    92 fun subgraph P G =
    93   let
    94     fun subg (k, (i, (preds, succs))) =
    95       if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
    96   in Graph (fold_graph subg G Table.empty) end;
    97 
    98 fun get_entry (Graph tab) x =
    99   (case Table.lookup tab x of
   100     SOME entry => entry
   101   | NONE => raise UNDEF x);
   102 
   103 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
   104 
   105 fun map_entry_yield x f (G as Graph tab) =
   106   let val (a, node') = f (get_entry G x)
   107   in (a, Graph (Table.update (x, node') tab)) end;
   108 
   109 
   110 (* nodes *)
   111 
   112 fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
   113 
   114 fun fold_map_nodes f (Graph tab) =
   115   apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab;
   116 
   117 fun get_node G = #1 o get_entry G;
   118 
   119 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
   120 
   121 fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
   122   let val (a, i') = f i in (a, (i', ps)) end);
   123 
   124 
   125 (* reachability *)
   126 
   127 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   128 fun reachable next xs =
   129   let
   130     fun reach x (rs, R) =
   131       if member_keys R x then (rs, R)
   132       else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
   133   in fold_map (fn x => reach x o pair []) xs empty_keys end;
   134 
   135 (*immediate*)
   136 fun imm_preds G = #1 o #2 o get_entry G;
   137 fun imm_succs G = #2 o #2 o get_entry G;
   138 
   139 (*transitive*)
   140 fun all_preds G = flat o fst o reachable (imm_preds G);
   141 fun all_succs G = flat o fst o reachable (imm_succs G);
   142 
   143 (*strongly connected components; see: David King and John Launchbury,
   144   "Structuring Depth First Search Algorithms in Haskell"*)
   145 fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
   146   (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
   147 
   148 
   149 (* nodes *)
   150 
   151 fun new_node (x, info) (Graph tab) =
   152   Graph (Table.update_new (x, (info, ([], []))) tab);
   153 
   154 fun default_node (x, info) (Graph tab) =
   155   Graph (Table.default (x, (info, ([], []))) tab);
   156 
   157 fun del_nodes xs (Graph tab) =
   158   Graph (tab
   159     |> fold Table.delete xs
   160     |> Table.map (fn (i, (preds, succs)) =>
   161       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   162 
   163 
   164 (* edges *)
   165 
   166 fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   167 
   168 fun add_edge (x, y) G =
   169   if is_edge G (x, y) then G
   170   else
   171     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   172       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
   173 
   174 fun del_edge (x, y) G =
   175   if is_edge G (x, y) then
   176     G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
   177       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   178   else G;
   179 
   180 fun diff_edges G1 G2 =
   181   flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
   182     if is_edge G2 (x, y) then NONE else SOME (x, y))));
   183 
   184 fun edges G = diff_edges G empty;
   185 
   186 
   187 (* join and merge *)
   188 
   189 fun no_edges (i, _) = (i, ([], []));
   190 
   191 fun join f (Graph tab1, G2 as Graph tab2) =
   192   let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
   193   in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
   194 
   195 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   196   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
   197   in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
   198 
   199 fun merge eq GG = gen_merge add_edge eq GG;
   200 
   201 
   202 (* irreducible paths -- Hasse diagram *)
   203 
   204 fun irreducible_preds G X path z =
   205   let
   206     fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   207     fun irreds [] xs' = xs'
   208       | irreds (x :: xs) xs' =
   209           if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
   210             exists (red x) xs orelse exists (red x) xs'
   211           then irreds xs xs'
   212           else irreds xs (x :: xs');
   213   in irreds (imm_preds G z) [] end;
   214 
   215 fun irreducible_paths G (x, y) =
   216   let
   217     val (_, X) = reachable (imm_succs G) [x];
   218     fun paths path z =
   219       if eq_key (x, z) then cons (z :: path)
   220       else fold (paths (z :: path)) (irreducible_preds G X path z);
   221   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
   222 
   223 
   224 (* all paths *)
   225 
   226 fun all_paths G (x, y) =
   227   let
   228     val (_, X) = reachable (imm_succs G) [x];
   229     fun paths path z =
   230       if not (null path) andalso eq_key (x, z) then [z :: path]
   231       else if member_keys X z andalso not (member_key path z)
   232       then maps (paths (z :: path)) (imm_preds G z)
   233       else [];
   234   in paths [] y end;
   235 
   236 
   237 (* maintain acyclic graphs *)
   238 
   239 exception CYCLES of key list list;
   240 
   241 fun add_edge_acyclic (x, y) G =
   242   if is_edge G (x, y) then G
   243   else
   244     (case irreducible_paths G (y, x) of
   245       [] => add_edge (x, y) G
   246     | cycles => raise CYCLES (map (cons x) cycles));
   247 
   248 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   249 
   250 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   251 
   252 
   253 (* maintain transitive acyclic graphs *)
   254 
   255 fun add_edge_trans_acyclic (x, y) G =
   256   add_edge_acyclic (x, y) G
   257   |> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
   258 
   259 fun merge_trans_acyclic eq (G1, G2) =
   260   merge_acyclic eq (G1, G2)
   261   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   262   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
   263 
   264 
   265 (*final declarations of this structure!*)
   266 val fold = fold_graph;
   267 
   268 end;
   269 
   270 structure Graph = GraphFun(type key = string val ord = fast_string_ord);
   271 structure IntGraph = GraphFun(type key = int val ord = int_ord);