@@ -6,6 +6,9 @@ import Data.Fin
66 -- to improve it! (EB)
77%access export
88
9+||| Finds the next exponent of a power of two.
10+||| For example `nextPow2 200 = 8`, because 2^8 = 256.
11+||| If it is an exact match, it is not rounded up: `nextPow2 256 = 8` because 2^8 = 256.
912public export
1013nextPow2 : Nat -> Nat
1114nextPow2 Z = Z
@@ -15,10 +18,17 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
1518 where
1619 l2x = log2NZ (S x) SIsNotZ
1720
21+||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.
22+||| For example, `nextBytes 10 = 16`.
23+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 16`.
1824public export
1925nextBytes : Nat -> Nat
2026nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
2127
28+||| An index function to access the Bits* types in order.
29+||| machineTy 0 = Bits8, machineTy 1 = Bits16, etc.
30+||| Any input that would result in getting a type that is larger than supported
31+||| will result in the largest supported type instead (currently 64 bits).
2232public export
2333machineTy : Nat -> Type
2434machineTy Z = Bits8
@@ -26,9 +36,13 @@ machineTy (S Z) = Bits16
2636machineTy (S (S Z)) = Bits32
2737machineTy (S (S (S _))) = Bits64
2838
39+||| Finds the number of bits used by `machineTy n`.
40+||| For example, bitsUsed 2 = 16
2941bitsUsed : Nat -> Nat
3042bitsUsed n = 8 * (2 `power` n)
3143
44+||| Converts a Nat to a machineTy n, with the first argument as an accumulator.
45+||| You shouldn't have to call this manually, use natToBits (without ') instead.
3246natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n
3347natToBits' a Z = a
3448natToBits' {n=n} a x with (n)
@@ -39,6 +53,7 @@ natToBits' {n=n} a x with (n)
3953 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
4054 natToBits' a _ | _ = assert_unreachable
4155
56+||| Converts a Nat to a machineTy n.
4257natToBits : %static {n : Nat} -> Nat -> machineTy n
4358natToBits {n=n} x with (n)
4459 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
@@ -50,8 +65,11 @@ natToBits {n=n} x with (n)
5065getPad : %static {n : Nat} -> Nat -> machineTy n
5166getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)
5267
68+||| A "high-level" wrapper to the types defined by `machineTy`.
5369public export
5470data Bits : Nat -> Type where
71+ ||| An bits type that has at least n bits available,
72+ ||| up to the maximum supported by `machineTy`.
5573 MkBits : machineTy (nextBytes n) -> Bits n
5674
5775pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
@@ -447,4 +465,3 @@ bitsToStr x = pack (helper last x)
447465
448466implementation Show (Bits n) where
449467 show = bitsToStr
450−