
  0 | module Data.Foldable.Dependent
  1 | 
  2 | import Data.SortedMap.Dependent
  3 | 
  4 | 
  5 | public export
  6 | interface DepFoldable (0 i : Type) (0 t : (i -> Type) -> Type) | t where
  7 |   dfoldl : {0 v : i -> Type} -> (m -> (x : i) -> v x -> m) -> m -> t v -> m
  8 |   dfoldr : {0 v : i -> Type} -> ((x : i) -> v x -> m -> m) -> m -> t v -> m
  9 | 
 10 |   dconcatMap : Monoid m => {0 v : i -> Type} -> ((x : i) -> v x -> m) -> t v -> m
 11 |   dconcatMap f = dfoldl (\a, x, y => a <+> f x y) neutral
 12 | 
 13 | ||| an alternative implementation, using a right fold instead
 14 | dconcatMap' : {0 i : Type} -> {0 t : (i -> Type) -> Type} -> (DepFoldable i t, Monoid m) => {0 v : i -> Type} -> ((x : i) -> v x -> m) -> t v -> m
 15 | dconcatMap' f = dfoldr (\x, y, a => f x y <+> a) neutral
 16 | 
 17 | export
 18 | dToList : DepFoldable i t => t v -> List (DPair i v)
 19 | dToList = dfoldr (\x, y, l => (x ** y)::l) []
 20 | 
 21 | export
 22 | indepToList : DepFoldable i t => t (const a) -> List (i, a)
 23 | indepToList = dfoldr (\x, y, l => (x, y)::l) []
 24 | 
 25 | 
 26 | export
 27 | {0 i : Type} -> DepFoldable i (DPair i) where
 28 |   dfoldl f z (x ** y) = f z x y
 29 |   dfoldr f z (x ** y) = f x y z
 30 |   dconcatMap f (x ** y) = f x y
 31 | 
 32 | export
 33 | DepFoldable k (SortedDMap k) where
 34 |   dfoldl f = let
 35 |     g : m -> DPair k v -> m
 36 |     g x (MkDPair k v) = f x k v
 37 |     in foldl g
 38 |   dfoldr f = let
 39 |     g : DPair k v -> m -> m
 40 |     g (MkDPair k v) x = f k v x
 41 |     in foldr g
 42 |   dconcatMap = foldMap
 43 |