0 | module Data.Compress.Utils.Bytes
 1 |
 2 | import Syntax.WithProof
 3 | import Data.Bits
 4 | import Data.DPair
 5 | import Data.Fin
 6 | import Data.Fin.Extra
 7 | import Data.Nat
 8 | import Data.List
 9 | import Data.Vect
10 | import Data.Nat.Factor
11 | import Data.Nat.Order.Properties
12 |
13 | weakenN' : {m : Nat} -> (0 n : Nat) -> Fin m -> Fin (n + m)
14 | weakenN' n m' = rewrite plusCommutative n m in weakenN n m'
15 |
16 | fix_fin : (m : Nat) -> (n : Nat) -> (S m) = n -> S (S (S (S (S (S (S (S (mult m 8)))))))) = mult n 8
17 | fix_fin m n prf = rewrite sym prf in Refl
18 |
19 | export
20 | to_le : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
21 | to_le x = let (S m) = n; nmeq = Refl in map (go nmeq x) Fin.range
22 |   where
23 |     go : {m : Nat} -> ((S m) = n) -> a -> Fin (S m) -> Bits8
24 |     go nmeq b i = cast $ shiftR b (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)
25 |
26 | export
27 | from_le : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
28 | from_le p = let (S m) = n; nmeq = Refl in foldl (.|.) zeroBits $ zipWith (go nmeq) p Fin.range
29 |   where
30 |     go : {m : Nat} -> ((S m) = n) -> Bits8 -> Fin (S m) -> a
31 |     go nmeq b i = shiftL (cast b) (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)
32 |
33 | export
34 | le_to_integer : Foldable t => t Bits8 -> Integer
35 | le_to_integer = go . toList
36 |   where
37 |   go : List Bits8 -> Integer
38 |   go v = foldr (.|.) 0 $ zipWith shiftL (cast {to=Integer} <$> v) ((*8) <$> [0..(length v)])
39 |
40 | export
41 | integer_to_le : (n : Nat) -> Integer -> Vect n Bits8
42 | integer_to_le n v = (cast . shiftR v) <$> (((*8) . finToNat) <$> Fin.range)
43 |
44 | export
45 | string_to_ascii : (x : String) -> List Bits8
46 | string_to_ascii = map (cast . ord) . unpack
47 |
48 | export
49 | ascii_to_string : List Bits8 -> String
50 | ascii_to_string = pack . map cast
51 |