@@ -130,7 +130,7 @@ intersperse sep [] = []
130intersperse sep (x::xs) = x :: intersperse' sep xs
130intersperse sep (x::xs) = x :: intersperse' sep xs
132 intersperse' : a -> Vect n a -> Vect (n + n) a
132 intersperse' : a -> Vect n a -> Vect (n + n) a
133− intersperse' sep [] = []
133+ intersperse' sep [] = []
134 intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
134 intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
136--------------------------------------------------------------------------------
136--------------------------------------------------------------------------------
@@ -222,15 +222,24 @@ instance Functor (Vect n) where
222 map f [] = []
222 map f [] = []
223 map f (x::xs) = f x :: map f xs
223 map f (x::xs) = f x :: map f xs
225−-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
225+
226−--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
226+||| Map a partial function across a vector, returning those elements for which
227−--mapMaybe f [] = (_ ** [])
227+||| the function had a value.
228−--mapMaybe f (x::xs) = mapMaybe' (f x)
228+|||
229−-- XXX: working around the type restrictions on case statements
229+||| The first projection of the resulting pair (ie the length) will always be
230−-- where
230+||| at most the length of the input vector. This is not, however, guaranteed
231−-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)
231+||| by the type.
232−-- mapMaybe' Nothing (n ** tail) = (n ** tail)
232+|||
233−-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)
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 [] = (_ ** [])
238+ let (len ** ys) = mapMaybe f xs
240+ Just y => (S len ** y :: ys)
241+ Nothing => ( len ** ys)
235--------------------------------------------------------------------------------
244--------------------------------------------------------------------------------