- data Bits : Nat ->
Type
A "high-level" wrapper to the types defined by machineTy
.
- MkBits : machineTy (nextBytes n) ->
Bits n
An bits type that has at least n bits available,
up to the maximum supported by machineTy
.
- and : Bits n ->
Bits n ->
Bits n
Binary and
- and' : machineTy n ->
machineTy n ->
machineTy n
Binary and
- bitAt : (at : Fin n) ->
Bits n
Create a bitstring of length n with the bit given as an argument set to one
and all other bits set to zero.
- bitsToHexStr : Bits n ->
String
- bitsToInt : Bits n ->
Integer
- bitsToInt' : machineTy (nextBytes n) ->
Integer
- bitsToStr : Bits n ->
String
- bitsUsed : Nat ->
Nat
Finds the number of bits used by machineTy n
.
For example, bitsUsed 2 = 16
- complement : Bits n ->
Bits n
Reverse all the bits in the argument.
- complement' : machineTy (nextBytes n) ->
machineTy (nextBytes n)
- eq : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
Int
- getBit : Fin n ->
Bits n ->
Bool
- getPad : Nat ->
machineTy n
- gt : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
Int
- gte : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
Int
- intToBits : Integer ->
Bits n
- intToBits' : Integer ->
machineTy (nextBytes n)
- lt : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
Int
- lte : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
Int
- machineTy : Nat ->
Type
An index function to access the Bits* types in order.
machineTy 0 = Bits8, machineTy 1 = Bits16, etc.
Any input that would result in getting a type that is larger than supported
will result in the largest supported type instead (currently 64 bits).
- minus : Bits n ->
Bits n ->
Bits n
Subtraction
- minus' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Subtraction
- natToBits : Nat ->
machineTy n
Converts a Nat to a machineTy n.
- natToBits' : machineTy n ->
Nat ->
machineTy n
Converts a Nat to a machineTy n, with the first argument as an accumulator.
You shouldn't have to call this manually, use natToBits (without ') instead.
- nextBytes : Nat ->
Nat
Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.
For example, nextBytes 10 = 1
.
Like with nextPow2, the result is not rounded up, so nextBytes 16 = 1
.
- nextPow2 : Nat ->
Nat
Finds the next exponent of a power of two.
For example nextPow2 200 = 8
, because 2^8 = 256.
If it is an exact match, it is not rounded up: nextPow2 256 = 8
because 2^8 = 256.
- or : Bits n ->
Bits n ->
Bits n
Binary or
- or' : machineTy n ->
machineTy n ->
machineTy n
Binary or
- pad16 : (n : Nat) ->
(Bits16 ->
Bits16 ->
Bits16) ->
Bits16 ->
Bits16 ->
Bits16
Perform a function over Bits16 as if it is carried out on n bits.
(n should be 16 or lower)
- pad16' : Nat ->
(Bits16 ->
Bits16 ->
Bits16) ->
Bits16 ->
Bits16 ->
Bits16
- pad32 : Nat ->
(Bits32 ->
Bits32 ->
Bits32) ->
Bits32 ->
Bits32 ->
Bits32
Perform a function over Bits32 as if it is carried out on n bits.
(n should be 32 or lower)
- pad32' : Nat ->
(Bits32 ->
Bits32 ->
Bits32) ->
Bits32 ->
Bits32 ->
Bits32
- pad64 : Nat ->
(Bits64 ->
Bits64 ->
Bits64) ->
Bits64 ->
Bits64 ->
Bits64
Perform a function over Bits64 as if it is carried out on n bits.
(n should be 64 or lower)
- pad64' : Nat ->
(Bits64 ->
Bits64 ->
Bits64) ->
Bits64 ->
Bits64 ->
Bits64
- pad8 : (n : Nat) ->
(Bits8 ->
Bits8 ->
Bits8) ->
Bits8 ->
Bits8 ->
Bits8
Perform a function over Bits8 as if it is carried out on n bits.
(n should be 8 or lower)
- pad8' : Nat ->
(Bits8 ->
Bits8 ->
Bits8) ->
Bits8 ->
Bits8 ->
Bits8
- plus : Bits n ->
Bits n ->
Bits n
Overflowing addition
- plus' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Overflowing addition
- sdiv : Bits n ->
Bits n ->
Bits n
Signed integer division
- sdiv' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Signed integer division
- setBit : Fin n ->
Bits n ->
Bits n
- sext' : machineTy (nextBytes n) ->
machineTy (nextBytes (n +
m))
- shiftLeft : Bits n ->
Bits n ->
Bits n
Binary left shift
- shiftLeft' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
- shiftRightArithmetic : Bits n ->
Bits n ->
Bits n
Arithematic binary right shift
- shiftRightArithmetic' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Arithematic binary right shift
- shiftRightLogical : Bits n ->
Bits n ->
Bits n
Logical binary right shift
- shiftRightLogical' : machineTy n ->
machineTy n ->
machineTy n
Logical binary right shift
- srem : Bits n ->
Bits n ->
Bits n
Signed remainder (mod)
- srem' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Signed remainder (mod)
- times : Bits n ->
Bits n ->
Bits n
Multiplication
- times' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Multiplication
- trunc' : machineTy (nextBytes (m +
n)) ->
machineTy (nextBytes n)
- truncate : Bits (m +
n) ->
Bits n
Truncate the high bits of a bitstring.
- udiv : Bits n ->
Bits n ->
Bits n
Unsigned integer division
- udiv' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Unsigned integer division
- unsetBit : Fin n ->
Bits n ->
Bits n
- urem : Bits n ->
Bits n ->
Bits n
Unsigned remainder (mod)
- urem' : machineTy (nextBytes n) ->
machineTy (nextBytes n) ->
machineTy (nextBytes n)
Unsigned remainder (mod)
- xor : Bits n ->
Bits n ->
Bits n
Binary xor
- xor' : machineTy n ->
machineTy n ->
machineTy n
Binary xor
- zeroExtend : Bits n ->
Bits (n +
m)
Extend the bitstring with zeros, leaving the first n bits unchanged.
- zeroUnused : machineTy (nextBytes n) ->
machineTy (nextBytes n)
Zero out the high bits of a truncated bitstring
- zext' : machineTy (nextBytes n) ->
machineTy (nextBytes (n +
m))