src/Pure/General/graph.ML
author wenzelm
Sun Sep 27 21:06:43 2009 +0200 (2009-09-27)
changeset 32710 fa46afc8c05f
parent 32709 c5956b54a460
child 35012 c3e3ac3ca091
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/General/graph.ML
     2     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3 
     4 Directed graphs.
     5 *)
     6 
     7 signature GRAPH =
     8 sig
     9   type key
    10   type 'a T
    11   exception DUP of key
    12   exception SAME
    13   exception UNDEF of key
    14   val empty: 'a T
    15   val is_empty: 'a T -> bool
    16   val keys: 'a T -> key list
    17   val dest: 'a T -> (key * key list) list
    18   val get_first: key option -> (key * ('a * (key list * key list)) -> 'b option) ->
    19     'a T -> 'b option
    20   val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    21   val minimals: 'a T -> key list
    22   val maximals: 'a T -> key list
    23   val subgraph: (key -> bool) -> 'a T -> 'a T
    24   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
    25   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    26   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    27   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    28   val imm_preds: 'a T -> key -> key list
    29   val imm_succs: 'a T -> key -> key list
    30   val all_preds: 'a T -> key list -> key list
    31   val all_succs: 'a T -> key list -> key list
    32   val strong_conn: 'a T -> 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 del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    37   val is_edge: 'a T -> key * key -> bool
    38   val add_edge: key * key -> 'a T -> 'a T
    39   val del_edge: key * key -> 'a T -> 'a T
    40   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    41   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    42     'a T * 'a T -> 'a T                                               (*exception DUP*)
    43   val irreducible_paths: 'a T -> key * key -> key list list
    44   val all_paths: 'a T -> key * key -> key list list
    45   exception CYCLES of key list list
    46   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    47   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    48   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    49   val topological_order: 'a T -> key list
    50   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    51   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    52   val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
    53 end;
    54 
    55 functor Graph(Key: KEY): GRAPH =
    56 struct
    57 
    58 (* keys *)
    59 
    60 type key = Key.key;
    61 
    62 val eq_key = is_equal o Key.ord;
    63 
    64 val member_key = member eq_key;
    65 val remove_key = remove eq_key;
    66 
    67 
    68 (* tables and sets of keys *)
    69 
    70 structure Table = Table(Key);
    71 type keys = unit Table.table;
    72 
    73 val empty_keys = Table.empty: keys;
    74 
    75 fun member_keys tab = Table.defined (tab: keys);
    76 fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    77 
    78 
    79 (* graphs *)
    80 
    81 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    82 
    83 exception DUP = Table.DUP;
    84 exception UNDEF = Table.UNDEF;
    85 exception SAME = Table.SAME;
    86 
    87 val empty = Graph Table.empty;
    88 fun is_empty (Graph tab) = Table.is_empty tab;
    89 fun keys (Graph tab) = Table.keys tab;
    90 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
    91 
    92 fun get_first b f (Graph tab) = Table.get_first b f tab;
    93 fun fold_graph f (Graph tab) = Table.fold f tab;
    94 
    95 fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
    96 fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
    97 
    98 fun subgraph P G =
    99   let
   100     fun subg (k, (i, (preds, succs))) =
   101       if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
   102   in Graph (fold_graph subg G Table.empty) end;
   103 
   104 fun get_entry (Graph tab) x =
   105   (case Table.lookup tab x of
   106     SOME entry => entry
   107   | NONE => raise UNDEF x);
   108 
   109 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
   110 
   111 fun map_entry_yield x f (G as Graph tab) =
   112   let val (a, node') = f (get_entry G x)
   113   in (a, Graph (Table.update (x, node') tab)) end;
   114 
   115 
   116 (* nodes *)
   117 
   118 fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
   119 
   120 fun get_node G = #1 o get_entry G;
   121 
   122 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
   123 
   124 fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
   125   let val (a, i') = f i in (a, (i', ps)) end);
   126 
   127 
   128 (* reachability *)
   129 
   130 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   131 fun reachable next xs =
   132   let
   133     fun reach x (rs, R) =
   134       if member_keys R x then (rs, R)
   135       else fold reach (next x) (rs, insert_keys x R) |>> cons x;
   136     fun reachs x (rss, R) =
   137       reach x ([], R) |>> (fn rs => rs :: rss);
   138   in fold reachs xs ([], empty_keys) end;
   139 
   140 (*immediate*)
   141 fun imm_preds G = #1 o #2 o get_entry G;
   142 fun imm_succs G = #2 o #2 o get_entry G;
   143 
   144 (*transitive*)
   145 fun all_preds G = flat o #1 o reachable (imm_preds G);
   146 fun all_succs G = flat o #1 o reachable (imm_succs G);
   147 
   148 (*strongly connected components; see: David King and John Launchbury,
   149   "Structuring Depth First Search Algorithms in Haskell"*)
   150 fun strong_conn G =
   151   rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
   152 
   153 
   154 (* nodes *)
   155 
   156 fun new_node (x, info) (Graph tab) =
   157   Graph (Table.update_new (x, (info, ([], []))) tab);
   158 
   159 fun default_node (x, info) (Graph tab) =
   160   Graph (Table.default (x, (info, ([], []))) tab);
   161 
   162 fun del_nodes xs (Graph tab) =
   163   Graph (tab
   164     |> fold Table.delete xs
   165     |> Table.map (fn (i, (preds, succs)) =>
   166       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   167 
   168 fun del_node x (G as Graph tab) =
   169   let
   170     fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
   171     val (preds, succs) = #2 (get_entry G x);
   172   in
   173     Graph (tab
   174       |> Table.delete x
   175       |> fold (del_adjacent apsnd) preds
   176       |> fold (del_adjacent apfst) succs)
   177   end;
   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   flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (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 fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
   209   in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
   210 
   211 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   212   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
   213   in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
   214 
   215 fun merge eq GG = gen_merge add_edge eq GG;
   216 
   217 
   218 (* irreducible paths -- Hasse diagram *)
   219 
   220 fun irreducible_preds G X path z =
   221   let
   222     fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   223     fun irreds [] xs' = xs'
   224       | irreds (x :: xs) xs' =
   225           if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
   226             exists (red x) xs orelse exists (red x) xs'
   227           then irreds xs xs'
   228           else irreds xs (x :: xs');
   229   in irreds (imm_preds G z) [] end;
   230 
   231 fun irreducible_paths G (x, y) =
   232   let
   233     val (_, X) = reachable (imm_succs G) [x];
   234     fun paths path z =
   235       if eq_key (x, z) then cons (z :: path)
   236       else fold (paths (z :: path)) (irreducible_preds G X path z);
   237   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
   238 
   239 
   240 (* all paths *)
   241 
   242 fun all_paths G (x, y) =
   243   let
   244     val (_, X) = reachable (imm_succs G) [x];
   245     fun paths path z =
   246       if not (null path) andalso eq_key (x, z) then [z :: path]
   247       else if member_keys X z andalso not (member_key path z)
   248       then maps (paths (z :: path)) (imm_preds G z)
   249       else [];
   250   in paths [] y end;
   251 
   252 
   253 (* maintain acyclic graphs *)
   254 
   255 exception CYCLES of key list list;
   256 
   257 fun add_edge_acyclic (x, y) G =
   258   if is_edge G (x, y) then G
   259   else
   260     (case irreducible_paths G (y, x) of
   261       [] => add_edge (x, y) G
   262     | cycles => raise CYCLES (map (cons x) cycles));
   263 
   264 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   265 
   266 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   267 
   268 fun topological_order G = minimals G |> all_succs G;
   269 
   270 
   271 (* maintain transitive acyclic graphs *)
   272 
   273 fun add_edge_trans_acyclic (x, y) G =
   274   add_edge_acyclic (x, y) G
   275   |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
   276 
   277 fun merge_trans_acyclic eq (G1, G2) =
   278   merge_acyclic eq (G1, G2)
   279   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   280   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
   281 
   282 
   283 (* constructing graphs *)
   284 
   285 fun extend explore =
   286   let
   287     fun ext x G =
   288       if can (get_entry G) x then G
   289       else
   290         let val (info, ys) = explore x in
   291           G
   292           |> new_node (x, info)
   293           |> fold ext ys
   294           |> fold (fn y => add_edge (x, y)) ys
   295         end
   296   in ext end;
   297 
   298 
   299 (*final declarations of this structure!*)
   300 val fold = fold_graph;
   301 
   302 end;
   303 
   304 structure Graph = Graph(type key = string val ord = fast_string_ord);
   305 structure IntGraph = Graph(type key = int val ord = int_ord);