Run-length encoding in Idris

rle.idr

rep : (n : Nat) -> a -> List a
rep Z x = []
rep (S k) x = x :: rep k x

data RLE : List Char -> Type where
     REnd : RLE []
     RChar : (n : Nat) -> (c : Char) -> (rs : RLE xs) -> RLE (rep n c ++ xs)

rle : (xs : List Char) -> RLE xs
rle [] = REnd
rle (x :: xs) with (rle xs)
  rle (x :: []) | REnd = RChar 1 x REnd
  rle (x :: (rep n c ++ ys)) | (RChar n c rs) with (decEq x c)
    rle (x :: (rep n x ++ ys)) | (RChar n x rs) | (Yes refl) = RChar (S n) x rs
    rle (x :: (rep n c ++ ys)) | (RChar n c rs) | (No f) = RChar 1 x (RChar n c rs)

data Singleton : (v : a) -> Type where
     MkSingleton : (v : a) -> Singleton v

unrle : RLE xs -> Singleton xs
unrle REnd = MkSingleton []
unrle (RChar n c rs) with (unrle rs)
  unrle (RChar n c rs) | (MkSingleton xs) = MkSingleton (rep n c ++ xs)