git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/test/basic001/basic001a.idr
34 lines 1.0 kB history raw
1module Main
3import Data.Vect
5data RLE : Vect n Char -> Type where
6 REnd : RLE []
7 RChar : {xs : Vect k Char} ->
8 (n : Nat) -> (c : Char) -> (rs : RLE xs) ->
9 RLE (replicate (S n) c ++ xs)
11------------
13rle : (xs : Vect n Char) -> RLE xs
14rle [] = REnd
15rle (x :: xs) with (rle xs)
16 rle (x :: []) | REnd = RChar 0 x REnd
17 rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) with (decEq x c)
18 rle (x :: (x :: (replicate n x ++ ys))) | (RChar n x rs) | (Yes Refl)
19 = RChar (S n) x rs
20 rle (x :: (c :: (replicate n c ++ ys))) | (RChar n c rs) | (No f)
21 = RChar 0 x (RChar n c rs)
23compress : Vect n Char -> String
24compress xs with (rle xs)
25 compress [] | REnd = ""
26 compress (c :: (replicate n c ++ xs1)) | (RChar n c rs)
27 = show (the Integer (cast (S n))) ++
28 strCons c (compress xs1)
30compressString : String -> String
31compressString xs = compress (fromList (unpack xs))
33main : IO ()
34main = putStrLn (compressString "foooobaaaarbaaaz")