src/Pure/General/graph.ML
changeset 18921 f47c46d7d654
parent 18133 1d403623dabc
child 18970 d055a29ddd23
     1.1 --- a/src/Pure/General/graph.ML	Fri Feb 03 17:08:03 2006 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Fri Feb 03 23:12:28 2006 +0100
     1.3 @@ -55,9 +55,7 @@
     1.4  
     1.5  val eq_key = equal EQUAL o Key.ord;
     1.6  
     1.7 -infix mem_key;
     1.8 -val op mem_key = gen_mem eq_key;
     1.9 -
    1.10 +val member_key = member eq_key;
    1.11  val remove_key = remove eq_key;
    1.12  
    1.13  
    1.14 @@ -68,11 +66,8 @@
    1.15  
    1.16  val empty_keys = Table.empty: keys;
    1.17  
    1.18 -infix mem_keys;
    1.19 -fun x mem_keys tab = Table.defined (tab: keys) x;
    1.20 -
    1.21 -infix ins_keys;
    1.22 -fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
    1.23 +fun member_keys tab = Table.defined (tab: keys);
    1.24 +fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    1.25  
    1.26  
    1.27  (* graphs *)
    1.28 @@ -126,8 +121,8 @@
    1.29  fun reachable next xs =
    1.30    let
    1.31      fun reach x (rs, R) =
    1.32 -      if x mem_keys R then (rs, R)
    1.33 -      else apfst (cons x) (fold reach (next x) (rs, x ins_keys R))
    1.34 +      if member_keys R x then (rs, R)
    1.35 +      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
    1.36    in fold_map (fn x => reach x o pair []) xs empty_keys end;
    1.37  
    1.38  (*immediate*)
    1.39 @@ -161,7 +156,7 @@
    1.40      val (_, X) = reachable (imm_succs G) [x];
    1.41      fun paths ps p =
    1.42        if not (null ps) andalso eq_key (p, x) then [p :: ps]
    1.43 -      else if p mem_keys X andalso not (p mem_key ps)
    1.44 +      else if member_keys X p andalso not (member_key ps p)
    1.45        then List.concat (map (paths (p :: ps)) (imm_preds G p))
    1.46        else [];
    1.47    in paths [] y end;
    1.48 @@ -184,7 +179,7 @@
    1.49  
    1.50  (* edges *)
    1.51  
    1.52 -fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
    1.53 +fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
    1.54  
    1.55  fun add_edge (x, y) G =
    1.56    if is_edge G (x, y) then G