úÎ1Ã-Å,      !"#$%&'()*+Iago Abal <iago.abal@gmail.com> Safe-Inferred, An alias for .  Big-endian pseudo size-polymorphic bit-vectors. The size of a bit-vector. 0The value of a bit-vector, as a natural number.  An alias for .  An alias for . 2'$s complement value of a bit-vector. 7Create 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]15Create a mask of ones. Create a mask of zeros. Fixed-size equality. In contrast with , , which is size-polymorphic, this equality 0 requires both bit-vectors to be of equal size.  [n]k ==. [m]kFalse [n]k == [n]kTrue Fixed-size inequality. The negated version of  . Bit indexing. u @. i stands for the i -th bit of u.  [4]2 @. 0False [4]2 @. 1True Bit-string extraction.  u @@ (j,i) == fromBits (map (u @ .) [j,j-1..i]) [4]7 @@ (3,1)[3]3Reverse bit-indexing. "Index from the end of the sequenc   u !. i == u @. (size u - i - 1) [3]3 !. 0FalseTake least significant bits. least m u == u @@ (m-1,0)Take most significant bits. most m u == u @@ (n-1,n-m)Most significant bit. msb u == u !. 0Least significant bit.  lsb u == u @. 0Most significant 1-bit. Pre: input must be non-zero.  msb1 [4]21 msb1 [4]422's complement signed division. 2'7s complement signed remainder (sign follows dividend). 2'6s complement signed remainder (sign follows divisor). Ceiling logarithm base 2. Pre%: input bit-vector must be non-zero. "Concatenation of two bit-vectors. Logical extension. zeroExtend 3 [1]1[4]1Arithmetic extension. signExtend 2 [2]1[4]1signExtend 2 [2]3[4]15 %foldl_ f z (fromBits [un, ..., u1, u0] ) == ((((z `f` un) `f` ...) `f` u1) `f` u0) *foldl_ f e = fromBits . foldl f e . toBits %foldr_ f z (fromBits [un, ..., u1, u0]) == un f (... f (u1 `f` (u0 `f` z))) *foldr_ f e = fromBits . foldr f e . toBits 'reverse_ == fromBits . reverse . toBitsPre: if replicate_ n u then n > 0 must hold. 8replicate_ n == fromBits . concat . replicate n . toBits An alias for -. Negated .. !Negated /. "Negated 0. # Left shift. $Logical right shift. %Arithmetic right shift & Rotate left. 'Rotate right. (4Create a bit-vector from a big-endian list of bits. fromBits [False, False, True][3]1)4Create a big-endian list of bits from a bit-vector.  toBits [4]11[True, False, True, True]*+Greatest natural number representable with n bits. +CMinimum width of a bit-vector to represent a given integer number.  integerWith 43integerWith (-4)451  !"#$%&'()*+23456789D:;<=>?@ABCDEFGHIJKL-0/.M  !"#$%&'()*+.  !"#$%&'()*+21  !"#$%&'()*+23456789N      !"#$%&'()*+,-./0123124125126789:;<=>12?12@12A12B12C12D12E12F12G12H12I12J12K12L12M12N12O12P12Q12RSbv-0.1.0Data.BitVector BitVectorBVsizenatwidthuintintbitVeconeszeros==./=.@.@@!.leastmostmsblsbmsb1sdivsremsmodlg2# zeroExtend signExtendfoldl_foldr_reverse_ replicate_not_nandnorxnor<<.>>.ashr<<<.>>>.fromBitstoBitsmaxNat integerWidthghc-prim GHC.Classes==base Data.Bits complement.&..|.xor$fBitsBV $fIntegralBV$fEnumBV$fRealBV$fNumBV$fOrdBV$fEqBV$fShowBVpopCountDefaulttestBitDefault bitDefaultpopCountrotateRrotateL unsafeShiftRshiftR unsafeShiftLshiftLisSignedbitSizetestBit complementBitclearBitsetBitbitrotateshiftBits