author  wenzelm 
Thu, 19 Jul 2012 15:45:59 +0200  
changeset 48350  09bf3b73e446 
parent 46668  9034b44844bd 
child 49560  11430dd89e35 
permissions  rwrr 
6134  1 
(* Title: Pure/General/graph.ML 
15759  2 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 
6134  3 

4 
Directed graphs. 

5 
*) 

6 

7 
signature GRAPH = 

8 
sig 

9 
type key 

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

28 
val get_entry: 'a T > key > key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*) 
15759  29 
val get_node: 'a T > key > 'a (*exception UNDEF*) 
6142  30 
val map_node: key > ('a > 'a) > 'a T > 'a T 
17767  31 
val map_node_yield: key > ('a > 'b * 'a) > 'a T > 'b * 'a T 
46611  32 
val map: (key > 'a > 'b) > 'a T > 'b 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

33 
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

34 
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

35 
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

36 
val immediate_succs: 'a T > key > key list 
6134  37 
val all_preds: 'a T > key list > key list 
38 
val all_succs: 'a T > key list > key list 

46613  39 
val strong_conn: 'a T > 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

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 
15759  44 
val new_node: key * 'a > 'a T > 'a T (*exception DUP*) 
17179  45 
val default_node: key * 'a > 'a T > 'a T 
28333
507b64f4cd2a
added del_node, which is more efficient for sparse graphs;
wenzelm
parents:
28204
diff
changeset

46 
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

47 
val is_edge: 'a T > key * key > bool 
44202  48 
val add_edge: key * key > 'a T > 'a T (*exception UNDEF*) 
49 
val del_edge: key * key > 'a T > 'a T (*exception UNDEF*) 

46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

50 
val restrict: (key > bool) > 'a T > 'a T 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21935
diff
changeset

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

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

54 
val irreducible_paths: 'a T > key * key > key list list 
6142  55 
exception CYCLES of key list list 
44202  56 
val add_edge_acyclic: key * key > 'a T > 'a T (*exception UNDEF  CYCLES*) 
57 
val add_deps_acyclic: key * key list > 'a T > 'a T (*exception UNDEF  CYCLES*) 

15759  58 
val merge_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception CYCLES*) 
23964  59 
val topological_order: 'a T > key list 
44202  60 
val add_edge_trans_acyclic: key * key > 'a T > 'a T (*exception UNDEF  CYCLES*) 
15759  61 
val merge_trans_acyclic: ('a * 'a > bool) > 'a T * 'a T > 'a T (*exception CYCLES*) 
44162  62 
exception DEP of key * key 
63 
val schedule: ((key * 'b) list > key * 'a > 'b) > 'a T > 'b list (*exception DEP*) 

6134  64 
end; 
65 

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

66 
functor Graph(Key: KEY): GRAPH = 
6134  67 
struct 
68 

69 
(* keys *) 

70 

71 
type key = Key.key; 

18970  72 
val eq_key = is_equal o Key.ord; 
6134  73 

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

74 
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

75 

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

77 
struct 
6152  78 

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

79 
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

80 
with 
6134  81 

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

82 
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

83 
fun is_empty (Keys tab) = Table.is_empty tab; 
6134  84 

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

85 
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

86 
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

87 
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

88 

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

90 
fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; 
6134  91 

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

92 
fun dest keys = fold_rev cons keys []; 
6142  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 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

95 

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

96 
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

97 
end; 
6134  98 

99 

6142  100 
(* graphs *) 
6134  101 

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

102 
datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table; 
6134  103 

9321  104 
exception DUP = Table.DUP; 
19029  105 
exception UNDEF = Table.UNDEF; 
106 
exception SAME = Table.SAME; 

6134  107 

108 
val empty = Graph Table.empty; 

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

111 
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

112 

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

113 
fun get_first f (Graph tab) = Table.get_first f tab; 
19615  114 
fun fold_graph f (Graph tab) = Table.fold f tab; 
115 

6142  116 
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

117 
(case Table.lookup_key tab x of 
15531  118 
SOME entry => entry 
119 
 NONE => raise UNDEF x); 

6134  120 

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

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

17767  123 
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

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

127 

6142  128 
(* nodes *) 
129 

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

130 
fun get_node G = #1 o #2 o get_entry G; 
18133  131 

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

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

6142  136 

46611  137 
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); 
138 

18133  139 

6142  140 
(* reachability *) 
141 

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

145 
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

146 
if Keys.member R x then (rs, R) 
48350
09bf3b73e446
clarified topological ordering: preserve order of adjacency via reverse fold;
wenzelm
parents:
46668
diff
changeset

147 
else Keys.fold_rev reach (next x) (rs, Keys.insert x R) >> cons x; 
32710  148 
fun reachs x (rss, R) = 
149 
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

150 
in fold reachs xs ([], Keys.empty) end; 
6134  151 

6142  152 
(*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

153 
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

154 
fun imm_succs G = #2 o #2 o #2 o get_entry G; 
6134  155 

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

157 
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

158 

6142  159 
(*transitive*) 
32710  160 
fun all_preds G = flat o #1 o reachable (imm_preds G); 
161 
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

162 

46613  163 
(*strongly connected components; see: David King and John Launchbury, 
164 
"Structuring Depth First Search Algorithms in Haskell"*) 

165 
fun strong_conn G = 

166 
rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); 

167 

168 

169 
(* minimal and maximal elements *) 

170 

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

171 
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

172 
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

173 
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

174 
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

175 

18133  176 

46668  177 
(* node operations *) 
6134  178 

6152  179 
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

180 
Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); 
6134  181 

17179  182 
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

183 
Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); 
17140  184 

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

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

186 
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

187 
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

188 
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

189 
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

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

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

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

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

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

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

196 

46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

197 
fun restrict pred G = 
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

198 
fold_graph (fn (x, _) => not (pred x) ? del_node x) G G; 
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
46613
diff
changeset

199 

6152  200 

46668  201 
(* edge operations *) 
9321  202 

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

203 
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

204 

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

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

206 
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

207 
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

208 
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

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

210 

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

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

212 
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

213 
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

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

215 
else G; 
9321  216 

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

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

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

220 

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

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

222 

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

223 

18126  224 
(* join and merge *) 
225 

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

226 
fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); 
18133  227 

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

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

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

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

232 
end; 
6152  233 

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

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

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

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

238 
end; 
6152  239 

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

240 
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

241 

18133  242 

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

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

244 

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

245 
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

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

247 
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

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

249 
 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

250 
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

251 
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

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

253 
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

254 
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

255 

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

256 
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

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

258 
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

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

260 
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

261 
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

262 
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

263 

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

264 

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

265 
(* maintain acyclic graphs *) 
6142  266 

267 
exception CYCLES of key list list; 

6134  268 

269 
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

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

272 
(case irreducible_paths G (y, x) of 
9347  273 
[] => add_edge (x, y) G 
274 
 cycles => raise CYCLES (map (cons x) cycles)); 

6134  275 

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

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

278 
fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 
9321  279 

23964  280 
fun topological_order G = minimals G > all_succs G; 
281 

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

282 

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

283 
(* maintain transitive acyclic graphs *) 
9321  284 

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

285 
fun add_edge_trans_acyclic (x, y) G = 
19290  286 
add_edge_acyclic (x, y) G 
25538  287 
> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); 
9321  288 

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

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

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

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

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

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

294 
> fold add_edge_trans_acyclic (diff_edges G2 G1); 
6134  295 

31540  296 

44162  297 
(* schedule acyclic graph *) 
298 

299 
exception DEP of key * key; 

300 

301 
fun schedule f G = 

302 
let 

303 
val xs = topological_order G; 

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

305 
let 

306 
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

307 
val deps = immediate_preds G x > map (fn y => 
44162  308 
(case Table.lookup tab y of 
309 
SOME b => (y, b) 

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

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

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

313 

314 

19615  315 
(*final declarations of this structure!*) 
39021  316 
val map = map_nodes; 
19615  317 
val fold = fold_graph; 
318 

6134  319 
end; 
320 

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

321 
structure Graph = Graph(type key = string val ord = fast_string_ord); 
46667  322 
structure String_Graph = Graph(type key = string val ord = string_ord); 
35403  323 
structure Int_Graph = Graph(type key = int val ord = int_ord); 