
  0 | module Data.Filterable.Indexed
  1 | 
  2 | import public Data.Filterable
  3 | import public Data.Functor.Indexed
  4 | 
  5 | 
  6 | ||| An IndFilterable is a Filterable with read-only access to extra
  7 | ||| indexing data.
  8 | public export
  9 | interface (Filterable t, IndFunctor i t) => IndFilterable i t | t where
 10 |   imapMaybe : (i -> a -> Maybe b) -> t a -> t b
 11 | 
 12 | export
 13 | IndFilterable () Maybe where
 14 |   imapMaybe f = mapMaybe (f ())
 15 | 
 16 | 
 17 | -- This is not a conformant implementation of IndFilterable, because
 18 | -- filtering changes the indices, but it's useful functionality.
 19 | export
 20 | enumFilter : (Nat -> a -> Maybe b) -> List a -> List b
 21 | enumFilter f = inner 0 where
 22 |   inner : Nat -> List a -> List b
 23 |   inner _ [] = []
 24 |   inner n (x::xs) = case f n x of
 25 |     Just y => y::inner (n+1) xs
 26 |     Nothing => inner (n+1) xs
 27 |