src/Pure/library.ML
changeset 33955 fff6f11b1f09
parent 33206 fee21bb23d22
child 34059 f3f0e20923a7
     1.1 --- a/src/Pure/library.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -81,6 +81,8 @@
     1.4    val filter: ('a -> bool) -> 'a list -> 'a list
     1.5    val filter_out: ('a -> bool) -> 'a list -> 'a list
     1.6    val map_filter: ('a -> 'b option) -> 'a list -> 'b list
     1.7 +  val take: int -> 'a list -> 'a list
     1.8 +  val drop: int -> 'a list -> 'a list
     1.9    val chop: int -> 'a list -> 'a list * 'a list
    1.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.11    val nth: 'a list -> int -> 'a
    1.12 @@ -224,8 +226,6 @@
    1.13    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    1.14    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.15    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.16 -  val take: int * 'a list -> 'a list
    1.17 -  val drop: int * 'a list -> 'a list
    1.18    val last_elem: 'a list -> 'a
    1.19  end;
    1.20  
    1.21 @@ -423,20 +423,20 @@
    1.22  fun filter_out f = filter (not o f);
    1.23  val map_filter = List.mapPartial;
    1.24  
    1.25 +fun take (0: int) xs = []
    1.26 +  | take _ [] = []
    1.27 +  | take n (x :: xs) =
    1.28 +      if n > 0 then x :: take (n - 1) xs else [];
    1.29 +
    1.30 +fun drop (0: int) xs = xs
    1.31 +  | drop _ [] = []
    1.32 +  | drop n (x :: xs) =
    1.33 +      if n > 0 then drop (n - 1) xs else x :: xs;
    1.34 +
    1.35  fun chop (0: int) xs = ([], xs)
    1.36    | chop _ [] = ([], [])
    1.37    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.38  
    1.39 -(*take the first n elements from a list*)
    1.40 -fun take (n: int, []) = []
    1.41 -  | take (n, x :: xs) =
    1.42 -      if n > 0 then x :: take (n - 1, xs) else [];
    1.43 -
    1.44 -(*drop the first n elements from a list*)
    1.45 -fun drop (n: int, []) = []
    1.46 -  | drop (n, x :: xs) =
    1.47 -      if n > 0 then drop (n - 1, xs) else x :: xs;
    1.48 -
    1.49  fun dropwhile P [] = []
    1.50    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
    1.51