SLP      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOO(c) 2012-2014 Iago Abal (c) 2012-2013 HASLab & University of MinhoBSD3Iago Abal <mail@iagoabal.eu> Safe-Inferred+P An alias for . Big-endian pseudo size-polymorphic bit-vectors.The size of a bit-vector./The value of a bit-vector, as a natural number. An alias for . An alias for .%2's complement value of a bit-vector.int [2]3-1 int [4]12-46Create 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. =Test if the signed value of a bit-vector is a natural number. >Test if the signed value of a bit-vector is a positive number. Fixed-size equality.In contrast with P , which is size-polymorphic?, this equality requires both bit-vectors to be of equal size. [n]k ==. [m]kFalse [n]k ==. [n]kTrue Fixed-size inequality.The negated version of  . Fixed-size  less-than. Fixed-size less-than-or-equals. Fixed-size  greater-than. Fixed-size greater-than-or-equals.Fixed-size signed  less-than.Fixed-size signed less-than-or-equals.Fixed-size signed  greater-than.Fixed-size signed greater-than-or-equals. Bit indexing.u @. i stands for the i -th bit of u. [4]2 @. 0False [4]2 @. 1True index i a == a @. iBit-string extraction. .u @@ (j,i) == fromBits (map (u @.) [j,j-1..i]) [4]7 @@ (3,1)[3]3 extract j i a == a @@ (j,i)Reverse bit-indexing.-Index starting from the most significant bit. 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]42 Least significant 1-bit.Pre: input must be non-zero. msb1 [4]30 msb1 [4]61! Bit-vector Q as an R."2's complement signed division.#82's complement signed remainder (sign follows dividend).$72's complement signed remainder (sign follows divisor).%Ceiling logarithm base 2.Pre$: input bit-vector must be non-zero.&!Concatenation of two bit-vectors.'!Concatenation of two bit-vectors.(Logical extension.zeroExtend 3 [1]1[4]1)Arithmetic extension.signExtend 2 [2]1[4]1signExtend 2 [2]3[4]15* Pfoldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0) )foldl f e = fromBits . foldl f e . toBits+ Pfoldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0) )foldl f e = fromBits . foldl f e . toBits, Nfoldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z))) )foldr f e = fromBits . foldr f e . toBits- Nfoldr 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 . toBits/ &reverse == fromBits . reverse . toBits0Pre: if replicate_ n u then n > 0 must hold. 8replicate_ n == fromBits . concat . replicate n . toBits1Pre: if replicate_ n u then n > 0 must hold. 8replicate_ n == fromBits . concat . replicate n . toBits2 Conjunction. and == foldr1 (.&.)3 Conjunction. and == foldr1 (.&.)4 Disjunction. or == foldr1 (.|.)5 Disjunction. or == foldr1 (.|.)6Split a bit-vector k times. split 3 [4]15[[2]0,[2]3,[2]3]7Split a bit-vector into n -wide pieces. group 3 [4]15 [[3]1,[3]7]8Split a bit-vector into n -wide pieces. group 3 [4]15 [[3]1,[3]7]9"Concatenate a list of bit-vectors.join [[2]3,[2]2][4]14: An alias for S.; An alias for S.<Negated T.=Negated U.>Negated V.? Left shift.@ Left shift.ALogical right shift.BLogical right shift.CArithmetic right shiftD Rotate left.E Rotate left.F Rotate right.G Rotate right.H&Create a bit-vector from a single bit.I3Create a bit-vector from a big-endian list of bits.fromBits [False, False, True][3]1J3Create a big-endian list of bits from a bit-vector. toBits [4]11[True, False, True, True]K!Show a bit-vector in binary form.L Show a bit-vector in octal form.M&Show a bit-vector in hexadecimal form.N+Greatest natural number representable with n bits.OBMinimum width of a bit-vector to represent a given integer number. integerWith 43integerWith (-4)4[W  !"#$%&'()*+,-./012345678X9:;<=>?@ABCDEFGHIJKYLMNOZ[\]^_`albcdefghijklmnopqrstuvSVUTwxy  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOR  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOXW  !"#$%&'()*+,-./012345678X9:;<=>?@ABCDEFGHIJKYLMNOZ[\]^_`a     &?@ABCDEFGz      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWUXYUZ[UZ\UZ]UZ^_`abcdefghUZiUZjUZkUZlUZmUZnUZoUZpUZqUZrUZsUZtUZuUZvUZwUZxUZyUZzUZ{UZ|UZ}UZ~UZUZbv-0.3.0Data.BitVector BitVectorBVsizenatwidthuintintbitVeconeszerosisNatisPos==./=.<.<=.>.>=.sltslesgtsge@.index@@extract!.leastmostmsblsbmsb1lsb1signumIsdivsremsmodlg2#cat zeroExtend signExtendfoldlfoldl_foldrfoldr_reversereverse_ replicate replicate_andand_oror_splitgroupgroup_joinnotnot_nandnorxnor<<.shl>>.shrashr<<<.rol>>>.rorfromBoolfromBitstoBitsshowBinshowOctshowHexmaxNat integerWidthghc-prim GHC.Classes==baseGHC.NumsignumGHC.RealIntegral Data.Bits complement.&..|.xor splitIntegerhexChar$fBitsBV $fIntegralBV$fEnumBV$fRealBV$fNumBV$fOrdBV$fEqBV$fShowBVpopCountDefaulttestBitDefault bitDefaultpopCountrotateRrotateL unsafeShiftRshiftR unsafeShiftLshiftLisSignedbitSize bitSizeMaybetestBit complementBitclearBitsetBitbitzeroBitsrotateshiftBits finiteBitSize FiniteBits