src/Pure/General/graph.ML
author wenzelm
Fri, 21 May 2004 21:28:01 +0200
changeset 14793 32d94d1e4842
parent 14161 73ad4884441f
child 14981 e73f8140af78
permissions -rw-r--r--
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/graph.ML
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
8806
wenzelm
parents: 6659
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     5
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     6
Directed graphs.
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     7
*)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     8
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
     9
signature GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    10
sig
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    11
  type key
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    12
  type 'a T
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    13
  exception UNDEF of key
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    14
  exception DUP of key
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    15
  exception DUPS of key list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    16
  val empty: 'a T
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    17
  val keys: 'a T -> key list
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    18
  val dest: 'a T -> (key * key list) list
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    19
  val minimals: 'a T -> key list
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    20
  val maximals: 'a T -> key list
6142
wenzelm
parents: 6134
diff changeset
    21
  val map_nodes: ('a -> 'b) -> 'a T -> 'b T
wenzelm
parents: 6134
diff changeset
    22
  val get_node: 'a T -> key -> 'a
wenzelm
parents: 6134
diff changeset
    23
  val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
wenzelm
parents: 6134
diff changeset
    24
  val imm_preds: 'a T -> key -> key list
wenzelm
parents: 6134
diff changeset
    25
  val imm_succs: 'a T -> key -> key list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    26
  val all_preds: 'a T -> key list -> key list
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    27
  val all_succs: 'a T -> key list -> key list
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
    28
  val strong_conn: 'a T -> key list list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    29
  val find_paths: 'a T -> key * key -> key list list
6152
wenzelm
parents: 6142
diff changeset
    30
  val new_node: key * 'a -> 'a T -> 'a T
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    31
  val del_nodes: key list -> 'a T -> 'a T
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    32
  val is_edge: 'a T -> key * key -> bool
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    33
  val add_edge: key * key -> 'a T -> 'a T
6152
wenzelm
parents: 6142
diff changeset
    34
  val del_edge: key * key -> 'a T -> 'a T
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    35
  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
6142
wenzelm
parents: 6134
diff changeset
    36
  exception CYCLES of key list list
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    37
  val add_edge_acyclic: key * key -> 'a T -> 'a T
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    38
  val add_deps_acyclic: key * key list -> 'a T -> 'a T
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    39
  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    40
  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    41
  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    42
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    43
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    44
functor GraphFun(Key: KEY): GRAPH =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    45
struct
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    46
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    47
(* keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    48
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    49
type key = Key.key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    50
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    51
val eq_key = equal EQUAL o Key.ord;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    52
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    53
infix mem_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    54
val op mem_key = gen_mem eq_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    55
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    56
infix ins_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    57
val op ins_key = gen_ins eq_key;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    58
6152
wenzelm
parents: 6142
diff changeset
    59
infix del_key;
wenzelm
parents: 6142
diff changeset
    60
fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
wenzelm
parents: 6142
diff changeset
    61
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    62
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    63
(* tables and sets of keys *)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    64
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    65
structure Table = TableFun(Key);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    66
type keys = unit Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    67
6142
wenzelm
parents: 6134
diff changeset
    68
val empty_keys = Table.empty: keys;
wenzelm
parents: 6134
diff changeset
    69
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    70
infix mem_keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    71
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    72
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    73
infix ins_keys;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    74
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    75
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    76
6142
wenzelm
parents: 6134
diff changeset
    77
(* graphs *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    78
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    79
datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    80
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    81
exception UNDEF of key;
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    82
exception DUP = Table.DUP;
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    83
exception DUPS = Table.DUPS;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    84
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    85
val empty = Graph Table.empty;
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
    86
fun keys (Graph tab) = Table.keys tab;
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    87
fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    88
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    89
fun minimals (Graph tab) =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    90
  Table.foldl (fn (ms, (m, (_, ([], _)))) => m :: ms | (ms, _) => ms) ([], tab);
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    91
fun maximals (Graph tab) =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
    92
  Table.foldl (fn (ms, (m, (_, (_, [])))) => m :: ms | (ms, _) => ms) ([], tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    93
6142
wenzelm
parents: 6134
diff changeset
    94
fun get_entry (Graph tab) x =
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    95
  (case Table.lookup (tab, x) of
6142
wenzelm
parents: 6134
diff changeset
    96
    Some entry => entry
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
    97
  | None => raise UNDEF x);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
    98
6142
wenzelm
parents: 6134
diff changeset
    99
fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   100
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   101
6142
wenzelm
parents: 6134
diff changeset
   102
(* nodes *)
wenzelm
parents: 6134
diff changeset
   103
wenzelm
parents: 6134
diff changeset
   104
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   105
6142
wenzelm
parents: 6134
diff changeset
   106
fun get_node G = #1 o get_entry G;
wenzelm
parents: 6134
diff changeset
   107
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
wenzelm
parents: 6134
diff changeset
   108
wenzelm
parents: 6134
diff changeset
   109
wenzelm
parents: 6134
diff changeset
   110
(* reachability *)
wenzelm
parents: 6134
diff changeset
   111
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   112
(*nodes reachable from xs -- topologically sorted for acyclic graphs*)
6142
wenzelm
parents: 6134
diff changeset
   113
fun reachable next xs =
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   114
  let
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   115
    fun reach ((R, rs), x) =
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   116
      if x mem_keys R then (R, rs)
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   117
      else apsnd (cons x) (reachs ((x ins_keys R, rs), next x))
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   118
    and reachs R_xs = foldl reach R_xs;
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   119
  in foldl_map (reach o apfst (rpair [])) (empty_keys, xs) end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   120
6142
wenzelm
parents: 6134
diff changeset
   121
(*immediate*)
wenzelm
parents: 6134
diff changeset
   122
fun imm_preds G = #1 o #2 o get_entry G;
wenzelm
parents: 6134
diff changeset
   123
fun imm_succs G = #2 o #2 o get_entry G;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   124
6142
wenzelm
parents: 6134
diff changeset
   125
(*transitive*)
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   126
fun all_preds G = flat o snd o reachable (imm_preds G);
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   127
fun all_succs G = flat o snd o reachable (imm_succs G);
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   128
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   129
(*strongly connected components; see: David King and John Launchbury,
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   130
  "Structuring Depth First Search Algorithms in Haskell"*)
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   131
fun strong_conn G = filter_out null (snd (reachable (imm_preds G)
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   132
  (flat (rev (snd (reachable (imm_succs G) (keys G)))))));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   133
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   134
6142
wenzelm
parents: 6134
diff changeset
   135
(* paths *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   136
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   137
fun find_paths G (x, y) =
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   138
  let
14161
73ad4884441f Added function strong_conn for computing the strongly connected components
berghofe
parents: 12451
diff changeset
   139
    val (X, _) = reachable (imm_succs G) [x];
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   140
    fun paths ps p =
12451
0224f472be71 Fixed bug in function find_paths.
berghofe
parents: 9347
diff changeset
   141
      if not (null ps) andalso eq_key (p, x) then [p :: ps]
0224f472be71 Fixed bug in function find_paths.
berghofe
parents: 9347
diff changeset
   142
      else if p mem_keys X andalso not (p mem_key ps)
0224f472be71 Fixed bug in function find_paths.
berghofe
parents: 9347
diff changeset
   143
      then flat (map (paths (p :: ps)) (imm_preds G p))
0224f472be71 Fixed bug in function find_paths.
berghofe
parents: 9347
diff changeset
   144
      else [];
0224f472be71 Fixed bug in function find_paths.
berghofe
parents: 9347
diff changeset
   145
  in paths [] y end;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   146
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   147
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   148
(* nodes *)
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   149
6142
wenzelm
parents: 6134
diff changeset
   150
exception DUPLICATE of key;
wenzelm
parents: 6134
diff changeset
   151
6152
wenzelm
parents: 6142
diff changeset
   152
fun new_node (x, info) (Graph tab) =
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   153
  Graph (Table.update_new ((x, (info, ([], []))), tab));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   154
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   155
fun del_nodes xs (Graph tab) =
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   156
  let
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   157
    fun del (x, (i, (preds, succs))) =
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   158
      if x mem_key xs then None
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   159
      else Some (x, (i, (foldl op del_key (preds, xs), foldl op del_key (succs, xs))));
6659
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   160
  in Graph (Table.make (mapfilter del (Table.dest tab))) end;
7a056250899d removed get_nodes;
wenzelm
parents: 6152
diff changeset
   161
6152
wenzelm
parents: 6142
diff changeset
   162
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   163
(* edges *)
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   164
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   165
fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   166
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   167
fun add_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   168
  if is_edge G (x, y) then G
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   169
  else
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   170
    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   171
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   172
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   173
fun del_edge (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   174
  if is_edge G (x, y) then
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   175
    G |> map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)))
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   176
      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y)))
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   177
  else G;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   178
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   179
fun diff_edges G1 G2 =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   180
  flat (dest G1 |> map (fn (x, ys) => ys |> mapfilter (fn y =>
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   181
    if is_edge G2 (x, y) then None else Some (x, y))));
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   182
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   183
fun edges G = diff_edges G empty;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   184
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   185
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   186
(* merge *)
6152
wenzelm
parents: 6142
diff changeset
   187
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   188
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   189
  let
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   190
    fun eq_node ((i1, _), (i2, _)) = eq (i1, i2);
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   191
    fun no_edges (i, _) = (i, ([], []));
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   192
  in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
6152
wenzelm
parents: 6142
diff changeset
   193
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   194
fun merge eq GG = gen_merge add_edge eq GG;
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   195
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   196
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   197
(* maintain acyclic graphs *)
6142
wenzelm
parents: 6134
diff changeset
   198
wenzelm
parents: 6134
diff changeset
   199
exception CYCLES of key list list;
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   200
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   201
fun add_edge_acyclic (x, y) G =
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   202
  if is_edge G (x, y) then G
9347
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   203
  else
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   204
    (case find_paths G (y, x) of
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   205
      [] => add_edge (x, y) G
1791a62b33e7 improved add_edges_cyclic;
wenzelm
parents: 9321
diff changeset
   206
    | cycles => raise CYCLES (map (cons x) cycles));
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   207
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   208
fun add_deps_acyclic (y, xs) G =
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   209
  foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   210
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   211
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   212
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   213
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   214
(* maintain transitive acyclic graphs *)
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   215
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   216
fun add_edge_trans_acyclic (x, y) G =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   217
  add_edge_acyclic (x, y) G |>
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   218
  fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
9321
e0dda4bde88c tuned exceptions;
wenzelm
parents: 8806
diff changeset
   219
14793
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   220
fun merge_trans_acyclic eq (G1, G2) =
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   221
  merge_acyclic eq (G1, G2) |>
32d94d1e4842 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents: 14161
diff changeset
   222
  fold add_edge_trans_acyclic (diff_edges G1 G2 @ diff_edges G2 G1);
6134
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   223
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   224
end;
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   225
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   226
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   227
(*graphs indexed by strings*)
ec6092b0599d added General/graph.ML: generic direct graphs;
wenzelm
parents:
diff changeset
   228
structure Graph = GraphFun(type key = string val ord = string_ord);