src/Pure/General/graph.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 44338 700008399ee5
child 46611 669601fa1a62
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     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   structure Keys:
    11   sig
    12     type T
    13     val is_empty: T -> bool
    14     val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
    15     val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
    16     val dest: T -> key list
    17   end
    18   type 'a T
    19   exception DUP of key
    20   exception SAME
    21   exception UNDEF of key
    22   val empty: 'a T
    23   val is_empty: 'a T -> bool
    24   val keys: 'a T -> key list
    25   val dest: 'a T -> (key * key list) list
    26   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
    27   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    28   val subgraph: (key -> bool) -> 'a T -> 'a T
    29   val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
    30   val map: (key -> 'a -> 'b) -> 'a T -> 'b T
    31   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    32   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    33   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    34   val imm_preds: 'a T -> key -> Keys.T
    35   val imm_succs: 'a T -> key -> Keys.T
    36   val immediate_preds: 'a T -> key -> key list
    37   val immediate_succs: 'a T -> key -> key list
    38   val all_preds: 'a T -> key list -> key list
    39   val all_succs: 'a T -> key list -> key list
    40   val minimals: 'a T -> key list
    41   val maximals: 'a T -> key list
    42   val is_minimal: 'a T -> key -> bool
    43   val is_maximal: 'a T -> key -> bool
    44   val strong_conn: 'a T -> key list list
    45   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    46   val default_node: key * 'a -> 'a T -> 'a T
    47   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    48   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    49   val is_edge: 'a T -> key * key -> bool
    50   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    51   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    52   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    53   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    54     'a T * 'a T -> 'a T                                               (*exception DUP*)
    55   val irreducible_paths: 'a T -> key * key -> key list list
    56   val all_paths: 'a T -> key * key -> key list list
    57   exception CYCLES of key list list
    58   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
    59   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
    60   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    61   val topological_order: 'a T -> key list
    62   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
    63   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    64   exception DEP of key * key
    65   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
    66 end;
    67 
    68 functor Graph(Key: KEY): GRAPH =
    69 struct
    70 
    71 (* keys *)
    72 
    73 type key = Key.key;
    74 val eq_key = is_equal o Key.ord;
    75 
    76 structure Table = Table(Key);
    77 
    78 structure Keys =
    79 struct
    80 
    81 abstype T = Keys of unit Table.table
    82 with
    83 
    84 val empty = Keys Table.empty;
    85 fun is_empty (Keys tab) = Table.is_empty tab;
    86 
    87 fun member (Keys tab) = Table.defined tab;
    88 fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
    89 fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
    90 
    91 fun fold f (Keys tab) = Table.fold (f o #1) tab;
    92 fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
    93 
    94 fun make xs = Basics.fold insert xs empty;
    95 fun dest keys = fold_rev cons keys [];
    96 
    97 fun filter P keys = fold (fn x => P x ? insert x) keys empty;
    98 
    99 end;
   100 end;
   101 
   102 
   103 (* graphs *)
   104 
   105 datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
   106 
   107 exception DUP = Table.DUP;
   108 exception UNDEF = Table.UNDEF;
   109 exception SAME = Table.SAME;
   110 
   111 val empty = Graph Table.empty;
   112 fun is_empty (Graph tab) = Table.is_empty tab;
   113 fun keys (Graph tab) = Table.keys tab;
   114 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
   115 
   116 fun get_first f (Graph tab) = Table.get_first f tab;
   117 fun fold_graph f (Graph tab) = Table.fold f tab;
   118 
   119 fun subgraph P G =
   120   let
   121     fun subg (k, (i, (preds, succs))) =
   122       if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
   123       else I;
   124   in Graph (fold_graph subg G Table.empty) end;
   125 
   126 fun get_entry (Graph tab) x =
   127   (case Table.lookup_key tab x of
   128     SOME entry => entry
   129   | NONE => raise UNDEF x);
   130 
   131 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
   132 
   133 fun map_entry_yield x f (G as Graph tab) =
   134   let val (a, node') = f (#2 (get_entry G x))
   135   in (a, Graph (Table.update (x, node') tab)) end;
   136 
   137 
   138 (* nodes *)
   139 
   140 fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
   141 
   142 fun get_node G = #1 o #2 o get_entry G;
   143 
   144 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
   145 
   146 fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
   147   let val (a, i') = f i in (a, (i', ps)) end);
   148 
   149 
   150 (* reachability *)
   151 
   152 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   153 fun reachable next xs =
   154   let
   155     fun reach x (rs, R) =
   156       if Keys.member R x then (rs, R)
   157       else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
   158     fun reachs x (rss, R) =
   159       reach x ([], R) |>> (fn rs => rs :: rss);
   160   in fold reachs xs ([], Keys.empty) end;
   161 
   162 (*immediate*)
   163 fun imm_preds G = #1 o #2 o #2 o get_entry G;
   164 fun imm_succs G = #2 o #2 o #2 o get_entry G;
   165 
   166 fun immediate_preds G = Keys.dest o imm_preds G;
   167 fun immediate_succs G = Keys.dest o imm_succs G;
   168 
   169 (*transitive*)
   170 fun all_preds G = flat o #1 o reachable (imm_preds G);
   171 fun all_succs G = flat o #1 o reachable (imm_succs G);
   172 
   173 (*minimal and maximal elements*)
   174 fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
   175 fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
   176 fun is_minimal G x = Keys.is_empty (imm_preds G x);
   177 fun is_maximal G x = Keys.is_empty (imm_succs G x);
   178 
   179 (*strongly connected components; see: David King and John Launchbury,
   180   "Structuring Depth First Search Algorithms in Haskell"*)
   181 fun strong_conn G =
   182   rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
   183 
   184 
   185 (* nodes *)
   186 
   187 fun new_node (x, info) (Graph tab) =
   188   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
   189 
   190 fun default_node (x, info) (Graph tab) =
   191   Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
   192 
   193 fun del_nodes xs (Graph tab) =
   194   Graph (tab
   195     |> fold Table.delete xs
   196     |> Table.map (fn _ => fn (i, (preds, succs)) =>
   197       (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
   198 
   199 fun del_node x (G as Graph tab) =
   200   let
   201     fun del_adjacent which y =
   202       Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
   203     val (preds, succs) = #2 (#2 (get_entry G x));
   204   in
   205     Graph (tab
   206       |> Table.delete x
   207       |> Keys.fold (del_adjacent apsnd) preds
   208       |> Keys.fold (del_adjacent apfst) succs)
   209   end;
   210 
   211 
   212 (* edges *)
   213 
   214 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
   215 
   216 fun add_edge (x, y) G =
   217   if is_edge G (x, y) then G
   218   else
   219     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
   220       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
   221 
   222 fun del_edge (x, y) G =
   223   if is_edge G (x, y) then
   224     G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
   225       |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   226   else G;
   227 
   228 fun diff_edges G1 G2 =
   229   flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
   230     if is_edge G2 (x, y) then NONE else SOME (x, y))));
   231 
   232 fun edges G = diff_edges G empty;
   233 
   234 
   235 (* join and merge *)
   236 
   237 fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
   238 
   239 fun join f (G1 as Graph tab1, G2 as Graph tab2) =
   240   let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
   241     if pointer_eq (G1, G2) then G1
   242     else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
   243   end;
   244 
   245 fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
   246   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
   247     if pointer_eq (G1, G2) then G1
   248     else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
   249   end;
   250 
   251 fun merge eq GG = gen_merge add_edge eq GG;
   252 
   253 
   254 (* irreducible paths -- Hasse diagram *)
   255 
   256 fun irreducible_preds G X path z =
   257   let
   258     fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   259     fun irreds [] xs' = xs'
   260       | irreds (x :: xs) xs' =
   261           if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
   262             exists (red x) xs orelse exists (red x) xs'
   263           then irreds xs xs'
   264           else irreds xs (x :: xs');
   265   in irreds (immediate_preds G z) [] end;
   266 
   267 fun irreducible_paths G (x, y) =
   268   let
   269     val (_, X) = reachable (imm_succs G) [x];
   270     fun paths path z =
   271       if eq_key (x, z) then cons (z :: path)
   272       else fold (paths (z :: path)) (irreducible_preds G X path z);
   273   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
   274 
   275 
   276 (* all paths *)
   277 
   278 fun all_paths G (x, y) =
   279   let
   280     val (_, X) = reachable (imm_succs G) [x];
   281     fun paths path z =
   282       if not (null path) andalso eq_key (x, z) then [z :: path]
   283       else if Keys.member X z andalso not (member eq_key path z)
   284       then maps (paths (z :: path)) (immediate_preds G z)
   285       else [];
   286   in paths [] y end;
   287 
   288 
   289 (* maintain acyclic graphs *)
   290 
   291 exception CYCLES of key list list;
   292 
   293 fun add_edge_acyclic (x, y) G =
   294   if is_edge G (x, y) then G
   295   else
   296     (case irreducible_paths G (y, x) of
   297       [] => add_edge (x, y) G
   298     | cycles => raise CYCLES (map (cons x) cycles));
   299 
   300 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   301 
   302 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   303 
   304 fun topological_order G = minimals G |> all_succs G;
   305 
   306 
   307 (* maintain transitive acyclic graphs *)
   308 
   309 fun add_edge_trans_acyclic (x, y) G =
   310   add_edge_acyclic (x, y) G
   311   |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
   312 
   313 fun merge_trans_acyclic eq (G1, G2) =
   314   if pointer_eq (G1, G2) then G1
   315   else
   316     merge_acyclic eq (G1, G2)
   317     |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   318     |> fold add_edge_trans_acyclic (diff_edges G2 G1);
   319 
   320 
   321 (* schedule acyclic graph *)
   322 
   323 exception DEP of key * key;
   324 
   325 fun schedule f G =
   326   let
   327     val xs = topological_order G;
   328     val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
   329       let
   330         val a = get_node G x;
   331         val deps = immediate_preds G x |> map (fn y =>
   332           (case Table.lookup tab y of
   333             SOME b => (y, b)
   334           | NONE => raise DEP (x, y)));
   335       in Table.update (x, f deps (x, a)) tab end);
   336   in map (the o Table.lookup results) xs end;
   337 
   338 
   339 (*final declarations of this structure!*)
   340 val map = map_nodes;
   341 val fold = fold_graph;
   342 
   343 end;
   344 
   345 structure Graph = Graph(type key = string val ord = fast_string_ord);
   346 structure Int_Graph = Graph(type key = int val ord = int_ord);