@@ -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,25 +65,36 @@ 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
57−pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
75+||| Perform a function over Bits8 as if it is carried out on n bits.
76+||| (n should be 8 or lower)
77+pad8 : (n : Nat) -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
5878pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
5979 where
6080 pad = getPad {n=0} n
6181
62−pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
82+||| Perform a function over Bits16 as if it is carried out on n bits.
83+||| (n should be 16 or lower)
84+pad16 : (n: Nat) -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
6385pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
6486 where
6587 pad = getPad {n=1} n
6688
89+||| Perform a function over Bits32 as if it is carried out on n bits.
90+||| (n should be 32 or lower)
6791pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
6892pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
6993 where
7094 pad = getPad {n=2} n
7195
96+||| Perform a function over Bits64 as if it is carried out on n bits.
97+||| (n should be 64 or lower)
7298pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
7399pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
74100 where
@@ -95,7 +121,7 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
95121 where
96122 pad = getPad {n=3} n
97123
98−-- TODO: This (and all the other functions along these lings) is -- because it is used by things. Do they really need to be
124+-- TODO: This (and all the other functions along these lines) is -- because it is used by things. Do they really need to be
99125-- public export, or is export good enough?
100126shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
101127shiftLeft' {n=n} x c with (nextBytes n)
@@ -105,9 +131,11 @@ shiftLeft' {n=n} x c with (nextBytes n)
105131 | S (S (S _)) = pad64' n prim__shlB64 x c
106132 | _ = assert_unreachable
107133
134+||| Binary left shift
108135shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n
109136shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
110137
138+||| Logical binary right shift
111139shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
112140shiftRightLogical' {n=n} x c with (n)
113141 | Z = prim__lshrB8 x c
@@ -116,10 +144,12 @@ shiftRightLogical' {n=n} x c with (n)
116144 | S (S (S _)) = prim__lshrB64 x c
117145 | _ = assert_unreachable
118146
147+||| Logical binary right shift
119148shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n
120149shiftRightLogical {n} (MkBits x) (MkBits y)
121150 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
122151
152+||| Arithematic binary right shift
123153shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
124154shiftRightArithmetic' {n=n} x c with (nextBytes n)
125155 | Z = pad8' n prim__ashrB8 x c
@@ -128,9 +158,11 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)
128158 | S (S (S _)) = pad64' n prim__ashrB64 x c
129159 | _ = assert_unreachable
130160
161+||| Arithematic binary right shift
131162shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n
132163shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
133164
165+||| Binary and
134166and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
135167and' {n=n} x y with (n)
136168 | Z = prim__andB8 x y
@@ -139,9 +171,11 @@ and' {n=n} x y with (n)
139171 | S (S (S _)) = prim__andB64 x y
140172 | _ = assert_unreachable
141173
174+||| Binary and
142175and : %static {n : Nat} -> Bits n -> Bits n -> Bits n
143176and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
144177
178+||| Binary or
145179or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
146180or' {n=n} x y with (n)
147181 | Z = prim__orB8 x y
@@ -150,9 +184,11 @@ or' {n=n} x y with (n)
150184 | S (S (S _)) = prim__orB64 x y
151185 | _ = assert_unreachable
152186
187+||| Binary or
153188or : %static {n : Nat} -> Bits n -> Bits n -> Bits n
154189or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
155190
191+||| Binary xor
156192xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
157193xor' {n=n} x y with (n)
158194 | Z = prim__xorB8 x y
@@ -161,9 +197,11 @@ xor' {n=n} x y with (n)
161197 | S (S (S _)) = prim__xorB64 x y
162198 | _ = assert_unreachable
163199
200+||| Binary xor
164201xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n
165202xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
166203
204+||| Overflowing addition
167205plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
168206plus' {n=n} x y with (nextBytes n)
169207 | Z = pad8 n prim__addB8 x y
@@ -172,9 +210,11 @@ plus' {n=n} x y with (nextBytes n)
172210 | S (S (S _)) = pad64 n prim__addB64 x y
173211 | _ = assert_unreachable
174212
213+||| Overflowing addition
175214plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
176215plus (MkBits x) (MkBits y) = MkBits (plus' x y)
177216
217+||| Subtraction
178218minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
179219minus' {n=n} x y with (nextBytes n)
180220 | Z = pad8 n prim__subB8 x y
@@ -183,9 +223,11 @@ minus' {n=n} x y with (nextBytes n)
183223 | S (S (S _)) = pad64 n prim__subB64 x y
184224 | _ = assert_unreachable
185225
226+||| Subtraction
186227minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
187228minus (MkBits x) (MkBits y) = MkBits (minus' x y)
188229
230+||| Multiplication
189231times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
190232times' {n=n} x y with (nextBytes n)
191233 | Z = pad8 n prim__mulB8 x y
@@ -194,9 +236,11 @@ times' {n=n} x y with (nextBytes n)
194236 | S (S (S _)) = pad64 n prim__mulB64 x y
195237 | _ = assert_unreachable
196238
239+||| Multiplication
197240times : %static {n : Nat} -> Bits n -> Bits n -> Bits n
198241times (MkBits x) (MkBits y) = MkBits (times' x y)
199242
243+||| Signed integer division
200244partial
201245sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
202246sdiv' {n=n} x y with (nextBytes n)
@@ -206,10 +250,12 @@ sdiv' {n=n} x y with (nextBytes n)
206250 | S (S (S _)) = prim__sdivB64 x y
207251 | _ = assert_unreachable
208252
253+||| Signed integer division
209254partial
210255sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
211256sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
212257
258+||| Unsigned integer division
213259partial
214260udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
215261udiv' {n=n} x y with (nextBytes n)
@@ -219,10 +265,12 @@ udiv' {n=n} x y with (nextBytes n)
219265 | S (S (S _)) = prim__udivB64 x y
220266 | _ = assert_unreachable
221267
268+||| Unsigned integer division
222269partial
223270udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
224271udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
225272
273+||| Signed remainder (mod)
226274partial
227275srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
228276srem' {n=n} x y with (nextBytes n)
@@ -232,10 +280,12 @@ srem' {n=n} x y with (nextBytes n)
232280 | S (S (S _)) = prim__sremB64 x y
233281 | _ = assert_unreachable
234282
283+||| Signed remainder (mod)
235284partial
236285srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
237286srem (MkBits x) (MkBits y) = MkBits (srem' x y)
238287
288+||| Unsigned remainder (mod)
239289partial
240290urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
241291urem' {n=n} x y with (nextBytes n)
@@ -245,6 +295,7 @@ urem' {n=n} x y with (nextBytes n)
245295 | S (S (S _)) = prim__uremB64 x y
246296 | _ = assert_unreachable
247297
298+||| Unsigned remainder (mod)
248299partial
249300urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
250301urem (MkBits x) (MkBits y) = MkBits (urem' x y)
@@ -447,4 +498,3 @@ bitsToStr x = pack (helper last x)
447498
448499implementation Show (Bits n) where
449500 show = bitsToStr
450−