src/Pure/General/graph.ML
author wenzelm
Thu Jul 09 22:01:41 2009 +0200 (2009-07-09)
changeset 31971 8c1b845ed105
parent 31616 63893e3a50a6
child 32709 c5956b54a460
permissions -rw-r--r--
renamed functor TableFun to Table, and GraphFun to Graph;
     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 apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
   136   in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end;
   137 
   138 (*immediate*)
   139 fun imm_preds G = #1 o #2 o get_entry G;
   140 fun imm_succs G = #2 o #2 o get_entry G;
   141 
   142 (*transitive*)
   143 fun all_preds G = flat o fst o reachable (imm_preds G);
   144 fun all_succs G = flat o fst o reachable (imm_succs G);
   145 
   146 (*strongly connected components; see: David King and John Launchbury,
   147   "Structuring Depth First Search Algorithms in Haskell"*)
   148 fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
   149   (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
   150 
   151 
   152 (* nodes *)
   153 
   154 fun new_node (x, info) (Graph tab) =
   155   Graph (Table.update_new (x, (info, ([], []))) tab);
   156 
   157 fun default_node (x, info) (Graph tab) =
   158   Graph (Table.default (x, (info, ([], []))) tab);
   159 
   160 fun del_nodes xs (Graph tab) =
   161   Graph (tab
   162     |> fold Table.delete xs
   163     |> Table.map (fn (i, (preds, succs)) =>
   164       (i, (fold remove_key xs preds, fold remove_key xs succs))));
   165 
   166 fun del_node x (G as Graph tab) =
   167   let
   168     fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
   169     val (preds, succs) = #2 (get_entry G x);
   170   in
   171     Graph (tab
   172       |> Table.delete x
   173       |> fold (del_adjacent apsnd) preds
   174       |> fold (del_adjacent apfst) succs)
   175   end;
   176 
   177 
   178 (* edges *)
   179 
   180 fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   181 
   182 fun add_edge (x, y) G =
   183   if is_edge G (x, y) then G
   184   else
   185     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   186       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
   187 
   188 fun del_edge (x, y) G =
   189   if is_edge G (x, y) then
   190     G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
   191       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   192   else G;
   193 
   194 fun diff_edges G1 G2 =
   195   flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
   196     if is_edge G2 (x, y) then NONE else SOME (x, y))));
   197 
   198 fun edges G = diff_edges G empty;
   199 
   200 
   201 (* join and merge *)
   202 
   203 fun no_edges (i, _) = (i, ([], []));
   204 
   205 fun join f (Graph tab1, G2 as Graph tab2) =
   206   let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
   207   in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
   208 
   209 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   210   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
   211   in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
   212 
   213 fun merge eq GG = gen_merge add_edge eq GG;
   214 
   215 
   216 (* irreducible paths -- Hasse diagram *)
   217 
   218 fun irreducible_preds G X path z =
   219   let
   220     fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   221     fun irreds [] xs' = xs'
   222       | irreds (x :: xs) xs' =
   223           if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
   224             exists (red x) xs orelse exists (red x) xs'
   225           then irreds xs xs'
   226           else irreds xs (x :: xs');
   227   in irreds (imm_preds G z) [] end;
   228 
   229 fun irreducible_paths G (x, y) =
   230   let
   231     val (_, X) = reachable (imm_succs G) [x];
   232     fun paths path z =
   233       if eq_key (x, z) then cons (z :: path)
   234       else fold (paths (z :: path)) (irreducible_preds G X path z);
   235   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
   236 
   237 
   238 (* all paths *)
   239 
   240 fun all_paths G (x, y) =
   241   let
   242     val (_, X) = reachable (imm_succs G) [x];
   243     fun paths path z =
   244       if not (null path) andalso eq_key (x, z) then [z :: path]
   245       else if member_keys X z andalso not (member_key path z)
   246       then maps (paths (z :: path)) (imm_preds G z)
   247       else [];
   248   in paths [] y end;
   249 
   250 
   251 (* maintain acyclic graphs *)
   252 
   253 exception CYCLES of key list list;
   254 
   255 fun add_edge_acyclic (x, y) G =
   256   if is_edge G (x, y) then G
   257   else
   258     (case irreducible_paths G (y, x) of
   259       [] => add_edge (x, y) G
   260     | cycles => raise CYCLES (map (cons x) cycles));
   261 
   262 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   263 
   264 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   265 
   266 fun topological_order G = minimals G |> all_succs G;
   267 
   268 
   269 (* maintain transitive acyclic graphs *)
   270 
   271 fun add_edge_trans_acyclic (x, y) G =
   272   add_edge_acyclic (x, y) G
   273   |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
   274 
   275 fun merge_trans_acyclic eq (G1, G2) =
   276   merge_acyclic eq (G1, G2)
   277   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   278   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
   279 
   280 
   281 (* constructing graphs *)
   282 
   283 fun extend explore =
   284   let
   285     fun ext x G =
   286       if can (get_entry G) x then G
   287       else
   288         let val (info, ys) = explore x in
   289           G
   290           |> new_node (x, info)
   291           |> fold ext ys
   292           |> fold (fn y => add_edge (x, y)) ys
   293         end
   294   in ext end;
   295 
   296 
   297 (*final declarations of this structure!*)
   298 val fold = fold_graph;
   299 
   300 end;
   301 
   302 structure Graph = Graph(type key = string val ord = fast_string_ord);
   303 structure IntGraph = Graph(type key = int val ord = int_ord);