equal
deleted
inserted
replaced
47 val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*) |
47 val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*) |
48 val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
48 val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
49 val topological_order: 'a T -> key list |
49 val topological_order: 'a T -> key list |
50 val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
50 val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) |
51 val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
51 val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) |
|
52 exception DEP of key * key |
|
53 val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*) |
52 end; |
54 end; |
53 |
55 |
54 functor Graph(Key: KEY): GRAPH = |
56 functor Graph(Key: KEY): GRAPH = |
55 struct |
57 struct |
56 |
58 |
283 merge_acyclic eq (G1, G2) |
285 merge_acyclic eq (G1, G2) |
284 |> fold add_edge_trans_acyclic (diff_edges G1 G2) |
286 |> fold add_edge_trans_acyclic (diff_edges G1 G2) |
285 |> fold add_edge_trans_acyclic (diff_edges G2 G1); |
287 |> fold add_edge_trans_acyclic (diff_edges G2 G1); |
286 |
288 |
287 |
289 |
|
290 (* schedule acyclic graph *) |
|
291 |
|
292 exception DEP of key * key; |
|
293 |
|
294 fun schedule f G = |
|
295 let |
|
296 val xs = topological_order G; |
|
297 val results = (xs, Table.empty) |-> fold (fn x => fn tab => |
|
298 let |
|
299 val a = get_node G x; |
|
300 val deps = imm_preds G x |> map (fn y => |
|
301 (case Table.lookup tab y of |
|
302 SOME b => (y, b) |
|
303 | NONE => raise DEP (x, y))); |
|
304 in Table.update (x, f deps (x, a)) tab end); |
|
305 in map (the o Table.lookup results) xs end; |
|
306 |
|
307 |
288 (*final declarations of this structure!*) |
308 (*final declarations of this structure!*) |
289 val map = map_nodes; |
309 val map = map_nodes; |
290 val fold = fold_graph; |
310 val fold = fold_graph; |
291 |
311 |
292 end; |
312 end; |