src/Pure/library.ML
changeset 15760 1ca99038c847
parent 15745 33bb955b2e73
child 15965 f422f8283491
     1.1 --- a/src/Pure/library.ML	Sun Apr 17 19:39:11 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Apr 17 19:39:39 2005 +0200
     1.3 @@ -83,10 +83,10 @@
     1.4    val single: 'a -> 'a list
     1.5    val append: 'a list -> 'a list -> 'a list
     1.6    val apply: ('a -> 'a) list -> 'a -> 'a
     1.7 -  val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.8    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.9    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.10    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.11 +  val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.12    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.13    val unflat: 'a list list -> 'b list -> 'b list list
    1.14    val splitAt: int * 'a list -> 'a list * 'a list
    1.15 @@ -174,6 +174,8 @@
    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 insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.20 +  val remove: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.21    val union: ''a list * ''a list -> ''a list
    1.22    val union_int: int list * int list -> int list
    1.23    val union_string: string list * string list -> string list
    1.24 @@ -192,8 +194,6 @@
    1.25    val \\ : ''a list * ''a list -> ''a list
    1.26    val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
    1.27    val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.28 -  val gen_remove: ('a * 'b -> bool) -> 'b -> 'a list -> 'a list
    1.29 -  val remove: ''a -> ''a list -> ''a list
    1.30    val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.31    val distinct: ''a list -> ''a list
    1.32    val findrep: ''a list -> ''a list
    1.33 @@ -445,8 +445,7 @@
    1.34  
    1.35  fun append xs ys = xs @ ys;
    1.36  
    1.37 -(* tail recursive version *)
    1.38 -fun rev_append xs ys = List.revAppend(xs,ys);
    1.39 +fun rev_append xs ys = List.revAppend (xs, ys);
    1.40  
    1.41  fun apply [] x = x
    1.42    | apply (f :: fs) x = apply fs (f x);
    1.43 @@ -454,6 +453,19 @@
    1.44  
    1.45  (* fold *)
    1.46  
    1.47 +fun fold _ [] y = y
    1.48 +  | fold f (x :: xs) y = fold f xs (f x y);
    1.49 +
    1.50 +fun fold_rev _ [] y = y
    1.51 +  | fold_rev f (x :: xs) y = f x (fold_rev f xs y);
    1.52 +
    1.53 +fun foldl_map _ (x, []) = (x, [])
    1.54 +  | foldl_map f (x, y :: ys) =
    1.55 +      let
    1.56 +        val (x', y') = f (x, y);
    1.57 +        val (x'', ys') = foldl_map f (x', ys);
    1.58 +      in (x'', y' :: ys') end;
    1.59 +
    1.60  (*the following versions of fold are designed to fit nicely with infixes*)
    1.61  
    1.62  (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
    1.63 @@ -477,17 +489,8 @@
    1.64          | itr (x::l) = f(x, itr l)
    1.65    in  itr l  end;
    1.66  
    1.67 -fun fold f xs y = foldl (fn (y', x) => f x y') (y, xs);
    1.68 -fun fold_rev f xs y = foldr (fn (x, y') => f x y') (xs, y);
    1.69 +fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
    1.70  
    1.71 -fun foldl_map _ (x, []) = (x, [])
    1.72 -  | foldl_map f (x, y :: ys) =
    1.73 -      let
    1.74 -        val (x', y') = f (x, y);
    1.75 -        val (x'', ys') = foldl_map f (x', ys);
    1.76 -      in (x'', y' :: ys') end;
    1.77 -
    1.78 -fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
    1.79  
    1.80  (* basic list functions *)
    1.81  
    1.82 @@ -845,6 +848,9 @@
    1.83  fun gen_mem eq (x, []) = false
    1.84    | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    1.85  
    1.86 +(*insert and remove*)
    1.87 +fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs;
    1.88 +fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs;
    1.89  
    1.90  (*insertion into list if not already there*)
    1.91  fun (x ins xs) = if x mem xs then xs else x :: xs;
    1.92 @@ -856,8 +862,7 @@
    1.93  fun (x ins_string xs) = if x mem_string xs then xs else x :: xs;
    1.94  
    1.95  (*generalized insertion*)
    1.96 -fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
    1.97 -
    1.98 +fun gen_ins eq (x, xs) = insert eq x xs;
    1.99  
   1.100  (*union of sets represented as lists: no repetitions*)
   1.101  fun xs union [] = xs
   1.102 @@ -935,9 +940,6 @@
   1.103  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   1.104  fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
   1.105  
   1.106 -fun gen_remove eq x xs = gen_rem eq (xs, x);
   1.107 -fun remove x xs = gen_rem (op =) (xs, x);
   1.108 -
   1.109  (*makes a list of the distinct members of the input; preserves order, takes
   1.110    first of equal elements*)
   1.111  fun gen_distinct eq lst =