improved eq_fst and eq_snd, removed some deprecated stuff
authorhaftmann
Tue Sep 20 08:24:18 2005 +0200 (2005-09-20)
changeset 17498d83af87bbdc5
parent 17497 539319bd6162
child 17499 5274ecba8fea
improved eq_fst and eq_snd, removed some deprecated stuff
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Sep 20 08:23:59 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 20 08:24:18 2005 +0200
     1.3 @@ -38,8 +38,6 @@
     1.4    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
     1.5    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
     1.6    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     1.7 -  val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
     1.8 -  val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
     1.9  
    1.10    (*old options -- invalidated*)
    1.11    datatype invalid = None of invalid
    1.12 @@ -69,8 +67,8 @@
    1.13    val rpair: 'a -> 'b -> 'b * 'a
    1.14    val fst: 'a * 'b -> 'a
    1.15    val snd: 'a * 'b -> 'b
    1.16 -  val eq_fst: (''a * 'b) * (''a * 'c) -> bool
    1.17 -  val eq_snd: ('a * ''b) * ('c * ''b) -> bool
    1.18 +  val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    1.19 +  val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    1.20    val swap: 'a * 'b -> 'b * 'a
    1.21    val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
    1.22    val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
    1.23 @@ -268,8 +266,6 @@
    1.24    val pwd: unit -> string
    1.25  
    1.26    (*misc*)
    1.27 -  val make_keylist: ('a -> 'b) -> 'a list -> ('a * 'b) list
    1.28 -  val keyfilter: ('a * ''b) list -> ''b -> 'a list
    1.29    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
    1.30    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
    1.31    val gensym: string -> string
    1.32 @@ -337,10 +333,6 @@
    1.33          | rep (n, x) = rep (n - 1, f x)
    1.34    in rep (n, x) end;
    1.35  
    1.36 -(*application of (infix) operator to its left or right argument*)
    1.37 -fun apl (x, f) y = f (x, y);
    1.38 -fun apr (f, y) x = f (x, y);
    1.39 -
    1.40  
    1.41  (** options **)
    1.42  
    1.43 @@ -407,8 +399,8 @@
    1.44  fun fst (x, y) = x;
    1.45  fun snd (x, y) = y;
    1.46  
    1.47 -fun eq_fst ((x1, _), (x2, _)) = x1 = x2;
    1.48 -fun eq_snd ((_, y1), (_, y2)) = y1 = y2;
    1.49 +fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
    1.50 +fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
    1.51  
    1.52  fun swap (x, y) = (y, x);
    1.53  
    1.54 @@ -1057,8 +1049,8 @@
    1.55  
    1.56  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    1.57  fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
    1.58 -fun merge_alists al = gen_merge_lists eq_fst al;
    1.59 -fun merge_alists' al = gen_merge_lists' eq_fst al;
    1.60 +fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
    1.61 +fun merge_alists' al = gen_merge_lists' (eq_fst (op =)) al;
    1.62  
    1.63  
    1.64  
    1.65 @@ -1258,19 +1250,6 @@
    1.66  
    1.67  (** misc **)
    1.68  
    1.69 -(*use the keyfun to make a list of (x, key) pairs*)
    1.70 -fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
    1.71 -  let fun keypair x = (x, keyfun x)
    1.72 -  in map keypair end;
    1.73 -
    1.74 -(*given a list of (x, key) pairs and a searchkey
    1.75 -  return the list of xs from each pair whose key equals searchkey*)
    1.76 -fun keyfilter [] searchkey = []
    1.77 -  | keyfilter ((x, key) :: pairs) searchkey =
    1.78 -      if key = searchkey then x :: keyfilter pairs searchkey
    1.79 -      else keyfilter pairs searchkey;
    1.80 -
    1.81 -
    1.82  (*Partition list into elements that satisfy predicate and those that don't.
    1.83    Preserves order of elements in both lists.*)
    1.84  val partition = List.partition;