@@ -0,0 +1,50 @@
1+module Main
2+
3+rep : (n : Nat) -> Char -> Vect Char n
4+rep O x = []
5+rep (S k) x = x :: rep k x
6+
7+data RLE : Vect Char n -> Set where
8+ REnd : RLE []
9+ RChar : {xs : Vect Char k} ->
10+ (n : Nat) -> (x : Char) -> RLE xs ->
11+ RLE (rep (S n) x ++ xs)
12+
13+eq : (x : Char) -> (y : Char) -> Maybe (x = y)
14+eq x y = if x == y then Just ?eqCharOK else Nothing
15+
16+------------
17+
18+rle : (xs : Vect Char n) -> RLE xs
19+rle [] = REnd
20+rle (x :: xs) with (rle xs)
21+ rle (x :: []) | REnd = RChar O x REnd
22+ rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
23+ rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p
24+ = RChar (S n) x rs
25+ rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
26+ = RChar O x (RChar n y rs)
27+
28+compress : Vect Char n -> String
29+compress xs with (rle xs)
30+ compress Nil | REnd = ""
31+ compress (rep (S n) x ++ xs) | RChar n x rs
32+ = let ni : Int = cast (S n) in
33+ show ni ++ show x ++ compress xs
34+
35+compressString : String -> String
36+compressString xs = compress (fromList (unpack xs))
37+
38+main : IO ()
39+main = putStrLn (compressString "foooobaaaarbaaaz")
40+
41+
42+
43+---------- Proofs ----------
44+
45+Main.eqCharOK = proof {
46+ intros;
47+ refine believe_me;
48+ exact x = x;
49+}
50+