author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23964  d2df2797519b 
child 25538  58e8ba3b792b 
permissions  rwrr 
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 
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 
19615  18 
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

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

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

21 
val subgraph: (key > bool) > 'a T > 'a T 
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 
15759  32 
val new_node: key * 'a > 'a T > 'a T (*exception DUP*) 
17179  33 
val default_node: key * 'a > 'a T > 'a T 
15759  34 
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

35 
val is_edge: 'a T > key * key > bool 
6134  36 
val add_edge: key * key > 'a T > 'a T 
6152  37 
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

38 
val merge: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception DUP*) 
19029  39 
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

40 
'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

41 
val irreducible_paths: 'a T > key * key > key list list 
20679  42 
val all_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*) 

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

6134  50 
end; 
51 

52 
functor GraphFun(Key: KEY): GRAPH = 

53 
struct 

54 

55 
(* keys *) 

56 

57 
type key = Key.key; 

58 

18970  59 
val eq_key = is_equal o Key.ord; 
6134  60 

18921  61 
val member_key = member eq_key; 
15759  62 
val remove_key = remove eq_key; 
6152  63 

6134  64 

65 
(* tables and sets of keys *) 

66 

67 
structure Table = TableFun(Key); 

68 
type keys = unit Table.table; 

69 

6142  70 
val empty_keys = Table.empty: keys; 
71 

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

6134  74 

75 

6142  76 
(* graphs *) 
6134  77 

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

79 

9321  80 
exception DUP = Table.DUP; 
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 

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

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

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

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

96 
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

97 
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

98 

6142  99 
fun get_entry (Graph tab) x = 
17412  100 
(case Table.lookup tab x of 
15531  101 
SOME entry => entry 
102 
 NONE => raise UNDEF x); 

6134  103 

17412  104 
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab); 
19290  105 

17767  106 
fun map_entry_yield x f (G as Graph tab) = 
107 
let val (a, node') = f (get_entry G x) 

108 
in (a, Graph (Table.update (x, node') tab)) end; 

6134  109 

110 

6142  111 
(* nodes *) 
112 

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

6134  114 

19290  115 
fun fold_map_nodes f (Graph tab) = 
116 
apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab; 

17580  117 

6142  118 
fun get_node G = #1 o get_entry G; 
18133  119 

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

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

6142  124 

18133  125 

6142  126 
(* reachability *) 
127 

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

131 
fun reach x (rs, R) = 
18921  132 
if member_keys R x then (rs, R) 
133 
else apfst (cons x) (fold reach (next x) (rs, insert_keys x R)) 

23964  134 
in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end; 
6134  135 

6142  136 
(*immediate*) 
137 
fun imm_preds G = #1 o #2 o get_entry G; 

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

6134  139 

6142  140 
(*transitive*) 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19409
diff
changeset

141 
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

142 
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

143 

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

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

145 
"Structuring Depth First Search Algorithms in Haskell"*) 
18006
535de280c812
reachable  abandoned foldl_map in favor of fold_map
haftmann
parents:
17912
diff
changeset

146 
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

147 
(flat (rev (fst (reachable (imm_succs G) (keys G))))))); 
6134  148 

18133  149 

9321  150 
(* nodes *) 
6134  151 

6152  152 
fun new_node (x, info) (Graph tab) = 
17412  153 
Graph (Table.update_new (x, (info, ([], []))) tab); 
6134  154 

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

17140  157 

6659  158 
fun del_nodes xs (Graph tab) = 
15759  159 
Graph (tab 
160 
> fold Table.delete xs 

161 
> Table.map (fn (i, (preds, succs)) => 

162 
(i, (fold remove_key xs preds, fold remove_key xs succs)))); 

6659  163 

6152  164 

9321  165 
(* edges *) 
166 

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

168 

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

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

170 
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

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

172 
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

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

174 

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

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

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

179 
else G; 
9321  180 

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

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

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

184 

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

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

186 

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

187 

18126  188 
(* join and merge *) 
189 

18133  190 
fun no_edges (i, _) = (i, ([], [])); 
191 

192 
fun join f (Graph tab1, G2 as Graph tab2) = 

19029  193 
let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) 
18133  194 
in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end; 
6152  195 

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

196 
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) = 
18133  197 
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

198 
in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end; 
6152  199 

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

200 
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

201 

18133  202 

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

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

204 

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

205 
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

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

207 
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

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

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

210 
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

211 
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

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

213 
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

214 
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

215 

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

216 
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

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

218 
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

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

220 
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

221 
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

222 
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

223 

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

224 

20736  225 
(* all paths *) 
20679  226 

227 
fun all_paths G (x, y) = 

228 
let 

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

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

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

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

20679  234 
else []; 
235 
in paths [] y end; 

236 

237 

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

238 
(* maintain acyclic graphs *) 
6142  239 

240 
exception CYCLES of key list list; 

6134  241 

242 
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

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

245 
(case irreducible_paths G (y, x) of 
9347  246 
[] => add_edge (x, y) G 
247 
 cycles => raise CYCLES (map (cons x) cycles)); 

6134  248 

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

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

251 
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 
9321  252 

23964  253 
fun topological_order G = minimals G > all_succs G; 
254 

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

255 

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

256 
(* maintain transitive acyclic graphs *) 
9321  257 

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

258 
fun add_edge_trans_acyclic (x, y) G = 
19290  259 
add_edge_acyclic (x, y) G 
260 
> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y])); 

9321  261 

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

262 
fun merge_trans_acyclic eq (G1, G2) = 
19290  263 
merge_acyclic eq (G1, G2) 
264 
> fold add_edge_trans_acyclic (diff_edges G1 G2) 

265 
> fold add_edge_trans_acyclic (diff_edges G2 G1); 

6134  266 

19615  267 

268 
(*final declarations of this structure!*) 

269 
val fold = fold_graph; 

270 

6134  271 
end; 
272 

16810  273 
structure Graph = GraphFun(type key = string val ord = fast_string_ord); 
19615  274 
structure IntGraph = GraphFun(type key = int val ord = int_ord); 