
   0 | module Data.Compress.GZip
   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 GZipParserState'
  18 |   = GZipHead
  19 |   | GZipFoot
  20 |   | GZipInflate
  21 | 
  22 | public export
  23 | data GZipParserState : GZipParserState' -> Type where
  24 |   AtGHeader : GZipParserState GZipHead
  25 |   AtInflate : (isize : Bits32) -> (crc32 : Bits32) -> InflateState -> GZipParserState GZipInflate
  26 |   AtGFooter : (isize : Bits32) -> (crc32 : Bits32) -> GZipParserState GZipFoot
  27 | 
  28 | public export
  29 | data GZipState
  30 |   = MkState (List Bits8) (DPair GZipParserState' GZipParserState)
  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 GZipFooter where
  36 |   constructor MkGZipFooter
  37 |   crc32 : Bits32
  38 |   isize : Bits32
  39 | 
  40 | export
  41 | parse_gzip_header : Parser (List Bits8) (SimpleError String) ()
  42 | parse_gzip_header = do
  43 |   [0x1f, 0x8b] <- count 2 token
  44 |   | x => fail $ msg "gzip magic number expected, got \{show x}"
  45 |   0x08 <- token
  46 |   | x => fail $ msg "deflate method magic number expected, got \{show x}"
  47 |   flag <- token
  48 |   mtime <- count 4 token
  49 |   xfl <- token
  50 |   os <- token
  51 | 
  52 |   fextra <- ifA (testBit flag 2) $ do
  53 |     xlen <- p_nat 2
  54 |     toList <$> count xlen token
  55 | 
  56 |   fname <- ifA (testBit flag 3) nul_term_string
  57 | 
  58 |   fcomment <- ifA (testBit flag 4) nul_term_string
  59 | 
  60 |   fhcrc <- ifA (testBit flag 1) (count 2 token)
  61 | 
  62 |   pure ()
  63 | 
  64 | export
  65 | parse_gzip_footer : Parser (List Bits8) (SimpleError String) GZipFooter
  66 | parse_gzip_footer = do
  67 |   crc32 <- cast <$> p_nat 4
  68 |   isize <- cast <$> p_nat 4
  69 |   pure (MkGZipFooter crc32 isize)
  70 | 
  71 | feed_gzip' : SnocList Bits8 -> DPair GZipParserState' GZipParserState -> List Bits8 -> Either String (SnocList Bits8, GZipState)
  72 | feed_gzip' acc (_ ** AtGHeader) [] = Right (acc, MkState [] (_ ** AtGHeader))
  73 | feed_gzip' acc (_ ** AtGHeader) content =
  74 |   case feed content parse_gzip_header of
  75 |     Pure leftover header => feed_gzip' acc (_ ** AtInflate 0 0 init) leftover
  76 |     Fail err => Left $ show err
  77 |     _ => Right (acc, MkState content (_ ** AtGHeader))
  78 | feed_gzip' acc (_ ** AtInflate isize crc32 inflate_state) content =
  79 |   case feed inflate_state content of
  80 |     Left err => Left err
  81 |     Right (uncompressed, (MkState _ _ (_ ** AtEnd leftover))) =>
  82 |       let isize = isize + (cast $ length uncompressed)
  83 |           crc32 = update_crc32 crc32 uncompressed
  84 |       in feed_gzip' (acc <>< uncompressed) (_ ** AtGFooter isize crc32) (toList leftover)
  85 |     Right (uncompressed, inflate_state) => -- underfed
  86 |       let isize = isize + (cast $ length uncompressed)
  87 |           crc32 = update_crc32 crc32 uncompressed
  88 |       in Right (acc <>< uncompressed, MkState [] (_ ** AtInflate isize crc32 inflate_state))
  89 | feed_gzip' acc (_ ** AtGFooter isize crc32) content =
  90 |   case feed content parse_gzip_footer of
  91 |     Pure leftover footer =>
  92 |       if footer.crc32 /= crc32 then Left "crc32 mismatch"
  93 |         else if footer.isize /= isize then Left "isize mismatch"
  94 |         else feed_gzip' acc (_ ** AtGHeader) leftover
  95 |     Fail err => Left $ show err
  96 |     _ => Right (acc, MkState content (_ ** AtGFooter isize crc32))
  97 | 
  98 | export
  99 | Decompressor GZipState where
 100 |   feed (MkState leftover state) input = mapFst toList <$> feed_gzip' Lin state (leftover <+> input)
 101 |   done (MkState [] (_ ** AtGHeader)) = Right []
 102 |   done (MkState _ (_ ** AtGHeader)) = Left "gzip: leftover data after header"
 103 |   done _ = Left "gzip: underfed"
 104 |   init = MkState [] (_ ** AtGHeader)
 105 |