Data.BitVector.Sized

This module defines a width-parameterized BV type and various associated operations. A BV w is a newtype around an Integer, so operations that require the width take an explicit NatRepr w argument. We explicitly do not allow widths that cannot be represented as an Int, as we appeal to the underlying Num and Bits instances on Integer for the implementation of many of the same operations (which, in turn, require those widths to be Ints).

We omit all typeclass instances that require compile-time knowledge of bitvector width, or force a signed or unsigned intepretation. Those instances can be recovered via the use of SignedBV or UnsignedBV.

This module should be imported qualified, as many of the names clash with those in Prelude or other base packages.

BV type

data BV (w :: Nat) :: Type

Bitvector datatype, parameterized by width.

Instances

EqF BV

Defined in Data.BitVector.Sized.Internal

Methods

eqF :: forall (a :: k). BV a -> BV a -> Bool

ShowF BV

Defined in Data.BitVector.Sized.Internal

Methods

withShow :: forall p q (tp :: k) a. p BV -> q tp -> (Show (BV tp) => a) -> a

showF :: forall (tp :: k). BV tp -> String

showsPrecF :: forall (tp :: k). Int -> BV tp -> String -> String

Lift (BV w :: Type)

Defined in Data.BitVector.Sized.Internal

Methods

lift :: BV w -> Q Exp

liftTyped :: BV w -> Q (TExp (BV w))

Eq (BV w)

Defined in Data.BitVector.Sized.Internal

Methods

(==) :: BV w -> BV w -> Bool

(/=) :: BV w -> BV w -> Bool

Ord (BV w)

Uses an unsigned ordering, but ule and ult are preferred. We provide this instance to allow the use of BV in situations where an arbitrary ordering is required (e.g., as the keys in a map)

Defined in Data.BitVector.Sized.Internal

Methods

compare :: BV w -> BV w -> Ordering

(<) :: BV w -> BV w -> Bool

(<=) :: BV w -> BV w -> Bool

(>) :: BV w -> BV w -> Bool

(>=) :: BV w -> BV w -> Bool

max :: BV w -> BV w -> BV w

min :: BV w -> BV w -> BV w

Read (BV w)

Defined in Data.BitVector.Sized.Internal

Methods

readsPrec :: Int -> ReadS (BV w)

readList :: ReadS [BV w]

readPrec :: ReadPrec (BV w)

readListPrec :: ReadPrec [BV w]

Show (BV w)

Defined in Data.BitVector.Sized.Internal

Methods

showsPrec :: Int -> BV w -> ShowS

show :: BV w -> String

showList :: [BV w] -> ShowS

Generic (BV w)

Defined in Data.BitVector.Sized.Internal

Associated Types

type Rep (BV w) :: Type -> Type

Methods

from :: BV w -> Rep (BV w) x

to :: Rep (BV w) x -> BV w

NFData (BV w)

Defined in Data.BitVector.Sized.Internal

Methods

rnf :: BV w -> ()

Hashable (BV w)

Defined in Data.BitVector.Sized.Internal

Methods

hashWithSalt :: Int -> BV w -> Int

hash :: BV w -> Int

type Rep (BV w)

Defined in Data.BitVector.Sized.Internal

type Rep (BV w) = D1 ('MetaData "BV" "Data.BitVector.Sized.Internal" "bv-sized-1.0.3-G3lfCRRp5IxDUT13KXmGib" 'False) (C1 ('MetaCons "BV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

pattern BV :: Integer -> BV w

Get the underlying Integer representation from a BV. We guarantee that (\(BV.BV x) -> x) == BV.asUnsigned.

NatReprs (from parameterized-utils)

data NatRepr (n :: Nat)

A runtime presentation of a type-level Nat.

This can be used for performing dynamic checks on a type-level natural numbers.

Instances

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b)

DecidableEq NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)

OrdF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

ShowF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

withShow :: forall p q (tp :: k) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a

showF :: forall (tp :: k). NatRepr tp -> String

showsPrecF :: forall (tp :: k). Int -> NatRepr tp -> String -> String

HashableF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSaltF :: forall (tp :: k). Int -> NatRepr tp -> Int

hashF :: forall (tp :: k). NatRepr tp -> Int

KnownNat n => KnownRepr NatRepr (n :: Nat)

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n

Eq (NatRepr m)

Defined in Data.Parameterized.NatRepr.Internal

Methods

(==) :: NatRepr m -> NatRepr m -> Bool

(/=) :: NatRepr m -> NatRepr m -> Bool

KnownNat n => Data (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n)

toConstr :: NatRepr n -> Constr

dataTypeOf :: NatRepr n -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n))

gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r

gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

Show (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

showsPrec :: Int -> NatRepr n -> ShowS

show :: NatRepr n -> String

showList :: [NatRepr n] -> ShowS

Hashable (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSalt :: Int -> NatRepr n -> Int

hash :: NatRepr n -> Int

PolyEq (NatRepr m) (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)

polyEq :: NatRepr m -> NatRepr n -> Bool

knownNat :: forall (n :: Nat). KnownNat n => NatRepr n

This generates a NatRepr from a type-level context.

Constructors

mkBV

Arguments

:: NatRepr w

Desired bitvector width

-> Integer

Integer value to truncate to bitvector width

-> BV w

Construct a bitvector with a particular width, where the width is provided as an explicit NatRepr argument. The input Integer, whether positive or negative, is silently truncated to fit into the number of bits demanded by the return type. The width cannot be arbitrarily large; it must be representable as an Int.

>>> mkBV (knownNat @4) 10
BV 10
>>> mkBV (knownNat @2) 10
BV 2
>>> mkBV (knownNat @4) (-2)
BV 14

mkBVUnsigned

Arguments

:: NatRepr w

Desired bitvector width

-> Integer

Integer value

-> Maybe (BV w)

Like mkBV, but returns Nothing if unsigned input integer cannot be represented in w bits.

mkBVSigned

Arguments

:: 1 <= w

=> NatRepr w

Desired bitvector width

-> Integer

Integer value

-> Maybe (BV w)

Like mkBV, but returns Nothing if signed input integer cannot be represented in w bits.

unsignedClamp :: NatRepr w -> Integer -> BV w

unsignedClamp w i rounds i to the nearest value between 0 and 2^w - 1 (inclusive).

signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w

signedClamp w i rounds i to the nearest value between -2^(w-1) and 2^(w-1) - 1 (inclusive).

minUnsigned :: NatRepr w -> BV w

The minimum unsigned value for bitvector with given width (always 0).

maxUnsigned :: NatRepr w -> BV w

The maximum unsigned value for bitvector with given width.

minSigned :: 1 <= w => NatRepr w -> BV w

The minimum value for bitvector in two's complement with given width.

maxSigned :: 1 <= w => NatRepr w -> BV w

The maximum value for bitvector in two's complement with given width.

zero :: NatRepr w -> BV w

The zero bitvector of any width.

one :: 1 <= w => NatRepr w -> BV w

The bitvector with value 1, of any positive width.

width :: NatRepr w -> BV w

The bitvector whose value is its own width, of any width.

Construction from fixed-width data types

bool :: Bool -> BV 1

Construct a BV from a Bool.

word8 :: Word8 -> BV 8

Construct a BV from a Word8.

word16 :: Word16 -> BV 16

Construct a BV from a Word16.

word32 :: Word32 -> BV 32

Construct a BV from a Word32.

word64 :: Word64 -> BV 64

Construct a BV from a Word64.

int8 :: Int8 -> BV 8

Construct a BV from an Int8.

int16 :: Int16 -> BV 16

Construct a BV from an Int16.

int32 :: Int32 -> BV 32

Construct a BV from an Int32.

int64 :: Int64 -> BV 64

Construct a BV from an Int64.

bitsBE :: [Bool] -> Pair NatRepr BV

Construct a BV from a list of bits, in big endian order (bits with lower value index in the list are mapped to higher order bits in the output bitvector). Return the resulting BV along with its width.

>>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
(2,BV 2)

bitsLE :: [Bool] -> Pair NatRepr BV

Construct a BV from a list of bits, in little endian order (bits with lower value index in the list are mapped to lower order bits in the output bitvector). Return the resulting BV along with its width.

>>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
(2,BV 1)

bytesBE :: [Word8] -> Pair NatRepr BV

Construct a BV from a list of bytes, in big endian order (bytes with lower value index in the list are mapped to higher order bytes in the output bitvector).

>>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)
(24,BV 257)

bytesLE :: [Word8] -> Pair NatRepr BV

Construct a BV from a list of bytes, in little endian order (bytes with lower value index in the list are mapped to lower order bytes in the output bitvector).

>>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)
(24,BV 65792)

bytestringBE :: ByteString -> Pair NatRepr BV

Construct a BV from a big-endian bytestring.

>>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
(24,BV 257)

bytestringLE :: ByteString -> Pair NatRepr BV

Construct a BV from a little-endian bytestring.

>>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
(24,BV 65792)

Conversions to primitive types

asSigned :: 1 <= w => NatRepr w -> BV w -> Integer

Signed interpretation of a bitvector as an Integer.

asUnsigned :: BV w -> Integer

Unsigned interpretation of a bitvector as a positive Integer.

asNatural :: BV w -> Natural

Unsigned interpretation of a bitvector as a Natural.

asBitsBE :: NatRepr w -> BV w -> [Bool]

Convert a bitvector to a list of bits, in big endian order (higher order bits in the bitvector are mapped to lower indices in the output list).

>>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
[False,True,True,False,True]

asBitsLE :: NatRepr w -> BV w -> [Bool]

Convert a bitvector to a list of bits, in little endian order (lower order bits in the bitvector are mapped to lower indices in the output list).

>>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
[True,False,True,True,False]

asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]

Convert a bitvector to a list of bytes, in big endian order (higher order bytes in the bitvector are mapped to lower indices in the output list). Return Nothing if the width is not a multiple of 8.

>>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
Just [170,187,204,221]

asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]

Convert a bitvector to a list of bytes, in little endian order (lower order bytes in the bitvector are mapped to lower indices in the output list). Return Nothing if the width is not a multiple of 8.

>>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
Just [221,204,187,170]

asBytestringBE :: NatRepr w -> BV w -> Maybe ByteString

asBytesBE, but for bytestrings.

asBytestringLE :: NatRepr w -> BV w -> Maybe ByteString

asBytesLE, but for bytestrings.

Bits operations (width-preserving)

BV versions of the functions in Data.Bits.

and :: BV w -> BV w -> BV w

Bitwise and.

or :: BV w -> BV w -> BV w

Bitwise or.

xor :: BV w -> BV w -> BV w

Bitwise xor.

complement :: NatRepr w -> BV w -> BV w

Bitwise complement (flip every bit).

shl :: NatRepr w -> BV w -> Natural -> BV w

Left shift by positive Natural.

lshr :: NatRepr w -> BV w -> Natural -> BV w

Right logical shift by positive Natural.

ashr :: 1 <= w => NatRepr w -> BV w -> Natural -> BV w

Right arithmetic shift by positive Natural.

rotateL :: NatRepr w -> BV w -> Natural -> BV w

Bitwise rotate left.

rotateR :: NatRepr w -> BV w -> Natural -> BV w

Bitwise rotate right.

bit

Arguments

:: (ix + 1) <= w

=> NatRepr w

Desired output width

-> NatRepr ix

Index of bit to set

-> BV w

The BV that has a particular bit set, and is 0 everywhere else.

bit'

Arguments

:: NatRepr w

Desired output width

-> Natural

Index of bit to set

-> BV w

Like bit, but without the requirement that the index bit refers to an actual bit in the output BV. If it is out of range, just silently return the zero bitvector.

setBit

Arguments

:: (ix + 1) <= w

=> NatRepr ix

Index of bit to set

-> BV w

Original bitvector

-> BV w

setBit bv ix is the same as or bv (bit knownNat ix).

setBit'

Arguments

:: NatRepr w

Desired output width

-> Natural

Index of bit to set

-> BV w

Original bitvector

-> BV w

Like setBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

clearBit

Arguments

:: (ix + 1) <= w

=> NatRepr w

Desired output width

-> NatRepr ix

Index of bit to clear

-> BV w

Original bitvector

-> BV w

clearBit w bv ix is the same as and bv (complement (bit w ix)).

clearBit'

Arguments

:: NatRepr w

Desired output width

-> Natural

Index of bit to clear

-> BV w

Original bitvector

-> BV w

Like clearBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

complementBit

Arguments

:: (ix + 1) <= w

=> NatRepr ix

Index of bit to flip

-> BV w

Original bitvector

-> BV w

complementBit bv ix is the same as xor bv (bit knownNat ix).

complementBit'

Arguments

:: NatRepr w

Desired output width

-> Natural

Index of bit to flip

-> BV w

Original bitvector

-> BV w

Like complementBit, but without the requirement that the index bit refers to an actual bit in the input BV. If it is out of range, just silently return the original input.

testBit :: (ix + 1) <= w => NatRepr ix -> BV w -> Bool

Test if a particular bit is set.

testBit' :: Natural -> BV w -> Bool

Like testBit, but takes a Natural for the bit index. If the index is out of bounds, return False.

popCount :: BV w -> BV w

Get the number of 1 bits in a BV.

ctz :: NatRepr w -> BV w -> BV w

Count trailing zeros in a BV.

clz :: NatRepr w -> BV w -> BV w

Count leading zeros in a BV.

truncBits :: Natural -> BV w -> BV w

Truncate a bitvector to a particular width given at runtime, while keeping the type-level width constant.

Arithmetic operations (width-preserving)

add :: NatRepr w -> BV w -> BV w -> BV w

Bitvector add.

sub :: NatRepr w -> BV w -> BV w -> BV w

Bitvector subtract.

mul :: NatRepr w -> BV w -> BV w -> BV w

Bitvector multiply.

uquot :: BV w -> BV w -> BV w

Bitvector division (unsigned). Rounds to zero. Division by zero yields a runtime error.

squot :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Bitvector division (signed). Rounds to zero. Division by zero yields a runtime error.

sdiv :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Bitvector division (signed). Rounds to negative infinity. Division by zero yields a runtime error.

urem :: BV w -> BV w -> BV w

Bitvector remainder after division (unsigned), when rounded to zero. Division by zero yields a runtime error.

srem :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Bitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.

smod :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Bitvector remainder after division (signed), when rounded to negative infinity. Division by zero yields a runtime error.

uquotRem :: BV w -> BV w -> (BV w, BV w)

uquot and urem returned as a pair.

squotRem :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)

squot and srem returned as a pair.

sdivMod :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)

sdiv and smod returned as a pair.

abs :: 1 <= w => NatRepr w -> BV w -> BV w

Bitvector absolute value. Returns the 2's complement magnitude of the bitvector.

negate :: NatRepr w -> BV w -> BV w

2's complement bitvector negation.

signBit :: 1 <= w => NatRepr w -> BV w -> BV w

Get the sign bit as a BV.

signum :: 1 <= w => NatRepr w -> BV w -> BV w

Return 1 if positive, -1 if negative, and 0 if 0.

slt :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool

Signed less than.

sle :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool

Signed less than or equal.

ult :: BV w -> BV w -> Bool

Unsigned less than.

ule :: BV w -> BV w -> Bool

Unsigned less than or equal.

umin :: BV w -> BV w -> BV w

Unsigned minimum of two bitvectors.

umax :: BV w -> BV w -> BV w

Unsigned maximum of two bitvectors.

smin :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Signed minimum of two bitvectors.

smax :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

Signed maximum of two bitvectors.

Variable-width operations

These are functions that involve bit vectors of different lengths.

concat

Arguments

:: NatRepr w

Width of higher-order bits

-> NatRepr w'

Width of lower-order bits

-> BV w

Higher-order bits

-> BV w'

Lower-order bits

-> BV (w + w')

Concatenate two bitvectors. The first argument gets placed in the higher order bits.

>>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
BV 6
>>> :type it
it :: BV 5

select

Arguments

:: (ix + w') <= w

=> NatRepr ix

Index to start selecting from

-> NatRepr w'

Desired output width

-> BV w

Bitvector to select from

-> BV w'

Slice out a smaller bitvector from a larger one.

>>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
BV 3
>>> :type it
it :: BV 4

select'

Arguments

:: Natural

Index to start selecting from

-> NatRepr w'

Desired output width

-> BV w

Bitvector to select from

-> BV w'

Like select, but takes a Natural as the index to start selecting from. Neither the index nor the output width is checked to ensure the resulting BV lies entirely within the bounds of the original bitvector. Any bits "selected" from beyond the bounds of the input bitvector will be 0.

>>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
BV 6
>>> :type it
it :: BV 4

zext

Arguments

:: (w + 1) <= w'

=> NatRepr w'

Desired output width

-> BV w

Bitvector to extend

-> BV w'

Zero-extend a bitvector to one of strictly greater width.

>>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
BV 13
>>> :type it
it :: BV 8

sext

Arguments

:: (1 <= w, (w + 1) <= w')

=> NatRepr w

Width of input bitvector

-> NatRepr w'

Desired output width

-> BV w

Bitvector to extend

-> BV w'

Sign-extend a bitvector to one of strictly greater width.

trunc

Arguments

:: (w' + 1) <= w

=> NatRepr w'

Desired output width

-> BV w

Bitvector to truncate

-> BV w'

Truncate a bitvector to one of strictly smaller width.

trunc'

Arguments

:: NatRepr w'

Desired output width

-> BV w

Bitvector to truncate

-> BV w'

Like trunc, but allows the input width to be greater than or equal to the output width, in which case it just performs a zero extension.

mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')

Wide multiply of two bitvectors.

Enum operations

succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)

Unsigned successor. succUnsigned w (maxUnsigned w) returns Nothing.

succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)

Signed successor. succSigned w (maxSigned w) returns Nothing.

predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)

Unsigned predecessor. predUnsigned w zero returns Nothing.

predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)

Signed predecessor. predSigned w (minSigned w) returns Nothing.

enumFromToUnsigned

Arguments

:: BV w

Lower bound

-> BV w

Upper bound

-> [BV w]

List of all unsigned bitvectors from a lower to an upper bound, inclusive.

enumFromToSigned

Arguments

:: 1 <= w

=> NatRepr w

-> BV w

Lower bound

-> BV w

Upper bound

-> [BV w]

List of all signed bitvectors from a lower to an upper bound, inclusive.

Generating random bitvectors

BV versions of the functions in Random.

uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)

Generates a bitvector uniformly distributed over all possible values for a given width. (See uniformM).

uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)

Generates a bitvector uniformly distributed over the provided range (interpreted as a range of unsigned bitvectors), which is interpreted as inclusive in the lower and upper bound. (See uniformRM).

sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)

Generates a bitvector uniformly distributed over the provided range (interpreted as a range of signed bitvectors), which is interpreted as inclusive in the lower and upper bound. (See uniformRM).

Pretty printing

ppHex :: NatRepr w -> BV w -> String

Pretty print in hex

ppBin :: NatRepr w -> BV w -> String

Pretty print in binary

ppOct :: NatRepr w -> BV w -> String

Pretty print in octal

ppDec :: NatRepr w -> BV w -> String

Pretty print in decimal