author  skalberg 
Thu, 03 Mar 2005 12:43:01 +0100  
changeset 15570  8d8c70b41bab 
parent 15531  08c8dad8e399 
child 15759  144c9f9a8ade 
permissions  rwrr 
6134  1 
(* Title: Pure/General/graph.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

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 
15160  21 
val get_node: 'a T > key > 'a (* UNDEF *) 
6142  22 
val map_node: key > ('a > 'a) > 'a T > 'a T 
23 
val imm_preds: 'a T > key > key list 

24 
val imm_succs: 'a T > key > key list 

6134  25 
val all_preds: 'a T > key list > key list 
26 
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

27 
val strong_conn: 'a T > key list list 
6134  28 
val find_paths: 'a T > key * key > key list list 
15160  29 
val new_node: key * 'a > 'a T > 'a T (* DUP *) 
6659  30 
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

31 
val is_edge: 'a T > key * key > bool 
6134  32 
val add_edge: key * key > 'a T > 'a T 
6152  33 
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

34 
val merge: ('a * 'a > bool) > 'a T * 'a T > 'a T 
6142  35 
exception CYCLES of key list list 
6134  36 
val add_edge_acyclic: key * key > 'a T > 'a T 
9321  37 
val add_deps_acyclic: key * key list > 'a T > 'a T 
38 
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

39 
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

40 
val merge_trans_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T 
6134  41 
end; 
42 

43 
functor GraphFun(Key: KEY): GRAPH = 

44 
struct 

45 

46 
(* keys *) 

47 

48 
type key = Key.key; 

49 

50 
val eq_key = equal EQUAL o Key.ord; 

51 

52 
infix mem_key; 

53 
val op mem_key = gen_mem eq_key; 

54 

55 
infix ins_key; 

56 
val op ins_key = gen_ins eq_key; 

57 

6152  58 
infix del_key; 
59 
fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs; 

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 

6134  69 
infix mem_keys; 
15570  70 
fun x mem_keys tab = isSome (Table.lookup (tab: keys, x)); 
6134  71 

72 
infix ins_keys; 

73 
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab); 

74 

75 

6142  76 
(* graphs *) 
6134  77 

78 
datatype 'a T = Graph of ('a * (key list * key list)) Table.table; 

79 

9321  80 
exception UNDEF of key; 
81 
exception DUP = Table.DUP; 

82 
exception DUPS = Table.DUPS; 

6134  83 

84 
val empty = Graph Table.empty; 

6659  85 
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

86 
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

87 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

88 
fun minimals (Graph tab) = 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

89 
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

90 
fun maximals (Graph tab) = 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

91 
Table.foldl (fn (ms, (m, (_, (_, [])))) => m :: ms  (ms, _) => ms) ([], tab); 
6134  92 

6142  93 
fun get_entry (Graph tab) x = 
6134  94 
(case Table.lookup (tab, x) of 
15531  95 
SOME entry => entry 
96 
 NONE => raise UNDEF x); 

6134  97 

6142  98 
fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab)); 
6134  99 

100 

6142  101 
(* nodes *) 
102 

103 
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab); 

6134  104 

6142  105 
fun get_node G = #1 o get_entry G; 
106 
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); 

107 

108 

109 
(* reachability *) 

110 

6659  111 
(*nodes reachable from xs  topologically sorted for acyclic graphs*) 
6142  112 
fun reachable next xs = 
6134  113 
let 
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

114 
fun reach ((R, rs), x) = 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

115 
if x mem_keys R then (R, rs) 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

116 
else apsnd (cons x) (reachs ((x ins_keys R, rs), next x)) 
15570  117 
and reachs R_xs = Library.foldl reach R_xs; 
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

118 
in foldl_map (reach o apfst (rpair [])) (empty_keys, xs) end; 
6134  119 

6142  120 
(*immediate*) 
121 
fun imm_preds G = #1 o #2 o get_entry G; 

122 
fun imm_succs G = #2 o #2 o get_entry G; 

6134  123 

6142  124 
(*transitive*) 
15570  125 
fun all_preds G = List.concat o snd o reachable (imm_preds G); 
126 
fun all_succs G = List.concat o snd o reachable (imm_succs G); 

14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

127 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

128 
(*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

129 
"Structuring Depth First Search Algorithms in Haskell"*) 
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

130 
fun strong_conn G = filter_out null (snd (reachable (imm_preds G) 
15570  131 
(List.concat (rev (snd (reachable (imm_succs G) (keys G))))))); 
6134  132 

133 

6142  134 
(* paths *) 
6134  135 

136 
fun find_paths G (x, y) = 

137 
let 

14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

138 
val (X, _) = reachable (imm_succs G) [x]; 
6134  139 
fun paths ps p = 
12451  140 
if not (null ps) andalso eq_key (p, x) then [p :: ps] 
141 
else if p mem_keys X andalso not (p mem_key ps) 

15570  142 
then List.concat (map (paths (p :: ps)) (imm_preds G p)) 
12451  143 
else []; 
144 
in paths [] y end; 

6134  145 

146 

9321  147 
(* nodes *) 
6134  148 

6142  149 
exception DUPLICATE of key; 
150 

6152  151 
fun new_node (x, info) (Graph tab) = 
9321  152 
Graph (Table.update_new ((x, (info, ([], []))), tab)); 
6134  153 

6659  154 
fun del_nodes xs (Graph tab) = 
155 
let 

156 
fun del (x, (i, (preds, succs))) = 

15531  157 
if x mem_key xs then NONE 
15570  158 
else SOME (x, (i, (Library.foldl op del_key (preds, xs), Library.foldl op del_key (succs, xs)))); 
159 
in Graph (Table.make (List.mapPartial del (Table.dest tab))) end; 

6659  160 

6152  161 

9321  162 
(* edges *) 
163 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

164 
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

165 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

166 
fun add_edge (x, y) G = 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

167 
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

168 
else 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

169 
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

170 
> 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

171 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

172 
fun del_edge (x, y) G = 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

173 
if is_edge G (x, y) then 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

174 
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

175 
> 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

176 
else G; 
9321  177 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

178 
fun diff_edges G1 G2 = 
15570  179 
List.concat (dest G1 > map (fn (x, ys) => ys > List.mapPartial (fn y => 
15531  180 
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

181 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

182 
fun edges G = diff_edges G empty; 
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 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

185 
(* merge *) 
6152  186 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

187 
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

188 
let 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

189 
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

190 
fun no_edges (i, _) = (i, ([], [])); 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

191 
in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end; 
6152  192 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

193 
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

194 

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 
(* maintain acyclic graphs *) 
6142  197 

198 
exception CYCLES of key list list; 

6134  199 

200 
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

201 
if is_edge G (x, y) then G 
9347  202 
else 
203 
(case find_paths G (y, x) of 

204 
[] => add_edge (x, y) G 

205 
 cycles => raise CYCLES (map (cons x) cycles)); 

6134  206 

9321  207 
fun add_deps_acyclic (y, xs) G = 
15570  208 
Library.foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs); 
9321  209 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

210 
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 
9321  211 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

212 

32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

213 
(* maintain transitive acyclic graphs *) 
9321  214 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

215 
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

216 
add_edge_acyclic (x, y) G > 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

217 
fold add_edge (Library.product (all_preds G [x]) (all_succs G [y])); 
9321  218 

14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

219 
fun merge_trans_acyclic eq (G1, G2) = 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

220 
merge_acyclic eq (G1, G2) > 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

221 
fold add_edge_trans_acyclic (diff_edges G1 G2 @ diff_edges G2 G1); 
6134  222 

223 
end; 

224 

225 

226 
(*graphs indexed by strings*) 

227 
structure Graph = GraphFun(type key = string val ord = string_ord); 