author | skalberg |
Fri, 05 Dec 2003 19:39:39 +0100 | |
changeset 14278 | ae499452700a |
parent 14161 | 73ad4884441f |
child 14793 | 32d94d1e4842 |
permissions | -rw-r--r-- |
6134 | 1 |
(* Title: Pure/General/graph.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
8806 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6134 | 5 |
|
6 |
Directed graphs. |
|
7 |
*) |
|
8 |
||
9 |
signature GRAPH = |
|
10 |
sig |
|
11 |
type key |
|
12 |
type 'a T |
|
9321 | 13 |
exception UNDEF of key |
14 |
exception DUP of key |
|
15 |
exception DUPS of key list |
|
6134 | 16 |
val empty: 'a T |
6659 | 17 |
val keys: 'a T -> key list |
6142 | 18 |
val map_nodes: ('a -> 'b) -> 'a T -> 'b T |
19 |
val get_node: 'a T -> key -> 'a |
|
20 |
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T |
|
21 |
val imm_preds: 'a T -> key -> key list |
|
22 |
val imm_succs: 'a T -> key -> key list |
|
6134 | 23 |
val all_preds: 'a T -> key list -> key list |
24 |
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
|
25 |
val strong_conn: 'a T -> key list list |
6134 | 26 |
val find_paths: 'a T -> key * key -> key list list |
6152 | 27 |
val new_node: key * 'a -> 'a T -> 'a T |
6659 | 28 |
val del_nodes: key list -> 'a T -> 'a T |
9321 | 29 |
val edges: 'a T -> (key * key) list |
6134 | 30 |
val add_edge: key * key -> 'a T -> 'a T |
6152 | 31 |
val del_edge: key * key -> 'a T -> 'a T |
6142 | 32 |
exception CYCLES of key list list |
6134 | 33 |
val add_edge_acyclic: key * key -> 'a T -> 'a T |
9321 | 34 |
val add_deps_acyclic: key * key list -> 'a T -> 'a T |
35 |
val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T |
|
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
36 |
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T |
6134 | 37 |
end; |
38 |
||
39 |
functor GraphFun(Key: KEY): GRAPH = |
|
40 |
struct |
|
41 |
||
42 |
||
43 |
(* keys *) |
|
44 |
||
45 |
type key = Key.key; |
|
46 |
||
47 |
val eq_key = equal EQUAL o Key.ord; |
|
48 |
||
49 |
infix mem_key; |
|
50 |
val op mem_key = gen_mem eq_key; |
|
51 |
||
52 |
infix ins_key; |
|
53 |
val op ins_key = gen_ins eq_key; |
|
54 |
||
6152 | 55 |
infix del_key; |
56 |
fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs; |
|
57 |
||
6659 | 58 |
infix del_keys; |
59 |
val op del_keys = foldl (op del_key); |
|
60 |
||
6134 | 61 |
|
62 |
(* tables and sets of keys *) |
|
63 |
||
64 |
structure Table = TableFun(Key); |
|
65 |
type keys = unit Table.table; |
|
66 |
||
6142 | 67 |
val empty_keys = Table.empty: keys; |
68 |
||
6134 | 69 |
infix mem_keys; |
70 |
fun x mem_keys tab = is_some (Table.lookup (tab: keys, x)); |
|
71 |
||
72 |
infix ins_keys; |
|
73 |
fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab); |
|
74 |
||
75 |
||
6142 | 76 |
(* graphs *) |
6134 | 77 |
|
78 |
datatype 'a T = Graph of ('a * (key list * key list)) Table.table; |
|
79 |
||
9321 | 80 |
exception UNDEF of key; |
81 |
exception DUP = Table.DUP; |
|
82 |
exception DUPS = Table.DUPS; |
|
6134 | 83 |
|
84 |
val empty = Graph Table.empty; |
|
6659 | 85 |
fun keys (Graph tab) = Table.keys tab; |
6134 | 86 |
|
6142 | 87 |
fun get_entry (Graph tab) x = |
6134 | 88 |
(case Table.lookup (tab, x) of |
6142 | 89 |
Some entry => entry |
9321 | 90 |
| None => raise UNDEF x); |
6134 | 91 |
|
6142 | 92 |
fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab)); |
6134 | 93 |
|
94 |
||
6142 | 95 |
(* nodes *) |
96 |
||
97 |
fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab); |
|
6134 | 98 |
|
6142 | 99 |
fun get_node G = #1 o get_entry G; |
100 |
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); |
|
101 |
||
102 |
||
103 |
(* reachability *) |
|
104 |
||
6659 | 105 |
(*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
6142 | 106 |
fun reachable next xs = |
6134 | 107 |
let |
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
108 |
fun reach ((R, rs), x) = |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
109 |
if x mem_keys R then (R, rs) |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
110 |
else apsnd (cons x) (reachs ((x ins_keys R, rs), next x)) |
6134 | 111 |
and reachs R_xs = foldl reach R_xs; |
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
112 |
in foldl_map (reach o apfst (rpair [])) (empty_keys, xs) end; |
6134 | 113 |
|
6142 | 114 |
(*immediate*) |
115 |
fun imm_preds G = #1 o #2 o get_entry G; |
|
116 |
fun imm_succs G = #2 o #2 o get_entry G; |
|
6134 | 117 |
|
6142 | 118 |
(*transitive*) |
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
119 |
fun all_preds G = flat o snd o reachable (imm_preds G); |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
120 |
fun all_succs G = flat o snd o reachable (imm_succs G); |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
121 |
|
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
122 |
(* strongly connected components; see: David King and John Launchbury, *) |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
123 |
(* "Structuring Depth First Search Algorithms in Haskell" *) |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
124 |
|
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
125 |
fun strong_conn G = filter_out null (snd (reachable (imm_preds G) |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
126 |
(flat (rev (snd (reachable (imm_succs G) (keys G))))))); |
6134 | 127 |
|
128 |
||
6142 | 129 |
(* paths *) |
6134 | 130 |
|
131 |
fun find_paths G (x, y) = |
|
132 |
let |
|
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
133 |
val (X, _) = reachable (imm_succs G) [x]; |
6134 | 134 |
fun paths ps p = |
12451 | 135 |
if not (null ps) andalso eq_key (p, x) then [p :: ps] |
136 |
else if p mem_keys X andalso not (p mem_key ps) |
|
137 |
then flat (map (paths (p :: ps)) (imm_preds G p)) |
|
138 |
else []; |
|
139 |
in paths [] y end; |
|
6134 | 140 |
|
141 |
||
9321 | 142 |
(* nodes *) |
6134 | 143 |
|
6142 | 144 |
exception DUPLICATE of key; |
145 |
||
6152 | 146 |
fun new_node (x, info) (Graph tab) = |
9321 | 147 |
Graph (Table.update_new ((x, (info, ([], []))), tab)); |
6134 | 148 |
|
6659 | 149 |
fun del_nodes xs (Graph tab) = |
150 |
let |
|
151 |
fun del (x, (i, (preds, succs))) = |
|
152 |
if x mem_key xs then None |
|
153 |
else Some (x, (i, (preds del_keys xs, succs del_keys xs))); |
|
154 |
in Graph (Table.make (mapfilter del (Table.dest tab))) end; |
|
155 |
||
6152 | 156 |
|
9321 | 157 |
(* edges *) |
158 |
||
159 |
fun edges (Graph tab) = |
|
160 |
flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab)); |
|
161 |
||
6152 | 162 |
fun add_edge (x, y) = |
163 |
map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o |
|
164 |
map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs))); |
|
165 |
||
166 |
fun del_edge (x, y) = |
|
167 |
map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o |
|
168 |
map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs))); |
|
169 |
||
6142 | 170 |
|
171 |
exception CYCLES of key list list; |
|
6134 | 172 |
|
173 |
fun add_edge_acyclic (x, y) G = |
|
9347 | 174 |
if y mem_key imm_succs G x then G |
175 |
else |
|
176 |
(case find_paths G (y, x) of |
|
177 |
[] => add_edge (x, y) G |
|
178 |
| cycles => raise CYCLES (map (cons x) cycles)); |
|
6134 | 179 |
|
9321 | 180 |
fun add_deps_acyclic (y, xs) G = |
181 |
foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs); |
|
182 |
||
183 |
||
184 |
(* merge_acyclic *) |
|
185 |
||
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
186 |
fun gen_merge add eq (Graph tab1, G2 as Graph tab2) = |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
187 |
foldl (fn (G, xy) => add xy G) |
9321 | 188 |
(Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2); |
189 |
||
14161
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
190 |
fun merge_acyclic eq p = gen_merge add_edge_acyclic eq p; |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
191 |
fun merge eq p = gen_merge add_edge eq p; |
73ad4884441f
Added function strong_conn for computing the strongly connected components
berghofe
parents:
12451
diff
changeset
|
192 |
|
6134 | 193 |
|
194 |
end; |
|
195 |
||
196 |
||
197 |
(*graphs indexed by strings*) |
|
198 |
structure Graph = GraphFun(type key = string val ord = string_ord); |