author | wenzelm |
Tue, 23 Sep 2008 15:48:55 +0200 | |
changeset 28333 | 507b64f4cd2a |
parent 28204 | 2d93b158ad99 |
child 29606 | fedb8be05f24 |
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 DUP of key |
19029 | 13 |
exception SAME |
14 |
exception UNDEF of key |
|
6134 | 15 |
val empty: 'a T |
28204 | 16 |
val is_empty: 'a T -> bool |
6659 | 17 |
val keys: 'a T -> key list |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
18 |
val dest: 'a T -> (key * key list) list |
28183 | 19 |
val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option |
19615 | 20 |
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
|
21 |
val minimals: 'a T -> key list |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
22 |
val maximals: 'a T -> key list |
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
23 |
val subgraph: (key -> bool) -> 'a T -> 'a T |
6142 | 24 |
val map_nodes: ('a -> 'b) -> 'a T -> 'b T |
19615 | 25 |
val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b |
15759 | 26 |
val get_node: 'a T -> key -> 'a (*exception UNDEF*) |
6142 | 27 |
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T |
17767 | 28 |
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T |
6142 | 29 |
val imm_preds: 'a T -> key -> key list |
30 |
val imm_succs: 'a T -> key -> key list |
|
6134 | 31 |
val all_preds: 'a T -> key list -> key list |
32 |
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
|
33 |
val strong_conn: 'a T -> key list list |
15759 | 34 |
val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*) |
17179 | 35 |
val default_node: key * 'a -> 'a T -> 'a T |
15759 | 36 |
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
|
37 |
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
|
38 |
val is_edge: 'a T -> key * key -> bool |
6134 | 39 |
val add_edge: key * key -> 'a T -> 'a T |
6152 | 40 |
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
|
41 |
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) |
19029 | 42 |
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
|
43 |
'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
|
44 |
val irreducible_paths: 'a T -> key * key -> key list list |
20679 | 45 |
val all_paths: 'a T -> key * key -> key list list |
6142 | 46 |
exception CYCLES of key list list |
15759 | 47 |
val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
48 |
val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*) |
|
49 |
val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
|
23964 | 50 |
val topological_order: 'a T -> key list |
15759 | 51 |
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
52 |
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
|
6134 | 53 |
end; |
54 |
||
55 |
functor GraphFun(Key: KEY): GRAPH = |
|
56 |
struct |
|
57 |
||
58 |
(* keys *) |
|
59 |
||
60 |
type key = Key.key; |
|
61 |
||
18970 | 62 |
val eq_key = is_equal o Key.ord; |
6134 | 63 |
|
18921 | 64 |
val member_key = member eq_key; |
15759 | 65 |
val remove_key = remove eq_key; |
6152 | 66 |
|
6134 | 67 |
|
68 |
(* tables and sets of keys *) |
|
69 |
||
70 |
structure Table = TableFun(Key); |
|
71 |
type keys = unit Table.table; |
|
72 |
||
6142 | 73 |
val empty_keys = Table.empty: keys; |
74 |
||
18921 | 75 |
fun member_keys tab = Table.defined (tab: keys); |
76 |
fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys); |
|
6134 | 77 |
|
78 |
||
6142 | 79 |
(* graphs *) |
6134 | 80 |
|
81 |
datatype 'a T = Graph of ('a * (key list * key list)) Table.table; |
|
82 |
||
9321 | 83 |
exception DUP = Table.DUP; |
19029 | 84 |
exception UNDEF = Table.UNDEF; |
85 |
exception SAME = Table.SAME; |
|
6134 | 86 |
|
87 |
val empty = Graph Table.empty; |
|
28204 | 88 |
fun is_empty (Graph tab) = Table.is_empty tab; |
6659 | 89 |
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
|
90 |
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
|
91 |
|
28183 | 92 |
fun get_first f (Graph tab) = Table.get_first f tab; |
19615 | 93 |
fun fold_graph f (Graph tab) = Table.fold f tab; |
94 |
||
95 |
fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G []; |
|
96 |
fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G []; |
|
6134 | 97 |
|
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
98 |
fun subgraph P G = |
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
99 |
let |
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
100 |
fun subg (k, (i, (preds, succs))) = |
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
101 |
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
|
102 |
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
|
103 |
|
6142 | 104 |
fun get_entry (Graph tab) x = |
17412 | 105 |
(case Table.lookup tab x of |
15531 | 106 |
SOME entry => entry |
107 |
| NONE => raise UNDEF x); |
|
6134 | 108 |
|
17412 | 109 |
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab); |
19290 | 110 |
|
17767 | 111 |
fun map_entry_yield x f (G as Graph tab) = |
112 |
let val (a, node') = f (get_entry G x) |
|
113 |
in (a, Graph (Table.update (x, node') tab)) end; |
|
6134 | 114 |
|
115 |
||
6142 | 116 |
(* nodes *) |
117 |
||
118 |
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab); |
|
6134 | 119 |
|
19290 | 120 |
fun fold_map_nodes f (Graph tab) = |
121 |
apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab; |
|
17580 | 122 |
|
6142 | 123 |
fun get_node G = #1 o get_entry G; |
18133 | 124 |
|
6142 | 125 |
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); |
19290 | 126 |
|
17767 | 127 |
fun map_node_yield x f = map_entry_yield x (fn (i, ps) => |
128 |
let val (a, i') = f i in (a, (i', ps)) end); |
|
6142 | 129 |
|
18133 | 130 |
|
6142 | 131 |
(* reachability *) |
132 |
||
6659 | 133 |
(*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
6142 | 134 |
fun reachable next xs = |
6134 | 135 |
let |
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
136 |
fun reach x (rs, R) = |
18921 | 137 |
if member_keys R x then (rs, R) |
138 |
else apfst (cons x) (fold reach (next x) (rs, insert_keys x R)) |
|
23964 | 139 |
in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end; |
6134 | 140 |
|
6142 | 141 |
(*immediate*) |
142 |
fun imm_preds G = #1 o #2 o get_entry G; |
|
143 |
fun imm_succs G = #2 o #2 o get_entry G; |
|
6134 | 144 |
|
6142 | 145 |
(*transitive*) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
146 |
fun all_preds G = flat o fst o reachable (imm_preds G); |
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
147 |
fun all_succs G = flat o fst 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"*) |
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
151 |
fun strong_conn G = filter_out null (fst (reachable (imm_preds G) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
152 |
(flat (rev (fst (reachable (imm_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 |
|
166 |
|> Table.map (fn (i, (preds, succs)) => |
|
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))); |
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
172 |
val (preds, succs) = #2 (get_entry G x); |
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 |
||
208 |
fun join f (Graph tab1, G2 as Graph tab2) = |
|
19029 | 209 |
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) |
18133 | 210 |
in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end; |
6152 | 211 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
212 |
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) = |
18133 | 213 |
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
|
214 |
in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end; |
6152 | 215 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
216 |
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
|
217 |
|
18133 | 218 |
|
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
219 |
(* irreducible paths -- Hasse diagram *) |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
220 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
221 |
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
|
222 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
223 |
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
|
224 |
fun irreds [] xs' = xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
225 |
| irreds (x :: xs) xs' = |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
226 |
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
|
227 |
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
|
228 |
then irreds xs xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
229 |
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
|
230 |
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
|
231 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
232 |
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
|
233 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
234 |
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
|
235 |
fun paths path z = |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
236 |
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
|
237 |
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
|
238 |
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
|
239 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
240 |
|
20736 | 241 |
(* all paths *) |
20679 | 242 |
|
243 |
fun all_paths G (x, y) = |
|
244 |
let |
|
245 |
val (_, X) = reachable (imm_succs G) [x]; |
|
20736 | 246 |
fun paths path z = |
247 |
if not (null path) andalso eq_key (x, z) then [z :: path] |
|
248 |
else if member_keys X z andalso not (member_key path z) |
|
249 |
then maps (paths (z :: path)) (imm_preds G z) |
|
20679 | 250 |
else []; |
251 |
in paths [] y end; |
|
252 |
||
253 |
||
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
254 |
(* maintain acyclic graphs *) |
6142 | 255 |
|
256 |
exception CYCLES of key list list; |
|
6134 | 257 |
|
258 |
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
|
259 |
if is_edge G (x, y) then G |
9347 | 260 |
else |
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
261 |
(case irreducible_paths G (y, x) of |
9347 | 262 |
[] => add_edge (x, y) G |
263 |
| cycles => raise CYCLES (map (cons x) cycles)); |
|
6134 | 264 |
|
15759 | 265 |
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs; |
9321 | 266 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
267 |
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; |
9321 | 268 |
|
23964 | 269 |
fun topological_order G = minimals G |> all_succs G; |
270 |
||
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
271 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
272 |
(* maintain transitive acyclic graphs *) |
9321 | 273 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
274 |
fun add_edge_trans_acyclic (x, y) G = |
19290 | 275 |
add_edge_acyclic (x, y) G |
25538 | 276 |
|> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); |
9321 | 277 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
278 |
fun merge_trans_acyclic eq (G1, G2) = |
19290 | 279 |
merge_acyclic eq (G1, G2) |
280 |
|> fold add_edge_trans_acyclic (diff_edges G1 G2) |
|
281 |
|> fold add_edge_trans_acyclic (diff_edges G2 G1); |
|
6134 | 282 |
|
19615 | 283 |
|
284 |
(*final declarations of this structure!*) |
|
285 |
val fold = fold_graph; |
|
286 |
||
6134 | 287 |
end; |
288 |
||
16810 | 289 |
structure Graph = GraphFun(type key = string val ord = fast_string_ord); |
19615 | 290 |
structure IntGraph = GraphFun(type key = int val ord = int_ord); |