author  berghofe 
Thu, 21 Aug 2003 16:18:43 +0200  
changeset 14161  73ad4884441f 
parent 12451  0224f472be71 
child 14793  32d94d1e4842 
permissions  rwrr 
6134  1 
(* Title: Pure/General/graph.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8806  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
6134  5 

6 
Directed graphs. 

7 
*) 

8 

9 
signature GRAPH = 

10 
sig 

11 
type key 

12 
type 'a T 

9321  13 
exception UNDEF of key 
14 
exception DUP of key 

15 
exception DUPS of key list 

6134  16 
val empty: 'a T 
6659  17 
val keys: 'a T > key list 
6142  18 
val map_nodes: ('a > 'b) > 'a T > 'b T 
19 
val get_node: 'a T > key > 'a 

20 
val map_node: key > ('a > 'a) > 'a T > 'a T 

21 
val imm_preds: 'a T > key > key list 

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

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

25 
val strong_conn: 'a T > key list list 
6134  26 
val find_paths: 'a T > key * key > key list list 
6152  27 
val new_node: key * 'a > 'a T > 'a T 
6659  28 
val del_nodes: key list > 'a T > 'a T 
9321  29 
val edges: 'a T > (key * key) list 
6134  30 
val add_edge: key * key > 'a T > 'a T 
6152  31 
val del_edge: key * key > 'a T > 'a T 
6142  32 
exception CYCLES of key list list 
6134  33 
val add_edge_acyclic: key * key > 'a T > 'a T 
9321  34 
val add_deps_acyclic: key * key list > 'a T > 'a T 
35 
val merge_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T 

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

36 
val merge: ('a * 'a > bool) > 'a T * 'a T > 'a T 
6134  37 
end; 
38 

39 
functor GraphFun(Key: KEY): GRAPH = 

40 
struct 

41 

42 

43 
(* keys *) 

44 

45 
type key = Key.key; 

46 

47 
val eq_key = equal EQUAL o Key.ord; 

48 

49 
infix mem_key; 

50 
val op mem_key = gen_mem eq_key; 

51 

52 
infix ins_key; 

53 
val op ins_key = gen_ins eq_key; 

54 

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

57 

6659  58 
infix del_keys; 
59 
val op del_keys = foldl (op del_key); 

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; 
70 
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x)); 

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; 
6134  86 

6142  87 
fun get_entry (Graph tab) x = 
6134  88 
(case Table.lookup (tab, x) of 
6142  89 
Some entry => entry 
9321  90 
 None => raise UNDEF x); 
6134  91 

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

94 

6142  95 
(* nodes *) 
96 

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

6134  98 

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

101 

102 

103 
(* reachability *) 

104 

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

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

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

110 
else apsnd (cons x) (reachs ((x ins_keys R, rs), next x)) 
6134  111 
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

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

6142  114 
(*immediate*) 
115 
fun imm_preds G = #1 o #2 o get_entry G; 

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

6134  117 

6142  118 
(*transitive*) 
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

119 
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

120 
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

121 

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

122 
(* strongly connected components; see: David King and John Launchbury, *) 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

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

124 

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

125 
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

126 
(flat (rev (snd (reachable (imm_succs G) (keys G))))))); 
6134  127 

128 

6142  129 
(* paths *) 
6134  130 

131 
fun find_paths G (x, y) = 

132 
let 

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

133 
val (X, _) = reachable (imm_succs G) [x]; 
6134  134 
fun paths ps p = 
12451  135 
if not (null ps) andalso eq_key (p, x) then [p :: ps] 
136 
else if p mem_keys X andalso not (p mem_key ps) 

137 
then flat (map (paths (p :: ps)) (imm_preds G p)) 

138 
else []; 

139 
in paths [] y end; 

6134  140 

141 

9321  142 
(* nodes *) 
6134  143 

6142  144 
exception DUPLICATE of key; 
145 

6152  146 
fun new_node (x, info) (Graph tab) = 
9321  147 
Graph (Table.update_new ((x, (info, ([], []))), tab)); 
6134  148 

6659  149 
fun del_nodes xs (Graph tab) = 
150 
let 

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

152 
if x mem_key xs then None 

153 
else Some (x, (i, (preds del_keys xs, succs del_keys xs))); 

154 
in Graph (Table.make (mapfilter del (Table.dest tab))) end; 

155 

6152  156 

9321  157 
(* edges *) 
158 

159 
fun edges (Graph tab) = 

160 
flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab)); 

161 

6152  162 
fun add_edge (x, y) = 
163 
map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o 

164 
map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs))); 

165 

166 
fun del_edge (x, y) = 

167 
map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o 

168 
map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs))); 

169 

6142  170 

171 
exception CYCLES of key list list; 

6134  172 

173 
fun add_edge_acyclic (x, y) G = 

9347  174 
if y mem_key imm_succs G x then G 
175 
else 

176 
(case find_paths G (y, x) of 

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

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

6134  179 

9321  180 
fun add_deps_acyclic (y, xs) G = 
181 
foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs); 

182 

183 

184 
(* merge_acyclic *) 

185 

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

186 
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) = 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

187 
foldl (fn (G, xy) => add xy G) 
9321  188 
(Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2); 
189 

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

190 
fun merge_acyclic eq p = gen_merge add_edge_acyclic eq p; 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

191 
fun merge eq p = gen_merge add_edge eq p; 
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset

192 

6134  193 

194 
end; 

195 

196 

197 
(*graphs indexed by strings*) 

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