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) = 136 Graph (Table.update (x, f (#2 (get_entry G x))) tab); 137 138 139(* nodes *) 140 141fun get_node G = #1 o #2 o get_entry G; 142 143fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); 144 145fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); 146 147 148(* reachability *) 149 150(*nodes reachable from xs -- topologically sorted for acyclic graphs*) 151fun reachable next xs = 152 let 153 fun reach x (rs, R) = 154 if Keys.member R x then (rs, R) 155 else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x; 156 fun reachs x (rss, R) = 157 reach x ([], R) |>> (fn rs => rs :: rss); 158 in foldl' reachs xs ([], Keys.empty) end; 159 160(*immediate*) 161fun imm_preds G = #1 o #2 o #2 o get_entry G; 162fun imm_succs G = #2 o #2 o #2 o get_entry G; 163 164fun immediate_preds G = Keys.dest o imm_preds G; 165fun immediate_succs G = Keys.dest o imm_succs G; 166 167(*transitive*) 168fun all_preds G = List.concat o #1 o reachable (imm_preds G); 169fun all_succs G = List.concat o #1 o reachable (imm_succs G); 170 171(*strongly connected components; see: David King and John Launchbury, 172 "Structuring Depth First Search Algorithms in Haskell"*) 173fun strong_conn G = 174 rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); 175 176fun map_strong_conn f G = 177 let 178 val xss = strong_conn G 179 fun map' xs A = 180 ListPair.foldl (fn (k,v,t) => Table.update(k,v) t) 181 A 182 (xs, f (AList.make (get_node G) xs)) 183 val tab' = Table.empty |> foldl' map' xss 184 in 185 map_nodes (fn x => fn _ => valOf (Table.lookup tab' x)) G 186 end 187 188 189(* minimal and maximal elements *) 190 191fun minimals G = 192 fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G []; 193fun maximals G = 194 fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G []; 195fun is_minimal G x = Keys.is_empty (imm_preds G x); 196fun is_maximal G x = Keys.is_empty (imm_succs G x); 197 198fun is_isolated G x = is_minimal G x andalso is_maximal G x; 199 200 201(* node operations *) 202 203fun new_node (x, info) (Graph tab) = 204 Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); 205 206fun default_node (x, info) (Graph tab) = 207 Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); 208 209fun del_node x (G as Graph tab) = 210 let 211 fun del_adjacent which y = 212 Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps))); 213 val (preds, succs) = #2 (#2 (get_entry G x)); 214 in 215 Graph (tab 216 |> Table.delete x 217 |> Keys.fold (del_adjacent apsnd) preds 218 |> Keys.fold (del_adjacent apfst) succs) 219 end; 220 221fun restrict pred G = 222 fold_graph (fn (x, _) => not (pred x) ? del_node x) G G; 223 224 225(* edge operations *) 226 227fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false; 228 229fun add_edge (x, y) G = 230 if is_edge G (x, y) then G 231 else 232 G |> map_entry y (fn (i, (preds,succs)) => (i,(Keys.insert x preds, succs))) 233 |> map_entry x (fn (i, (preds,succs)) => (i,(preds, Keys.insert y succs))) 234 235fun del_edge (x, y) G = 236 if is_edge G (x, y) then 237 G |> map_entry y (fn (i,(preds,succs)) => (i, (Keys.remove x preds, succs))) 238 |> map_entry x (fn (i,(preds,succs)) => (i, (preds, Keys.remove y succs))) 239 else G; 240 241fun diff_edges G1 G2 = 242 fold_graph (fn (x, (_, (_, succs))) => 243 Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 []; 244 245fun edges G = diff_edges G empty; 246 247 248(* dest and make *) 249 250fun dest G = 251 fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G []; 252 253fun make entries = 254 empty 255 |> foldl' (new_node o fst) entries 256 |> foldl' 257 (fn ((x, _), ys) => foldl' (fn y => add_edge (x, y)) ys) entries 258 259(* join and merge *) 260 261fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); 262 263fun join f (G1 as Graph tab1, G2 as Graph tab2) = 264 let 265 fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) 266 in 267 if pointer_eq (G1, G2) then G1 268 else foldl' add_edge 269 (edges G2) 270 (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2))) 271 end; 272 273fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) = 274 let 275 fun eq_node (i1, _) (i2, _) = eq i1 i2 276 in 277 if pointer_eq (G1, G2) then G1 278 else foldl' 279 add 280 (edges G2) 281 (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2))) 282 end; 283 284fun merge eq GG = gen_merge add_edge eq GG; 285 286 287(* irreducible paths -- Hasse diagram *) 288 289fun irreducible_preds G X path z = 290 let 291 fun red x x' = is_edge G (x, x') andalso not (eq_key x' z); 292 fun irreds [] xs' = xs' 293 | irreds (x :: xs) xs' = 294 if not (Keys.member X x) orelse eq_key x z orelse 295 op_mem eq_key x path orelse 296 exists (red x) xs orelse exists (red x) xs' 297 then irreds xs xs' 298 else irreds xs (x :: xs'); 299 in irreds (immediate_preds G z) [] end; 300 301fun irreducible_paths G (x, y) = 302 let 303 val (_, X) = reachable (imm_succs G) [x]; 304 fun paths path z = 305 if eq_key x z then cons (z :: path) 306 else foldl' (paths (z :: path)) (irreducible_preds G X path z) 307 in 308 if eq_key x y andalso not (is_edge G (x, x)) then [[]] 309 else paths [] y [] 310 end; 311 312 313(* maintain acyclic graphs *) 314 315exception CYCLES of key list list; 316 317fun add_edge_acyclic (x, y) G = 318 if is_edge G (x, y) then G 319 else 320 (case irreducible_paths G (y, x) of 321 [] => add_edge (x, y) G 322 | cycles => raise CYCLES (map (cons x) cycles)); 323 324fun add_deps_acyclic (y, xs) = 325 foldl' (fn x => add_edge_acyclic (x, y)) xs; 326 327fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; 328 329fun topological_order G = minimals G |> all_succs G; 330 331 332(* maintain transitive acyclic graphs *) 333 334fun add_edge_trans_acyclic (x, y) G = 335 add_edge_acyclic (x, y) G 336 |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); 337 338fun merge_trans_acyclic eq (G1, G2) = 339 if pointer_eq (G1, G2) then G1 340 else 341 merge_acyclic eq (G1, G2) 342 |> foldl' add_edge_trans_acyclic (diff_edges G1 G2) 343 |> foldl' add_edge_trans_acyclic (diff_edges G2 G1); 344 345 346(* schedule acyclic graph *) 347 348exception DEP of key * key; 349 350fun schedule f G = 351 let 352 val xs = topological_order G; 353 val results = (xs, Table.empty) ||-> foldl' (fn x => fn tab => 354 let 355 val a = get_node G x; 356 val deps = immediate_preds G x |> map (fn y => 357 (case Table.lookup tab y of 358 SOME b => (y, b) 359 | NONE => raise DEP (x, y))); 360 in Table.update (x, f deps (x, a)) tab end); 361 in map (valOf o Table.lookup results) xs end; 362 363 364(*final declarations of this structure!*) 365val map = map_nodes; 366val fold = fold_graph; 367 368end; 369