author  wenzelm 
Fri, 03 Feb 2006 23:12:28 +0100  
changeset 18921  f47c46d7d654 
parent 18133  1d403623dabc 
child 18970  d055a29ddd23 
permissions  rwrr 
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 

56 
val eq_key = equal EQUAL o Key.ord; 

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); 