added chop (sane version of splitAt);
authorwenzelm
Sat Feb 11 17:17:45 2006 +0100 (2006-02-11)
changeset 19011d1c3294ca417
parent 19010 fef9e4881e83
child 19012 2577ac76cdc6
added chop (sane version of splitAt);
added prefixes, suffixes;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Feb 11 14:25:23 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Feb 11 17:17:45 2006 +0100
     1.3 @@ -113,6 +113,7 @@
     1.4    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.5    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     1.6    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
     1.7 +  val chop: int -> 'a list -> 'a list * 'a list
     1.8    val splitAt: int * 'a list -> 'a list * 'a list
     1.9    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.10    val nth: 'a list -> int -> 'a
    1.11 @@ -141,7 +142,9 @@
    1.12    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.13    val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.14    val prefixes1: 'a list -> 'a list list
    1.15 +  val prefixes: 'a list -> 'a list list
    1.16    val suffixes1: 'a list -> 'a list list
    1.17 +  val suffixes: 'a list -> 'a list list
    1.18  
    1.19    (*integers*)
    1.20    val gcd: IntInf.int * IntInf.int -> IntInf.int
    1.21 @@ -565,6 +568,12 @@
    1.22  
    1.23  (* basic list functions *)
    1.24  
    1.25 +fun chop 0 xs = ([], xs)
    1.26 +  | chop _ [] = ([], [])
    1.27 +  | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.28 +
    1.29 +fun splitAt (n, xs) = chop n xs;
    1.30 +
    1.31  (*take the first n elements from a list*)
    1.32  fun take (n, []) = []
    1.33    | take (n, x :: xs) =
    1.34 @@ -575,11 +584,6 @@
    1.35    | drop (n, x :: xs) =
    1.36        if n > 0 then drop (n - 1, xs) else x :: xs;
    1.37  
    1.38 -fun splitAt(n,[]) = ([],[])
    1.39 -  | splitAt(n,xs as x::ys) =
    1.40 -      if n>0 then let val (ps,qs) = splitAt(n-1,ys) in (x::ps,qs) end
    1.41 -      else ([],xs)
    1.42 -
    1.43  fun dropwhile P [] = []
    1.44    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
    1.45  
    1.46 @@ -742,8 +746,10 @@
    1.47  fun prefixes1 [] = []
    1.48    | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
    1.49  
    1.50 +fun prefixes xs = [] :: prefixes1 xs;
    1.51 +
    1.52  fun suffixes1 xs = map rev (prefixes1 (rev xs));
    1.53 -
    1.54 +fun suffixes xs = [] :: suffixes1 xs;
    1.55  
    1.56  
    1.57  (** integers **)