120 (* reachability *) |
120 (* reachability *) |
121 |
121 |
122 (*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
122 (*nodes reachable from xs -- topologically sorted for acyclic graphs*) |
123 fun reachable next xs = |
123 fun reachable next xs = |
124 let |
124 let |
125 fun reach ((R, rs), x) = |
125 fun reach x (rs, R) = |
126 if x mem_keys R then (R, rs) |
126 if x mem_keys R then (rs, R) |
127 else apsnd (cons x) (reachs ((x ins_keys R, rs), next x)) |
127 else apfst (cons x) (fold reach (next x) (rs, x ins_keys R)) |
128 and reachs R_xs = Library.foldl reach R_xs; |
128 in fold_map (fn x => reach x o pair []) xs empty_keys end; |
129 in foldl_map (reach o apfst (rpair [])) (empty_keys, xs) end; |
|
130 |
129 |
131 (*immediate*) |
130 (*immediate*) |
132 fun imm_preds G = #1 o #2 o get_entry G; |
131 fun imm_preds G = #1 o #2 o get_entry G; |
133 fun imm_succs G = #2 o #2 o get_entry G; |
132 fun imm_succs G = #2 o #2 o get_entry G; |
134 |
133 |
135 (*transitive*) |
134 (*transitive*) |
136 fun all_preds G = List.concat o snd o reachable (imm_preds G); |
135 fun all_preds G = List.concat o fst o reachable (imm_preds G); |
137 fun all_succs G = List.concat o snd o reachable (imm_succs G); |
136 fun all_succs G = List.concat o fst o reachable (imm_succs G); |
138 |
137 |
139 (*strongly connected components; see: David King and John Launchbury, |
138 (*strongly connected components; see: David King and John Launchbury, |
140 "Structuring Depth First Search Algorithms in Haskell"*) |
139 "Structuring Depth First Search Algorithms in Haskell"*) |
141 fun strong_conn G = filter_out null (snd (reachable (imm_preds G) |
140 fun strong_conn G = filter_out null (fst (reachable (imm_preds G) |
142 (List.concat (rev (snd (reachable (imm_succs G) (keys G))))))); |
141 (List.concat (rev (fst (reachable (imm_succs G) (keys G))))))); |
143 |
142 |
144 (*subgraph induced by node subset*) |
143 (*subgraph induced by node subset*) |
145 fun subgraph keys (Graph tab) = |
144 fun subgraph keys (Graph tab) = |
146 let |
145 let |
147 val select = member eq_key keys; |
146 val select = member eq_key keys; |
153 |
152 |
154 (* paths *) |
153 (* paths *) |
155 |
154 |
156 fun find_paths G (x, y) = |
155 fun find_paths G (x, y) = |
157 let |
156 let |
158 val (X, _) = reachable (imm_succs G) [x]; |
157 val (_, X) = reachable (imm_succs G) [x]; |
159 fun paths ps p = |
158 fun paths ps p = |
160 if not (null ps) andalso eq_key (p, x) then [p :: ps] |
159 if not (null ps) andalso eq_key (p, x) then [p :: ps] |
161 else if p mem_keys X andalso not (p mem_key ps) |
160 else if p mem_keys X andalso not (p mem_key ps) |
162 then List.concat (map (paths (p :: ps)) (imm_preds G p)) |
161 then List.concat (map (paths (p :: ps)) (imm_preds G p)) |
163 else []; |
162 else []; |