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