0 | ||| We can make any collection into an indexed collection by storing
 1 | ||| pairs
 2 | module Data.Indexed.Add
 3 |
 4 | import Data.Witherable.Indexed
 5 |
 6 |
 7 |
 8 | public export
 9 | record Indexed (t : Type -> Type) (i : Type) (a : Type) where
10 |   constructor AddIndex
11 |   unIndex : t (Pair i a)
12 |
13 |
14 | export
15 | (Functor t) => Functor (Indexed t i) where
16 |   map f (AddIndex p) = AddIndex (map f <$> p)
17 |
18 | export
19 | (Functor t) => IndFunctor i (Indexed t i) where
20 |   imap f (AddIndex p) = AddIndex (imap f <$> p)
21 |
22 | export
23 | (Foldable t) => Foldable (Indexed t i) where
24 |   foldr f z (AddIndex p) = foldr (\(_,a), x => f a x) z p
25 |   foldl f z (AddIndex p) = foldl (\x, (_,a) => f x a) z p
26 | --  concatMap f (AddIndex p) = concatMap (f . snd) p
27 |
28 | export
29 | (Functor t, Foldable t) => IndFoldable i (Indexed t i) where
30 |   ifoldr f z (AddIndex p) = foldr (\(i,a), x => f i a x) z p
31 |   ifoldl f z (AddIndex p) = foldl (\x, (i,a) => f x i a) z p
32 |
33 | export
34 | (Traversable t) => Traversable (Indexed t i) where
35 |   traverse f (AddIndex p) = AddIndex <$> traverse (traverse f) p
36 |
37 | export
38 | (Traversable t) => IndTraversable i (Indexed t i) where
39 |   itraverse f (AddIndex p) = AddIndex <$> traverse (itraverse f) p
40 |
41 | export
42 | (Filterable t) => Filterable (Indexed t i) where
43 |   mapMaybe f (AddIndex p) = AddIndex $ mapMaybe (traverse f) p
44 |
45 | export
46 | (Filterable t) => IndFilterable i (Indexed t i) where
47 |   imapMaybe f (AddIndex p) = AddIndex $ mapMaybe (itraverse f) p
48 |
49 | export
50 | (Witherable t) => Witherable (Indexed t i) where
51 |
52 | export
53 | [indWitherableIndexed] (Witherable t) => IndWitherable i (Indexed t i) where
54 |