tuned;
authorwenzelm
Mon Jan 25 20:35:19 1999 +0100 (1999-01-25)
changeset 6152bc1e27bcc195
parent 6151 5892fdda22c9
child 6153 bff90585cce5
tuned;
src/Pure/General/graph.ML
     1.1 --- a/src/Pure/General/graph.ML	Sun Jan 24 11:33:54 1999 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Mon Jan 25 20:35:19 1999 +0100
     1.3 @@ -21,11 +21,11 @@
     1.4    val all_succs: 'a T -> key list -> key list
     1.5    val find_paths: 'a T -> key * key -> key list list
     1.6    exception DUPLICATE of key
     1.7 -  val add_node: key * 'a -> 'a T -> 'a T
     1.8 +  val new_node: key * 'a -> 'a T -> 'a T
     1.9    val add_edge: key * key -> 'a T -> 'a T
    1.10 +  val del_edge: key * key -> 'a T -> 'a T
    1.11    exception CYCLES of key list list
    1.12    val add_edge_acyclic: key * key -> 'a T -> 'a T
    1.13 -  val derive_node: key * 'a -> key list -> 'a T -> 'a T
    1.14  end;
    1.15  
    1.16  functor GraphFun(Key: KEY): GRAPH =
    1.17 @@ -44,6 +44,9 @@
    1.18  infix ins_key;
    1.19  val op ins_key = gen_ins eq_key;
    1.20  
    1.21 +infix del_key;
    1.22 +fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
    1.23 +
    1.24  
    1.25  (* tables and sets of keys *)
    1.26  
    1.27 @@ -123,13 +126,19 @@
    1.28  
    1.29  exception DUPLICATE of key;
    1.30  
    1.31 -fun add_node (x, info) (Graph tab) =
    1.32 +fun new_node (x, info) (Graph tab) =
    1.33    Graph (Table.update_new ((x, (info, ([], []))), tab)
    1.34      handle Table.DUP key => raise DUPLICATE key);
    1.35  
    1.36 -fun add_edge (x, y) G =
    1.37 -  G |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs)))
    1.38 -    |> map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
    1.39 +
    1.40 +fun add_edge (x, y) =
    1.41 +  map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o
    1.42 +   map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
    1.43 +
    1.44 +fun del_edge (x, y) =
    1.45 +  map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o
    1.46 +   map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));
    1.47 +
    1.48  
    1.49  exception CYCLES of key list list;
    1.50  
    1.51 @@ -138,9 +147,6 @@
    1.52      [] => add_edge (x, y) G
    1.53    | cycles => raise CYCLES (map (cons x) cycles));
    1.54  
    1.55 -fun derive_node (x, y) zs G =
    1.56 -  foldl (fn (H, z) => add_edge_acyclic (z, x) H) (add_node (x, y) G, zs);
    1.57 -
    1.58  
    1.59  end;
    1.60