@@ -130,7 +130,7 @@ intersperse sep [] = []
130130intersperse sep (x::xs) = x :: intersperse' sep xs
131131 where
132132 intersperse' : a -> Vect n a -> Vect (n + n) a
133− intersperse' sep [] = []
133+ intersperse' sep [] = []
134134 intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
135135
136136--------------------------------------------------------------------------------
@@ -222,15 +222,24 @@ instance Functor (Vect n) where
222222 map f [] = []
223223 map f (x::xs) = f x :: map f xs
224224
225−-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
226−--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
227−--mapMaybe f [] = (_ ** [])
228−--mapMaybe f (x::xs) = mapMaybe' (f x)
229−-- XXX: working around the type restrictions on case statements
230−-- where
231−-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)
232−-- mapMaybe' Nothing (n ** tail) = (n ** tail)
233−-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)
225+
226+||| Map a partial function across a vector, returning those elements for which
227+||| the function had a value.
228+|||
229+||| The first projection of the resulting pair (ie the length) will always be
230+||| at most the length of the input vector. This is not, however, guaranteed
231+||| by the type.
232+|||
233+||| @ f the partial function (expressed by returning `Maybe`)
234+||| @ xs the vector to check for results
235+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)
236+mapMaybe f [] = (_ ** [])
237+mapMaybe f (x::xs) =
238+ let (len ** ys) = mapMaybe f xs
239+ in case f x of
240+ Just y => (S len ** y :: ys)
241+ Nothing => ( len ** ys)
242+
234243
235244--------------------------------------------------------------------------------
236245-- Folds