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