# HG changeset patch # User wenzelm # Date 1139674665 -3600 # Node ID d1c3294ca41788431f5277cd93a995115e86eba5 # Parent fef9e4881e833bb1198ce469c893d45ac047d45f added chop (sane version of splitAt); added prefixes, suffixes; diff -r fef9e4881e83 -r d1c3294ca417 src/Pure/library.ML --- a/src/Pure/library.ML Sat Feb 11 14:25:23 2006 +0100 +++ b/src/Pure/library.ML Sat Feb 11 17:17:45 2006 +0100 @@ -113,6 +113,7 @@ val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd + val chop: int -> 'a list -> 'a list * 'a list val splitAt: int * 'a list -> 'a list * 'a list val dropwhile: ('a -> bool) -> 'a list -> 'a list val nth: 'a list -> int -> 'a @@ -141,7 +142,9 @@ val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list val prefixes1: 'a list -> 'a list list + val prefixes: 'a list -> 'a list list val suffixes1: 'a list -> 'a list list + val suffixes: 'a list -> 'a list list (*integers*) val gcd: IntInf.int * IntInf.int -> IntInf.int @@ -565,6 +568,12 @@ (* basic list functions *) +fun chop 0 xs = ([], xs) + | chop _ [] = ([], []) + | chop n (x :: xs) = chop (n - 1) xs |>> cons x; + +fun splitAt (n, xs) = chop n xs; + (*take the first n elements from a list*) fun take (n, []) = [] | take (n, x :: xs) = @@ -575,11 +584,6 @@ | drop (n, x :: xs) = if n > 0 then drop (n - 1, xs) else x :: xs; -fun splitAt(n,[]) = ([],[]) - | splitAt(n,xs as x::ys) = - if n>0 then let val (ps,qs) = splitAt(n-1,ys) in (x::ps,qs) end - else ([],xs) - fun dropwhile P [] = [] | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys; @@ -742,8 +746,10 @@ fun prefixes1 [] = [] | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); +fun prefixes xs = [] :: prefixes1 xs; + fun suffixes1 xs = map rev (prefixes1 (rev xs)); - +fun suffixes xs = [] :: suffixes1 xs; (** integers **)