0 | module Data.Compress.ZLib
  1 |
  2 | import Data.Compress.Utils.Parser
  3 | import Data.Compress.Utils.Bytes
  4 | import Data.Compress.Utils.Misc
  5 | import Data.Compress.Interface
  6 | import Data.Vect
  7 | import Data.Bits
  8 | import Data.List
  9 | import Data.SnocList
 10 | import Data.Stream
 11 | import Data.Compress.CRC
 12 | import Control.Monad.Error.Either
 13 |
 14 | import public Data.Compress.Inflate
 15 |
 16 | public export
 17 | data ZLibParserState'
 18 |   = ZLibHead
 19 |   | ZLibFoot
 20 |   | ZLibInflate
 21 |
 22 | public export
 23 | data ZLibParserState : ZLibParserState' -> Type where
 24 |   AtZHeader : ZLibParserState ZLibHead
 25 |   AtInflate : (adler32 : Bits32) -> InflateState -> ZLibParserState ZLibInflate
 26 |   AtZFooter : (adler32 : Bits32) -> ZLibParserState ZLibFoot
 27 |
 28 | public export
 29 | data ZLibState
 30 |   = MkState (List Bits8) (DPair ZLibParserState' ZLibParserState)
 31 |
 32 | nul_term_string : Semigroup e => Parser (List Bits8) e String
 33 | nul_term_string = map ascii_to_string $ take_until (0 ==) token
 34 |
 35 | record ZLibFooter where
 36 |   constructor MkZLibFooter
 37 |   adler32 : Bits32
 38 |
 39 | export
 40 | parse_zlib_header : Parser (List Bits8) (SimpleError String) ()
 41 | parse_zlib_header = do
 42 |   cmf <- token
 43 |   flg <- token
 44 |
 45 |   let True = 0 == (((shiftL {a=Bits16} (cast cmf) 8) .|. cast flg) `mod` 31)
 46 |   | False => fail $ msg "zlib: fcheck checksum failed"
 47 |
 48 |   let False = testBit flg 5
 49 |   | True => fail $ msg "zlib: fdict is set"
 50 |
 51 |   pure ()
 52 |
 53 | update_adler32 : Bits32 -> List Bits8 -> Bits32
 54 | update_adler32 alder = go (alder .&. 0xffff) (shiftR alder 16) where
 55 |   go : Bits32 -> Bits32 -> List Bits8 -> Bits32
 56 |   go a b (x :: xs) =
 57 |     let base = 65521
 58 |         a' = (a + (cast x)) `mod` base
 59 |         b' = (a' + b) `mod` base
 60 |     in go a' b' xs
 61 |   go a b [] = (shiftL b 16) .|. a
 62 |
 63 | export
 64 | parse_zlib_footer : Parser (List Bits8) (SimpleError String) ZLibFooter
 65 | parse_zlib_footer = do
 66 |   adler32 <- cast <$> p_be_nat 4
 67 |   pure (MkZLibFooter adler32)
 68 |
 69 | feed_zlib' : SnocList Bits8 -> DPair ZLibParserState' ZLibParserState -> List Bits8 -> Either String (SnocList Bits8, ZLibState)
 70 | feed_zlib' acc (_ ** AtZHeader) [] = Right (acc, MkState [] (_ ** AtZHeader))
 71 | feed_zlib' acc (_ ** AtZHeader) content =
 72 |   case feed content parse_zlib_header of
 73 |     Pure leftover header => feed_zlib' acc (_ ** AtInflate 1 init) leftover
 74 |     Fail err => Left $ show err
 75 |     _ => Right (acc, MkState content (_ ** AtZHeader))
 76 | feed_zlib' acc (_ ** AtInflate adler32 inflate_state) content =
 77 |   case feed inflate_state content of
 78 |     Left err => Left err
 79 |     Right (uncompressed, (MkState _ _ (_ ** AtEnd leftover))) =>
 80 |       let adler32 = update_adler32 adler32 uncompressed
 81 |       in feed_zlib' (acc <>< uncompressed) (_ ** AtZFooter adler32) (toList leftover)
 82 |     Right (uncompressed, inflate_state) => -- underfed
 83 |       let adler32 = update_adler32 adler32 uncompressed
 84 |       in Right (acc <>< uncompressed, MkState [] (_ ** AtInflate adler32 inflate_state))
 85 | feed_zlib' acc (_ ** AtZFooter adler32) content =
 86 |   case feed content parse_zlib_footer of
 87 |     Pure leftover footer =>
 88 |       if footer.adler32 /= adler32
 89 |          then Left "adler32 mismatch \{show footer.adler32} \{show adler32}"
 90 |         else feed_zlib' acc (_ ** AtZHeader) leftover
 91 |     Fail err => Left $ show err
 92 |     _ => Right (acc, MkState content (_ ** AtZFooter adler32))
 93 |
 94 | export
 95 | Decompressor ZLibState where
 96 |   feed (MkState leftover state) input = mapFst toList <$> feed_zlib' Lin state (leftover <+> input)
 97 |   done (MkState [] (_ ** AtZHeader)) = Right []
 98 |   done (MkState _ (_ ** AtZHeader)) = Left "zlib: leftover data after header"
 99 |   done _ = Left "zlib: underfed"
100 |   init = MkState [] (_ ** AtZHeader)
101 |