Language.Hasmtlib.Type.Bitvec

This module provides the type-level length-indexed and MSB-first bitvector Bitvec built on top of the package bitvec and Vector.

It also holds it's type of encoding as a phantom-type via BvEnc.

Examples

>>> minBound @(Bitvec Unsigned 8)
00000000

>>> maxBound @(Bitvec Signed 8)
01111111

>>> (5 :: Bitvec Unsigned 4) + 10
1111

Bitvector encoding

data BvEnc

Type of Bitvector encoding - used as promoted type (data-kind).

Constructors

Unsigned

Signed

Instances

Show BvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

showsPrec :: Int -> BvEnc -> ShowS

show :: BvEnc -> String

showList :: [BvEnc] -> ShowS

Eq BvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

(==) :: BvEnc -> BvEnc -> Bool

(/=) :: BvEnc -> BvEnc -> Bool

Ord BvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

compare :: BvEnc -> BvEnc -> Ordering

(<) :: BvEnc -> BvEnc -> Bool

(<=) :: BvEnc -> BvEnc -> Bool

(>) :: BvEnc -> BvEnc -> Bool

(>=) :: BvEnc -> BvEnc -> Bool

max :: BvEnc -> BvEnc -> BvEnc

min :: BvEnc -> BvEnc -> BvEnc

GCompare SBvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

gcompare :: forall (a :: k) (b :: k). SBvEnc a -> SBvEnc b -> GOrdering a b

GEq SBvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

geq :: forall (a :: k) (b :: k). SBvEnc a -> SBvEnc b -> Maybe (a :~: b)

data SBvEnc (enc :: BvEnc) where

Singleton for BvEnc.

Constructors

SUnsigned :: SBvEnc Unsigned

SSigned :: SBvEnc Signed

Instances

GCompare SBvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

gcompare :: forall (a :: k) (b :: k). SBvEnc a -> SBvEnc b -> GOrdering a b

GEq SBvEnc

Defined in Language.Hasmtlib.Type.Bitvec

Methods

geq :: forall (a :: k) (b :: k). SBvEnc a -> SBvEnc b -> Maybe (a :~: b)

Show (SBvEnc enc)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

showsPrec :: Int -> SBvEnc enc -> ShowS

show :: SBvEnc enc -> String

showList :: [SBvEnc enc] -> ShowS

Eq (SBvEnc enc)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

(==) :: SBvEnc enc -> SBvEnc enc -> Bool

(/=) :: SBvEnc enc -> SBvEnc enc -> Bool

Ord (SBvEnc enc)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

compare :: SBvEnc enc -> SBvEnc enc -> Ordering

(<) :: SBvEnc enc -> SBvEnc enc -> Bool

(<=) :: SBvEnc enc -> SBvEnc enc -> Bool

(>) :: SBvEnc enc -> SBvEnc enc -> Bool

(>=) :: SBvEnc enc -> SBvEnc enc -> Bool

max :: SBvEnc enc -> SBvEnc enc -> SBvEnc enc

min :: SBvEnc enc -> SBvEnc enc -> SBvEnc enc

class KnownBvEnc (enc :: BvEnc) where

Compute singleton SBvEnc from it's promoted type BvEnc.

Methods

bvEncSing :: SBvEnc enc

Instances

KnownBvEnc 'Signed

Defined in Language.Hasmtlib.Type.Bitvec

Methods

bvEncSing :: SBvEnc 'Signed

KnownBvEnc 'Unsigned

Defined in Language.Hasmtlib.Type.Bitvec

Methods

bvEncSing :: SBvEnc 'Unsigned

bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc

Wrapper for bvEncSing which takes a Proxy.

bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc

Wrapper for bvEncSing which takes a Proxy and some ballast. This is helpful for singing on values of type Bitvec where the ballst is a Nat.

Bitvec type

newtype Bitvec (enc :: BvEnc) (n :: Nat)

Length-indexed bitvector (Vector) carrying a phantom type-level BvEnc.

Most significant bit is first (index 0) for unsigned bitvectors. Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1).

Constructors

Bitvec

Fields

• unBitvec :: Vector n Bit

Instances

(KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

(.&.) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(.|.) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

xor :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

complement :: Bitvec enc n -> Bitvec enc n

shift :: Bitvec enc n -> Int -> Bitvec enc n

rotate :: Bitvec enc n -> Int -> Bitvec enc n

zeroBits :: Bitvec enc n

bit :: Int -> Bitvec enc n

setBit :: Bitvec enc n -> Int -> Bitvec enc n

clearBit :: Bitvec enc n -> Int -> Bitvec enc n

complementBit :: Bitvec enc n -> Int -> Bitvec enc n

testBit :: Bitvec enc n -> Int -> Bool

bitSizeMaybe :: Bitvec enc n -> Maybe Int

bitSize :: Bitvec enc n -> Int

isSigned :: Bitvec enc n -> Bool

shiftL :: Bitvec enc n -> Int -> Bitvec enc n

unsafeShiftL :: Bitvec enc n -> Int -> Bitvec enc n

shiftR :: Bitvec enc n -> Int -> Bitvec enc n

unsafeShiftR :: Bitvec enc n -> Int -> Bitvec enc n

rotateL :: Bitvec enc n -> Int -> Bitvec enc n

rotateR :: Bitvec enc n -> Int -> Bitvec enc n

popCount :: Bitvec enc n -> Int

(KnownBvEnc enc, KnownNat n) => Bounded (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

minBound :: Bitvec enc n

maxBound :: Bitvec enc n

(KnownBvEnc enc, KnownNat n) => Enum (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

succ :: Bitvec enc n -> Bitvec enc n

pred :: Bitvec enc n -> Bitvec enc n

toEnum :: Int -> Bitvec enc n

fromEnum :: Bitvec enc n -> Int

enumFrom :: Bitvec enc n -> [Bitvec enc n]

enumFromThen :: Bitvec enc n -> Bitvec enc n -> [Bitvec enc n]

enumFromTo :: Bitvec enc n -> Bitvec enc n -> [Bitvec enc n]

enumFromThenTo :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n -> [Bitvec enc n]

(KnownBvEnc enc, KnownNat n) => Num (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

(+) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(-) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(*) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

negate :: Bitvec enc n -> Bitvec enc n

abs :: Bitvec enc n -> Bitvec enc n

signum :: Bitvec enc n -> Bitvec enc n

fromInteger :: Integer -> Bitvec enc n

(KnownBvEnc enc, KnownNat n) => Integral (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

quot :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

rem :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

div :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

mod :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

quotRem :: Bitvec enc n -> Bitvec enc n -> (Bitvec enc n, Bitvec enc n)

divMod :: Bitvec enc n -> Bitvec enc n -> (Bitvec enc n, Bitvec enc n)

toInteger :: Bitvec enc n -> Integer

(KnownBvEnc enc, KnownNat n) => Real (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

toRational :: Bitvec enc n -> Rational

Show (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

showsPrec :: Int -> Bitvec enc n -> ShowS

show :: Bitvec enc n -> String

showList :: [Bitvec enc n] -> ShowS

Eq (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

(==) :: Bitvec enc n -> Bitvec enc n -> Bool

(/=) :: Bitvec enc n -> Bitvec enc n -> Bool

Ord (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

compare :: Bitvec enc n -> Bitvec enc n -> Ordering

(<) :: Bitvec enc n -> Bitvec enc n -> Bool

(<=) :: Bitvec enc n -> Bitvec enc n -> Bool

(>) :: Bitvec enc n -> Bitvec enc n -> Bool

(>=) :: Bitvec enc n -> Bitvec enc n -> Bool

max :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

min :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

KnownNat n => Boolean (Bitvec enc n)

Defined in Language.Hasmtlib.Type.Bitvec

Methods

bool :: Bool -> Bitvec enc n

true :: Bitvec enc n

false :: Bitvec enc n

(&&) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(||) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(==>) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(<==) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

(<==>) :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

not :: Bitvec enc n -> Bitvec enc n

xor :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n

Render (Bitvec enc n)

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Bitvec enc n -> Builder

Construction

bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)

Concatenation of two bitvectors.

Conversion

Sign

asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n

Convert Bitvec with any encoding BvEnc to Unsigned.

asSigned :: forall enc n. Bitvec enc n -> Bitvec Signed n

Convert Bitvec with any encoding BvEnc to Signed.

Lists

bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)

Constructing a bitvector from a list.

bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)

Constructing a bitvector from a list with length given as Proxy.

Lens

_signBit :: KnownNat (n + 1) => Lens' (Bitvec Signed (n + 1)) Bit

A Lens on the sign-bit of a signed bitvector.