@@ -111,6 +111,31 @@ drop : (n : Nat) -> Vect (n + m) a -> Vect m a
111111drop Z xs = xs
112112drop (S k) (x :: xs) = drop k xs
113113
114+||| Take the longest prefix of a Vect such that all elements satisfy some
115+||| Boolean predicate.
116+|||
117+||| @ p the predicate
118+takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
119+takeWhile p [] = (_ ** [])
120+takeWhile p (x::xs) =
121+ let (len ** ys) = takeWhile p xs
122+ in if p x then
123+ (S len ** x :: ys)
124+ else
125+ (_ ** [])
126+
127+||| Remove the longest prefix of a Vect such that all removed elements satisfy some
128+||| Boolean predicate.
129+|||
130+||| @ p the predicate
131+dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
132+dropWhile p [] = (_ ** [])
133+dropWhile p (x::xs) =
134+ if p x then
135+ dropWhile p xs
136+ else
137+ (_ ** x::xs)
138+
114139--------------------------------------------------------------------------------
115140-- Transformations
116141--------------------------------------------------------------------------------
@@ -401,6 +426,15 @@ nubBy = nubBy' []
401426nub : Eq a => Vect n a -> (p ** Vect p a)
402427nub = nubBy (==)
403428
429+deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)
430+deleteBy _ _ [] = (_ ** [])
431+deleteBy eq x (y::ys) =
432+ let (len ** zs) = deleteBy eq x ys
433+ in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
434+
435+delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)
436+delete = deleteBy (==)
437+
404438--------------------------------------------------------------------------------
405439-- Splitting and breaking lists
406440--------------------------------------------------------------------------------
@@ -413,6 +447,15 @@ nub = nubBy (==)
413447splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
414448splitAt n xs = (take n xs, drop n xs)
415449
450+partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))
451+partition p [] = ((_ ** []), (_ ** []))
452+partition p (x::xs) =
453+ let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
454+ if p x then
455+ ((S leftLen ** x::lefts), (rightLen ** rights))
456+ else
457+ ((leftLen ** lefts), (S rightLen ** x::rights))
458+
416459--------------------------------------------------------------------------------
417460-- Predicates
418461--------------------------------------------------------------------------------