author  wenzelm 
Fri, 12 Aug 2011 20:32:25 +0200  
changeset 44162  5434899d955c 
parent 43792  d5803c3d537a 
child 44202  44c4ae5c5ce2 
permissions  rwrr 
6134  1 
(* Title: Pure/General/graph.ML 
15759  2 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 
6134  3 

4 
Directed graphs. 

5 
*) 

6 

7 
signature GRAPH = 

8 
sig 

9 
type key 

10 
type 'a T 

9321  11 
exception DUP of key 
19029  12 
exception SAME 
13 
exception UNDEF of key 

6134  14 
val empty: 'a T 
28204  15 
val is_empty: 'a T > bool 
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 
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
32710
diff
changeset

18 
val get_first: (key * ('a * (key list * key list)) > 'b option) > 'a T > 'b option 
19615  19 
val fold: (key * ('a * (key list * key list)) > 'b > 'b) > 'a T > 'b > 'b 
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

20 
val minimals: 'a T > key list 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

21 
val maximals: 'a T > key list 
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

22 
val subgraph: (key > bool) > 'a T > 'a T 
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

23 
val get_entry: 'a T > key > key * ('a * (key list * key list)) (*exception UNDEF*) 
39021  24 
val map: (key > 'a > 'b) > 'a T > 'b T 
15759  25 
val get_node: 'a T > key > 'a (*exception UNDEF*) 
6142  26 
val map_node: key > ('a > 'a) > 'a T > 'a T 
17767  27 
val map_node_yield: key > ('a > 'b * 'a) > 'a T > 'b * 'a T 
6142  28 
val imm_preds: 'a T > key > key list 
29 
val imm_succs: 'a T > key > key list 

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

32 
val strong_conn: 'a T > 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*) 
28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

36 
val del_node: key > 'a T > 'a T (*exception UNDEF*) 
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

37 
val is_edge: 'a T > key * key > bool 
6134  38 
val add_edge: key * key > 'a T > 'a T 
6152  39 
val del_edge: key * key > 'a T > 'a T 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21935
diff
changeset

40 
val merge: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception DUP*) 
19029  41 
val join: (key > 'a * 'a > 'a) (*exception DUP/SAME*) > 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21935
diff
changeset

42 
'a T * 'a T > 'a T (*exception DUP*) 
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

43 
val irreducible_paths: 'a T > key * key > key list list 
20679  44 
val all_paths: 'a T > key * key > key list list 
6142  45 
exception CYCLES of key list list 
15759  46 
val add_edge_acyclic: key * key > 'a T > 'a T (*exception CYCLES*) 
47 
val add_deps_acyclic: key * key list > 'a T > 'a T (*exception CYCLES*) 

48 
val merge_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception CYCLES*) 

23964  49 
val topological_order: 'a T > key list 
15759  50 
val add_edge_trans_acyclic: key * key > 'a T > 'a T (*exception CYCLES*) 
51 
val merge_trans_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception CYCLES*) 

44162  52 
exception DEP of key * key 
53 
val schedule: ((key * 'b) list > key * 'a > 'b) > 'a T > 'b list (*exception DEP*) 

6134  54 
end; 
55 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31616
diff
changeset

56 
functor Graph(Key: KEY): GRAPH = 
6134  57 
struct 
58 

59 
(* keys *) 

60 

61 
type key = Key.key; 

62 

18970  63 
val eq_key = is_equal o Key.ord; 
6134  64 

18921  65 
val member_key = member eq_key; 
15759  66 
val remove_key = remove eq_key; 
6152  67 

6134  68 

69 
(* tables and sets of keys *) 

70 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31616
diff
changeset

71 
structure Table = Table(Key); 
6134  72 
type keys = unit Table.table; 
73 

6142  74 
val empty_keys = Table.empty: keys; 
75 

18921  76 
fun member_keys tab = Table.defined (tab: keys); 
77 
fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys); 

6134  78 

79 

6142  80 
(* graphs *) 
6134  81 

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

83 

9321  84 
exception DUP = Table.DUP; 
19029  85 
exception UNDEF = Table.UNDEF; 
86 
exception SAME = Table.SAME; 

6134  87 

88 
val empty = Graph Table.empty; 

28204  89 
fun is_empty (Graph tab) = Table.is_empty tab; 
6659  90 
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

91 
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

92 

35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
32710
diff
changeset

93 
fun get_first f (Graph tab) = Table.get_first f tab; 
19615  94 
fun fold_graph f (Graph tab) = Table.fold f tab; 
95 

96 
fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m  _ => I) G []; 

97 
fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m  _ => I) G []; 

6134  98 

21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

99 
fun subgraph P G = 
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

100 
let 
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

101 
fun subg (k, (i, (preds, succs))) = 
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

102 
if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I; 
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

103 
in Graph (fold_graph subg G Table.empty) end; 
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset

104 

6142  105 
fun get_entry (Graph tab) x = 
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

106 
(case Table.lookup_key tab x of 
15531  107 
SOME entry => entry 
108 
 NONE => raise UNDEF x); 

6134  109 

43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

110 
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab); 
19290  111 

17767  112 
fun map_entry_yield x f (G as Graph tab) = 
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

113 
let val (a, node') = f (#2 (get_entry G x)) 
17767  114 
in (a, Graph (Table.update (x, node') tab)) end; 
6134  115 

116 

6142  117 
(* nodes *) 
118 

39021  119 
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); 
6134  120 

43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

121 
fun get_node G = #1 o #2 o get_entry G; 
18133  122 

6142  123 
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); 
19290  124 

17767  125 
fun map_node_yield x f = map_entry_yield x (fn (i, ps) => 
126 
let val (a, i') = f i in (a, (i', ps)) end); 

6142  127 

18133  128 

6142  129 
(* reachability *) 
130 

6659  131 
(*nodes reachable from xs  topologically sorted for acyclic graphs*) 
6142  132 
fun reachable next xs = 
6134  133 
let 
18006
535de280c812
reachable  abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset

134 
fun reach x (rs, R) = 
18921  135 
if member_keys R x then (rs, R) 
32710  136 
else fold reach (next x) (rs, insert_keys x R) >> cons x; 
137 
fun reachs x (rss, R) = 

138 
reach x ([], R) >> (fn rs => rs :: rss); 

139 
in fold reachs xs ([], empty_keys) end; 

6134  140 

6142  141 
(*immediate*) 
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

142 
fun imm_preds G = #1 o #2 o #2 o get_entry G; 
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

143 
fun imm_succs G = #2 o #2 o #2 o get_entry G; 
6134  144 

6142  145 
(*transitive*) 
32710  146 
fun all_preds G = flat o #1 o reachable (imm_preds G); 
147 
fun all_succs G = flat o #1 o reachable (imm_succs G); 

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

148 

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

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

150 
"Structuring Depth First Search Algorithms in Haskell"*) 
32710  151 
fun strong_conn G = 
152 
rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); 

6134  153 

18133  154 

9321  155 
(* nodes *) 
6134  156 

6152  157 
fun new_node (x, info) (Graph tab) = 
17412  158 
Graph (Table.update_new (x, (info, ([], []))) tab); 
6134  159 

17179  160 
fun default_node (x, info) (Graph tab) = 
161 
Graph (Table.default (x, (info, ([], []))) tab); 

17140  162 

6659  163 
fun del_nodes xs (Graph tab) = 
15759  164 
Graph (tab 
165 
> fold Table.delete xs 

39020  166 
> Table.map (fn _ => fn (i, (preds, succs)) => 
15759  167 
(i, (fold remove_key xs preds, fold remove_key xs succs)))); 
6659  168 

28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

169 
fun del_node x (G as Graph tab) = 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

170 
let 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

171 
fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps))); 
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39021
diff
changeset

172 
val (preds, succs) = #2 (#2 (get_entry G x)); 
28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

173 
in 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

174 
Graph (tab 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

175 
> Table.delete x 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

176 
> fold (del_adjacent apsnd) preds 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

177 
> fold (del_adjacent apfst) succs) 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

178 
end; 
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

179 

6152  180 

9321  181 
(* edges *) 
182 

18921  183 
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

184 

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

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

186 
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

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

188 
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

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

190 

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

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

192 
if is_edge G (x, y) then 
15759  193 
G > map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs))) 
194 
> 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

195 
else G; 
9321  196 

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

197 
fun diff_edges G1 G2 = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset

198 
flat (dest G1 > map (fn (x, ys) => ys > map_filter (fn y => 
15531  199 
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

200 

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

201 
fun edges G = diff_edges G empty; 
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset

202 

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

203 

18126  204 
(* join and merge *) 
205 

18133  206 
fun no_edges (i, _) = (i, ([], [])); 
207 

35974
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

208 
fun join f (G1 as Graph tab1, G2 as Graph tab2) = 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

209 
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

210 
if pointer_eq (G1, G2) then G1 
39020  211 
else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2))) 
35974
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

212 
end; 
6152  213 

35974
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

214 
fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) = 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

215 
let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

216 
if pointer_eq (G1, G2) then G1 
39020  217 
else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2))) 
35974
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

218 
end; 
6152  219 

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

220 
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

221 

18133  222 

19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

223 
(* irreducible paths  Hasse diagram *) 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

224 

c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

225 
fun irreducible_preds G X path z = 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

226 
let 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

227 
fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z)); 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

228 
fun irreds [] xs' = xs' 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

229 
 irreds (x :: xs) xs' = 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

230 
if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

231 
exists (red x) xs orelse exists (red x) xs' 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

232 
then irreds xs xs' 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

233 
else irreds xs (x :: xs'); 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

234 
in irreds (imm_preds G z) [] end; 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

235 

c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

236 
fun irreducible_paths G (x, y) = 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

237 
let 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

238 
val (_, X) = reachable (imm_succs G) [x]; 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

239 
fun paths path z = 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

240 
if eq_key (x, z) then cons (z :: path) 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

241 
else fold (paths (z :: path)) (irreducible_preds G X path z); 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

242 
in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end; 
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

243 

c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

244 

20736  245 
(* all paths *) 
20679  246 

247 
fun all_paths G (x, y) = 

248 
let 

249 
val (_, X) = reachable (imm_succs G) [x]; 

20736  250 
fun paths path z = 
251 
if not (null path) andalso eq_key (x, z) then [z :: path] 

252 
else if member_keys X z andalso not (member_key path z) 

253 
then maps (paths (z :: path)) (imm_preds G z) 

20679  254 
else []; 
255 
in paths [] y end; 

256 

257 

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

258 
(* maintain acyclic graphs *) 
6142  259 

260 
exception CYCLES of key list list; 

6134  261 

262 
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

263 
if is_edge G (x, y) then G 
9347  264 
else 
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset

265 
(case irreducible_paths G (y, x) of 
9347  266 
[] => add_edge (x, y) G 
267 
 cycles => raise CYCLES (map (cons x) cycles)); 

6134  268 

15759  269 
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs; 
9321  270 

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

271 
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 
9321  272 

23964  273 
fun topological_order G = minimals G > all_succs G; 
274 

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

275 

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

276 
(* maintain transitive acyclic graphs *) 
9321  277 

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

278 
fun add_edge_trans_acyclic (x, y) G = 
19290  279 
add_edge_acyclic (x, y) G 
25538  280 
> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); 
9321  281 

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

282 
fun merge_trans_acyclic eq (G1, G2) = 
35974
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

283 
if pointer_eq (G1, G2) then G1 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

284 
else 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

285 
merge_acyclic eq (G1, G2) 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

286 
> fold add_edge_trans_acyclic (diff_edges G1 G2) 
3a588b344749
lowlevel tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset

287 
> fold add_edge_trans_acyclic (diff_edges G2 G1); 
6134  288 

31540  289 

44162  290 
(* schedule acyclic graph *) 
291 

292 
exception DEP of key * key; 

293 

294 
fun schedule f G = 

295 
let 

296 
val xs = topological_order G; 

297 
val results = (xs, Table.empty) > fold (fn x => fn tab => 

298 
let 

299 
val a = get_node G x; 

300 
val deps = imm_preds G x > map (fn y => 

301 
(case Table.lookup tab y of 

302 
SOME b => (y, b) 

303 
 NONE => raise DEP (x, y))); 

304 
in Table.update (x, f deps (x, a)) tab end); 

305 
in map (the o Table.lookup results) xs end; 

306 

307 

19615  308 
(*final declarations of this structure!*) 
39021  309 
val map = map_nodes; 
19615  310 
val fold = fold_graph; 
311 

6134  312 
end; 
313 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31616
diff
changeset

314 
structure Graph = Graph(type key = string val ord = fast_string_ord); 
35403  315 
structure Int_Graph = Graph(type key = int val ord = int_ord); 