@@ -72,22 +72,29 @@ data Bits : Nat -> Type where
7272 ||| up to the maximum supported by `machineTy`.
7373 MkBits : machineTy (nextBytes n) -> Bits n
7474
75−||| Perform a function over Bits8 as if it is carried out on n bits
76−pad8 : (n : Nat) -> (f :(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
7778pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
7879 where
7980 pad = getPad {n=0} n
8081
81−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
8285pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
8386 where
8487 pad = getPad {n=1} n
8588
89+||| Perform a function over Bits32 as if it is carried out on n bits.
90+||| (n should be 32 or lower)
8691pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
8792pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
8893 where
8994 pad = getPad {n=2} n
9095
96+||| Perform a function over Bits64 as if it is carried out on n bits.
97+||| (n should be 64 or lower)
9198pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
9299pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
93100 where
@@ -114,7 +121,7 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
114121 where
115122 pad = getPad {n=3} n
116123
117−-- 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
118125-- public export, or is export good enough?
119126shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
120127shiftLeft' {n=n} x c with (nextBytes n)
@@ -124,9 +131,11 @@ shiftLeft' {n=n} x c with (nextBytes n)
124131 | S (S (S _)) = pad64' n prim__shlB64 x c
125132 | _ = assert_unreachable
126133
134+||| Binary left shift
127135shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n
128136shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
129137
138+||| Logical binary right shift
130139shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
131140shiftRightLogical' {n=n} x c with (n)
132141 | Z = prim__lshrB8 x c
@@ -135,10 +144,12 @@ shiftRightLogical' {n=n} x c with (n)
135144 | S (S (S _)) = prim__lshrB64 x c
136145 | _ = assert_unreachable
137146
147+||| Logical binary right shift
138148shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n
139149shiftRightLogical {n} (MkBits x) (MkBits y)
140150 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
141151
152+||| Arithematic binary right shift
142153shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
143154shiftRightArithmetic' {n=n} x c with (nextBytes n)
144155 | Z = pad8' n prim__ashrB8 x c
@@ -147,9 +158,11 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)
147158 | S (S (S _)) = pad64' n prim__ashrB64 x c
148159 | _ = assert_unreachable
149160
161+||| Arithematic binary right shift
150162shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n
151163shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
152164
165+||| Binary and
153166and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
154167and' {n=n} x y with (n)
155168 | Z = prim__andB8 x y
@@ -158,9 +171,11 @@ and' {n=n} x y with (n)
158171 | S (S (S _)) = prim__andB64 x y
159172 | _ = assert_unreachable
160173
174+||| Binary and
161175and : %static {n : Nat} -> Bits n -> Bits n -> Bits n
162176and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
163177
178+||| Binary or
164179or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
165180or' {n=n} x y with (n)
166181 | Z = prim__orB8 x y
@@ -169,9 +184,11 @@ or' {n=n} x y with (n)
169184 | S (S (S _)) = prim__orB64 x y
170185 | _ = assert_unreachable
171186
187+||| Binary or
172188or : %static {n : Nat} -> Bits n -> Bits n -> Bits n
173189or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
174190
191+||| Binary xor
175192xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
176193xor' {n=n} x y with (n)
177194 | Z = prim__xorB8 x y
@@ -180,9 +197,11 @@ xor' {n=n} x y with (n)
180197 | S (S (S _)) = prim__xorB64 x y
181198 | _ = assert_unreachable
182199
200+||| Binary xor
183201xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n
184202xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
185203
204+||| Overflowing addition
186205plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
187206plus' {n=n} x y with (nextBytes n)
188207 | Z = pad8 n prim__addB8 x y
@@ -191,9 +210,11 @@ plus' {n=n} x y with (nextBytes n)
191210 | S (S (S _)) = pad64 n prim__addB64 x y
192211 | _ = assert_unreachable
193212
213+||| Overflowing addition
194214plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
195215plus (MkBits x) (MkBits y) = MkBits (plus' x y)
196216
217+||| Subtraction
197218minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
198219minus' {n=n} x y with (nextBytes n)
199220 | Z = pad8 n prim__subB8 x y
@@ -202,9 +223,11 @@ minus' {n=n} x y with (nextBytes n)
202223 | S (S (S _)) = pad64 n prim__subB64 x y
203224 | _ = assert_unreachable
204225
226+||| Subtraction
205227minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
206228minus (MkBits x) (MkBits y) = MkBits (minus' x y)
207229
230+||| Multiplication
208231times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
209232times' {n=n} x y with (nextBytes n)
210233 | Z = pad8 n prim__mulB8 x y
@@ -213,9 +236,11 @@ times' {n=n} x y with (nextBytes n)
213236 | S (S (S _)) = pad64 n prim__mulB64 x y
214237 | _ = assert_unreachable
215238
239+||| Multiplication
216240times : %static {n : Nat} -> Bits n -> Bits n -> Bits n
217241times (MkBits x) (MkBits y) = MkBits (times' x y)
218242
243+||| Signed integer division
219244partial
220245sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221246sdiv' {n=n} x y with (nextBytes n)
@@ -225,10 +250,12 @@ sdiv' {n=n} x y with (nextBytes n)
225250 | S (S (S _)) = prim__sdivB64 x y
226251 | _ = assert_unreachable
227252
253+||| Signed integer division
228254partial
229255sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
230256sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
231257
258+||| Unsigned integer division
232259partial
233260udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
234261udiv' {n=n} x y with (nextBytes n)
@@ -238,10 +265,12 @@ udiv' {n=n} x y with (nextBytes n)
238265 | S (S (S _)) = prim__udivB64 x y
239266 | _ = assert_unreachable
240267
268+||| Unsigned integer division
241269partial
242270udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
243271udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
244272
273+||| Signed remainder (mod)
245274partial
246275srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
247276srem' {n=n} x y with (nextBytes n)
@@ -251,10 +280,12 @@ srem' {n=n} x y with (nextBytes n)
251280 | S (S (S _)) = prim__sremB64 x y
252281 | _ = assert_unreachable
253282
283+||| Signed remainder (mod)
254284partial
255285srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
256286srem (MkBits x) (MkBits y) = MkBits (srem' x y)
257287
288+||| Unsigned remainder (mod)
258289partial
259290urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
260291urem' {n=n} x y with (nextBytes n)
@@ -264,6 +295,7 @@ urem' {n=n} x y with (nextBytes n)
264295 | S (S (S _)) = prim__uremB64 x y
265296 | _ = assert_unreachable
266297
298+||| Unsigned remainder (mod)
267299partial
268300urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
269301urem (MkBits x) (MkBits y) = MkBits (urem' x y)