
  0 | module Data.Compress.Interface
  1 | 
  2 | public export
  3 | interface Decompressor a where
  4 |   ||| decompress a part of the compressed stream
  5 |   feed : a -> List Bits8 -> Either String (List Bits8, a)
  6 |   ||| signify the compressed stream has been completely consumed
  7 |   ||| return the leftover data
  8 |   done : a -> Either String (List Bits8)
  9 |   ||| init state
 10 |   init : a
 11 | 
 12 | public export
 13 | data IdentityState = Id
 14 | 
 15 | public export
 16 | Decompressor IdentityState where
 17 |   feed Id content = Right (content, Id)
 18 |   done Id = Right []
 19 |   init = Id
 20 | 
 21 | export
 22 | decompress : a -> Decompressor a => List Bits8 -> Either String (List Bits8)
 23 | decompress _ compressed = do
 24 |   (uncompressed, state) <- feed {a} init compressed
 25 |   [] <- done state
 26 |   | x => Left "{\show (length x)} leftover bytes"
 27 |   pure uncompressed
 28 |