0 | module Data.List.Extra
 1 |
 2 | %default total
 3 |
 4 | ||| Analogous to `map` for `List`, but the function is applied to the index of
 5 | ||| the element as first argument (counting from 0), and the element itself as
 6 | ||| second argument.
 7 | public export
 8 | mapi : ((n : Nat) -> (a -> b))
 9 |     -> (xs : List a)
10 |     -> List b
11 | mapi = h 0 where
12 |   h : Nat -> ((n : Nat) -> (a -> b))
13 |    -> (xs : List a)
14 |    -> List b
15 |   h i f [] = []
16 |   h i f (x :: xs) = f i x :: h (S i) f xs
17 |
18 | ||| Applied to a predicate and a list, returns the list of those elements that
19 | ||| satisfy the predicate with corresponding indices in a stand-alone list.
20 | ||| See also `Data.List.Extra.filterLoc'`.
21 | public export
22 | filterLoc : (a -> Bool) -> List a -> (List a, List Nat)
23 | filterLoc p = h 0 where
24 |   h : Nat -> List a -> (List a, List Nat)
25 |   h _ [] = ([], [])
26 |   h lvl (x :: xs) = if p x
27 |       then let (ms, ns) = h (S lvl) xs in (x :: ms, lvl :: ns)
28 |       else h (S lvl) xs
29 |
30 | ||| Applied to a predicate and a list, returns the list of those elements that
31 | ||| satisfy the predicate with corresponding indices.
32 | public export
33 | filterLoc' : (a -> Bool) -> List a -> List (a, Nat)
34 | filterLoc' p = h 0 where
35 |   h : Nat -> List a -> List (a, Nat)
36 |   h _ [] = []
37 |   h lvl (x :: xs) = if p x
38 |     then (x, lvl) :: h (S lvl) xs
39 |     else             h (S lvl) xs
40 |