0 | module Data.Bytes.Impls
  1 |
  2 | import Data.Vect
  3 | import public Data.Bits
  4 | import Data.Bytes.Interfaces
  5 | import Data.Bytes.Proofs
  6 | import Data.Bytes.Prims
  7 |
  8 | %default total
  9 |
 10 | %defaulthint
 11 | public export
 12 | implBytesForFiniteBits : 
 13 |      {auto _ : FiniteBits num}
 14 |   -> {auto _ : Cast num Bits8}
 15 |   -> {auto _ : Cast Bits8 num}
 16 |   -> {auto prfMult8: IsJust (isMultN 8 (bitSize {a = num}))}
 17 |   -> Bytes num
 18 | implBytesForFiniteBits = finiteBytes byteSView.fst {prf = byteSView.snd} where
 19 |   byteSView: (x : Nat ** bitSize {a = num} = (mult x 8))
 20 |   byteSView = viewMultN 8 (bitSize {a = num}) (fromJust (isMultN 8 (bitSize {a = num})))
 21 |
 22 |   finiteBytes : (byteS:Nat) -> {auto prf: bitSize {a = num} = (mult byteS 8)} -> Bytes num
 23 |   finiteBytes byteS = MkBytes byteS toBytes fromBytes where
 24 |     byteToIndex : Fin byteS -> Index {a = num}
 25 |     byteToIndex = 
 26 |       let f: Fin byteS -> Fin (bitSize {a = num}) = rewrite prf in byteToBits
 27 |       in bitsToIndex . f
 28 |     
 29 |     getByte : num -> Fin byteS -> Bits8
 30 |     getByte value byteIndex = cast (value `shiftR` (byteToIndex byteIndex))
 31 |
 32 |     toBytes : Endian -> num -> Vect byteS Bits8
 33 |     toBytes LittleEndian value = (allFins byteS) |> map (\shiftAmount => getByte value shiftAmount)
 34 |     toBytes _ value            = assert_total reverse (toBytes LittleEndian value)
 35 |
 36 |     fromBytes: Endian -> Vect byteS Bits8 -> num
 37 |     fromBytes LittleEndian bytes =
 38 |       bytes 
 39 |       |> map (\value => cast value) 
 40 |       |> zip (allFins byteS) 
 41 |       |> foldl (\acc,(shiftAmount, value) => 
 42 |         acc .|. (value `shiftL` (byteToIndex shiftAmount)))
 43 |         zeroBits
 44 |     fromBytes _ value = assert_total fromBytes LittleEndian (reverse value)
 45 |
 46 | public export
 47 | Bytes Double where
 48 |   byteSize = 8
 49 |   toBytes endian x = toBytes endian (prim__flBitField x)
 50 |   fromBytes endian x = prim__bitFieldFl (fromBytes endian x)
 51 |
 52 | --------------------
 53 | -- SPECIFIC IMPLS --
 54 | --------------------
 55 | -- the default hint on implBytesForFiniteBits works fine but leaves a lot of runtime information. These specific
 56 | -- impls have the runtime information optimized out
 57 |
 58 | %hint
 59 | public export
 60 | bytesForBits8: Bytes Bits8
 61 | bytesForBits8 = implBytesForFiniteBits
 62 |
 63 | %hint
 64 | public export
 65 | bytesForBits16: Bytes Bits16
 66 | bytesForBits16 = implBytesForFiniteBits
 67 |
 68 | %hint
 69 | public export
 70 | bytesForBits32: Bytes Bits32
 71 | bytesForBits32 = implBytesForFiniteBits
 72 |
 73 | %hint
 74 | public export
 75 | bytesForBits64: Bytes Bits64
 76 | bytesForBits64 = implBytesForFiniteBits
 77 |
 78 | %hint
 79 | public export
 80 | bytesForInt8: Bytes Int8
 81 | bytesForInt8 = implBytesForFiniteBits
 82 |
 83 | %hint
 84 | public export
 85 | bytesForInt16: Bytes Int16
 86 | bytesForInt16 = implBytesForFiniteBits
 87 |
 88 | %hint
 89 | public export
 90 | bytesForInt32: Bytes Int32
 91 | bytesForInt32 = implBytesForFiniteBits
 92 |
 93 | %hint
 94 | public export
 95 | bytesForInt64: Bytes Int64
 96 | bytesForInt64 = implBytesForFiniteBits
 97 |
 98 | %hint
 99 | public export
100 | bytesForInt: Bytes Int
101 | bytesForInt = implBytesForFiniteBits
102 |