
  0 | module Libraries.Data.List.Extra
  1 | 
  2 | import public Data.List
  3 | 
  4 | %default total
  5 | 
  6 | ||| Fetches the element at a given position.
  7 | ||| Returns `Nothing` if the position beyond the list's end.
  8 | public export
  9 | elemAt : List a -> Nat -> Maybe a
 10 | elemAt []        _     = Nothing
 11 | elemAt (l :: _)  Z     = Just l
 12 | elemAt (_ :: ls) (S n) = elemAt ls n
 13 | 
 14 | export
 15 | findBy : (a -> Maybe b) -> List a -> Maybe b
 16 | findBy p [] = Nothing
 17 | findBy p (x :: xs)
 18 |   = case p x of
 19 |       Nothing => findBy p xs
 20 |       Just win => pure win
 21 | 
 22 | export
 23 | findBy' : (a -> Bool) -> List a -> (List a, Maybe a, List a)
 24 | findBy' f [] = ([], Nothing, [])
 25 | findBy' f (x :: xs) =
 26 |   case f x of
 27 |     True  => ([], Just x, xs)
 28 |     False =>
 29 |       let (pre, mb, post) = findBy' f xs in
 30 |       (x :: pre, mb, post)
 31 | 
 32 | ||| Returns first element that matches the predicate and the list without it
 33 | export
 34 | findAndDeleteBy : (a -> Bool) -> List a -> Maybe (a, List a)
 35 | findAndDeleteBy f xs
 36 |   = case findBy' f xs of
 37 |       (pre, Just x, post) => Just (x, pre ++ post)
 38 |       _                   => Nothing
 39 | 
 40 | ||| Compute the difference of two lists by the given predicate.
 41 | ||| Lists are treated as bags.
 42 | export
 43 | diffBy : (a -> a -> Bool)
 44 |       -> List a
 45 |       -> List a
 46 |       -> List a
 47 | diffBy f [] ys = []
 48 | diffBy f (x :: xs) ys =
 49 |   let whole@(pre, mb, post) = findBy' (f x) ys
 50 |       ys' = pre ++ post in
 51 |   case mb of
 52 |     Just _  =>      diffBy f xs ys'
 53 |     Nothing => x :: diffBy f xs ys'
 54 | 
 55 | ||| Remove adjacent duplicates
 56 | export
 57 | dedup : Eq a => List a -> List a
 58 | dedup (a :: xs@(b :: _)) = if a == b then dedup xs else a :: dedup xs
 59 | dedup xs                = xs
 60 | 
 61 | ||| O(n * log(n)). Sort a list and remove duplicates
 62 | export
 63 | sortedNub : Ord a => List a -> List a
 64 | sortedNub = dedup . sort
 65 | 
 66 | export
 67 | lengthDistributesOverAppend
 68 |   : (xs, ys : List a)
 69 |   -> length (xs ++ ys) = length xs + length ys
 70 | lengthDistributesOverAppend [] ys = Refl
 71 | lengthDistributesOverAppend (x :: xs) ys =
 72 |   cong S $ lengthDistributesOverAppend xs ys
 73 |