git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/basic001/reg005.idr
50 lines 1.4 kB history raw
1module Main
3%flag C "-g3 -ggdb -O0"
5rep : (n : Nat) -> Char -> Vect n Char
6rep Z x = []
7rep (S k) x = x :: rep k x
9data RLE : Vect n Char -> Type where
10 REnd : RLE []
11 RChar : .{k : Nat}
12 -> {xs : Vect k Char}
13 -> (n : Nat)
14 -> (x : Char)
15 -> RLE xs
16 -> RLE (rep (S n) x ++ xs)
18eq : (x : Char) -> (y : Char) -> Maybe (x = y)
19eq x y = if x == y then Just (believe_me (Refl {x})) else Nothing
21------------
23rle : (xs : Vect n Char) -> RLE xs
24rle [] = REnd
25rle (x :: xs) with (rle xs)
26 rle (x :: Vect.Nil) | REnd = RChar Z x REnd
27 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
28 rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just Refl
29 = RChar (S n) x rs
30 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
31 = RChar Z x (RChar n y rs)
33compress : Vect n Char -> String
34compress xs with (rle xs)
35 compress Nil | REnd = ""
36 compress (rep (S n) x ++ xs) | RChar _ _ rs
37 = let ni : Integer = cast (S n) in
38 show ni ++ strCons x (compress xs)
40{-
41fmt : {xs : Vect n Char} -> RLE xs -> String
42fmt REnd = ""
43fmt (RChar n c xs) = show n ++ show c ++ fmt xs
44-}
46compressString : String -> String
47compressString xs = compress (fromList (unpack xs))
49main : IO ()
50main = putStrLn (compressString "foooobaaaarbaaaz")