test/basic001/reg005.idr · Idris-dev

git.iko.soy/Idris-dev

on 76ec3fe help sign in

54 lines 1.4 kB history raw

1module Main

3import Data.Vect

5%flag C "-g3"

6%flag C "-ggdb"

7%flag C "-O0"

9rep : (n : Nat) -> Char -> Vect n Char

10rep Z x = []

11rep (S k) x = x :: rep k x

13data RLE : Vect n Char -> Type where

14 REnd : RLE []

15 RChar : .{k : Nat}

16 -> {xs : Vect k Char}

17 -> (n : Nat)

18 -> (x : Char)

19 -> RLE xs

20 -> RLE (rep (S n) x ++ xs)

22eq : (x : Char) -> (y : Char) -> Maybe (x = y)

23eq x y = if x == y then Just (believe_me (Refl {x})) else Nothing

25------------

27rle : (xs : Vect n Char) -> RLE xs

28rle [] = REnd

29rle (x :: xs) with (rle xs)

30 rle (x :: Vect.Nil) | REnd = RChar Z x REnd

31 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

32 rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just Refl

33 = RChar (S n) x rs

34 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

35 = RChar Z x (RChar n y rs)

37compress : Vect n Char -> String

38compress xs with (rle xs)

39 compress Nil | REnd = ""

40 compress (rep (S n) x ++ xs) | RChar _ _ rs

41 = let ni : Integer = cast (S n) in

42 show ni ++ strCons x (compress xs)

45fmt : {xs : Vect n Char} -> RLE xs -> String

46fmt REnd = ""

47fmt (RChar n c xs) = show n ++ show c ++ fmt xs

50compressString : String -> String

51compressString xs = compress (fromList (unpack xs))

53main : IO ()

54main = putStrLn (compressString "foooobaaaarbaaaz")