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