removed obsolete gen_ins/mem;
authorwenzelm
Fri Feb 03 23:12:31 2006 +0100 (2006-02-03)
changeset 1892334f9df073ad9
parent 18922 b05a2952de73
child 18924 83acd39b1bab
removed obsolete gen_ins/mem;
added merge -- supercedes gen_merge_lists';
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Feb 03 23:12:30 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Feb 03 23:12:31 2006 +0100
     1.3 @@ -183,17 +183,16 @@
     1.4    val translate_string: (string -> string) -> string -> string
     1.5  
     1.6    (*lists as sets -- see also Pure/General/ord_list.ML*)
     1.7 +  val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
     1.8 +  val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.9 +  val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.10 +  val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.11    val mem: ''a * ''a list -> bool
    1.12    val mem_int: int * int list -> bool
    1.13    val mem_string: string * string list -> bool
    1.14 -  val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
    1.15    val ins: ''a * ''a list -> ''a list
    1.16    val ins_int: int * int list -> int list
    1.17    val ins_string: string * string list -> string list
    1.18 -  val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
    1.19 -  val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.20 -  val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.21 -  val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.22    val union: ''a list * ''a list -> ''a list
    1.23    val union_int: int list * int list -> int list
    1.24    val union_string: string list * string list -> string list
    1.25 @@ -907,38 +906,27 @@
    1.26  
    1.27  (** lists as sets -- see also Pure/General/ord_list.ML **)
    1.28  
    1.29 -(*membership in a list*)
    1.30 -fun x mem [] = false
    1.31 -  | x mem (y :: ys) = x = y orelse x mem ys;
    1.32 -
    1.33 -(*membership in a list, optimized version for ints*)
    1.34 -fun (x:int) mem_int [] = false
    1.35 -  | x mem_int (y :: ys) = x = y orelse x mem_int ys;
    1.36 +(*canonical member, insert, remove*)
    1.37 +fun member eq list x =
    1.38 +  let
    1.39 +    fun memb [] = false
    1.40 +      | memb (y :: ys) = eq (x, y) orelse memb ys;
    1.41 +  in memb list end;
    1.42  
    1.43 -(*membership in a list, optimized version for strings*)
    1.44 -fun (x:string) mem_string [] = false
    1.45 -  | x mem_string (y :: ys) = x = y orelse x mem_string ys;
    1.46 -
    1.47 -(*generalized membership test*)
    1.48 -fun gen_mem eq (x, []) = false
    1.49 -  | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    1.50 +fun insert eq x xs = if member eq xs x then xs else x :: xs;
    1.51 +fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
    1.52  
    1.53 -(*member, insert, and remove -- with canonical argument order*)
    1.54 -fun member eq xs x = gen_mem eq (x, xs);
    1.55 -fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs;
    1.56 -fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs;
    1.57 -
    1.58 -(*insertion into list if not already there*)
    1.59 -fun (x ins xs) = if x mem xs then xs else x :: xs;
    1.60 +fun merge _ ([], ys) = ys
    1.61 +  | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
    1.62  
    1.63 -(*insertion into list, optimized version for ints*)
    1.64 -fun (x ins_int xs) = if x mem_int xs then xs else x :: xs;
    1.65 +(*old-style infixes*)
    1.66 +fun x mem xs = member (op =) xs x;
    1.67 +fun (x: int) mem_int xs = member (op =) xs x;
    1.68 +fun (x: string) mem_string xs = member (op =) xs x;
    1.69  
    1.70 -(*insertion into list, optimized version for strings*)
    1.71 -fun (x ins_string xs) = if x mem_string xs then xs else x :: xs;
    1.72 -
    1.73 -(*generalized insertion*)
    1.74 -fun gen_ins eq (x, xs) = insert eq x xs;
    1.75 +fun x ins xs = insert (op =) x xs;
    1.76 +fun (x:int) ins_int xs = insert (op =) x xs;
    1.77 +fun (x:string) ins_string xs = insert (op =) x xs;
    1.78  
    1.79  (*union of sets represented as lists: no repetitions*)
    1.80  fun xs union [] = xs
    1.81 @@ -958,7 +946,7 @@
    1.82  (*generalized union*)
    1.83  fun gen_union eq (xs, []) = xs
    1.84    | gen_union eq ([], ys) = ys
    1.85 -  | gen_union eq (x :: xs, ys) = gen_union eq (xs, gen_ins eq (x, ys));
    1.86 +  | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
    1.87  
    1.88  
    1.89  (*intersection*)
    1.90 @@ -979,8 +967,8 @@
    1.91  (*generalized intersection*)
    1.92  fun gen_inter eq ([], ys) = []
    1.93    | gen_inter eq (x::xs, ys) =
    1.94 -      if gen_mem eq (x,ys) then x :: gen_inter eq (xs, ys)
    1.95 -                           else      gen_inter eq (xs, ys);
    1.96 +      if member eq ys x then x :: gen_inter eq (xs, ys)
    1.97 +      else gen_inter eq (xs, ys);
    1.98  
    1.99  
   1.100  (*subset*)
   1.101 @@ -1003,7 +991,7 @@
   1.102  fun eq_set_string ((xs: string list), ys) =
   1.103    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
   1.104  
   1.105 -fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
   1.106 +fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
   1.107  
   1.108  
   1.109  (*removing an element from a list WITHOUT duplicates*)
   1.110 @@ -1014,17 +1002,15 @@
   1.111  
   1.112  (*removing an element from a list -- possibly WITH duplicates*)
   1.113  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   1.114 -fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
   1.115 +fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
   1.116  
   1.117  (*makes a list of the distinct members of the input; preserves order, takes
   1.118    first of equal elements*)
   1.119  fun gen_distinct eq lst =
   1.120    let
   1.121 -    val memb = gen_mem eq;
   1.122 -
   1.123      fun dist (rev_seen, []) = rev rev_seen
   1.124        | dist (rev_seen, x :: xs) =
   1.125 -          if memb (x, rev_seen) then dist (rev_seen, xs)
   1.126 +          if member eq rev_seen x then dist (rev_seen, xs)
   1.127            else dist (x :: rev_seen, xs);
   1.128    in
   1.129      dist ([], lst)
   1.130 @@ -1041,11 +1027,9 @@
   1.131    order, takes first of equal elements*)
   1.132  fun gen_duplicates eq lst =
   1.133    let
   1.134 -    val memb = gen_mem eq;
   1.135 -
   1.136      fun dups (rev_dups, []) = rev rev_dups
   1.137        | dups (rev_dups, x :: xs) =
   1.138 -          if memb (x, rev_dups) orelse not (memb (x, xs)) then
   1.139 +          if member eq rev_dups x orelse not (member eq xs x) then
   1.140              dups (rev_dups, xs)
   1.141            else dups (x :: rev_dups, xs);
   1.142    in
   1.143 @@ -1064,7 +1048,7 @@
   1.144  
   1.145  (** association lists **)
   1.146  
   1.147 -(* lists as tables *)
   1.148 +(* lists as tables -- legacy operations *)
   1.149  
   1.150  fun gen_merge_lists _ xs [] = xs
   1.151    | gen_merge_lists _ [] ys = ys