
  0 | module Data.Compress.Utils.Misc
  1 | 
  2 | import Data.Fin
  3 | import Data.Vect
  4 | import Data.List
  5 | import Data.Bits
  6 | import Data.List1
  7 | import Data.SnocList
  8 | 
  9 | export
 10 | take_last : Nat -> SnocList a -> Maybe (List a)
 11 | take_last = loop Lin where
 12 |   loop : SnocList a -> Nat -> SnocList a -> Maybe (List a)
 13 |   loop acc Z _ = Just (asList acc)
 14 |   loop acc (S n) (init :< last) = loop (acc :< last) n init
 15 |   loop acc _ Lin = Nothing
 16 | 
 17 | export
 18 | stream_concat : Stream (List a) -> Stream a
 19 | stream_concat ([] :: ys) = stream_concat ys
 20 | stream_concat ((x :: xs) :: ys) = x :: stream_concat (xs :: ys)
 21 | 
 22 | export
 23 | index_may : Nat -> List a -> Maybe a
 24 | index_may Z (x :: xs) = Just x
 25 | index_may (S n) (x :: xs) = index_may n xs
 26 | index_may _ [] = Nothing
 27 | 
 28 | export
 29 | count : Ord a => List a -> List (a, Nat)
 30 | count = map (\xs => (head xs, length xs)) . group . sort
 31 |