1(* Title: Pure/General/graph.ML 2 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 3 4Directed graphs. 5*) 6 7signature GRAPH = 8sig 9 type key 10 structure Keys: 11 sig 12 type T 13 val is_empty: T -> bool 14 val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a 15 val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a 16 val dest: T -> key list 17 end 18 type 'a T 19 exception DUP of key 20 exception SAME 21 exception UNDEF of key 22 val empty: 'a T 23 val is_empty: 'a T -> bool 24 val keys: 'a T -> key list 25 val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 26 'b option 27 val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b 28 val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*) 29 val get_node: 'a T -> key -> 'a (*exception UNDEF*) 30 val map_node: key -> ('a -> 'a) -> 'a T -> 'a T 31 val map: (key -> 'a -> 'b) -> 'a T -> 'b T 32 val imm_preds: 'a T -> key -> Keys.T 33 val imm_succs: 'a T -> key -> Keys.T 34 val immediate_preds: 'a T -> key -> key list 35 val immediate_succs: 'a T -> key -> key list 36 val all_preds: 'a T -> key list -> key list 37 val all_succs: 'a T -> key list -> key list 38 val strong_conn: 'a T -> key list list 39 val map_strong_conn: ((key * 'a) list -> 'b list) -> 'a T -> 'b T 40 val minimals: 'a T -> key list 41 val maximals: 'a T -> key list 42 val is_minimal: 'a T -> key -> bool 43 val is_maximal: 'a T -> key -> bool 44 val is_isolated: 'a T -> key -> bool 45 val new_node: key * 'a -> 'a T -> 'a T (*exn DUP*) 46 val default_node: key * 'a -> 'a T -> 'a T 47 val del_node: key -> 'a T -> 'a T (*exn UNDEF*) 48 val is_edge: 'a T -> key * key -> bool 49 val add_edge: key * key -> 'a T -> 'a T (*exn UNDEF*) 50 val del_edge: key * key -> 'a T -> 'a T (*exn UNDEF*) 51 val restrict: (key -> bool) -> 'a T -> 'a T 52 val dest: 'a T -> ((key * 'a) * key list) list 53 val make: ((key * 'a) * key list) list -> 'a T (*exn DUP | UNDEF*) 54 val merge: ('a -> 'a -> bool) -> 'a T * 'a T -> 'a T (*exn DUP*) 55 val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> 56 'a T * 'a T -> 'a T (*exn DUP*) 57 val irreducible_paths: 'a T -> key * key -> key list list 58 exception CYCLES of key list list 59 val add_edge_acyclic: key * key -> 'a T -> 'a T (*exn UNDEF | CYCLES*) 60 val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exn UNDEF | CYCLES*) 61 val merge_acyclic: ('a -> 'a -> bool) -> 'a T * 'a T -> 'a T (*exn CYCLES*) 62 val topological_order: 'a T -> key list 63 val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exn UNDEF | CYCLES*) 64 val merge_trans_acyclic: ('a -> 'a -> bool) -> 'a T * 'a T -> 'a T 65 (*exn CYCLES*) 66 exception DEP of key * key 67 val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list 68 (*exn DEP*) 69end; 70 71functor Graph(Key: KEY): GRAPH = 72struct 73 74 75open Portable 76(* keys *) 77 78infix ? |> |>> ||-> 79fun fold_product f _ [] z = z 80 | fold_product f [] _ z = z 81 | fold_product f (x :: xs) ys z = 82 z |> foldl' (f x) ys |> fold_product f xs ys 83 84 85type key = Key.key; 86fun eq_key k1 k2 = Key.ord(k1,k2) = EQUAL 87 88structure Table = Table(Key); 89 90structure Keys = 91struct 92 93abstype T = Keys of unit Table.table 94with 95 96val empty = Keys Table.empty; 97fun is_empty (Keys tab) = Table.is_empty tab; 98 99fun member (Keys tab) = Table.defined tab; 100fun insert x (Keys tab) = 101 Keys (Table.insert (fn _ => fn _ => true) (x, ()) tab); 102fun remove x (Keys tab) = Keys (Table.delete_safe x tab); 103 104fun fold f (Keys tab) = Table.fold (f o #1) tab; 105fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; 106 107fun dest keys = fold_rev cons keys []; 108 109fun filter P keys = fold (fn x => P x ? insert x) keys empty; 110 111end; 112end; 113 114 115(* graphs *) 116 117datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table; 118 119exception DUP = Table.DUP; 120exception UNDEF = Table.UNDEF; 121exception SAME = Table.SAME; 122 123val empty = Graph Table.empty; 124fun is_empty (Graph tab) = Table.is_empty tab; 125fun keys (Graph tab) = Table.keys tab; 126 127fun get_first f (Graph tab) = Table.get_first f tab; 128fun fold_graph f (Graph tab) = Table.fold f tab; 129 130fun get_entry (Graph tab) x = 131 (case Table.lookup_key tab x of 132 SOME entry => entry 133 | NONE => raise UNDEF x); 134 135fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab); 136 137 138(* nodes *) 139 140fun get_node G = #1 o #2 o get_entry G; 141 142fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); 143 144fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); 145 146 147(* reachability *) 148 149(*nodes reachable from xs -- topologically sorted for acyclic graphs*) 150fun reachable next xs = 151 let 152 fun reach x (rs, R) = 153 if Keys.member R x then (rs, R) 154 else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x; 155 fun reachs x (rss, R) = 156 reach x ([], R) |>> (fn rs => rs :: rss); 157 in foldl' reachs xs ([], Keys.empty) end; 158 159(*immediate*) 160fun imm_preds G = #1 o #2 o #2 o get_entry G; 161fun imm_succs G = #2 o #2 o #2 o get_entry G; 162 163fun immediate_preds G = Keys.dest o imm_preds G; 164fun immediate_succs G = Keys.dest o imm_succs G; 165 166(*transitive*) 167fun all_preds G = List.concat o #1 o reachable (imm_preds G); 168fun all_succs G = List.concat o #1 o reachable (imm_succs G); 169 170(*strongly connected components; see: David King and John Launchbury, 171 "Structuring Depth First Search Algorithms in Haskell"*) 172fun strong_conn G = 173 rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); 174 175fun map_strong_conn f G = 176 let 177 val xss = strong_conn G 178 fun map' xs A = 179 ListPair.foldl (fn (k,v,t) => Table.update(k,v) t) 180 A 181 (xs, f (AList.make (get_node G) xs)) 182 val tab' = Table.empty |> foldl' map' xss 183 in 184 map_nodes (fn x => fn _ => valOf (Table.lookup tab' x)) G 185 end 186 187 188(* minimal and maximal elements *) 189 190fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G []; 191fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G []; 192fun is_minimal G x = Keys.is_empty (imm_preds G x); 193fun is_maximal G x = Keys.is_empty (imm_succs G x); 194 195fun is_isolated G x = is_minimal G x andalso is_maximal G x; 196 197 198(* node operations *) 199 200fun new_node (x, info) (Graph tab) = 201 Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); 202 203fun default_node (x, info) (Graph tab) = 204 Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); 205 206fun del_node x (G as Graph tab) = 207 let 208 fun del_adjacent which y = 209 Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps))); 210 val (preds, succs) = #2 (#2 (get_entry G x)); 211 in 212 Graph (tab 213 |> Table.delete x 214 |> Keys.fold (del_adjacent apsnd) preds 215 |> Keys.fold (del_adjacent apfst) succs) 216 end; 217 218fun restrict pred G = 219 fold_graph (fn (x, _) => not (pred x) ? del_node x) G G; 220 221 222(* edge operations *) 223 224fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false; 225 226fun add_edge (x, y) G = 227 if is_edge G (x, y) then G 228 else 229 G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs))) 230 |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs))); 231 232fun del_edge (x, y) G = 233 if is_edge G (x, y) then 234 G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs))) 235 |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs))) 236 else G; 237 238fun diff_edges G1 G2 = 239 fold_graph (fn (x, (_, (_, succs))) => 240 Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 []; 241 242fun edges G = diff_edges G empty; 243 244 245(* dest and make *) 246 247fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G []; 248 249fun make entries = 250 empty 251 |> foldl' (new_node o fst) entries 252 |> foldl' 253 (fn ((x, _), ys) => foldl' (fn y => add_edge (x, y)) ys) entries 254 255(* join and merge *) 256 257fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); 258 259fun join f (G1 as Graph tab1, G2 as Graph tab2) = 260 let 261 fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) 262 in 263 if pointer_eq (G1, G2) then G1 264 else foldl' add_edge 265 (edges G2) 266 (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2))) 267 end; 268 269fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) = 270 let 271 fun eq_node (i1, _) (i2, _) = eq i1 i2 272 in 273 if pointer_eq (G1, G2) then G1 274 else foldl' 275 add 276 (edges G2) 277 (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2))) 278 end; 279 280fun merge eq GG = gen_merge add_edge eq GG; 281 282 283(* irreducible paths -- Hasse diagram *) 284 285fun irreducible_preds G X path z = 286 let 287 fun red x x' = is_edge G (x, x') andalso not (eq_key x' z); 288 fun irreds [] xs' = xs' 289 | irreds (x :: xs) xs' = 290 if not (Keys.member X x) orelse eq_key x z orelse 291 op_mem eq_key x path orelse 292 exists (red x) xs orelse exists (red x) xs' 293 then irreds xs xs' 294 else irreds xs (x :: xs'); 295 in irreds (immediate_preds G z) [] end; 296 297fun irreducible_paths G (x, y) = 298 let 299 val (_, X) = reachable (imm_succs G) [x]; 300 fun paths path z = 301 if eq_key x z then cons (z :: path) 302 else foldl' (paths (z :: path)) (irreducible_preds G X path z) 303 in 304 if eq_key x y andalso not (is_edge G (x, x)) then [[]] 305 else paths [] y [] 306 end; 307 308 309(* maintain acyclic graphs *) 310 311exception CYCLES of key list list; 312 313fun add_edge_acyclic (x, y) G = 314 if is_edge G (x, y) then G 315 else 316 (case irreducible_paths G (y, x) of 317 [] => add_edge (x, y) G 318 | cycles => raise CYCLES (map (cons x) cycles)); 319 320fun add_deps_acyclic (y, xs) = 321 foldl' (fn x => add_edge_acyclic (x, y)) xs; 322 323fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 324 325fun topological_order G = minimals G |> all_succs G; 326 327 328(* maintain transitive acyclic graphs *) 329 330fun add_edge_trans_acyclic (x, y) G = 331 add_edge_acyclic (x, y) G 332 |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); 333 334fun merge_trans_acyclic eq (G1, G2) = 335 if pointer_eq (G1, G2) then G1 336 else 337 merge_acyclic eq (G1, G2) 338 |> foldl' add_edge_trans_acyclic (diff_edges G1 G2) 339 |> foldl' add_edge_trans_acyclic (diff_edges G2 G1); 340 341 342(* schedule acyclic graph *) 343 344exception DEP of key * key; 345 346fun schedule f G = 347 let 348 val xs = topological_order G; 349 val results = (xs, Table.empty) ||-> foldl' (fn x => fn tab => 350 let 351 val a = get_node G x; 352 val deps = immediate_preds G x |> map (fn y => 353 (case Table.lookup tab y of 354 SOME b => (y, b) 355 | NONE => raise DEP (x, y))); 356 in Table.update (x, f deps (x, a)) tab end); 357 in map (valOf o Table.lookup results) xs end; 358 359 360(*final declarations of this structure!*) 361val map = map_nodes; 362val fold = fold_graph; 363 364end; 365 366structure Graph = Graph( 367 type key = string 368 val ord = String.compare 369 val pp = HOLPP.add_string o Portable.mlquote 370); 371