2 | module Huffman.HTree

 4 | import Huffman.Table

 5 | import Data.Vect as V

 6 | import Data.Fin

 7 | import Data.List

 8 | import Data.Fin.Extra as Extra

10 | public export

11 | data HTree = Tip

12 |              (Maybe Nat)

13 |              (Maybe Bits8) -- Decoded value. Essentially Word8

14 |            | Bin

15 |              (Maybe Nat)            -- EOS info from 1

16 |              (Fin 256) -- Sequence no from 0

17 |              HTree              -- Left

18 |              HTree              -- Right

21 | mark : Nat -> Bits -> HTree -> HTree

22 | mark i []     (Tip Nothing v)      = Tip (Just i) v

23 | mark i (F::bs) (Bin Nothing n l r) = Bin (Just i) n (mark (i+1) bs l) r

24 | mark i (T::bs) (Bin Nothing n l r) = Bin (Just i) n l (mark (i+1) bs r)

25 | mark _ _      _                    = idris_crash "mark"

27 | second : (b -> c) -> Pair a b -> Pair a c

28 | second f (a, b) = (a, (f b))

30 | public export

32 | fromJustPartial : Maybe a -> a

33 | fromJustPartial (Just x) = x

35 | public export

37 | build : Fin 257 -> List (Pair (Maybe Bits8) Bits) -> Pair (Fin 257) HTree

38 | build _ [] = idris_crash "empty"

39 | build cnt0 [(v, [])] =

40 |   (cnt0, Tip Nothing v)

41 | build cnt0 xs =

42 |   let

43 |     sum : Fin (256 + 1)

44 |     sum = cnt0

45 |     splitted : Either (Fin 256) (Fin 1)

46 |     splitted = Extra.splitSum sum

47 |     p1 : Fin 256

48 |     p1 =

49 |       fromJustPartial $

50 |         case splitted of

51 |           Right _ =>

52 |             Nothing

53 |           Left low =>

54 |             Just low

55 |   in

56 |       let (fs', ts') = partition ((== F) . fromJustPartial . head' . snd) xs

57 |           fs = map (second $ fromJustPartial . tail') fs'

58 |           ts = map (second $ fromJustPartial . tail') ts'

59 |           (cnt1, l) = build (FS p1) fs

60 |           (cnt2, r) = build cnt1 ts

61 |        in (cnt2, Bin Nothing p1 l r)

63 | public export

64 | allBits8 : V.Vect 256 Bits8

65 | allBits8 = V.fromList

66 |   [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32

67 |   , 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64

68 |   , 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96

69 |   , 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123

70 |   , 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150

71 |   , 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177

72 |   , 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204

73 |   , 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231

74 |   , 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255 ]

76 | public export

78 | toHTree : Fin n -> V.Vect n Bits -> HTree

79 | toHTree idxEos bs = mark 1 eos $ snd $ build 0 $ zip (map Just (toList allBits8) ++ [Nothing]) (toList bs)

80 |   where

81 |     eos : Bits

82 |     eos = V.index idxEos bs