
   0 | -- Copyright (c) 2013, IIJ Innovation Institute Inc.
   1 | -- See Huffman/LICENSE
   2 | module Huffman.WayStep
   3 | 
   4 | import Data.Fin as Fin
   5 | import Data.Vect as V
   6 | import Data.Bits
   7 | import Data.List
   8 | import Decidable.Equality
   9 | 
  10 | import Data.Array.Indexed
  11 | import Data.Array.Core
  12 | 
  13 | import Huffman.HTree
  14 | import Huffman.Table
  15 | 
  16 | public export
  17 | data Pin = EndOfString
  18 |          | Forward (Fin 256) -- node no.
  19 |          | GoBack  (Fin 256) -- node no.
  20 |                    Bits8 -- a decoded value
  21 |          | GoBack2 (Fin 256) -- node no.
  22 |                    Bits8 -- a decoded value
  23 |                    Bits8 -- a decoded value
  24 | 
  25 | public export
  26 | Show Pin where
  27 |   show EndOfString = "EndOfString"
  28 |   show (Forward n) = "Forward " ++ show (finToNat n)
  29 |   show (GoBack n v) = "GoBack " ++ show (finToNat n) ++ " " ++ show v
  30 |   show (GoBack2 n v w) = "GoBack2 " ++ show (finToNat n) ++ " " ++ show v ++ " " ++ show w
  31 | 
  32 | public export
  33 | data WayStep = MkWayStep (Maybe Nat) (V.Vect 256 Pin)
  34 | 
  35 | public export
  36 | Show WayStep where
  37 |   show (MkWayStep a b) = "WayStep " ++ show a ++ " " ++ show b
  38 | 
  39 | data Chara = Non
  40 |            | One Bits8
  41 |            | Two Bits8 Bits8
  42 | 
  43 | partial
  44 | inc : Chara -> Bits8 -> Chara
  45 | inc Non w     = One w
  46 | inc (One v) w = Two v w
  47 | inc _       _ = idris_crash "inc"
  48 | 
  49 | partial
  50 | step : HTree -> HTree -> Chara -> Nat -> Bits8 -> Pin
  51 | step root (Tip _ v) x ctr bss =
  52 |   case v of
  53 |     Nothing => EndOfString
  54 |     Just w =>
  55 |           let x' = inc x w
  56 |           in step root root x' ctr bss
  57 | step _    (Bin _ n _ _) Non       0 _ = Forward n
  58 | step _    (Bin _ n _ _) (One w)   0 _ = GoBack n w
  59 | step _    (Bin _ n _ _) (Two w z) 0 _ = GoBack2 n w z
  60 | step root (Bin _ _ l r) mx        (S ctrMinusOne) b =
  61 |   step root (if b .&. (1 `shiftL` 7) == 0 then l else r) mx ctrMinusOne (b `shiftL` 1)
  62 | step _    (Bin _ _ _ _) _         Z _ =
  63 |   idris_crash "counter reached zero"
  64 | 
  65 | eosInfo : HTree -> Maybe Nat
  66 | eosInfo (Tip mx _)     = mx
  67 | eosInfo (Bin mx _ _ _) = mx
  68 | 
  69 | 
  70 | flatten : HTree -> List HTree
  71 | flatten (Tip _ _)       = []
  72 | flatten t@(Bin _ _ l r) = t :: (flatten l ++ flatten r)
  73 | 
  74 | partial
  75 | construct : HTree -> List WayStep
  76 | construct decoder =
  77 |   let
  78 |     to16ways : HTree -> WayStep
  79 |     to16ways x =
  80 |       let
  81 |         ei = eosInfo x
  82 |         a16 : V.Vect 256 Pin
  83 |         a16 = map (step decoder x Non 8) allBits8
  84 |        in
  85 |         MkWayStep ei a16
  86 |    in
  87 |     map to16ways $ flatten decoder
  88 | 
  89 | partial
  90 | bigTree : HTree
  91 | bigTree = toHTree 256 huffmanTable
  92 | 
  93 | partial
  94 | way256L : List WayStep
  95 | way256L = construct bigTree
  96 | 
  97 | total
  98 | fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
  99 | fromListOfLength n xs with (decEq (length xs) n)
 100 |   fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
 101 |   fromListOfLength n xs | (No _) = Nothing
 102 | 
 103 | export
 104 | way256 : IArray 256 WayStep
 105 | way256 =
 106 |   array vect
 107 |   where
 108 |   vect : V.Vect 256 WayStep
 109 |   vect = assert_total $ fromJustPartial $ fromListOfLength 256 way256L
 110 |