
  0 | module Data.List.Ex
  1 | 
  2 | import Data.Alternative
  3 | import Data.List
  4 | import Data.List.Lazy
  5 | import Data.Vect
  6 | import Data.Vect.Dependent
  7 | 
  8 | import public Syntax.IHateParens
  9 | 
 10 | %default total
 11 | 
 12 | -- Calculates all pairs except for the pairs of elements with themselves.
 13 | public export
 14 | notTrivPairs : List a -> LazyList (a, a)
 15 | notTrivPairs []      = empty
 16 | notTrivPairs (x::xs) = (x,) <$> fromList xs <|> notTrivPairs xs
 17 | 
 18 | public export
 19 | findDiffPairWhich : (a -> a -> Bool) -> List a -> LazyList (a, a)
 20 | findDiffPairWhich p = filter (uncurry p) . notTrivPairs
 21 | 
 22 | public export
 23 | findConsequentsWhich : (a -> a -> Bool) -> List a -> LazyList (a, a)
 24 | findConsequentsWhich f xs =
 25 |   let xs = Lazy.fromList xs in
 26 |   case tail' xs of
 27 |     Nothing => []
 28 |     Just tl => filter .| uncurry f .| xs `zip` tl
 29 | 
 30 | public export
 31 | infixOf : Eq a => List a -> List a -> Maybe (List a, List a)
 32 | infixOf = map (map snd) .: infixOfBy (\x, y => if x == y then Just () else Nothing)
 33 | 
 34 | public export %inline
 35 | toNatList : Foldable f => f (Fin n) -> List Nat
 36 | toNatList = map finToNat . toList
 37 | 
 38 | public export
 39 | mapI : (xs : List a) -> (Fin xs.length -> a -> b) -> List b
 40 | mapI []      _ = []
 41 | mapI (x::xs) f = f FZ x :: mapI xs (f . FS)
 42 | 
 43 | public export
 44 | mapMaybeI : (xs : List a) -> (Fin xs.length -> a -> Maybe b) -> List b
 45 | mapMaybeI []      _ = []
 46 | mapMaybeI (x::xs) f = maybe id (::) .| f FZ x .| mapMaybeI xs (f . FS)
 47 | 
 48 | public export
 49 | filterI : (xs : List a) -> (Fin xs.length -> a -> Bool) -> List a
 50 | filterI []      _ = []
 51 | filterI (x::xs) f = let fxs = filterI xs $ f . FS in
 52 |                     if f FZ x then x :: fxs else fxs
 53 | 
 54 | public export
 55 | withIndex : (xs : List a) -> List (Fin xs.length, a)
 56 | withIndex []      = []
 57 | withIndex (x::xs) = (FZ, x) :: map (mapFst FS) (withIndex xs)
 58 | 
 59 | public export
 60 | drop' : (xs : List a) -> (count : Fin $ S xs.length) -> List a
 61 | drop' xs      FZ     = xs
 62 | drop' (_::xs) (FS c) = drop' xs c
 63 | 
 64 | export
 65 | inits' : (xs : List a) -> DVect xs.length $ \idx => Vect (S $ finToNat idx) a
 66 | inits' []      = []
 67 | inits' (x::xs) = [x] :: ((x ::) <$> inits' xs)
 68 | 
 69 | export
 70 | findLastIndex : (a -> Bool) -> (xs : List a) -> Maybe $ Fin xs.length
 71 | findLastIndex f []      = Nothing
 72 | findLastIndex f (x::xs) = FS <$> findLastIndex f xs <|> whenT (f x) FZ
 73 | 
 74 | export
 75 | zipV : (xs : List a) -> Vect xs.length b -> List (a, b)
 76 | zipV []      []      = []
 77 | zipV (x::xs) (y::ys) = (x, y) :: zipV xs ys
 78 | 
 79 | export infixr 6 `zipV` -- as `zip`
 80 | 
 81 | export
 82 | lengthConcat : (xs, ys : List a) -> length (xs ++ ys) = length xs + length ys
 83 | lengthConcat []      ys = Refl
 84 | lengthConcat (_::xs) ys = rewrite lengthConcat xs ys in Refl
 85 |