0 | -- Copyright (c) 2013, IIJ Innovation Institute Inc.
  1 | -- See Huffman/LICENSE
  2 | module Huffman.Decode
  3 |
  4 | import Data.SnocList
  5 | import Data.Vect as V
  6 | import Control.Monad.State.State
  7 | import Control.Monad.State.Interface
  8 | import Control.Monad.Error.Either
  9 | import Control.Monad.Trans
 10 | import Data.Array.Indexed -- atNat
 11 | import Data.Fin.Extra -- elemSmallerThanBound
 12 |
 13 | -- These are only needed due to the transitive import bug
 14 | import Data.Array.Core
 15 | import Control.Monad.Identity
 16 |
 17 | import Huffman.WayStep
 18 | import Huffman.Fin256
 19 |
 20 | record ReadWriter where
 21 |   constructor MkReadWriter
 22 |   toRead : List Bits8
 23 |   written : SnocList Bits8
 24 |   wayStep : Fin 256 -> WayStep
 25 |
 26 | public export
 27 | data HpackErr = TooLongEos | IllegalEos | EosInTheMiddle
 28 |
 29 | public export
 30 | Show HpackErr where
 31 |   show TooLongEos = "TooLongEos"
 32 |   show IllegalEos = "IllegalEos"
 33 |   show EosInTheMiddle = "EosInTheMiddle"
 34 |
 35 | partial
 36 | read8 : State ReadWriter Bits8
 37 | read8 = do
 38 |   read <- get
 39 |   let readByte :: rest = read.toRead
 40 |       newRec : ReadWriter
 41 |       newRec = { toRead := rest } read
 42 |   put newRec
 43 |   pure readByte
 44 |
 45 | write8 : Bits8 -> State ReadWriter Unit
 46 | write8 newByte = do
 47 |   read <- get
 48 |   let new = read.written :< newByte
 49 |       newRec : ReadWriter
 50 |       newRec = { written := new } read
 51 |   put newRec
 52 |   pure ()
 53 |
 54 | partial
 55 | next : WayStep -> Bits8 -> Pin
 56 | next (MkWayStep _ a16) w = V.index (bits8ToFin256 w) a16
 57 |
 58 | doit : WayStep -> Bits8 -> EitherT HpackErr (State ReadWriter) WayStep
 59 | doit way w = do
 60 |   tbl <- (.wayStep) <$> lift get
 61 |   case next way w of
 62 |     EndOfString => throwE EosInTheMiddle
 63 |     Forward n   =>
 64 |       let val: WayStep
 65 |           val = tbl n
 66 |        in pure val
 67 |     GoBack  n v => do
 68 |         lift $ write8 v
 69 |         pure $ tbl n
 70 |     GoBack2 n v1 v2 => do
 71 |         lift $ write8 v1
 72 |         lift $ write8 v2
 73 |         pure $ tbl n
 74 |
 75 | partial
 76 | go : Nat -> WayStep -> EitherT HpackErr (State ReadWriter) Unit
 77 | go 0 way0 = case way0 of
 78 |     MkWayStep Nothing  _ => throwE IllegalEos
 79 |     MkWayStep (Just i) _ =>
 80 |       if i <= 8
 81 |         then pure ()
 82 |         else throwE TooLongEos
 83 | go (S n) way0 = do
 84 |     w <- lift read8
 85 |     way <- doit way0 w
 86 |     go n way
 87 |
 88 | decH : (Fin 256 -> WayStep) -> Nat -> EitherT HpackErr (State ReadWriter) Unit
 89 | decH lookupWayStep len =
 90 |   assert_total $ go len (lookupWayStep 0)
 91 |
 92 | public export
 93 | decodeHuffman : List Bits8 -> Either HpackErr (List Bits8)
 94 | decodeHuffman inp =
 95 |   let
 96 |     -- Don't inline this! Otherwise the table will be computed multiple times
 97 |     tbl = way256
 98 |     lookupWayStep : Fin 256 -> WayStep
 99 |     lookupWayStep fin =
100 |       let
101 |         prf: LT (finToNat fin) 256
102 |         prf = elemSmallerThanBound fin
103 |       in
104 |       atNat tbl (finToNat fin) {lt=prf}
105 |     rw = MkReadWriter inp Lin lookupWayStep
106 |     stateComp : State ReadWriter (Either HpackErr Unit)
107 |     stateComp = runEitherT (decH lookupWayStep (length inp))
108 |   in
109 |     case runState rw stateComp of
110 |       (_, Left err) => Left err
111 |       (x, Right ()) => Right $ (the (SnocList Bits8 -> List Bits8) cast) x.written
112 |
113 | -- execute with
114 | -- > idris2 -p contrib HuffmanDecode.idr -x main
115 | -- (too slow to work in when interpreted in repl!)
116 | partial
117 | main : IO ()
118 | main =
119 |   print $ decodeHuffman [97,98,99]
120 |