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