38 lines
853 B
Idris
38 lines
853 B
Idris
module RLE
|
|
-- run length encoding?
|
|
-- ?name means a hole
|
|
|
|
import Decidable.Equality
|
|
|
|
-- repeat an element n times
|
|
rep : Nat -> a -> List a
|
|
rep 0 x = []
|
|
rep (S k) x = x :: rep k x
|
|
|
|
data RunLength : List ty -> Type where
|
|
Empty : RunLength []
|
|
Run : (n:Nat) ->
|
|
(x:ty) ->
|
|
RunLength more ->
|
|
RunLength (rep n x ++ more)
|
|
|
|
testComp : RunLength {ty=Char} ?
|
|
testComp = Run 3 'x' $ Run 4 'y' $ Empty
|
|
|
|
data Singleton : a -> Type where
|
|
Val : (x:a) -> Singleton x
|
|
|
|
uncompress : RunLength {ty} xs -> Singleton xs
|
|
uncompress Empty = Val []
|
|
uncompress (Run n x y) = let Val ys = uncompress y in Val (rep n x ++ ys)
|
|
|
|
-- uncompress x = ?uncompress_rhs
|
|
--
|
|
-- uncompress Empty = []
|
|
-- uncompress (Run n x y) = rep n x :: uncompress y
|
|
|
|
|
|
rel : DecEq a => (xs:List a) -> RunLength xs
|
|
-- C-c C-s: initial
|
|
rel xs = ?rel_rhs
|