author | wenzelm |
Sun, 09 Oct 2011 16:47:58 +0200 | |
changeset 45107 | 76fef3e57004 |
parent 44338 | 700008399ee5 |
child 46611 | 669601fa1a62 |
permissions | -rw-r--r-- |
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 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
10 |
structure Keys: |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
11 |
sig |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
12 |
type T |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
13 |
val is_empty: T -> bool |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
14 |
val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
15 |
val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
16 |
val dest: T -> key list |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
17 |
end |
6134 | 18 |
type 'a T |
9321 | 19 |
exception DUP of key |
19029 | 20 |
exception SAME |
21 |
exception UNDEF of key |
|
6134 | 22 |
val empty: 'a T |
28204 | 23 |
val is_empty: 'a T -> bool |
6659 | 24 |
val keys: 'a T -> key list |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
25 |
val dest: 'a T -> (key * key list) list |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
26 |
val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
27 |
val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b |
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
28 |
val subgraph: (key -> bool) -> 'a T -> 'a T |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
29 |
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*) |
39021 | 30 |
val map: (key -> 'a -> 'b) -> 'a T -> 'b T |
15759 | 31 |
val get_node: 'a T -> key -> 'a (*exception UNDEF*) |
6142 | 32 |
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T |
17767 | 33 |
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
34 |
val imm_preds: 'a T -> key -> Keys.T |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
35 |
val imm_succs: 'a T -> key -> Keys.T |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
36 |
val immediate_preds: 'a T -> key -> key list |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
37 |
val immediate_succs: 'a T -> key -> key list |
6134 | 38 |
val all_preds: 'a T -> key list -> key list |
39 |
val all_succs: 'a T -> key list -> key list |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
40 |
val minimals: 'a T -> key list |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
41 |
val maximals: 'a T -> key list |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
42 |
val is_minimal: 'a T -> key -> bool |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
43 |
val is_maximal: 'a T -> key -> bool |
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
44 |
val strong_conn: 'a T -> key list list |
15759 | 45 |
val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*) |
17179 | 46 |
val default_node: key * 'a -> 'a T -> 'a T |
15759 | 47 |
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
|
48 |
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
|
49 |
val is_edge: 'a T -> key * key -> bool |
44202 | 50 |
val add_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) |
51 |
val del_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) |
|
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21935
diff
changeset
|
52 |
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) |
19029 | 53 |
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
|
54 |
'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
|
55 |
val irreducible_paths: 'a T -> key * key -> key list list |
20679 | 56 |
val all_paths: 'a T -> key * key -> key list list |
6142 | 57 |
exception CYCLES of key list list |
44202 | 58 |
val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) |
59 |
val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception UNDEF | CYCLES*) |
|
15759 | 60 |
val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
23964 | 61 |
val topological_order: 'a T -> key list |
44202 | 62 |
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) |
15759 | 63 |
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
44162 | 64 |
exception DEP of key * key |
65 |
val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*) |
|
6134 | 66 |
end; |
67 |
||
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31616
diff
changeset
|
68 |
functor Graph(Key: KEY): GRAPH = |
6134 | 69 |
struct |
70 |
||
71 |
(* keys *) |
|
72 |
||
73 |
type key = Key.key; |
|
18970 | 74 |
val eq_key = is_equal o Key.ord; |
6134 | 75 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
76 |
structure Table = Table(Key); |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
77 |
|
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
78 |
structure Keys = |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
79 |
struct |
6152 | 80 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
81 |
abstype T = Keys of unit Table.table |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
82 |
with |
6134 | 83 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
84 |
val empty = Keys Table.empty; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
85 |
fun is_empty (Keys tab) = Table.is_empty tab; |
6134 | 86 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
87 |
fun member (Keys tab) = Table.defined tab; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
88 |
fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab); |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
89 |
fun remove x (Keys tab) = Keys (Table.delete_safe x tab); |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
90 |
|
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
91 |
fun fold f (Keys tab) = Table.fold (f o #1) tab; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
92 |
fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; |
6134 | 93 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
94 |
fun make xs = Basics.fold insert xs empty; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
95 |
fun dest keys = fold_rev cons keys []; |
6142 | 96 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
97 |
fun filter P keys = fold (fn x => P x ? insert x) keys empty; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
98 |
|
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
99 |
end; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
100 |
end; |
6134 | 101 |
|
102 |
||
6142 | 103 |
(* graphs *) |
6134 | 104 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
105 |
datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table; |
6134 | 106 |
|
9321 | 107 |
exception DUP = Table.DUP; |
19029 | 108 |
exception UNDEF = Table.UNDEF; |
109 |
exception SAME = Table.SAME; |
|
6134 | 110 |
|
111 |
val empty = Graph Table.empty; |
|
28204 | 112 |
fun is_empty (Graph tab) = Table.is_empty tab; |
6659 | 113 |
fun keys (Graph tab) = Table.keys tab; |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
114 |
fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab); |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
115 |
|
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
32710
diff
changeset
|
116 |
fun get_first f (Graph tab) = Table.get_first f tab; |
19615 | 117 |
fun fold_graph f (Graph tab) = Table.fold f tab; |
118 |
||
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
119 |
fun subgraph P G = |
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
120 |
let |
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
121 |
fun subg (k, (i, (preds, succs))) = |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
122 |
if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs))) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
123 |
else I; |
21935
4e20a5397b57
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
wenzelm
parents:
21565
diff
changeset
|
124 |
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
|
125 |
|
6142 | 126 |
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
|
127 |
(case Table.lookup_key tab x of |
15531 | 128 |
SOME entry => entry |
129 |
| NONE => raise UNDEF x); |
|
6134 | 130 |
|
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
|
131 |
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab); |
19290 | 132 |
|
17767 | 133 |
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
|
134 |
let val (a, node') = f (#2 (get_entry G x)) |
17767 | 135 |
in (a, Graph (Table.update (x, node') tab)) end; |
6134 | 136 |
|
137 |
||
6142 | 138 |
(* nodes *) |
139 |
||
39021 | 140 |
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); |
6134 | 141 |
|
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 get_node G = #1 o #2 o get_entry G; |
18133 | 143 |
|
6142 | 144 |
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); |
19290 | 145 |
|
17767 | 146 |
fun map_node_yield x f = map_entry_yield x (fn (i, ps) => |
147 |
let val (a, i') = f i in (a, (i', ps)) end); |
|
6142 | 148 |
|
18133 | 149 |
|
6142 | 150 |
(* reachability *) |
151 |
||
6659 | 152 |
(*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
6142 | 153 |
fun reachable next xs = |
6134 | 154 |
let |
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
155 |
fun reach x (rs, R) = |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
156 |
if Keys.member R x then (rs, R) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
157 |
else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x; |
32710 | 158 |
fun reachs x (rss, R) = |
159 |
reach x ([], R) |>> (fn rs => rs :: rss); |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
160 |
in fold reachs xs ([], Keys.empty) end; |
6134 | 161 |
|
6142 | 162 |
(*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
|
163 |
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
|
164 |
fun imm_succs G = #2 o #2 o #2 o get_entry G; |
6134 | 165 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
166 |
fun immediate_preds G = Keys.dest o imm_preds G; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
167 |
fun immediate_succs G = Keys.dest o imm_succs G; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
168 |
|
6142 | 169 |
(*transitive*) |
32710 | 170 |
fun all_preds G = flat o #1 o reachable (imm_preds G); |
171 |
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
|
172 |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
173 |
(*minimal and maximal elements*) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
174 |
fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G []; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
175 |
fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G []; |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
176 |
fun is_minimal G x = Keys.is_empty (imm_preds G x); |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
177 |
fun is_maximal G x = Keys.is_empty (imm_succs G x); |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
178 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
179 |
(*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
|
180 |
"Structuring Depth First Search Algorithms in Haskell"*) |
32710 | 181 |
fun strong_conn G = |
182 |
rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); |
|
6134 | 183 |
|
18133 | 184 |
|
9321 | 185 |
(* nodes *) |
6134 | 186 |
|
6152 | 187 |
fun new_node (x, info) (Graph tab) = |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
188 |
Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); |
6134 | 189 |
|
17179 | 190 |
fun default_node (x, info) (Graph tab) = |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
191 |
Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); |
17140 | 192 |
|
6659 | 193 |
fun del_nodes xs (Graph tab) = |
15759 | 194 |
Graph (tab |
195 |
|> fold Table.delete xs |
|
39020 | 196 |
|> Table.map (fn _ => fn (i, (preds, succs)) => |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
197 |
(i, (fold Keys.remove xs preds, fold Keys.remove xs succs)))); |
6659 | 198 |
|
28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
199 |
fun del_node x (G as Graph tab) = |
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
200 |
let |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
201 |
fun del_adjacent which y = |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
202 |
Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove 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
|
203 |
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
|
204 |
in |
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
205 |
Graph (tab |
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
206 |
|> Table.delete x |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
207 |
|> Keys.fold (del_adjacent apsnd) preds |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
208 |
|> Keys.fold (del_adjacent apfst) succs) |
28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
209 |
end; |
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset
|
210 |
|
6152 | 211 |
|
9321 | 212 |
(* edges *) |
213 |
||
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
214 |
fun is_edge G (x, y) = Keys.member (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
|
215 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
216 |
fun add_edge (x, y) G = |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
217 |
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
|
218 |
else |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
219 |
G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs))) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
220 |
|> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs))); |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
221 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
222 |
fun del_edge (x, y) G = |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
223 |
if is_edge G (x, y) then |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
224 |
G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs))) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
225 |
|> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs))) |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
226 |
else G; |
9321 | 227 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
228 |
fun diff_edges G1 G2 = |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
229 |
flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y => |
15531 | 230 |
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
|
231 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
232 |
fun edges G = diff_edges G empty; |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
233 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
234 |
|
18126 | 235 |
(* join and merge *) |
236 |
||
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
237 |
fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); |
18133 | 238 |
|
35974
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
239 |
fun join f (G1 as Graph tab1, G2 as Graph tab2) = |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
240 |
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
241 |
if pointer_eq (G1, G2) then G1 |
39020 | 242 |
else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2))) |
35974
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
243 |
end; |
6152 | 244 |
|
35974
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
245 |
fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) = |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
246 |
let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
247 |
if pointer_eq (G1, G2) then G1 |
39020 | 248 |
else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2))) |
35974
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
249 |
end; |
6152 | 250 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
251 |
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
|
252 |
|
18133 | 253 |
|
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
254 |
(* irreducible paths -- Hasse diagram *) |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
255 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
256 |
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
|
257 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
258 |
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
|
259 |
fun irreds [] xs' = xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
260 |
| irreds (x :: xs) xs' = |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
261 |
if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse |
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
262 |
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
|
263 |
then irreds xs xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
264 |
else irreds xs (x :: xs'); |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
265 |
in irreds (immediate_preds G z) [] end; |
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
266 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
267 |
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
|
268 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
269 |
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
|
270 |
fun paths path z = |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
271 |
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
|
272 |
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
|
273 |
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
|
274 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
275 |
|
20736 | 276 |
(* all paths *) |
20679 | 277 |
|
278 |
fun all_paths G (x, y) = |
|
279 |
let |
|
280 |
val (_, X) = reachable (imm_succs G) [x]; |
|
20736 | 281 |
fun paths path z = |
282 |
if not (null path) andalso eq_key (x, z) then [z :: path] |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
283 |
else if Keys.member X z andalso not (member eq_key path z) |
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
284 |
then maps (paths (z :: path)) (immediate_preds G z) |
20679 | 285 |
else []; |
286 |
in paths [] y end; |
|
287 |
||
288 |
||
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
289 |
(* maintain acyclic graphs *) |
6142 | 290 |
|
291 |
exception CYCLES of key list list; |
|
6134 | 292 |
|
293 |
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
|
294 |
if is_edge G (x, y) then G |
9347 | 295 |
else |
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
296 |
(case irreducible_paths G (y, x) of |
9347 | 297 |
[] => add_edge (x, y) G |
298 |
| cycles => raise CYCLES (map (cons x) cycles)); |
|
6134 | 299 |
|
15759 | 300 |
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs; |
9321 | 301 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
302 |
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; |
9321 | 303 |
|
23964 | 304 |
fun topological_order G = minimals G |> all_succs G; |
305 |
||
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
306 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
307 |
(* maintain transitive acyclic graphs *) |
9321 | 308 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
309 |
fun add_edge_trans_acyclic (x, y) G = |
19290 | 310 |
add_edge_acyclic (x, y) G |
25538 | 311 |
|> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); |
9321 | 312 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
313 |
fun merge_trans_acyclic eq (G1, G2) = |
35974
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
314 |
if pointer_eq (G1, G2) then G1 |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
315 |
else |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
316 |
merge_acyclic eq (G1, G2) |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
317 |
|> fold add_edge_trans_acyclic (diff_edges G1 G2) |
3a588b344749
low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35405
diff
changeset
|
318 |
|> fold add_edge_trans_acyclic (diff_edges G2 G1); |
6134 | 319 |
|
31540 | 320 |
|
44162 | 321 |
(* schedule acyclic graph *) |
322 |
||
323 |
exception DEP of key * key; |
|
324 |
||
325 |
fun schedule f G = |
|
326 |
let |
|
327 |
val xs = topological_order G; |
|
328 |
val results = (xs, Table.empty) |-> fold (fn x => fn tab => |
|
329 |
let |
|
330 |
val a = get_node G x; |
|
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44202
diff
changeset
|
331 |
val deps = immediate_preds G x |> map (fn y => |
44162 | 332 |
(case Table.lookup tab y of |
333 |
SOME b => (y, b) |
|
334 |
| NONE => raise DEP (x, y))); |
|
335 |
in Table.update (x, f deps (x, a)) tab end); |
|
336 |
in map (the o Table.lookup results) xs end; |
|
337 |
||
338 |
||
19615 | 339 |
(*final declarations of this structure!*) |
39021 | 340 |
val map = map_nodes; |
19615 | 341 |
val fold = fold_graph; |
342 |
||
6134 | 343 |
end; |
344 |
||
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31616
diff
changeset
|
345 |
structure Graph = Graph(type key = string val ord = fast_string_ord); |
35403 | 346 |
structure Int_Graph = Graph(type key = int val ord = int_ord); |