src/Pure/General/graph.ML
changeset 18006 535de280c812
parent 17912 410ec3b7e771
child 18126 b74145e46e0d
equal deleted inserted replaced
18005:a444181a45ce 18006:535de280c812
   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 [];