added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
authorwenzelm
Fri May 21 21:28:01 2004 +0200 (2004-05-21)
changeset 1479332d94d1e4842
parent 14792 b7dac2fae5bb
child 14794 751d5af6d91e
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
src/Pure/General/graph.ML
     1.1 --- a/src/Pure/General/graph.ML	Fri May 21 21:27:42 2004 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Fri May 21 21:28:01 2004 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4    exception DUPS of key list
     1.5    val empty: 'a T
     1.6    val keys: 'a T -> key list
     1.7 +  val dest: 'a T -> (key * key list) list
     1.8 +  val minimals: 'a T -> key list
     1.9 +  val maximals: 'a T -> key list
    1.10    val map_nodes: ('a -> 'b) -> 'a T -> 'b T
    1.11    val get_node: 'a T -> key -> 'a
    1.12    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    1.13 @@ -26,20 +29,21 @@
    1.14    val find_paths: 'a T -> key * key -> key list list
    1.15    val new_node: key * 'a -> 'a T -> 'a T
    1.16    val del_nodes: key list -> 'a T -> 'a T
    1.17 -  val edges: 'a T -> (key * key) list
    1.18 +  val is_edge: 'a T -> key * key -> bool
    1.19    val add_edge: key * key -> 'a T -> 'a T
    1.20    val del_edge: key * key -> 'a T -> 'a T
    1.21 +  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.22    exception CYCLES of key list list
    1.23    val add_edge_acyclic: key * key -> 'a T -> 'a T
    1.24    val add_deps_acyclic: key * key list -> 'a T -> 'a T
    1.25    val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.26 -  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.27 +  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T
    1.28 +  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.29  end;
    1.30  
    1.31  functor GraphFun(Key: KEY): GRAPH =
    1.32  struct
    1.33  
    1.34 -
    1.35  (* keys *)
    1.36  
    1.37  type key = Key.key;
    1.38 @@ -55,9 +59,6 @@
    1.39  infix del_key;
    1.40  fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
    1.41  
    1.42 -infix del_keys;
    1.43 -val op del_keys = foldl (op del_key);
    1.44 -
    1.45  
    1.46  (* tables and sets of keys *)
    1.47  
    1.48 @@ -83,6 +84,12 @@
    1.49  
    1.50  val empty = Graph Table.empty;
    1.51  fun keys (Graph tab) = Table.keys tab;
    1.52 +fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
    1.53 +
    1.54 +fun minimals (Graph tab) =
    1.55 +  Table.foldl (fn (ms, (m, (_, ([], _)))) => m :: ms | (ms, _) => ms) ([], tab);
    1.56 +fun maximals (Graph tab) =
    1.57 +  Table.foldl (fn (ms, (m, (_, (_, [])))) => m :: ms | (ms, _) => ms) ([], tab);
    1.58  
    1.59  fun get_entry (Graph tab) x =
    1.60    (case Table.lookup (tab, x) of
    1.61 @@ -119,9 +126,8 @@
    1.62  fun all_preds G = flat o snd o reachable (imm_preds G);
    1.63  fun all_succs G = flat o snd o reachable (imm_succs G);
    1.64  
    1.65 -(* strongly connected components; see: David King and John Launchbury, *)
    1.66 -(* "Structuring Depth First Search Algorithms in Haskell"              *)
    1.67 -
    1.68 +(*strongly connected components; see: David King and John Launchbury,
    1.69 +  "Structuring Depth First Search Algorithms in Haskell"*)
    1.70  fun strong_conn G = filter_out null (snd (reachable (imm_preds G)
    1.71    (flat (rev (snd (reachable (imm_succs G) (keys G)))))));
    1.72  
    1.73 @@ -150,28 +156,50 @@
    1.74    let
    1.75      fun del (x, (i, (preds, succs))) =
    1.76        if x mem_key xs then None
    1.77 -      else Some (x, (i, (preds del_keys xs, succs del_keys xs)));
    1.78 +      else Some (x, (i, (foldl op del_key (preds, xs), foldl op del_key (succs, xs))));
    1.79    in Graph (Table.make (mapfilter del (Table.dest tab))) end;
    1.80  
    1.81  
    1.82  (* edges *)
    1.83  
    1.84 -fun edges (Graph tab) =
    1.85 -  flat (map (fn (x, (_, (_, succs))) => (map (pair x) succs)) (Table.dest tab));
    1.86 +fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
    1.87 +
    1.88 +fun add_edge (x, y) G =
    1.89 +  if is_edge G (x, y) then G
    1.90 +  else
    1.91 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
    1.92 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
    1.93 +
    1.94 +fun del_edge (x, y) G =
    1.95 +  if is_edge G (x, y) then
    1.96 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)))
    1.97 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y)))
    1.98 +  else G;
    1.99  
   1.100 -fun add_edge (x, y) =
   1.101 -  map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o
   1.102 -   map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
   1.103 +fun diff_edges G1 G2 =
   1.104 +  flat (dest G1 |> map (fn (x, ys) => ys |> mapfilter (fn y =>
   1.105 +    if is_edge G2 (x, y) then None else Some (x, y))));
   1.106 +
   1.107 +fun edges G = diff_edges G empty;
   1.108 +
   1.109 +
   1.110 +(* merge *)
   1.111  
   1.112 -fun del_edge (x, y) =
   1.113 -  map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o
   1.114 -   map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));
   1.115 +fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   1.116 +  let
   1.117 +    fun eq_node ((i1, _), (i2, _)) = eq (i1, i2);
   1.118 +    fun no_edges (i, _) = (i, ([], []));
   1.119 +  in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
   1.120  
   1.121 +fun merge eq GG = gen_merge add_edge eq GG;
   1.122 +
   1.123 +
   1.124 +(* maintain acyclic graphs *)
   1.125  
   1.126  exception CYCLES of key list list;
   1.127  
   1.128  fun add_edge_acyclic (x, y) G =
   1.129 -  if y mem_key imm_succs G x then G
   1.130 +  if is_edge G (x, y) then G
   1.131    else
   1.132      (case find_paths G (y, x) of
   1.133        [] => add_edge (x, y) G
   1.134 @@ -180,16 +208,18 @@
   1.135  fun add_deps_acyclic (y, xs) G =
   1.136    foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
   1.137  
   1.138 +fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   1.139  
   1.140 -(* merge_acyclic *)
   1.141 +
   1.142 +(* maintain transitive acyclic graphs *)
   1.143  
   1.144 -fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
   1.145 -  foldl (fn (G, xy) => add xy G)
   1.146 -    (Graph (Table.merge (fn ((i1, _), (i2, _)) => eq (i1, i2)) (tab1, tab2)), edges G2);
   1.147 +fun add_edge_trans_acyclic (x, y) G =
   1.148 +  add_edge_acyclic (x, y) G |>
   1.149 +  fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
   1.150  
   1.151 -fun merge_acyclic eq p = gen_merge add_edge_acyclic eq p;
   1.152 -fun merge eq p = gen_merge add_edge eq p;
   1.153 -
   1.154 +fun merge_trans_acyclic eq (G1, G2) =
   1.155 +  merge_acyclic eq (G1, G2) |>
   1.156 +  fold add_edge_trans_acyclic (diff_edges G1 G2 @ diff_edges G2 G1);
   1.157  
   1.158  end;
   1.159