aZT      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSO(c) 2012-2016 Iago Abal (c) 2012-2013 HASLab & University of MinhoBSD3Iago Abal <mail@iagoabal.eu>None+;U 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-4The empty bit-vector, ie. [0]0.6Create 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 ,List of bit-vector literals of the same sizeJWhen a list of integer literals is interpreted as a list of bit-vectors, T' is applied to each element invidually:[1,3,5] :: [BV][ [1]1, [2]3, [3]5 ]gSometimes 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 ] Create 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 U , which is size-polymorphic?, this equality requires both bit-vectors to be of equal size. [n]k ==. [m]kFalse [n]k ==. [n]kTrueFixed-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)Bit list indexing.)u @: is ==. fromBits $ List.map (u @.) isReverse 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 !. 0!Least significant bit. lsb u == u @. 0"Most 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 V as an W.%Bit-vector exponentiation. pow [n]k e computes k raised to e modulo n.dThis is faster than Haskell's (^) operator because it performs modulo division just once. Besides,  a^0 == [1]0 !!!&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.,!Concatenation of two bit-vectors.- An alias for ?..Logical extension.zeroExtend 3 [1]1[4]1/Arithmetic extension.signExtend 2 [2]1[4]1signExtend 2 [2]3[4]150 Pfoldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0) )foldl f e = fromBits . foldl f e . toBits1 Pfoldl f z (fromBits [un, ..., u1, u0]) == ((((z `f` un) `f` ...) `f` u1) `f` u0) )foldl f e = fromBits . foldl f e . toBits2 Nfoldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z))) )foldr f e = fromBits . foldr f e . toBits3 Nfoldr f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 `f` (u0 `f` z))) )foldr f e = fromBits . foldr f e . toBits4 &reverse == fromBits . reverse . toBits5 &reverse == fromBits . reverse . toBits6Pre: if replicate_ n u then n > 0 must hold. 8replicate_ n == fromBits . concat . replicate n . toBits7Pre: if replicate_ n u then n > 0 must hold. 8replicate_ n == fromBits . concat . replicate n . toBits8 Conjunction. Essentially, and == foldr1 (.&.).Returns [1]1 if the input list is empty.9 Conjunction. Essentially, and == foldr1 (.&.).Returns [1]1 if the input list is empty.: Disjunction. Essentially, or == foldr1 (.|.).Returns [1]0 if the input list is empty.; Disjunction. Essentially, or == foldr1 (.|.).Returns [1]0 if the input list is empty.<Split a bit-vector k times. split 3 [4]15[[2]0,[2]3,[2]3]=Split a bit-vector into n -wide pieces. group 3 [4]15 [[3]1,[3]7]>Split a bit-vector into n -wide pieces. group 3 [4]15 [[3]1,[3]7]?3Concatenate a (possibly empty) list of bit-vectors.join [[2]3,[2]2][4]14@ An alias for X.A An alias for X.BNegated Y.CNegated Z.DNegated [.E Left shift.F Left shift.GLogical right shift.HLogical right shift.IArithmetic right shiftJ Rotate left.K Rotate left.L Rotate right.M Rotate right.N&Create a bit-vector from a single bit.O3Create a bit-vector from a big-endian list of bits.fromBits [False, False, True][3]1P3Create a big-endian list of bits from a bit-vector. toBits [4]11[True, False, True, True]Q!Show a bit-vector in binary form.R Show a bit-vector in octal form.S&Show a bit-vector in hexadecimal form.\+Greatest natural number representable with n bits.a]  !"#$%&'()*+,-./0123456789:;<=>^?@ABCDEFGHIJKLMNOPQ_RS\`abcdefghpijklmnopqrstuvwxyz{|}X[ZY~  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSV  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRS^]  !"#$%&'()*+,-./0123456789:;<=>^?@ABCDEFGHIJKLMNOPQ_RS\`abcdefgh    *EFGHIJKLM      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[VW\V]^V_`V_aV_bV_cdefghijklmnoV_pV_qV_rV_sV_tV_uV_vV_wV_xV_yV_zV_{V_|V_}V_~V_V_V_V_V_V_V_V_V_bv-0.4.0Data.BitVector BitVectorBVsizenatwidthuintintnilbitVecbitVecsoneszerosisNatisPos==./=.<.<=.>.>=.sltslesgtsge@.index@@extract@:!.leastmostmsblsbmsb1lsb1signumIpowsdivsremsmodlg2#catappendconcat zeroExtend signExtendfoldlfoldl_foldrfoldr_reversereverse_ replicate replicate_andand_oror_splitgroupgroup_joinnotnot_nandnorxnor<<.shl>>.shrashr<<<.rol>>>.rorfromBoolfromBitstoBitsshowBinshowOctshowHexbaseGHC.Num fromIntegerghc-prim GHC.Classes==signumGHC.RealIntegral Data.Bits complement.&..|.xormaxNat splitIntegerhexChar$fBitsBV $fMonoidBV $fIntegralBV$fEnumBV$fRealBV$fNumBV$fOrdBV$fEqBV$fShowBVpopCountDefaulttestBitDefault bitDefaultpopCountrotateRrotateL unsafeShiftRshiftR unsafeShiftLshiftLisSignedbitSize bitSizeMaybetestBit complementBitclearBitsetBitbitzeroBitsrotateshiftBits finiteBitSize FiniteBits