author | wenzelm |
Thu, 27 Jul 2006 13:43:03 +0200 | |
changeset 20225 | 4b8e42490e58 |
parent 19950 | fd74bf4e603e |
child 20679 | c09af1bd255a |
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 |
13 |
exception DUPS of key list |
|
19029 | 14 |
exception SAME |
15 |
exception UNDEF of key |
|
6134 | 16 |
val empty: 'a T |
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 |
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 |
6142 | 22 |
val map_nodes: ('a -> 'b) -> 'a T -> 'b T |
19615 | 23 |
val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b |
15759 | 24 |
val get_node: 'a T -> key -> 'a (*exception UNDEF*) |
6142 | 25 |
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T |
17767 | 26 |
val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T |
6142 | 27 |
val imm_preds: 'a T -> key -> key list |
28 |
val imm_succs: 'a T -> key -> key list |
|
6134 | 29 |
val all_preds: 'a T -> key list -> key list |
30 |
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
|
31 |
val strong_conn: 'a T -> key list list |
19950 | 32 |
val project: (key -> bool) -> 'a T -> 'a T |
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*) |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
36 |
val is_edge: 'a T -> key * key -> bool |
6134 | 37 |
val add_edge: key * key -> 'a T -> 'a T |
6152 | 38 |
val del_edge: key * key -> 'a T -> 'a T |
15759 | 39 |
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUPS*) |
19029 | 40 |
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> |
41 |
'a T * 'a T -> 'a T (*exception DUPS*) |
|
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
42 |
val irreducible_paths: 'a T -> key * key -> key list list |
6142 | 43 |
exception CYCLES of key list list |
15759 | 44 |
val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
45 |
val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*) |
|
46 |
val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
|
47 |
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
|
48 |
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
|
6134 | 49 |
end; |
50 |
||
51 |
functor GraphFun(Key: KEY): GRAPH = |
|
52 |
struct |
|
53 |
||
54 |
(* keys *) |
|
55 |
||
56 |
type key = Key.key; |
|
57 |
||
18970 | 58 |
val eq_key = is_equal o Key.ord; |
6134 | 59 |
|
18921 | 60 |
val member_key = member eq_key; |
15759 | 61 |
val remove_key = remove eq_key; |
6152 | 62 |
|
6134 | 63 |
|
64 |
(* tables and sets of keys *) |
|
65 |
||
66 |
structure Table = TableFun(Key); |
|
67 |
type keys = unit Table.table; |
|
68 |
||
6142 | 69 |
val empty_keys = Table.empty: keys; |
70 |
||
18921 | 71 |
fun member_keys tab = Table.defined (tab: keys); |
72 |
fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys); |
|
6134 | 73 |
|
74 |
||
6142 | 75 |
(* graphs *) |
6134 | 76 |
|
77 |
datatype 'a T = Graph of ('a * (key list * key list)) Table.table; |
|
78 |
||
9321 | 79 |
exception DUP = Table.DUP; |
80 |
exception DUPS = Table.DUPS; |
|
19029 | 81 |
exception UNDEF = Table.UNDEF; |
82 |
exception SAME = Table.SAME; |
|
6134 | 83 |
|
84 |
val empty = Graph Table.empty; |
|
6659 | 85 |
fun keys (Graph tab) = Table.keys tab; |
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
86 |
fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab); |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
87 |
|
19615 | 88 |
fun fold_graph f (Graph tab) = Table.fold f tab; |
89 |
||
90 |
fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G []; |
|
91 |
fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G []; |
|
6134 | 92 |
|
6142 | 93 |
fun get_entry (Graph tab) x = |
17412 | 94 |
(case Table.lookup tab x of |
15531 | 95 |
SOME entry => entry |
96 |
| NONE => raise UNDEF x); |
|
6134 | 97 |
|
17412 | 98 |
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab); |
19290 | 99 |
|
17767 | 100 |
fun map_entry_yield x f (G as Graph tab) = |
101 |
let val (a, node') = f (get_entry G x) |
|
102 |
in (a, Graph (Table.update (x, node') tab)) end; |
|
6134 | 103 |
|
104 |
||
6142 | 105 |
(* nodes *) |
106 |
||
107 |
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab); |
|
6134 | 108 |
|
19290 | 109 |
fun fold_map_nodes f (Graph tab) = |
110 |
apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab; |
|
17580 | 111 |
|
6142 | 112 |
fun get_node G = #1 o get_entry G; |
18133 | 113 |
|
6142 | 114 |
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); |
19290 | 115 |
|
17767 | 116 |
fun map_node_yield x f = map_entry_yield x (fn (i, ps) => |
117 |
let val (a, i') = f i in (a, (i', ps)) end); |
|
6142 | 118 |
|
18133 | 119 |
|
6142 | 120 |
(* reachability *) |
121 |
||
6659 | 122 |
(*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
6142 | 123 |
fun reachable next xs = |
6134 | 124 |
let |
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
125 |
fun reach x (rs, R) = |
18921 | 126 |
if member_keys R x then (rs, R) |
127 |
else apfst (cons x) (fold reach (next x) (rs, insert_keys x R)) |
|
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
128 |
in fold_map (fn x => reach x o pair []) xs empty_keys end; |
6134 | 129 |
|
6142 | 130 |
(*immediate*) |
131 |
fun imm_preds G = #1 o #2 o get_entry G; |
|
132 |
fun imm_succs G = #2 o #2 o get_entry G; |
|
6134 | 133 |
|
6142 | 134 |
(*transitive*) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
138 |
(*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
|
139 |
"Structuring Depth First Search Algorithms in Haskell"*) |
18006
535de280c812
reachable - abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset
|
140 |
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
|
141 |
(flat (rev (fst (reachable (imm_succs G) (keys G))))))); |
6134 | 142 |
|
17912 | 143 |
(*subgraph induced by node subset*) |
19950 | 144 |
fun project proj G = |
17912 | 145 |
let |
19409 | 146 |
fun subg (k, (i, (preds, succs))) = |
19950 | 147 |
K (proj k) ? Table.update (k, (i, (filter proj preds, filter proj succs))); |
19615 | 148 |
in Graph (fold_graph subg G Table.empty) end; |
6134 | 149 |
|
18133 | 150 |
|
9321 | 151 |
(* nodes *) |
6134 | 152 |
|
6152 | 153 |
fun new_node (x, info) (Graph tab) = |
17412 | 154 |
Graph (Table.update_new (x, (info, ([], []))) tab); |
6134 | 155 |
|
17179 | 156 |
fun default_node (x, info) (Graph tab) = |
157 |
Graph (Table.default (x, (info, ([], []))) tab); |
|
17140 | 158 |
|
6659 | 159 |
fun del_nodes xs (Graph tab) = |
15759 | 160 |
Graph (tab |
161 |
|> fold Table.delete xs |
|
162 |
|> Table.map (fn (i, (preds, succs)) => |
|
163 |
(i, (fold remove_key xs preds, fold remove_key xs succs)))); |
|
6659 | 164 |
|
6152 | 165 |
|
9321 | 166 |
(* edges *) |
167 |
||
18921 | 168 |
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
|
169 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
170 |
fun add_edge (x, y) G = |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
171 |
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
|
172 |
else |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
173 |
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
|
174 |
|> 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
|
175 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
176 |
fun del_edge (x, y) G = |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
177 |
if is_edge G (x, y) then |
15759 | 178 |
G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs))) |
179 |
|> 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
|
180 |
else G; |
9321 | 181 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
182 |
fun diff_edges G1 G2 = |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset
|
183 |
flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y => |
15531 | 184 |
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
|
185 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
186 |
fun edges G = diff_edges G empty; |
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
187 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
188 |
|
18126 | 189 |
(* join and merge *) |
190 |
||
18133 | 191 |
fun no_edges (i, _) = (i, ([], [])); |
192 |
||
193 |
fun join f (Graph tab1, G2 as Graph tab2) = |
|
19029 | 194 |
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) |
18133 | 195 |
in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end; |
6152 | 196 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
197 |
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) = |
18133 | 198 |
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
|
199 |
in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end; |
6152 | 200 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
201 |
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
|
202 |
|
18133 | 203 |
|
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
204 |
(* irreducible paths -- Hasse diagram *) |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
205 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
206 |
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
|
207 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
208 |
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
|
209 |
fun irreds [] xs' = xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
210 |
| irreds (x :: xs) xs' = |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
211 |
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
|
212 |
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
|
213 |
then irreds xs xs' |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
217 |
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
|
218 |
let |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
219 |
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
|
220 |
fun paths path z = |
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
|
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
225 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
226 |
(* maintain acyclic graphs *) |
6142 | 227 |
|
228 |
exception CYCLES of key list list; |
|
6134 | 229 |
|
230 |
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
|
231 |
if is_edge G (x, y) then G |
9347 | 232 |
else |
19580
c878a09fb849
replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;
wenzelm
parents:
19482
diff
changeset
|
233 |
(case irreducible_paths G (y, x) of |
9347 | 234 |
[] => add_edge (x, y) G |
235 |
| cycles => raise CYCLES (map (cons x) cycles)); |
|
6134 | 236 |
|
15759 | 237 |
fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs; |
9321 | 238 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
239 |
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; |
9321 | 240 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
241 |
|
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
242 |
(* maintain transitive acyclic graphs *) |
9321 | 243 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
244 |
fun add_edge_trans_acyclic (x, y) G = |
19290 | 245 |
add_edge_acyclic (x, y) G |
246 |
|> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y])); |
|
9321 | 247 |
|
14793
32d94d1e4842
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
wenzelm
parents:
14161
diff
changeset
|
248 |
fun merge_trans_acyclic eq (G1, G2) = |
19290 | 249 |
merge_acyclic eq (G1, G2) |
250 |
|> fold add_edge_trans_acyclic (diff_edges G1 G2) |
|
251 |
|> fold add_edge_trans_acyclic (diff_edges G2 G1); |
|
6134 | 252 |
|
19615 | 253 |
|
254 |
(*final declarations of this structure!*) |
|
255 |
val fold = fold_graph; |
|
256 |
||
6134 | 257 |
end; |
258 |
||
16810 | 259 |
structure Graph = GraphFun(type key = string val ord = fast_string_ord); |
19615 | 260 |
structure IntGraph = GraphFun(type key = int val ord = int_ord); |