--- 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 **)