src/Pure/General/graph.ML
changeset 14161 73ad4884441f
parent 12451 0224f472be71
child 14793 32d94d1e4842
equal deleted inserted replaced
14160:6750ff1dfc32 14161:73ad4884441f
    20   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    20   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    21   val imm_preds: 'a T -> key -> key list
    21   val imm_preds: 'a T -> key -> key list
    22   val imm_succs: 'a T -> key -> key list
    22   val imm_succs: 'a T -> key -> key list
    23   val all_preds: 'a T -> key list -> key list
    23   val all_preds: 'a T -> key list -> key list
    24   val all_succs: 'a T -> key list -> key list
    24   val all_succs: 'a T -> key list -> key list
       
    25   val strong_conn: 'a T -> key list list
    25   val find_paths: 'a T -> key * key -> key list list
    26   val find_paths: 'a T -> key * key -> key list list
    26   val new_node: key * 'a -> 'a T -> 'a T
    27   val new_node: key * 'a -> 'a T -> 'a T
    27   val del_nodes: key list -> 'a T -> 'a T
    28   val del_nodes: key list -> 'a T -> 'a T
    28   val edges: 'a T -> (key * key) list
    29   val edges: 'a T -> (key * key) list
    29   val add_edge: key * key -> 'a T -> 'a T
    30   val add_edge: key * key -> 'a T -> 'a T
    30   val del_edge: key * key -> 'a T -> 'a T
    31   val del_edge: key * key -> 'a T -> 'a T
    31   exception CYCLES of key list list
    32   exception CYCLES of key list list
    32   val add_edge_acyclic: key * key -> 'a T -> 'a T
    33   val add_edge_acyclic: key * key -> 'a T -> 'a T
    33   val add_deps_acyclic: key * key list -> 'a T -> 'a T
    34   val add_deps_acyclic: key * key list -> 'a T -> 'a T
    34   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    35   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
       
    36   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    35 end;
    37 end;
    36 
    38 
    37 functor GraphFun(Key: KEY): GRAPH =
    39 functor GraphFun(Key: KEY): GRAPH =
    38 struct
    40 struct
    39 
    41 
   101 (* reachability *)
   103 (* reachability *)
   102 
   104 
   103 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   105 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
   104 fun reachable next xs =
   106 fun reachable next xs =
   105   let
   107   let
   106     fun reach ((rs, R), x) =
   108     fun reach ((R, rs), x) =
   107       if x mem_keys R then (rs, R)
   109       if x mem_keys R then (R, rs)
   108       else apfst (cons x) (reachs ((rs, x ins_keys R), next x))
   110       else apsnd (cons x) (reachs ((x ins_keys R, rs), next x))
   109     and reachs R_xs = foldl reach R_xs;
   111     and reachs R_xs = foldl reach R_xs;
   110   in reachs (([], empty_keys), xs) end;
   112   in foldl_map (reach o apfst (rpair [])) (empty_keys, xs) end;
   111 
   113 
   112 (*immediate*)
   114 (*immediate*)
   113 fun imm_preds G = #1 o #2 o get_entry G;
   115 fun imm_preds G = #1 o #2 o get_entry G;
   114 fun imm_succs G = #2 o #2 o get_entry G;
   116 fun imm_succs G = #2 o #2 o get_entry G;
   115 
   117 
   116 (*transitive*)
   118 (*transitive*)
   117 fun all_preds G = #1 o reachable (imm_preds G);
   119 fun all_preds G = flat o snd o reachable (imm_preds G);
   118 fun all_succs G = #1 o reachable (imm_succs G);
   120 fun all_succs G = flat o snd o reachable (imm_succs G);
       
   121 
       
   122 (* strongly connected components; see: David King and John Launchbury, *)
       
   123 (* "Structuring Depth First Search Algorithms in Haskell"              *)
       
   124 
       
   125 fun strong_conn G = filter_out null (snd (reachable (imm_preds G)
       
   126   (flat (rev (snd (reachable (imm_succs G) (keys G)))))));
   119 
   127 
   120 
   128 
   121 (* paths *)
   129 (* paths *)
   122 
   130 
   123 fun find_paths G (x, y) =
   131 fun find_paths G (x, y) =
   124   let
   132   let
   125     val (_, X) = reachable (imm_succs G) [x];
   133     val (X, _) = reachable (imm_succs G) [x];
   126     fun paths ps p =
   134     fun paths ps p =
   127       if not (null ps) andalso eq_key (p, x) then [p :: ps]
   135       if not (null ps) andalso eq_key (p, x) then [p :: ps]
   128       else if p mem_keys X andalso not (p mem_key ps)
   136       else if p mem_keys X andalso not (p mem_key ps)
   129       then flat (map (paths (p :: ps)) (imm_preds G p))
   137       then flat (map (paths (p :: ps)) (imm_preds G p))
   130       else [];
   138       else [];
   173   foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
   181   foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
   174 
   182 
   175 
   183 
   176 (* merge_acyclic *)
   184 (* merge_acyclic *)
   177 
   185 
   178 fun merge_acyclic eq (Graph tab1, G2 as Graph tab2) =
   186 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   179   foldl (fn (G, xy) => add_edge_acyclic xy G)
   187   foldl (fn (G, xy) => add xy G)
   180     (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
   188     (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
       
   189 
       
   190 fun merge_acyclic eq p = gen_merge add_edge_acyclic eq p;
       
   191 fun merge eq p = gen_merge add_edge eq p;
   181 
   192 
   182 
   193 
   183 end;
   194 end;
   184 
   195 
   185 
   196