git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1609 from johnny-john/vectfuncs
8ad2124David Christiansen
libs/prelude/Prelude/Vect.idr+43
compare with master
unifiedsplit
@@ -111,6 +111,31 @@ drop : (n : Nat) -> Vect (n + m) a -> Vect m a
111drop Z xs = xs
111drop Z xs = xs
112drop (S k) (x :: xs) = drop k xs
112drop (S k) (x :: xs) = drop k xs
113
113
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+
114--------------------------------------------------------------------------------
139--------------------------------------------------------------------------------
115-- Transformations
140-- Transformations
116--------------------------------------------------------------------------------
141--------------------------------------------------------------------------------
@@ -401,6 +426,15 @@ nubBy = nubBy' []
401nub : Eq a => Vect n a -> (p ** Vect p a)
426nub : Eq a => Vect n a -> (p ** Vect p a)
402nub = nubBy (==)
427nub = nubBy (==)
403
428
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+
404--------------------------------------------------------------------------------
438--------------------------------------------------------------------------------
405-- Splitting and breaking lists
439-- Splitting and breaking lists
406--------------------------------------------------------------------------------
440--------------------------------------------------------------------------------
@@ -413,6 +447,15 @@ nub = nubBy (==)
413splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
447splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
414splitAt n xs = (take n xs, drop n xs)
448splitAt n xs = (take n xs, drop n xs)
415
449
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+
416--------------------------------------------------------------------------------
459--------------------------------------------------------------------------------
417-- Predicates
460-- Predicates
418--------------------------------------------------------------------------------
461--------------------------------------------------------------------------------