git.iko.soy/Idris-dev
on master help sign in
Fix reg005.
73d95bbMatus Tejiscak
test/basic001/reg005.idr+15−16
compare with master
unifiedsplit
@@ -1,17 +1,22 @@
1module Main
1module Main
2
2
3+%flag C "-g3 -ggdb -O0"
4+
3rep : (n : Nat) -> Char -> Vect n Char
5rep : (n : Nat) -> Char -> Vect n Char
4rep Z x = []
6rep Z x = []
5rep (S k) x = x :: rep k x
7rep (S k) x = x :: rep k x
6
8
7data RLE : Vect n Char -> Type where
9data RLE : Vect n Char -> Type where
8 REnd : RLE []
10 REnd : RLE []
11+ RChar : .{k : Nat}
9− RChar : {xs : Vect k Char} ->
12+ -> {xs : Vect k Char}
13+ -> (n : Nat)
10− (n : Nat) -> (x : Char) -> RLE xs ->
14+ -> (x : Char)
15+ -> RLE xs
11− RLE (rep (S n) x ++ xs)
16+ -> RLE (rep (S n) x ++ xs)
12
17
13eq : (x : Char) -> (y : Char) -> Maybe (x = y)
18eq : (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
15
20
16------------
21------------
17
22
@@ -32,20 +37,14 @@ compress xs with (rle xs)
32 = let ni : Integer = cast (S n) in
37 = let ni : Integer = cast (S n) in
33 show ni ++ strCons x (compress xs)
38 show ni ++ strCons x (compress xs)
34
39
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+
35compressString : String -> String
46compressString : String -> String
36compressString xs = compress (fromList (unpack xs))
47compressString xs = compress (fromList (unpack xs))
37
48
38main : IO ()
49main : IO ()
39main = putStrLn (compressString "foooobaaaarbaaaz")
50main = 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−