-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Bit-vector arithmetic library -- -- Bit-vectors implemented as a thin wrapper over integers. @package bv @version 0.4.1 -- | Bit-vector arithmetic inspired by SMT-LIB http://smt-lib.org/ -- and Cryptol http://cryptol.net/. -- -- Bit-vectors are represented as a pair size and value, -- where sizes are of type Int and values are Integer. -- --

Bit-vectors are interpreted as unsigned integers (i.e. natural -- numbers) except for some specific signed operations.
Most operations are in some way size-polymorphic and, if -- required, will perform padding to adjust the size of input -- bit-vectors.

-- -- For documentation purposes we will write [n]k to denote a -- bit-vector of size n representing the natural number -- k. module Data.BitVector -- | An alias for BV. type BitVector = BV -- | Big-endian pseudo size-polymorphic bit-vectors. data BV -- | The size of a bit-vector. size :: BV -> Int -- | An alias for size. width :: BV -> Int -- | The value of a bit-vector, as a natural number. nat :: BV -> Integer -- | An alias for nat. uint :: BV -> Integer -- | 2's complement value of a bit-vector. -- --

--   >>> int [2]3
--   -1
--

-- --

--   >>> int [4]12
--   -4
--

int :: BV -> Integer -- | The empty bit-vector, ie. [0]0. nil :: BV -- | Create a bit-vector given a size and an integer value. -- --

--   >>> bitVec 4 3
--   [4]3
--

-- -- This function also handles negative values. -- --

--   >>> bitVec 4 (-1)
--   [4]15
--

bitVec :: Integral a => Int -> a -> BV -- | List of bit-vector literals of the same size -- -- When a list of integer literals is interpreted as a list of -- bit-vectors, fromInteger is applied to each element invidually: -- --

--   >>> [1,3,5] :: [BV]
--   [ [1]1, [2]3, [3]5 ]
--

-- -- Sometimes we want to specify a list of bit-vectors literals of the -- same size, and for that we can use bitVects: -- --

--   >>> bitVecs 3 [1,3,5]
--   [ [3]1, [3]3, [3]5 ]
--

bitVecs :: Integral a => Int -> [a] -> [BV] -- | Create a mask of ones. ones :: Int -> BV -- | Create a mask of zeros. zeros :: Int -> BV -- | Test if the signed value of a bit-vector is a natural number. isNat :: BV -> Bool -- | Test if the signed value of a bit-vector is a positive number. isPos :: BV -> Bool -- | Fixed-size equality. -- -- In contrast with ==, which is size-polymorphic, this -- equality requires both bit-vectors to be of equal size. -- --

--   >>> [n]k ==. [m]k
--   False
--

-- --

--   >>> [n]k ==. [n]k
--   True
--

(==.) :: BV -> BV -> Bool -- | Fixed-size inequality. -- -- The negated version of ==.. (/=.) :: BV -> BV -> Bool -- | Fixed-size less-than. (<.) :: BV -> BV -> Bool -- | Fixed-size less-than-or-equals. (<=.) :: BV -> BV -> Bool -- | Fixed-size greater-than. (>.) :: BV -> BV -> Bool -- | Fixed-size greater-than-or-equals. (>=.) :: BV -> BV -> Bool -- | Fixed-size signed less-than. slt :: BV -> BV -> Bool -- | Fixed-size signed less-than-or-equals. sle :: BV -> BV -> Bool -- | Fixed-size signed greater-than. sgt :: BV -> BV -> Bool -- | Fixed-size signed greater-than-or-equals. sge :: BV -> BV -> Bool -- | Bit indexing. -- -- u @. i stands for the i-th bit of u. -- --

--   >>> [4]2 @. 0
--   False
--

-- --

--   >>> [4]2 @. 1
--   True
--

(@.) :: Integral ix => BV -> ix -> Bool -- |

--   index i a == a @. i
--

index :: Integral ix => ix -> BV -> Bool -- | Bit-string extraction. -- --

--   u @@ (j,i) == fromBits (map (u @.) [j,j-1..i])
--

-- --

--   >>> [4]7 @@ (3,1)
--   [3]3
--

(@@) :: Integral ix => BV -> (ix, ix) -> BV -- |

--   extract j i a == a @@ (j,i)
--

extract :: Integral ix => ix -> ix -> BV -> BV -- | Bit list indexing. -- --

--   u @: is ==. fromBits $ List.map (u @.) is
--

(@:) :: Integral ix => BV -> [ix] -> BV -- | Reverse bit-indexing. -- -- Index starting from the most significant bit. -- --

--   u !. i == u @. (size u - i - 1)
--

-- --

--   >>> [3]3 !. 0
--   False
--

(!.) :: Integral ix => BV -> ix -> Bool -- | Take least significant bits. -- --

--   least m u == u @@ (m-1,0)
--

least :: Integral ix => ix -> BV -> BV -- | Take most significant bits. -- --

--   most m u == u @@ (n-1,n-m)
--

most :: Integral ix => ix -> BV -> BV -- | Most significant bit. -- --

--   msb u == u !. 0
--

msb :: BV -> Bool -- | Least significant bit. -- --

--   lsb u == u @. 0
--

lsb :: BV -> Bool -- | Most significant 1-bit. -- -- Pre: input must be non-zero. -- --

--   >>> msb1 [4]2
--   1
--

-- --

--   >>> msb1 [4]4
--   2
--

msb1 :: BV -> Int -- | Least significant 1-bit. -- -- Pre: input must be non-zero. -- --

--   >>> msb1 [4]3
--   0
--

-- --

--   >>> msb1 [4]6
--   1
--

lsb1 :: BV -> Int -- | Bit-vector signum as an Integral. signumI :: Integral a => BV -> a -- | Bit-vector exponentiation. -- -- pow [n]k e computes k raised to e modulo -- n. -- -- This is faster than Haskell's (^) operator because it performs modulo -- division just once. Besides, a^0 == [1]0 !!! pow :: Integral exp => BV -> exp -> BV -- | 2's complement signed division. sdiv :: BV -> BV -> BV -- | 2's complement signed remainder (sign follows dividend). srem :: BV -> BV -> BV -- | 2's complement signed remainder (sign follows divisor). smod :: BV -> BV -> BV -- | Ceiling logarithm base 2. -- -- Pre: input bit-vector must be non-zero. lg2 :: BV -> BV -- | Concatenation of two bit-vectors. (#) :: BV -> BV -> BV -- | Concatenation of two bit-vectors. -- | Deprecated: Use (#) or append instead cat :: BV -> BV -> BV -- | Concatenation of two bit-vectors. append :: BV -> BV -> BV -- | An alias for join. concat :: [BV] -> BV -- | Logical extension. -- --

--   >>> zeroExtend 3 [1]1
--   [4]1
--

zeroExtend :: Integral size => size -> BV -> BV -- | Arithmetic extension. -- --

--   >>> signExtend 2 [2]1
--   [4]1
--

-- --

--   >>> signExtend 2 [2]3
--   [4]15
--

signExtend :: Integral size => size -> BV -> BV -- |

--   foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
--

-- --

--   foldl f e = fromBits . foldl f e . toBits
--

foldl :: (a -> Bool -> a) -> a -> BV -> a -- |

--   foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
--

-- --

--   foldl f e = fromBits . foldl f e . toBits
--

-- | Deprecated: Use corresponding versions without underscore foldl_ :: (a -> Bool -> a) -> a -> BV -> a -- |

--   foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
--

-- --

--   foldr f e = fromBits . foldr f e . toBits
--

foldr :: (Bool -> a -> a) -> a -> BV -> a -- |

--   foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
--

-- --

--   foldr f e = fromBits . foldr f e . toBits
--

-- | Deprecated: Use corresponding versions without underscore foldr_ :: (Bool -> a -> a) -> a -> BV -> a -- |

--   reverse == fromBits . reverse . toBits
--

reverse :: BV -> BV -- |

--   reverse == fromBits . reverse . toBits
--

-- | Deprecated: Use corresponding versions without underscore reverse_ :: BV -> BV -- | Pre: if replicate_ n u then n > 0 must -- hold. -- --

--   replicate_ n == fromBits . concat . replicate n . toBits
--

replicate :: Integral size => size -> BV -> BV -- | Pre: if replicate_ n u then n > 0 must -- hold. -- --

--   replicate_ n == fromBits . concat . replicate n . toBits
--

-- | Deprecated: Use corresponding versions without underscore replicate_ :: Integral size => size -> BV -> BV -- | Conjunction. -- -- Essentially, and == foldr1 (.&.). -- -- Returns [1]1 if the input list is empty. and :: [BV] -> BV -- | Conjunction. -- -- Essentially, and == foldr1 (.&.). -- -- Returns [1]1 if the input list is empty. -- | Deprecated: Use corresponding versions without underscore and_ :: [BV] -> BV -- | Disjunction. -- -- Essentially, or == foldr1 (.|.). -- -- Returns [1]0 if the input list is empty. or :: [BV] -> BV -- | Disjunction. -- -- Essentially, or == foldr1 (.|.). -- -- Returns [1]0 if the input list is empty. -- | Deprecated: Use corresponding versions without underscore or_ :: [BV] -> BV -- | Split a bit-vector k times. -- --

--   >>> split 3 [4]15
--   [[2]0,[2]3,[2]3]
--

split :: Integral times => times -> BV -> [BV] -- | Split a bit-vector into n-wide pieces. -- --

--   >>> group 3 [4]15
--   [[3]1,[3]7]
--

group :: Integral size => size -> BV -> [BV] -- | Split a bit-vector into n-wide pieces. -- --

--   >>> group 3 [4]15
--   [[3]1,[3]7]
--

-- | Deprecated: Use corresponding versions without underscore group_ :: Integral size => size -> BV -> [BV] -- | Concatenate a (possibly empty) list of bit-vectors. -- --

--   >>> join [[2]3,[2]2]
--   [4]14
--

--   >>> fromBits [False, False, True]
--   [3]1
--

fromBits :: [Bool] -> BV -- | Create a big-endian list of bits from a bit-vector. -- --

--   >>> toBits [4]11
--   [True, False, True, True]
--

toBits :: BV -> [Bool] -- | Show a bit-vector in binary form. showBin :: BV -> String -- | Show a bit-vector in octal form. showOct :: BV -> String -- | Show a bit-vector in hexadecimal form. showHex :: BV -> String instance Typeable BV instance Data BV instance Bits BV instance Monoid BV instance Integral BV instance Enum BV instance Real BV instance Num BV instance Ord BV instance Eq BV instance Show BV