Hale.Base.Data.Bits

Typeclass for types supporting bitwise operations.

$$\text{Bits}(\alpha)$$ requires at minimum: bitwise AND, OR, XOR, complement, shifts, bit testing, and a notion of zero bits.

Corresponds to Haskell's Data.Bits.Bits.

and : α → α → α
Bitwise AND. $$a \mathbin{\&} b$$
or : α → α → α
Bitwise OR. $$a \mathbin{|} b$$
xor : α → α → α
Bitwise XOR. $$a \oplus b$$
complement : α → α
Bitwise complement. $$\sim a$$
shiftL : α → Nat → α
Left shift by $n$ bits. $$a \ll n$$
shiftR : α → Nat → α
Right shift by $n$ bits. $$a \gg n$$
testBit : α → Nat → Bool
Test bit at position $n$ (zero-indexed from LSB). $$\text{testBit}(a, n) = ((a \gg n) \mathbin{\&} 1) \neq 0$$
bit : Nat → α
The value with only bit $n$ set. $$\text{bit}(n) = 1 \ll n$$
popCount : α → Nat
Count the number of set bits (population count). $$\text{popCount}(a) = |\{i \mid \text{testBit}(a, i)\}|$$
zeroBits : α
The all-zeros value. $$\text{zeroBits} = 0$$
bitSizeMaybe : Option Nat
Bit size if fixed-width, none for arbitrary-width. $$\text{bitSizeMaybe} \in \{\text{none}\} \cup \{\text{some}(n) \mid n \in \mathbb{N}\}$$

Instances

class Data.FiniteBits (α : Type u) extends Data.Bits α :

Typeclass for fixed-width bit types, extending Bits.

$$\text{FiniteBits}(\alpha)$$ adds finiteBitSize, countLeadingZeros, and countTrailingZeros.

and : α → α → α
or : α → α → α
xor : α → α → α
complement : α → α
shiftL : α → Nat → α
shiftR : α → Nat → α
testBit : α → Nat → Bool
bit : Nat → α
popCount : α → Nat
zeroBits : α
bitSizeMaybe : Option Nat
finiteBitSize : Nat
The fixed bit width. $$\text{finiteBitSize} \in \mathbb{N}$$
popCountBounded : α → { n : Nat // n ≤ finiteBitSize α }
Count of set bits (population count), bounded by finiteBitSize. $$\text{popCount}(a) \leq \text{finiteBitSize}$$
countLeadingZeros : α → { n : Nat // n ≤ finiteBitSize α }
Count of leading zeros from MSB, bounded by finiteBitSize.
countTrailingZeros : α → { n : Nat // n ≤ finiteBitSize α }
Count of trailing zeros from LSB, bounded by finiteBitSize.