bv 0.1.0 → 0.2.0

raw patch · 2 files changed

+274/−86 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/BitVector.hs +270/−83
• bv.cabal +4/−3

@@ -4,7 +4,8 @@  -- | -- Module    : Data.BitVector--- Copyright : (c) Iago Abal, 2012+-- Copyright : (c) Iago Abal, 2012-2013+--             (c) University of Minho, 2012 -- License   : BSD3 -- Maintainer: Iago Abal <iago.abal@gmail.com> --@@ -14,12 +15,11 @@ --   (i.e. natural numbers) except for some very specific cases. -- -- * Bit-vectors are /size-polymorphic/ insofar as most operations treat---   a bit-vector of size /k/ as of size /n/ for /n >= k/ if required.+--   a bit-vector of size /n/ as of size /m/ for /m >= n/ if required. -- -- For documentation purposes we will write @[n]k@ to denote a bit-vector -- of size @n@ representing the natural number @k@.----module Data.BitVector +module Data.BitVector   ( -- * Bit-vectors     BitVector   , BV@@ -30,8 +30,11 @@   , ones, zeros     -- * Comparison   , (==.), (/=.)+  , (<.), (<=.), (>.), (>=.)+  , slt, sle, sgt, sge     -- * Indexing-  , (@.), (@@)+  , (@.), index+  , (@@), extract   , (!.)   , least, most   , msb, lsb, msb1@@ -39,18 +42,26 @@   , sdiv, srem, smod   , lg2   -- * List-like operations-  , (#)+  , (#), cat   , zeroExtend, signExtend   , foldl_, foldr_   , reverse_   , replicate_+  , and_, or_+  , split, group_, join   -- * Bitwise operations   , module Data.Bits   , not_, nand, nor, xnor-  , (<<.), (>>.), ashr, (<<<.), (>>>.)+  , (<<.), shl, (>>.), shr, ashr+  , (<<<.), rol, (>>>.), ror   -- * Conversion+  , fromBool   , fromBits   , toBits+  -- * Pretty-printing+  , showBin+  , showOct+  , showHex   -- * Utilities   , maxNat   , integerWidth@@ -59,13 +70,18 @@ import Control.Exception ( assert )  import Data.Bits+import Data.List ( foldl1' ) import Data.Ord+import Data.Typeable ( Typeable(..), mkTyConApp, mkTyCon3 )+import Data.Data+  ( Data(..), Fixity(Prefix)+  , constrIndex, indexConstr, mkDataType, mkConstr+  )  ---------------------------------------------------------------------- --- Bit-vectors  -- | Big-endian /pseudo size-polymorphic/ bit-vectors.--- data BV     = BV {       size :: !Int      -- ^ The /size/ of a bit-vector.@@ -73,18 +89,17 @@     }  -- | An alias for 'BV'.--- type BitVector = BV  -- | An alias for 'size'.--- width :: BV -> Int width = size+{-# INLINE width #-}  -- | An alias for 'nat'.--- uint :: BV -> Integer uint = nat+{-# INLINE uint #-}  -- | 2's complement value of a bit-vector. int :: BV -> Integer@@ -94,6 +109,21 @@ instance Show BV where   show (BV n a) = "[" ++ show n ++ "]" ++ show a +instance Typeable BV where+  typeOf _ = mkTyConApp bvTyCon []+    where bvTyCon = mkTyCon3 "bv" "Data.BitVector" "BV"++instance Data BV where+  gfoldl k r (BV x1 x2) = r BV `k` x1 `k` x2+  gunfold k z c+    = case constrIndex c - 1 of+          0 -> k $ k $ z BV+          i -> error $ "Data.gunfold for BV, unknown index: " ++ show i+  toConstr x@BV{} = indexConstr (dataTypeOf x) 1+  dataTypeOf _ = ty+    where ty = mkDataType "Data.BitVector.BV"+                  [mkConstr ty "BV" ["size", "nat"] Prefix]+ ---------------------------------------------------------------------- --- Construction @@ -106,20 +136,19 @@ -- -- >>> bitVec 4 (-1) -- [4]15--- bitVec :: Integral a => Int -> a -> BV bitVec n a | a >= 0    = BV n $ fromIntegral a            | otherwise = negate $ BV n $ fromIntegral (-a)-{-# INLINE bitVec #-}+{-# RULES "bitVec/Integer" bitVec = BV #-}+{-# SPECIALIZE bitVec :: Int -> Int -> BV #-}+{-# INLINE[1] bitVec #-}  -- | Create a mask of ones.--- ones :: Int -> BV ones n = BV n $ 2^n - 1 {-# INLINE ones #-}  -- | Create a mask of zeros.--- zeros :: Int -> BV zeros n = BV n 0 {-# INLINE zeros #-}@@ -141,19 +170,58 @@ -- >>> [n]k ==. [m]k -- False ----- >>> [n]k == [n]k+-- >>> [n]k ==. [n]k -- True--- (==.) :: BV -> BV -> Bool (BV n a) ==. (BV m b) = n == m && a == b  -- | Fixed-size inequality. -- -- The negated version of '==.'.--- (/=.) :: BV -> BV -> Bool u /=. v = not $ u ==. v+{-# INLINE (/=.) #-} +-- | Fixed-size /less-than/.+(<.) :: BV -> BV -> Bool+(BV n a) <. (BV m b) = n == m && a < b+{-# INLINE (<.) #-}++-- | Fixed-size /less-than-or-equals/.+(<=.) :: BV -> BV -> Bool+(BV n a) <=. (BV m b) = n == m && a <= b+{-# INLINE (<=.) #-}++-- | Fixed-size /greater-than/.+(>.) :: BV -> BV -> Bool+(BV n a) >. (BV m b) = n == m && a > b+{-# INLINE (>.) #-}++-- | Fixed-size /greater-than-or-equals/.+(>=.) :: BV -> BV -> Bool+(BV n a) >=. (BV m b) = n == m && a >= b+{-# INLINE (>=.) #-}++-- | Fixed-size signed /less-than/.+slt :: BV -> BV -> Bool+u@BV{size=n} `slt` v@BV{size=m} = n == m && int u < int v+{-# INLINE slt #-}++-- | Fixed-size signed /less-than-or-equals/.+sle :: BV -> BV -> Bool+u@BV{size=n} `sle` v@BV{size=m} = n == m && int u <= int v+{-# INLINE sle #-}++-- | Fixed-size signed /greater-than/.+sgt :: BV -> BV -> Bool+u@BV{size=n} `sgt` v@BV{size=m} = n == m && int u > int v+{-# INLINE sgt #-}++-- | Fixed-size signed /greater-than-or-equals/.+sge :: BV -> BV -> Bool+u@BV{size=n} `sge` v@BV{size=m} = n == m && int u >= int v+{-# INLINE sge #-}+ ---------------------------------------------------------------------- --- Indexing @@ -166,66 +234,83 @@ -- -- >>> [4]2 @. 1 -- True----(@.) :: BV -> Int -> Bool-(BV _ a) @. i = testBit a i-{-# INLINE (@.) #-}+(@.) :: Integral ix => BV -> ix -> Bool+(BV _ a) @. i = testBit a (fromIntegral i)+{-# SPECIALIZE (@.) :: BV -> Int     -> Bool #-}+{-# SPECIALIZE (@.) :: BV -> Integer -> Bool #-}+{-# INLINE[1] (@.) #-} +-- | @index i a == a \@. i@+index :: Integral ix => ix -> BV -> Bool+index = flip (@.)+{-# INLINE index #-}+ -- | Bit-string extraction. -- -- @u \@\@ (j,i) == fromBits (map (u \@.) [j,j-1..i])@ -- -- >>> [4]7 @@ (3,1) -- [3]3----(@@) :: BV -> (Int,Int) -> BV-(BV _ a) @@ (j,i) = assert (j >= i) $-    BV m $ (a `shiftR` i) `mod` 2^m-  where m = j - i + 1+(@@) :: Integral ix => BV -> (ix,ix) -> BV+(BV _ a) @@ (j,i) = assert (i >= 0 && j >= i) $+    BV m $ (a `shiftR` i') `mod` 2^m+  where i' = fromIntegral i+        m  = fromIntegral $ j - i + 1+{-# SPECIALIZE (@@) :: BV -> (Int,Int)         -> BV #-}+{-# SPECIALIZE (@@) :: BV -> (Integer,Integer) -> BV #-} +-- | @extract j i a == a \@\@ (j,i)@+extract :: Integral ix => ix -> ix -> BV -> BV+extract j i = (@@ (j,i))+{-# INLINE extract #-}+ -- | Reverse bit-indexing. ----- Index from the end of the sequenc+-- Index starting from the most significant bit. -- -- @u !. i == u \@. (size u - i - 1) @ -- -- >>> [3]3 !. 0 -- False----(!.) :: BV -> Int -> Bool-(BV n a) !. i = assert (i < n) $ testBit a (n-i-1)-{-# INLINE (!.) #-}+(!.) :: Integral ix => BV -> ix -> Bool+(BV n a) !. i = assert (i' < n) $ testBit a (n-i'-1)+  where i' = fromIntegral i+{-# SPECIALIZE (!.) :: BV -> Int     -> Bool #-}+{-# SPECIALIZE (!.) :: BV -> Integer -> Bool #-}+{-# INLINE[1] (!.) #-}  -- | Take least significant bits. -- -- @least m u == u \@\@ (m-1,0)@----least :: Int -> BV -> BV+least :: Integral ix => ix -> BV -> BV least m (BV _ a) = assert (m >= 1) $-  BV m $ a `mod` 2^m+  BV m' $ a `mod` 2^m+  where m' = fromIntegral m+{-# SPECIALIZE least :: Int     -> BV -> BV #-}+{-# SPECIALIZE least :: Integer -> BV -> BV #-}  -- | Take most significant bits. -- -- @most m u == u \@\@ (n-1,n-m)@----most :: Int -> BV -> BV-most m (BV n a) = assert (m >= 1 && m <= n) $-  BV m $ a `shiftR` (n-m)+most :: Integral ix => ix -> BV -> BV+most m (BV n a) = assert (m' >= 1 && m' <= n) $+  BV m' $ a `shiftR` (n-m')+  where m' = fromIntegral m+{-# SPECIALIZE most :: Int     -> BV -> BV #-}+{-# SPECIALIZE most :: Integer -> BV -> BV #-}  -- | Most significant bit. -- -- @msb u == u !. 0@--- msb :: BV -> Bool-msb = (!. 0)+msb = (!. (0::Int)) {-# INLINE msb #-}  -- | Least significant bit. -- -- @lsb u == u \@. 0@--- lsb :: BV -> Bool-lsb = (@. 0)+lsb = (@. (0::Int)) {-# INLINE lsb #-}  -- | Most significant 1-bit.@@ -237,7 +322,6 @@ -- -- >>> msb1 [4]4 -- 2--- msb1 :: BV -> Int msb1 (BV _ 0) = error "Data.BitVector.msb1: zero bit-vector" msb1 (BV n a) = go (n-1)@@ -274,21 +358,18 @@   toInteger = nat  -- | 2's complement signed division.--- sdiv :: BV -> BV -> BV sdiv u@(BV n1 _) v@(BV n2 _) = bitVec n q   where n = max n1 n2         q = int u `quot` int v  -- | 2's complement signed remainder (sign follows dividend).--- srem :: BV -> BV -> BV srem u@(BV n1 _) v@(BV n2 _) = bitVec n r   where n = max n1 n2         r = int u `rem` int v  -- | 2's complement signed remainder (sign follows divisor).--- smod :: BV -> BV -> BV smod u@(BV n1 _) v@(BV n2 _) = bitVec n r   where n = max n1 n2@@ -297,7 +378,6 @@ -- | Ceiling logarithm base 2. -- -- /Pre/: input bit-vector must be non-zero.--- lg2 :: BV -> BV lg2 (BV _ 0) = error "Data.BitVector.lg2: zero bit-vector" lg2 (BV n 1) = BV n 0@@ -307,19 +387,23 @@ --- List-like operations  -- | Concatenation of two bit-vectors.----(#) :: BV -> BV -> BV+(#), cat :: BV -> BV -> BV (BV n a) # (BV m b) = BV (n + m) ((a `shiftL` m) + b) {-# INLINABLE (#) #-} +cat = (#)+{-# INLINE cat #-}+ -- | Logical extension. -- -- >>> zeroExtend 3 [1]1 -- [4]1----zeroExtend :: Int -> BV -> BV-zeroExtend d (BV n a) = BV (n+d) a-{-# INLINE zeroExtend #-}+zeroExtend :: Integral size => size -> BV -> BV+zeroExtend d (BV n a) = BV (n+d') a+  where d' = fromIntegral d+{-# SPECIALIZE zeroExtend :: Int     -> BV -> BV #-}+{-# SPECIALIZE zeroExtend :: Integer -> BV -> BV #-}+{-# INLINE[1] zeroExtend #-}  -- | Arithmetic extension. --@@ -328,17 +412,19 @@ -- -- >>> signExtend 2 [2]3 -- [4]15----signExtend :: Int -> BV -> BV+signExtend :: Integral size => size -> BV -> BV signExtend d (BV n a)-  | testBit a (n-1) = BV (n+d) $ (maxNat d `shiftL` n) + a-  | otherwise       = BV (n+d) a+  | testBit a (n-1) = BV (n+d') $ (maxNat d `shiftL` n) + a+  | otherwise       = BV (n+d') a+  where d' = fromIntegral d+{-# SPECIALIZE signExtend :: Int     -> BV -> BV #-}+{-# SPECIALIZE signExtend :: Integer -> BV -> BV #-}+{-# INLINE[1] signExtend #-}  -- | -- @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 e (BV n a) = go (n-1) e   where go i !x | i >= 0    = let !b = testBit a i in go (i-1) $ f x b@@ -346,10 +432,9 @@ {-# INLINE foldl_ #-}  -- |--- @foldr_ f z (fromBits [un, ..., u1, u0]) == un `f` (... `f` (u1 \`f\` (u0 \`f\` z)))@+-- @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 e (BV n a) = go (n-1) e  where go i !x | i >= 0    = let !b = testBit a i in f b (go (i-1) x)@@ -358,7 +443,6 @@  -- | -- @reverse_ == fromBits . reverse . toBits@--- reverse_ :: BV -> BV reverse_ bv@(BV n _) = BV n $ snd $ foldl_ go (1,0) bv   where go (v,acc) b | b         = (v',acc+v)@@ -369,13 +453,73 @@ -- /Pre/: if @replicate_ n u@ then @n > 0@ must hold. -- -- @replicate_ n == fromBits . concat . replicate n . toBits @----replicate_ :: Int -> BV -> BV+replicate_ :: Integral size => size -> BV -> BV replicate_ 0 _ = error "Data.BitVector.replicate_: cannot replicate 0-times" replicate_ n u = go (n-1) u   where go 0 !acc = acc         go k !acc = go (k-1) (u # acc)+{-# SPECIALIZE replicate_ :: Int     -> BV -> BV #-}+{-# SPECIALIZE replicate_ :: Integer -> BV -> BV #-} +-- | Conjunction.+--+-- @and_ == foldr1 (.&.)@+and_ :: [BV] -> BV+and_ [] = error "Data.BitVector.and_: empty list"+and_ ws = BV n' $ foldl1' (.&.) $ map nat ws+  where n' = maximum $ map size ws+{-# INLINE and_ #-}++-- | Disjunction.+--+-- @or_ == foldr1 (.|.)@+or_ :: [BV] -> BV+or_ [] = error "Data.BitVector.or_: empty list"+or_ ws = BV n' $ foldl1' (.|.) $ map nat ws+  where n' = maximum $ map size ws+{-# INLINE or_ #-}++-- | Split a bit-vector /k/ times.+--+-- >>> split 3 [4]15+-- [[2]0,[2]3,[2]3]+split :: Integral times => times -> BV -> [BV]+split k (BV n a) = assert (k > 0) $+  map (BV s) $ splitInteger s k' a+  where k' = fromIntegral k+        (q,r) = divMod n k'+        s = q + signum r++-- | Split a bit-vector into /n/-wide pieces.+--+-- >>> group_ 3 [4]15+-- [[3]1,[3]7]+group_ :: Integral size => size -> BV -> [BV]+group_ s (BV n a) = assert (s > 0) $+  map (BV s') $ splitInteger s' k a+  where s' = fromIntegral s+        (q,r) = divMod n s'+        k = q + signum r++splitInteger :: (Integral size, Integral times) =>+                    size -> times -> Integer -> [Integer]+splitInteger n = go []+  where n' = fromIntegral n+        go acc 0 _ = acc+        go acc k a = go (v:acc) (k-1) a'+          where v  = a `mod` 2^n+                a' = a `shiftR` n'+{-# SPECIALIZE splitInteger :: Int     -> Int     -> Integer -> [Integer] #-}+{-# SPECIALIZE splitInteger :: Integer -> Integer -> Integer -> [Integer] #-}+{-# INLINE[1] splitInteger #-}++-- | Concatenate a list of bit-vectors.+--+-- >>> join [[2]3,[2]2]+-- [4]14+join :: [BV] -> BV+join = foldl1' (#)+ ---------------------------------------------------------------------- --- Bitwise operations @@ -386,7 +530,7 @@     where n = max n1 n2   (BV n1 a) `xor` (BV n2 b) = BV n $ a `xor` b     where n = max n1 n2-  complement (BV n a) = BV n $ 2^n - 1 - a +  complement (BV n a) = BV n $ 2^n - 1 - a   bit i = BV (i+1) (2^i)   testBit (BV n a) i | i < n     = testBit a i                      | otherwise = False@@ -416,77 +560,87 @@           h = (a `shiftL` s) `mod` 2^n  -- | An alias for 'complement'.--- not_ :: BV -> BV not_ = complement {-# INLINE not_ #-}  -- | Negated '.&.'.--- nand :: BV -> BV -> BV nand u v = not_ $ u .&. v {-# INLINE nand #-}  -- | Negated '.|.'.--- nor :: BV -> BV -> BV nor u v = not_ $ u .|. v {-# INLINE nor #-}  -- | Negated 'xor'.--- xnor :: BV -> BV -> BV xnor u v = not_ $ u `xor` v {-# INLINE xnor #-}  -- | Left shift.----(<<.) :: BV -> BV -> BV+(<<.), shl :: BV -> BV -> BV bv@BV{size=n} <<. (BV _ k)   | k >= fromIntegral n  = BV n 0   | otherwise            = bv `shiftL` (fromIntegral k) {-# INLINE (<<.) #-} +shl = (<<.)+{-# INLINE shl #-}+ -- | Logical right shift.----(>>.) :: BV -> BV -> BV+(>>.), shr :: BV -> BV -> BV bv@BV{size=n} >>. (BV _ k)   | k >= fromIntegral n  = BV n 0   | otherwise            = bv `shiftR` (fromIntegral k) {-# INLINE (>>.) #-} +shr = (>>.)+{-# INLINE shr #-}+ -- | Arithmetic right shift--- ashr :: BV -> BV -> BV ashr u v | msb u     = not_ ((not_ u) >>. v)          | otherwise = u >>. v  -- | Rotate left.----(<<<.) :: BV -> BV -> BV+(<<<.), rol :: BV -> BV -> BV+ bv@BV{size=n} <<<. (BV _ k)   | k >= n'   = bv `rotateL` (fromIntegral $ k `mod` n')   | otherwise = bv `rotateL` (fromIntegral k)   where n' = fromIntegral n {-# INLINE (<<<.) #-} +rol = (<<<.)+{-# INLINE rol #-}+ -- | Rotate right.----(>>>.) :: BV -> BV -> BV+(>>>.), ror :: BV -> BV -> BV+ bv@BV{size=n} >>>. (BV _ k)   | k >= n'   = bv `rotateR` (fromIntegral $ k `mod` n')   | otherwise = bv `rotateR` (fromIntegral k)   where n' = fromIntegral n {-# INLINE (>>>.) #-} +ror = (>>>.)+{-# INLINE ror #-}+ ---------------------------------------------------------------------- --- Conversion +-- | Create a bit-vector from a single bit.+fromBool :: Bool -> BV+fromBool False = BV 1 0+fromBool True  = BV 1 1+{-# INLINE fromBool #-}+ -- | Create a bit-vector from a big-endian list of bits. -- -- >>> fromBits [False, False, True] -- [3]1--- fromBits :: [Bool] -> BV fromBits bs = BV n $ snd $ foldr go (1,0) bs   where n = length bs@@ -498,16 +652,50 @@ -- -- >>> toBits [4]11 -- [True, False, True, True]--- toBits :: BV -> [Bool] toBits (BV n a) = map (testBit a) [n-1,n-2..0]  ----------------------------------------------------------------------+--- Pretty-printing++-- | Show a bit-vector in binary form.+showBin :: BV -> String+showBin = ("0b" ++) . map showBit . toBits+  where showBit True  = '1'+        showBit False = '0'++hexChar :: Integral a => a -> Char+hexChar 0 = '0'+hexChar 1 = '1'+hexChar 2 = '2'+hexChar 3 = '3'+hexChar 4 = '4'+hexChar 5 = '5'+hexChar 6 = '6'+hexChar 7 = '7'+hexChar 8 = '8'+hexChar 9 = '9'+hexChar 10 = 'a'+hexChar 11 = 'b'+hexChar 12 = 'c'+hexChar 13 = 'd'+hexChar 14 = 'e'+hexChar 15 = 'f'+hexChar _  = error "Data.BitVector.hexChar: invalid input"++-- | Show a bit-vector in octal form.+showOct :: BV -> String+showOct = ("0o" ++) . map (hexChar . nat) . group_ (3::Int)++-- | Show a bit-vector in hexadecimal form.+showHex :: BV -> String+showHex = ("0x" ++) . map (hexChar . nat) . group_ (4::Int)++---------------------------------------------------------------------- --- Utilities  -- | Greatest natural number representable with /n/ bits.----maxNat :: Integral a => Int -> a+maxNat :: (Integral a, Integral b) => a -> b maxNat n = 2^n - 1 {-# INLINE maxNat #-} @@ -518,7 +706,6 @@ -- -- >>> integerWith (-4) -- 4--- integerWidth :: Integer -> Int integerWidth !n   | n >= 0    = go 1 1

@@ -1,6 +1,6 @@  Name:                bv-Version:             0.1.0+Version:             0.2.0 Synopsis:            Bit-vectors library Description:         Bit-vectors implemented as a wrapper over integers. Homepage:            http://bitbucket.org/iago/bv-haskell@@ -9,7 +9,8 @@ License-file:        LICENSE Author:              Iago Abal <iago.abal@gmail.com> Maintainer:          Iago Abal <iago.abal@gmail.com>-Copyright:           2012, Iago Abal+Copyright:           2012-2013, Iago Abal+                     2012, University of Minho Category:            Data, Bit Vectors Build-type:          Simple Cabal-version:       >=1.6@@ -20,6 +21,6 @@  Library   Exposed-modules:     Data.BitVector-  -- Other-modules:       +  -- Other-modules:   ghc-options:         -Wall   Build-depends:       base >=4 && <5