-- 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.5


-- | Bit-vector arithmetic inspired by SMT-LIB <a>http://smt-lib.org/</a>
--   and Cryptol <a>http://cryptol.net/</a>.
--   
--   Bit-vectors are represented as a pair <i>size</i> and <i>value</i>,
--   where sizes are of type <a>Int</a> and values are <a>Integer</a>.
--   
--   <ul>
--   <li>Bit-vectors are interpreted as unsigned integers (i.e. natural
--   numbers) except for some specific <i>signed</i> operations.</li>
--   <li>Most operations are in some way <i>size-polymorphic</i> and, if
--   required, will perform padding to adjust the size of input
--   bit-vectors.</li>
--   </ul>
--   
--   For documentation purposes we will write <tt>[n]k</tt> to denote a
--   bit-vector of size <tt>n</tt> representing the natural number
--   <tt>k</tt>.
module Data.BitVector

-- | An alias for <a>BV</a>.
type BitVector = BV

-- | Big-endian <i>pseudo size-polymorphic</i> bit-vectors.
data BV

-- | The <i>size</i> of a bit-vector.
size :: BV -> Int

-- | An alias for <a>size</a>.
width :: BV -> Int

-- | The value of a bit-vector, as a natural number.
nat :: BV -> Integer

-- | An alias for <a>nat</a>.
uint :: BV -> Integer

-- | 2's complement value of a bit-vector.
--   
--   <pre>
--   &gt;&gt;&gt; int [2]3
--   -1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; int [4]12
--   -4
--   </pre>
int :: BV -> Integer

-- | The <i>empty</i> bit-vector, ie. <tt>[0]0</tt>.
nil :: BV

-- | Create a bit-vector given a size and an integer value.
--   
--   <pre>
--   &gt;&gt;&gt; bitVec 4 3
--   [4]3
--   </pre>
--   
--   This function also handles negative values.
--   
--   <pre>
--   &gt;&gt;&gt; bitVec 4 (-1)
--   [4]15
--   </pre>
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, <a>fromInteger</a> is applied to each element invidually:
--   
--   <pre>
--   &gt;&gt;&gt; [1,3,5] :: [BV]
--   [ [1]1, [2]3, [3]5 ]
--   </pre>
--   
--   Sometimes we want to specify a list of bit-vectors literals of the
--   same size, and for that we can use <tt>bitVects</tt>:
--   
--   <pre>
--   &gt;&gt;&gt; bitVecs 3 [1,3,5]
--   [ [3]1, [3]3, [3]5 ]
--   </pre>
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 <a>==</a>, which is <i>size-polymorphic</i>, this
--   equality requires both bit-vectors to be of equal size.
--   
--   <pre>
--   &gt;&gt;&gt; [n]k ==. [m]k
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [n]k ==. [n]k
--   True
--   </pre>
(==.) :: BV -> BV -> Bool
infix 4 ==.

-- | Fixed-size inequality.
--   
--   The negated version of <a>==.</a>.
(/=.) :: BV -> BV -> Bool
infix 4 /=.

-- | Fixed-size <i>less-than</i>.
(<.) :: BV -> BV -> Bool
infix 4 <.

-- | Fixed-size <i>less-than-or-equals</i>.
(<=.) :: BV -> BV -> Bool
infix 4 <=.

-- | Fixed-size <i>greater-than</i>.
(>.) :: BV -> BV -> Bool
infix 4 >.

-- | Fixed-size <i>greater-than-or-equals</i>.
(>=.) :: BV -> BV -> Bool
infix 4 >=.

-- | Fixed-size signed <i>less-than</i>.
slt :: BV -> BV -> Bool
infix 4 `slt`

-- | Fixed-size signed <i>less-than-or-equals</i>.
sle :: BV -> BV -> Bool
infix 4 `sle`

-- | Fixed-size signed <i>greater-than</i>.
sgt :: BV -> BV -> Bool
infix 4 `sgt`

-- | Fixed-size signed <i>greater-than-or-equals</i>.
sge :: BV -> BV -> Bool
infix 4 `sge`

-- | Bit indexing.
--   
--   <tt>u @. i</tt> stands for the <i>i</i>-th bit of <i>u</i>.
--   
--   <pre>
--   &gt;&gt;&gt; [4]2 @. 0
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [4]2 @. 1
--   True
--   </pre>
(@.) :: Integral ix => BV -> ix -> Bool
infixl 9 @.

-- | <pre>
--   index i a == a @. i
--   </pre>
index :: Integral ix => ix -> BV -> Bool

-- | Bit-string extraction.
--   
--   <pre>
--   u @@ (j,i) == fromBits (map (u @.) [j,j-1..i])
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [4]7 @@ (3,1)
--   [3]3
--   </pre>
(@@) :: Integral ix => BV -> (ix, ix) -> BV
infixl 9 @@

-- | <pre>
--   extract j i a == a @@ (j,i)
--   </pre>
extract :: Integral ix => ix -> ix -> BV -> BV

-- | Bit list indexing.
--   
--   <pre>
--   u @: is ==. fromBits $ List.map (u @.) is
--   </pre>
(@:) :: Integral ix => BV -> [ix] -> BV
infixl 9 @:

-- | Reverse bit-indexing.
--   
--   Index starting from the most significant bit.
--   
--   <pre>
--   u !. i == u @. (size u - i - 1)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [3]3 !. 0
--   False
--   </pre>
(!.) :: Integral ix => BV -> ix -> Bool
infixl 9 !.

-- | Take least significant bits.
--   
--   <pre>
--   least m u == u @@ (m-1,0)
--   </pre>
least :: Integral ix => ix -> BV -> BV

-- | Take most significant bits.
--   
--   <pre>
--   most m u == u @@ (n-1,n-m)
--   </pre>
most :: Integral ix => ix -> BV -> BV

-- | Most significant bit.
--   
--   <pre>
--   msb u == u !. 0
--   </pre>
msb :: BV -> Bool

-- | Least significant bit.
--   
--   <pre>
--   lsb u == u @. 0
--   </pre>
lsb :: BV -> Bool

-- | Most significant 1-bit.
--   
--   <i>Pre</i>: input must be non-zero.
--   
--   <pre>
--   &gt;&gt;&gt; msb1 [4]2
--   1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; msb1 [4]4
--   2
--   </pre>
msb1 :: BV -> Int

-- | Least significant 1-bit.
--   
--   <i>Pre</i>: input must be non-zero.
--   
--   <pre>
--   &gt;&gt;&gt; msb1 [4]3
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; msb1 [4]6
--   1
--   </pre>
lsb1 :: BV -> Int

-- | Bit-vector <a>signum</a> as an <a>Integral</a>.
signumI :: Integral a => BV -> a

-- | Bit-vector exponentiation.
--   
--   <tt>pow [n]k e</tt> computes <tt>k</tt> raised to <tt>e</tt> modulo
--   <tt>n</tt>.
--   
--   This is faster than Haskell's (^) operator because it performs modulo
--   division just once. Besides, <tt>a^0 == [1]0</tt> !!!
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.
--   
--   <i>Pre</i>: input bit-vector must be non-zero.
lg2 :: BV -> BV

-- | Concatenation of two bit-vectors.
(#) :: BV -> BV -> BV
infixr 5 #

-- | Concatenation of two bit-vectors.

-- | <i>Deprecated: Use (#) or append instead</i>
cat :: BV -> BV -> BV

-- | Concatenation of two bit-vectors.
append :: BV -> BV -> BV

-- | An alias for <a>join</a>.
concat :: [BV] -> BV

-- | Logical extension.
--   
--   <pre>
--   &gt;&gt;&gt; zeroExtend 3 [1]1
--   [4]1
--   </pre>
zeroExtend :: Integral size => size -> BV -> BV

-- | Arithmetic extension.
--   
--   <pre>
--   &gt;&gt;&gt; signExtend 2 [2]1
--   [4]1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; signExtend 2 [2]3
--   [4]15
--   </pre>
signExtend :: Integral size => size -> BV -> BV

-- | <pre>
--   foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
--   </pre>
--   
--   <pre>
--   foldl f e = fromBits . foldl f e . toBits
--   </pre>
foldl :: (a -> Bool -> a) -> a -> BV -> a

-- | <pre>
--   foldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0)
--   </pre>
--   
--   <pre>
--   foldl f e = fromBits . foldl f e . toBits
--   </pre>

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

-- | <pre>
--   foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
--   </pre>
--   
--   <pre>
--   foldr f e = fromBits . foldr f e . toBits
--   </pre>
foldr :: (Bool -> a -> a) -> a -> BV -> a

-- | <pre>
--   foldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z)))
--   </pre>
--   
--   <pre>
--   foldr f e = fromBits . foldr f e . toBits
--   </pre>

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

-- | <pre>
--   reverse == fromBits . reverse . toBits
--   </pre>
reverse :: BV -> BV

-- | <pre>
--   reverse == fromBits . reverse . toBits
--   </pre>

-- | <i>Deprecated: Use corresponding versions without underscore</i>
reverse_ :: BV -> BV

-- | <i>Pre</i>: if <tt>replicate_ n u</tt> then <tt>n &gt; 0</tt> must
--   hold.
--   
--   <pre>
--   replicate_ n == fromBits . concat . replicate n . toBits
--   </pre>
replicate :: Integral size => size -> BV -> BV

-- | <i>Pre</i>: if <tt>replicate_ n u</tt> then <tt>n &gt; 0</tt> must
--   hold.
--   
--   <pre>
--   replicate_ n == fromBits . concat . replicate n . toBits
--   </pre>

-- | <i>Deprecated: Use corresponding versions without underscore</i>
replicate_ :: Integral size => size -> BV -> BV

-- | Conjunction.
--   
--   Essentially, <tt>and == foldr1 (.&amp;.)</tt>.
--   
--   Returns <tt>[1]1</tt> if the input list is empty.
and :: [BV] -> BV

-- | Conjunction.
--   
--   Essentially, <tt>and == foldr1 (.&amp;.)</tt>.
--   
--   Returns <tt>[1]1</tt> if the input list is empty.

-- | <i>Deprecated: Use corresponding versions without underscore</i>
and_ :: [BV] -> BV

-- | Disjunction.
--   
--   Essentially, <tt>or == foldr1 (.|.)</tt>.
--   
--   Returns <tt>[1]0</tt> if the input list is empty.
or :: [BV] -> BV

-- | Disjunction.
--   
--   Essentially, <tt>or == foldr1 (.|.)</tt>.
--   
--   Returns <tt>[1]0</tt> if the input list is empty.

-- | <i>Deprecated: Use corresponding versions without underscore</i>
or_ :: [BV] -> BV

-- | Split a bit-vector <i>k</i> times.
--   
--   <pre>
--   &gt;&gt;&gt; split 3 [4]15
--   [[2]0,[2]3,[2]3]
--   </pre>
split :: Integral times => times -> BV -> [BV]

-- | Split a bit-vector into <i>n</i>-wide pieces.
--   
--   <pre>
--   &gt;&gt;&gt; group 3 [4]15
--   [[3]1,[3]7]
--   </pre>
group :: Integral size => size -> BV -> [BV]

-- | Split a bit-vector into <i>n</i>-wide pieces.
--   
--   <pre>
--   &gt;&gt;&gt; group 3 [4]15
--   [[3]1,[3]7]
--   </pre>

-- | <i>Deprecated: Use corresponding versions without underscore</i>
group_ :: Integral size => size -> BV -> [BV]

-- | Concatenate a (possibly empty) list of bit-vectors.
--   
--   <pre>
--   &gt;&gt;&gt; join [[2]3,[2]2]
--   [4]14
--   </pre>
join :: [BV] -> BV

-- | An alias for <a>complement</a>.
not :: BV -> BV

-- | An alias for <a>complement</a>.

-- | <i>Deprecated: Use corresponding versions without underscore</i>
not_ :: BV -> BV

-- | Negated <a>.&amp;.</a>.
nand :: BV -> BV -> BV

-- | Negated <a>.|.</a>.
nor :: BV -> BV -> BV

-- | Negated <a>xor</a>.
xnor :: BV -> BV -> BV

-- | Left shift.
(<<.) :: BV -> BV -> BV
infixl 8 <<.

-- | Left shift.
shl :: BV -> BV -> BV
infixl 8 `shl`

-- | Logical right shift.
(>>.) :: BV -> BV -> BV
infixl 8 >>.

-- | Logical right shift.
shr :: BV -> BV -> BV
infixl 8 `shr`

-- | Arithmetic right shift
ashr :: BV -> BV -> BV
infixl 8 `ashr`

-- | Rotate left.
(<<<.) :: BV -> BV -> BV
infixl 8 <<<.

-- | Rotate left.
rol :: BV -> BV -> BV
infixl 8 `rol`

-- | Rotate right.
(>>>.) :: BV -> BV -> BV
infixl 8 >>>.

-- | Rotate right.
ror :: BV -> BV -> BV
infixl 8 `ror`

-- | Create a bit-vector from a single bit.
fromBool :: Bool -> BV

-- | Create a bit-vector from a big-endian list of bits.
--   
--   <pre>
--   &gt;&gt;&gt; fromBits [False, False, True]
--   [3]1
--   </pre>
fromBits :: [Bool] -> BV

-- | Create a big-endian list of bits from a bit-vector.
--   
--   <pre>
--   &gt;&gt;&gt; toBits [4]11
--   [True, False, True, True]
--   </pre>
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 Data.Data.Data Data.BitVector.BV
instance GHC.Show.Show Data.BitVector.BV
instance GHC.Read.Read Data.BitVector.BV
instance GHC.Classes.Eq Data.BitVector.BV
instance GHC.Classes.Ord Data.BitVector.BV
instance GHC.Num.Num Data.BitVector.BV
instance GHC.Real.Real Data.BitVector.BV
instance GHC.Enum.Enum Data.BitVector.BV
instance GHC.Real.Integral Data.BitVector.BV
instance GHC.Base.Monoid Data.BitVector.BV
instance Data.Bits.Bits Data.BitVector.BV
