@@ -205,16 +205,31 @@ zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
205zipWith f [] [] = []
205zipWith f [] [] = []
206zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
206zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
208+||| Combine three equal-length vectors into a vector with some function
209+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
210+zipWith3 f [] [] [] = []
211+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 xs ys zs
208||| Combine two equal-length vectors pairwise
213||| Combine two equal-length vectors pairwise
209zip : Vect n a -> Vect n b -> Vect n (a, b)
214zip : Vect n a -> Vect n b -> Vect n (a, b)
210zip = zipWith (\x => \y => (x,y))
215zip = zipWith (\x => \y => (x,y))
217+||| Combine three equal-length vectors elementwise into a vector of tuples
218+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)
219+zip3 = zipWith3 (\x => \y => \z => (x,y,z))
212||| Convert a vector of pairs to a pair of vectors
221||| Convert a vector of pairs to a pair of vectors
213unzip : Vect n (a, b) -> (Vect n a, Vect n b)
222unzip : Vect n (a, b) -> (Vect n a, Vect n b)
214unzip [] = ([], [])
223unzip [] = ([], [])
215unzip ((l, r)::xs) with (unzip xs)
224unzip ((l, r)::xs) with (unzip xs)
216 | (lefts, rights) = (l::lefts, r::rights)
225 | (lefts, rights) = (l::lefts, r::rights)
227+||| Convert a vector of three-tuples to a triplet of vectors
228+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)
230+unzip3 [(l,c,r):xs] with (unzip3 xs) |
231+ | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
218--------------------------------------------------------------------------------
233--------------------------------------------------------------------------------
219-- Equality
234-- Equality
220--------------------------------------------------------------------------------
235--------------------------------------------------------------------------------