@@ -1,17 +1,22 @@
11module Main
22
3+%flag C "-g3 -ggdb -O0"
4+
35rep : (n : Nat) -> Char -> Vect n Char
46rep Z x = []
57rep (S k) x = x :: rep k x
68
79data RLE : Vect n Char -> Type where
810 REnd : RLE []
9− RChar : {xs : Vect k Char} ->
10− (n : Nat) -> (x : Char) -> RLE xs ->
11− RLE (rep (S n) x ++ xs)
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)
1217
1318eq : (x : Char) -> (y : Char) -> Maybe (x = y)
14−eq x y = if x == y then Just ?eqCharOK else Nothing
19+eq x y = if x == y then Just (believe_me (refl {x})) else Nothing
1520
1621------------
1722
@@ -32,20 +37,14 @@ compress xs with (rle xs)
3237 = let ni : Integer = cast (S n) in
3338 show ni ++ strCons x (compress xs)
3439
40+{-
41+fmt : {xs : Vect n Char} -> RLE xs -> String
42+fmt REnd = ""
43+fmt (RChar n c xs) = show n ++ show c ++ fmt xs
44+-}
45+
3546compressString : String -> String
3647compressString xs = compress (fromList (unpack xs))
3748
3849main : IO ()
3950main = 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−
51−