
  0 | ||| A Foldable that is able to read extra data, the index
  1 | module Data.Foldable.Indexed
  2 | 
  3 | import Data.Vect
  4 | 
  5 | 
  6 | -- I would propose that the ordinary Foldable interface also make
  7 | -- concatMap a method, since whether left folds or right folds are
  8 | -- faster depends on the data structure.
  9 | 
 10 | 
 11 | public export
 12 | interface (Foldable f) => IndFoldable i f | f where
 13 | 
 14 |   ifoldl : (a -> i -> x -> a) -> a -> f x -> a
 15 |   ifoldr : (i -> x -> a -> a) -> a -> f x -> a
 16 | 
 17 |   iconcatMap : Monoid m => (i -> x -> m) -> f x -> m
 18 |   iconcatMap f = ifoldl (\a, i, x => a <+> f i x) neutral
 19 | 
 20 | export
 21 | iconcatMapRight : (IndFoldable i f, Monoid m) => (i -> x -> m) -> f x -> m
 22 | iconcatMapRight f = ifoldr (\i, x, a => f i x <+> a) neutral
 23 | 
 24 | export
 25 | IndFoldable () Maybe where
 26 |   ifoldl f = foldl (\x => f x ())
 27 |   ifoldr f = foldr (f ())
 28 |   iconcatMap f = concatMap (f ())
 29 | 
 30 | export
 31 | IndFoldable a (Pair a) where
 32 |   ifoldl f z (MkPair x y) = f z x y
 33 |   ifoldr f z (MkPair x y) = f x y z
 34 | 
 35 | export
 36 | IndFoldable Nat List where
 37 |   ifoldl f = inner 0 where
 38 |     inner : Nat -> a -> List x -> a
 39 |     inner _ z [] = z
 40 |     inner i z (x::xs) = inner (i+1) (f z i x) xs
 41 |   ifoldr f z = inner 0 where
 42 |     inner : Nat -> List x -> a
 43 |     inner _ [] = z
 44 |     inner i (x::xs) = f i x (inner (i+1) xs)
 45 | 
 46 | export
 47 | IndFoldable (Fin k) (Vect k) where
 48 |   ifoldl f a [] = a
 49 |   ifoldl f a (x::xs) = ifoldl (\y, i => f y (FS i)) (f a FZ x) xs
 50 |   ifoldr f a [] = a
 51 |   ifoldr f a (x::xs) = f FZ x (ifoldr (f . FS) a xs)
 52 |