@@ -19,8 +19,8 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
1919 l2x = log2NZ (S x) SIsNotZ
2020
2121||| 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`.
22+||| For example, `nextBytes 10 = 1`.
23+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 1`.
2424public export
2525nextBytes : Nat -> Nat
2626nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
@@ -368,6 +368,7 @@ complement' {n=n} x with (nextBytes n)
368368 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
369369 | _ = assert_unreachable
370370
371+||| Reverse all the bits in the argument.
371372complement : %static {n : Nat} -> Bits n -> Bits n
372373complement (MkBits x) = MkBits (complement' x)
373374
@@ -386,6 +387,7 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
386387 | (S (S (S _)), S (S (S _))) = believe_me x
387388 | _ = assert_unreachable
388389
390+||| Extend the bitstring with zeros, leaving the first n bits unchanged.
389391zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
390392zeroExtend (MkBits x) = MkBits (zext' x)
391393
@@ -418,7 +420,7 @@ bitsToInt' {n=n} x with (nextBytes n)
418420bitsToInt : %static {n : Nat} -> Bits n -> Integer
419421bitsToInt (MkBits x) = bitsToInt' x
420422
421−-- Zero out the high bits of a truncated bitstring
423+||| Zero out the high bits of a truncated bitstring
422424zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
423425zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
424426
@@ -474,10 +476,13 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
474476 | (S (S (S _)), S (S (S _))) = believe_me x
475477 | _ = assert_unreachable
476478
479+||| Truncate the high bits of a bitstring.
477480truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n
478481truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
479482
480−bitAt : %static {n : Nat} -> Fin n -> Bits n
483+||| Create a bitstring of length n with the bit given as an argument set to one
484+||| and all other bits set to zero.
485+bitAt : %static {n : Nat} -> (at : Fin n) -> Bits n
481486bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
482487
483488getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool