@@ -6,6 +6,9 @@ import Data.Fin
6 -- to improve it! (EB)
6 -- to improve it! (EB)
7%access export
7%access export
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.
9public export
12public export
10nextPow2 : Nat -> Nat
13nextPow2 : Nat -> Nat
11nextPow2 Z = Z
14nextPow2 Z = Z
@@ -15,10 +18,17 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
16 l2x = log2NZ (S x) SIsNotZ
19 l2x = log2NZ (S x) SIsNotZ
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`.
18public export
24public export
19nextBytes : Nat -> Nat
25nextBytes : Nat -> Nat
20nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
26nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
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).
22public export
32public export
23machineTy : Nat -> Type
33machineTy : Nat -> Type
24machineTy Z = Bits8
34machineTy Z = Bits8
@@ -26,9 +36,13 @@ machineTy (S Z) = Bits16
26machineTy (S (S Z)) = Bits32
36machineTy (S (S Z)) = Bits32
27machineTy (S (S (S _))) = Bits64
37machineTy (S (S (S _))) = Bits64
39+||| Finds the number of bits used by `machineTy n`.
40+||| For example, bitsUsed 2 = 16
29bitsUsed : Nat -> Nat
41bitsUsed : Nat -> Nat
30bitsUsed n = 8 * (2 `power` n)
42bitsUsed n = 8 * (2 `power` n)
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.
32natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n
46natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n
33natToBits' a Z = a
47natToBits' a Z = a
34natToBits' {n=n} a x with (n)
48natToBits' {n=n} a x with (n)
@@ -39,6 +53,7 @@ natToBits' {n=n} a x with (n)
39 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
53 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
40 natToBits' a _ | _ = assert_unreachable
54 natToBits' a _ | _ = assert_unreachable
56+||| Converts a Nat to a machineTy n.
42natToBits : %static {n : Nat} -> Nat -> machineTy n
57natToBits : %static {n : Nat} -> Nat -> machineTy n
43natToBits {n=n} x with (n)
58natToBits {n=n} x with (n)
44 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
59 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
@@ -50,8 +65,11 @@ natToBits {n=n} x with (n)
50getPad : %static {n : Nat} -> Nat -> machineTy n
65getPad : %static {n : Nat} -> Nat -> machineTy n
51getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)
66getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)
68+||| A "high-level" wrapper to the types defined by `machineTy`.
53public export
69public export
54data Bits : Nat -> Type where
70data Bits : Nat -> Type where
71+ ||| An bits type that has at least n bits available,
72+ ||| up to the maximum supported by `machineTy`.
55 MkBits : machineTy (nextBytes n) -> Bits n
73 MkBits : machineTy (nextBytes n) -> Bits n
57pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
75pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
@@ -447,4 +465,3 @@ bitsToStr x = pack (helper last x)
448implementation Show (Bits n) where
466implementation Show (Bits n) where
449 show = bitsToStr
467 show = bitsToStr