module Data.BitVector
(
BitVector
, BV
, size, width
, nat, uint, int
, bitVec
, ones, zeros
, (==.), (/=.)
, (@.), (@@)
, (!.)
, least, most
, msb, lsb, msb1
, sdiv, srem, smod
, lg2
, (#)
, zeroExtend, signExtend
, foldl_, foldr_
, reverse_
, replicate_
, module Data.Bits
, not_, nand, nor, xnor
, (<<.), (>>.), ashr, (<<<.), (>>>.)
, fromBits
, toBits
, maxNat
, integerWidth
) where
import Control.Exception ( assert )
import Data.Bits
import Data.Ord
data BV
= BV {
size :: !Int
, nat :: !Integer
}
type BitVector = BV
width :: BV -> Int
width = size
uint :: BV -> Integer
uint = nat
int :: BV -> Integer
int u | msb u = nat(u)
| otherwise = nat u
instance Show BV where
show (BV n a) = "[" ++ show n ++ "]" ++ show a
bitVec :: Integral a => Int -> a -> BV
bitVec n a | a >= 0 = BV n $ fromIntegral a
| otherwise = negate $ BV n $ fromIntegral (a)
ones :: Int -> BV
ones n = BV n $ 2^n 1
zeros :: Int -> BV
zeros n = BV n 0
instance Eq BV where
(BV _ a) == (BV _ b) = a == b
instance Ord BV where
compare = comparing nat
(==.) :: BV -> BV -> Bool
(BV n a) ==. (BV m b) = n == m && a == b
(/=.) :: BV -> BV -> Bool
u /=. v = not $ u ==. v
(@.) :: BV -> Int -> Bool
(BV _ a) @. i = testBit a i
(@@) :: BV -> (Int,Int) -> BV
(BV _ a) @@ (j,i) = assert (j >= i) $
BV m $ (a `shiftR` i) `mod` 2^m
where m = j i + 1
(!.) :: BV -> Int -> Bool
(BV n a) !. i = assert (i < n) $ testBit a (ni1)
least :: Int -> BV -> BV
least m (BV _ a) = assert (m >= 1) $
BV m $ a `mod` 2^m
most :: Int -> BV -> BV
most m (BV n a) = assert (m >= 1 && m <= n) $
BV m $ a `shiftR` (nm)
msb :: BV -> Bool
msb = (!. 0)
lsb :: BV -> Bool
lsb = (@. 0)
msb1 :: BV -> Int
msb1 (BV _ 0) = error "Data.BitVector.msb1: zero bit-vector"
msb1 (BV n a) = go (n1)
where go i | testBit a i = i
| otherwise = go (i1)
instance Num BV where
(BV n1 a) + (BV n2 b) = BV n $ (a + b) `mod` 2^n
where n = max n1 n2
(BV n1 a) * (BV n2 b) = BV n $ (a * b) `mod` 2^n
where n = max n1 n2
negate (BV n a) = BV n $ 2^n a
abs u | msb u = negate u
| otherwise = u
signum u = bitVec 2 $ int u
fromInteger i = bitVec (integerWidth i) i
instance Real BV where
toRational = toRational . nat
instance Enum BV where
toEnum = fromIntegral
fromEnum (BV _ a) = assert (a < max_int) $ fromIntegral a
where max_int = toInteger (maxBound::Int)
instance Integral BV where
quotRem (BV n1 a) (BV n2 b) = (BV n q,BV n r)
where n = max n1 n2
(q,r) = quotRem a b
divMod = quotRem
toInteger = nat
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
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
smod :: BV -> BV -> BV
smod u@(BV n1 _) v@(BV n2 _) = bitVec n r
where n = max n1 n2
r = int u `mod` int v
lg2 :: BV -> BV
lg2 (BV _ 0) = error "Data.BitVector.lg2: zero bit-vector"
lg2 (BV n 1) = BV n 0
lg2 (BV n a) = BV n $ toInteger $ integerWidth (a1)
(#) :: BV -> BV -> BV
(BV n a) # (BV m b) = BV (n + m) ((a `shiftL` m) + b)
zeroExtend :: Int -> BV -> BV
zeroExtend d (BV n a) = BV (n+d) a
signExtend :: Int -> BV -> BV
signExtend d (BV n a)
| testBit a (n1) = BV (n+d) $ (maxNat d `shiftL` n) + a
| otherwise = BV (n+d) a
foldl_ :: (a -> Bool -> a) -> a -> BV -> a
foldl_ f e (BV n a) = go (n1) e
where go i !x | i >= 0 = let !b = testBit a i in go (i1) $ f x b
| otherwise = x
foldr_ :: (Bool -> a -> a) -> a -> BV -> a
foldr_ f e (BV n a) = go (n1) e
where go i !x | i >= 0 = let !b = testBit a i in f b (go (i1) x)
| otherwise = x
reverse_ :: BV -> BV
reverse_ bv@(BV n _) = BV n $ snd $ foldl_ go (1,0) bv
where go (v,acc) b | b = (v',acc+v)
| otherwise = (v',acc)
where v' = 2*v
replicate_ :: Int -> BV -> BV
replicate_ 0 _ = error "Data.BitVector.replicate_: cannot replicate 0-times"
replicate_ n u = go (n1) u
where go 0 !acc = acc
go k !acc = go (k1) (u # acc)
instance Bits BV where
(BV n1 a) .&. (BV n2 b) = BV n $ a .&. b
where n = max n1 n2
(BV n1 a) .|. (BV n2 b) = BV n $ a .|. b
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
bit i = BV (i+1) (2^i)
testBit (BV n a) i | i < n = testBit a i
| otherwise = False
bitSize = undefined
isSigned = const False
shiftL (BV n a) k
| k > n = BV n 0
| otherwise = BV n $ shiftL a k `mod` 2^n
shiftR (BV n a) k
| k > n = BV n 0
| otherwise = BV n $ shiftR a k
rotateL bv 0 = bv
rotateL (BV n a) k
| k == n = BV n a
| k > n = rotateL (BV n a) (k `mod` n)
| otherwise = BV n $ h + l
where s = n k
l = a `shiftR` s
h = (a `shiftL` k) `mod` 2^n
rotateR bv 0 = bv
rotateR (BV n a) k
| k == n = BV n a
| k > n = rotateR (BV n a) (k `mod` n)
| otherwise = BV n $ h + l
where s = n k
l = a `shiftR` k
h = (a `shiftL` s) `mod` 2^n
not_ :: BV -> BV
not_ = complement
nand :: BV -> BV -> BV
nand u v = not_ $ u .&. v
nor :: BV -> BV -> BV
nor u v = not_ $ u .|. v
xnor :: BV -> BV -> BV
xnor u v = not_ $ u `xor` v
(<<.) :: BV -> BV -> BV
bv@BV{size=n} <<. (BV _ k)
| k >= fromIntegral n = BV n 0
| otherwise = bv `shiftL` (fromIntegral k)
(>>.) :: BV -> BV -> BV
bv@BV{size=n} >>. (BV _ k)
| k >= fromIntegral n = BV n 0
| otherwise = bv `shiftR` (fromIntegral k)
ashr :: BV -> BV -> BV
ashr u v | msb u = not_ ((not_ u) >>. v)
| otherwise = u >>. v
(<<<.) :: 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
(>>>.) :: 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
fromBits :: [Bool] -> BV
fromBits bs = BV n $ snd $ foldr go (1,0) bs
where n = length bs
go b (!v,!acc) | b = (v',acc+v)
| otherwise = (v',acc)
where v' = 2*v
toBits :: BV -> [Bool]
toBits (BV n a) = map (testBit a) [n1,n2..0]
maxNat :: Integral a => Int -> a
maxNat n = 2^n 1
integerWidth :: Integer -> Int
integerWidth !n
| n >= 0 = go 1 1
| otherwise = 1 + integerWidth (abs n)
where go !k !k_max | k_max >= n = k
| otherwise = go (k+1) (2*k_max+1)