packages feed

bv-sized 0.1.0.0 → 0.1.1.0

raw patch · 5 files changed

+331/−329 lines, 5 filesdep +containersdep +lensPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: containers, lens

API changes (from Hackage documentation)

- Data.BitVector.Sized.Internal: (<:>) :: BitVector v -> BitVector w -> BitVector (v + w)
- Data.BitVector.Sized.Internal: [BV] :: NatRepr w -> Integer -> BitVector w
- Data.BitVector.Sized.Internal: bv :: KnownNat w => Integer -> BitVector w
- Data.BitVector.Sized.Internal: bvAbs :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvAdd :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvAnd :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvComplement :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvConcat :: BitVector v -> BitVector w -> BitVector (v + w)
- Data.BitVector.Sized.Internal: bvExtract :: forall w w'. (KnownNat w') => Int -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvExtractWithRepr :: NatRepr w' -> Int -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvIntegerS :: BitVector w -> Integer
- Data.BitVector.Sized.Internal: bvIntegerU :: BitVector w -> Integer
- Data.BitVector.Sized.Internal: bvMul :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvNegate :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvOr :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvPopCount :: BitVector w -> Int
- Data.BitVector.Sized.Internal: bvRotate :: BitVector w -> Int -> BitVector w
- Data.BitVector.Sized.Internal: bvSext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvSextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvShift :: BitVector w -> Int -> BitVector w
- Data.BitVector.Sized.Internal: bvSignum :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvTestBit :: BitVector w -> Int -> Bool
- Data.BitVector.Sized.Internal: bvWidth :: BitVector w -> Int
- Data.BitVector.Sized.Internal: bvXor :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvZext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvZextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: data BitVector (w :: Nat) :: *
- Data.BitVector.Sized.Internal: infixl 6 <:>
- Data.BitVector.Sized.Internal: instance Data.Parameterized.Classes.EqF Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance Data.Parameterized.Classes.ShowF Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance Data.Type.Equality.TestEquality Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance GHC.Classes.Eq (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.Show.Show (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => Data.Bits.Bits (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => Data.Bits.FiniteBits (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Enum.Bounded (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Enum.Enum (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Num.Num (Data.BitVector.Sized.Internal.BitVector w)
+ Data.BitVector.Sized: [BV] :: NatRepr w -> Integer -> BitVector w
+ Data.BitVector.Sized: bvAbs :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvAdd :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvAnd :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvComplement :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvExtractWithRepr :: NatRepr w' -> Int -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: bvMul :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvMulFS :: BitVector w -> BitVector w' -> BitVector (w + w')
+ Data.BitVector.Sized: bvMulFU :: BitVector w -> BitVector w' -> BitVector (w + w')
+ Data.BitVector.Sized: bvNegate :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvOr :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvPopCount :: BitVector w -> Int
+ Data.BitVector.Sized: bvRotate :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvSextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: bvShift :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvSignum :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvTestBit :: BitVector w -> Int -> Bool
+ Data.BitVector.Sized: bvTruncBits :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvWidth :: BitVector w -> Int
+ Data.BitVector.Sized: bvXor :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvZextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: instance Data.Parameterized.Classes.EqF Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance Data.Parameterized.Classes.ShowF Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance Data.Type.Equality.TestEquality Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance GHC.Classes.Eq (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.Classes.Ord (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.Show.Show (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => Data.Bits.Bits (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => Data.Bits.FiniteBits (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Enum.Bounded (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Enum.Enum (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Num.Num (Data.BitVector.Sized.BitVector w)

Files

bv-sized.cabal view
@@ -1,5 +1,5 @@ name:                bv-sized-version:             0.1.0.0+version:             0.1.1.0 category:            Bit Vectors synopsis:            a BitVector datatype that is parameterized by the vector width description:@@ -17,8 +17,9 @@  library   exposed-modules:     Data.BitVector.Sized-                       Data.BitVector.Sized.Internal   build-depends:       base >= 4.7 && < 5+                     , containers >= 0.5.11 && < 0.6+                     , lens >= 4 && < 5                      , parameterized-utils   hs-source-dirs:      src   default-language:    Haskell2010
+ changelog.md view
@@ -0,0 +1,10 @@+# Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized)++## 0.1.0.0 *March 2018*+  * First release++## 0.1.1.0 *March 2018*+  * added functions `bvMulFS`/`bvMulFU` for full bitvector multiplication+    without truncation+  * removed Internal module, now export all those functions in Data.BitVector.Sized+  * fixed the bv*WithRepr functions, which were not truncating the inputs properly
src/Data/BitVector/Sized.hs view
@@ -5,7 +5,7 @@ {-# LANGUAGE TypeOperators #-}  {-|-Module      : Data.BitVector.Sized+Module      : Data.BitVector.Sized.Internal Copyright   : (c) Benjamin Selfridge, 2018                   Galois Inc. License     : BSD3@@ -15,24 +15,330 @@  This module defines a width-parameterized 'BitVector' type and various associated operations that assume a 2's complement representation.--For more fine-grained access to the internals (including explicit 'Data.Parameterized.NatRepr's), see-'Data.BitVector.Sized.Internal'. -}  module Data.BitVector.Sized   ( -- * BitVector type-    BitVector+    BitVector(..)   , bv-    -- * Bitwise operations (variable width)+    -- * Bitwise operations (width-preserving)+    -- | These are alternative versions of some of the 'Bits' functions where we do+    -- not need to know the width at compile time. They are all width-preserving.+  , bvAnd, bvOr, bvXor+  , bvComplement+  , bvShift, bvRotate+  , bvWidth+  , bvTestBit+  , bvPopCount+  , bvTruncBits+    -- * Arithmetic operations (width-preserving)+  , bvAdd, bvMul+  , bvAbs, bvNegate+  , bvSignum+    -- * Variable-width operations     -- | These are functions that involve bit vectors of different lengths.   , bvConcat, (<:>)-  , bvExtract-  , bvZext-  , bvSext+  , bvExtract, bvExtractWithRepr+  , bvZext, bvZextWithRepr+  , bvSext, bvSextWithRepr+  , bvMulFU, bvMulFS     -- * Conversions to Integer   , bvIntegerU   , bvIntegerS   ) where -import Data.BitVector.Sized.Internal+import Data.Bits+import Data.Parameterized.Classes+import Data.Parameterized.NatRepr+import GHC.TypeLits+import Text.Printf+import Unsafe.Coerce (unsafeCoerce)+----------------------------------------+-- BitVector data type definitions++-- | BitVector datatype, parameterized by width.+data BitVector (w :: Nat) :: * where+  BV :: NatRepr w -> Integer -> BitVector w++-- | Construct a bit vector in a context where the width is inferrable from the type+-- context. The 'Integer' input (an unbounded data type, hence with an infinite-width+-- bit representation), whether positive or negative is silently truncated to fit+-- into the number of bits demanded by the return type.+--+-- >>> bv 0xA :: BitVector 4+-- 0xa<4>+-- >>> bv 0xA :: BitVector 3+-- 0x2<3>+-- >>> bv (-1) :: BitVector 8+-- 0xff<8>+-- >>> bv (-1) :: BitVector 32+-- 0xffffffff<32>++bv :: KnownNat w => Integer -> BitVector w+bv x = BV wRepr (truncBits width (fromIntegral x))+  where wRepr = knownNat+        width = natValue wRepr++----------------------------------------+-- BitVector -> Integer functions++-- | Unsigned interpretation of a bit vector as a (positive) Integer.+bvIntegerU :: BitVector w -> Integer+bvIntegerU (BV _ x) = x++-- | Signed interpretation of a bit vector as an Integer.+bvIntegerS :: BitVector w -> Integer+bvIntegerS bvec = case bvTestBit bvec (width - 1) of+  True  -> bvIntegerU bvec - (1 `shiftL` width)+  False -> bvIntegerU bvec+  where width = bvWidth bvec++----------------------------------------+-- BitVector w operations (fixed width)++-- | Bitwise and.+bvAnd :: BitVector w -> BitVector w -> BitVector w+bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)++-- | Bitwise or.+bvOr :: BitVector w -> BitVector w -> BitVector w+bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)++-- | Bitwise xor.+bvXor :: BitVector w -> BitVector w -> BitVector w+bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)++-- | Bitwise complement (flip every bit).+bvComplement :: BitVector w -> BitVector w+bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))+  where width = natValue wRepr++-- | Bitwise shift.+bvShift :: BitVector w -> Int -> BitVector w+bvShift bvec@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))+  where width = natValue wRepr+        x     = bvIntegerS bvec -- arithmetic right shift when negative++-- | Bitwise rotate.+bvRotate :: BitVector w -> Int -> BitVector w+bvRotate bvec rot' = leftChunk `bvOr` rightChunk+  where rot = rot' `mod` (bvWidth bvec)+        leftChunk = bvShift bvec rot+        rightChunk = bvShift bvec (rot - bvWidth bvec)++-- | Get the width of a 'BitVector'.+bvWidth :: BitVector w -> Int+bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)++-- | Test if a particular bit is set.+bvTestBit :: BitVector w -> Int -> Bool+bvTestBit (BV _ x) b = testBit x b++-- | Get the number of 1 bits in a 'BitVector'.+bvPopCount :: BitVector w -> Int+bvPopCount (BV _ x) = popCount x++-- | Truncate a bit vector to a particular width given at runtime, while keeping the+-- type-level width constant.+bvTruncBits :: BitVector w -> Int -> BitVector w+bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)++----------------------------------------+-- BitVector w arithmetic operations (fixed width)++-- | Bitwise add.+bvAdd :: BitVector w -> BitVector w -> BitVector w+bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))+  where width = natValue wRepr++-- | Bitwise multiply.+bvMul :: BitVector w -> BitVector w -> BitVector w+bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))+  where width = natValue wRepr++-- | Bitwise absolute value.+bvAbs :: BitVector w -> BitVector w+bvAbs bvec@(BV wRepr _) = BV wRepr abs_x+  where width = natValue wRepr+        x     = bvIntegerS bvec+        abs_x = truncBits width (abs x) -- this is necessary++-- | Bitwise negation.+bvNegate :: BitVector w -> BitVector w+bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))+  where width = fromIntegral (natValue wRepr) :: Integer++-- | Get the sign bit as a 'BitVector'.+bvSignum :: BitVector w -> BitVector w+bvSignum bvec@(BV wRepr _) = (bvShift bvec (1 - width)) `bvAnd` (BV wRepr 0x1)+  where width = fromIntegral (natValue wRepr)++----------------------------------------+-- Width-changing operations++-- | Concatenate two bit vectors.+--+-- >>> (bv 0xAA :: BitVector 8) `bvConcat` (bv 0xBCDEF0 :: BitVector 24)+-- 0xaabcdef0<32>+-- >>> :type it+-- it :: BitVector 32+--+-- Note that the first argument gets placed in the higher-order bits. The above+-- example should be illustrative enough.+bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)+bvConcat (BV hiWRepr hi) (BV loWRepr lo) =+  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)+  where loWidth = fromIntegral (natValue loWRepr)++-- | Infix 'bvConcat'.+(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)+(<:>) = bvConcat++infixl 6 <:>++-- | Slice out a smaller bit vector from a larger one. The lowest significant bit is+-- given explicitly as an argument of type 'Int', and the length of the slice is+-- inferred from a type-level context.+--+-- >>> bvExtract 12 (bv 0xAABCDEF0 :: BitVector 32) :: BitVector 8+-- 0xcd<8>+--+-- Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and+-- extract bits that aren't present in the input, you will get 0's.+bvExtract :: forall w w' . (KnownNat w')+          => Int+          -> BitVector w+          -> BitVector w'+bvExtract pos bvec = bv xShf+  where (BV _ xShf) = bvShift bvec (- pos)++-- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.+bvExtractWithRepr :: NatRepr w'+                  -> Int+                  -> BitVector w+                  -> BitVector w'+bvExtractWithRepr repr pos bvec = BV repr (truncBits width xShf)+  where (BV _ xShf) = bvShift bvec (- pos)+        width = natValue repr++-- | Zero-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvZext :: forall w w' . KnownNat w'+       => BitVector w+       -> BitVector w'+bvZext (BV _ x) = bv x++-- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.+bvZextWithRepr :: NatRepr w'+               -> BitVector w+               -> BitVector w'+bvZextWithRepr repr (BV _ x) = BV repr (truncBits width x)+  where width = natValue repr++-- | Sign-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvSext :: forall w w' . KnownNat w'+       => BitVector w+       -> BitVector w'+bvSext bvec = bv (bvIntegerS bvec)++-- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.+bvSextWithRepr :: NatRepr w'+               -> BitVector w+               -> BitVector w'+bvSextWithRepr repr bvec = BV repr (truncBits width (bvIntegerS bvec))+  where width = natValue repr++-- | Fully multiply two bit vectors as unsigned integers, returning a bit vector+-- whose length is equal to the sum of the inputs.+bvMulFU :: BitVector w -> BitVector w' -> BitVector (w+w')+bvMulFU (BV wRepr x) (BV wRepr' y) = BV (wRepr `addNat` wRepr') (x*y)++-- | Fully multiply two bit vectors as signed integers, returning a bit vector whose+-- length is equal to the sum of the inputs.+bvMulFS :: BitVector w -> BitVector w' -> BitVector (w+w')+bvMulFS bvec1@(BV wRepr _) bvec2@(BV wRepr' _) = BV prodRepr (truncBits width (x'*y'))+  where x' = bvIntegerS bvec1+        y' = bvIntegerS bvec2+        prodRepr = wRepr `addNat` wRepr'+        width = natValue prodRepr++----------------------------------------+-- Class instances++instance Show (BitVector w) where+  show (BV wRepr val) = prettyHex width val+    where width = natValue wRepr++instance ShowF BitVector++instance Eq (BitVector w) where+  (BV _ x) == (BV _ y) = x == y++instance EqF BitVector where+  (BV _ x) `eqF` (BV _ y) = x == y++instance Ord (BitVector w) where+  (BV _ x) `compare` (BV _ y) = x `compare` y++instance TestEquality BitVector where+  testEquality (BV wRepr x) (BV wRepr' y) =+    case natValue wRepr == natValue wRepr' && x == y of+      True  -> Just (unsafeCoerce (Refl :: a :~: a))+      False -> Nothing++instance KnownNat w => Bits (BitVector w) where+  (.&.)        = bvAnd+  (.|.)        = bvOr+  xor          = bvXor+  complement   = bvComplement+  shift        = bvShift+  rotate       = bvRotate+  bitSize      = bvWidth+  bitSizeMaybe = Just . bvWidth+  isSigned     = const False+  testBit      = bvTestBit+  bit          = bv . bit+  popCount     = bvPopCount++instance KnownNat w => FiniteBits (BitVector w) where+  finiteBitSize = bvWidth++instance KnownNat w => Num (BitVector w) where+  (+)         = bvAdd+  (*)         = bvMul+  abs         = bvAbs+  signum      = bvSignum+  fromInteger = bv+  negate      = bvNegate++instance KnownNat w => Enum (BitVector w) where+  toEnum   = bv . fromIntegral+  fromEnum = fromIntegral . bvIntegerU++instance KnownNat w => Bounded (BitVector w) where+  minBound = bv 0+  maxBound = bv (-1)++----------------------------------------+-- UTILITIES++----------------------------------------+-- Pretty Printing++-- | Print an integral value in hex with a leading "0x"+prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String+prettyHex width val = printf format val width+  where numDigits = (width+3) `div` 4+        format = "0x%." ++ show numDigits ++ "x<%d>"++----------------------------------------+-- Bits++-- | Mask for a specified number of lower bits.+lowMask :: (Integral a, Bits b) => a -> b+lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)++-- | Truncate to a specified number of lower bits.+truncBits :: (Integral a, Bits b) => a -> b -> b+truncBits width b = b .&. lowMask width
− src/Data/BitVector/Sized/Internal.hs
@@ -1,317 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}--{-|-Module      : Data.BitVector.Sized.Internal-Copyright   : (c) Benjamin Selfridge, 2018-                  Galois Inc.-License     : BSD3-Maintainer  : benselfridge@galois.com-Stability   : experimental-Portability : portable--This module defines a width-parameterized 'BitVector' type and various associated-operations that assume a 2's complement representation. This module exports more of-the internals of the type as well as several functions that operate on explicit-'NatRepr's instead of requiring a 'KnownNat' constraint.--}--module Data.BitVector.Sized.Internal-  ( -- * BitVector type-    BitVector(..)-  , bv-    -- * Bitwise operations (width-preserving)-    -- | These are alternative versions of some of the 'Bits' functions where we do-    -- not need to know the width at compile time. They are all width-preserving.-  , bvAnd, bvOr, bvXor-  , bvComplement-  , bvShift, bvRotate-  , bvWidth-  , bvTestBit-  , bvPopCount-    -- * Arithmetic operations (width-preserving)-  , bvAdd, bvMul-  , bvAbs, bvNegate-  , bvSignum-    -- * Bitwise operations (variable width)-    -- | These are functions that involve bit vectors of different lengths.-  , bvConcat, (<:>)-  , bvExtract, bvExtractWithRepr-  , bvZext, bvZextWithRepr-  , bvSext, bvSextWithRepr-    -- * Conversions to Integer-  , bvIntegerU-  , bvIntegerS-  ) where--import Data.Bits-import Data.Parameterized.Classes-import Data.Parameterized.NatRepr-import GHC.TypeLits-import Text.Printf-import Unsafe.Coerce (unsafeCoerce)-------------------------------------------- BitVector data type definitions---- | BitVector datatype, parameterized by width.-data BitVector (w :: Nat) :: * where-  BV :: NatRepr w -> Integer -> BitVector w---- | Construct a bit vector in a context where the width is inferrable from the type--- context. The 'Integer' input (an unbounded data type, hence with an infinite-width--- bit representation), whether positive or negative is silently truncated to fit--- into the number of bits demanded by the return type.------ >>> bv 0xA :: BitVector 4--- 0xa<4>--- >>> bv 0xA :: BitVector 3--- 0x2<3>--- >>> bv (-1) :: BitVector 8--- 0xff<8>--- >>> bv (-1) :: BitVector 32--- 0xffffffff<32>--bv :: KnownNat w => Integer -> BitVector w-bv x = BV wRepr (truncBits width (fromIntegral x))-  where wRepr = knownNat-        width = natValue wRepr--------------------------------------------- BitVector -> Integer functions---- | Unsigned interpretation of a bit vector as a (positive) Integer.-bvIntegerU :: BitVector w -> Integer-bvIntegerU (BV _ x) = x---- | Signed interpretation of a bit vector as an Integer.-bvIntegerS :: BitVector w -> Integer-bvIntegerS bvec = case bvTestBit bvec (width - 1) of-  True  -> bvIntegerU bvec - (1 `shiftL` width)-  False -> bvIntegerU bvec-  where width = bvWidth bvec--------------------------------------------- BitVector w operations (fixed width)---- | Bitwise and.-bvAnd :: BitVector w -> BitVector w -> BitVector w-bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)---- | Bitwise or.-bvOr :: BitVector w -> BitVector w -> BitVector w-bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)---- | Bitwise xor.-bvXor :: BitVector w -> BitVector w -> BitVector w-bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)---- | Bitwise complement (flip every bit).-bvComplement :: BitVector w -> BitVector w-bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))-  where width = natValue wRepr---- | Bitwise shift.-bvShift :: BitVector w -> Int -> BitVector w-bvShift bvec@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))-  where width = natValue wRepr-        x     = bvIntegerS bvec -- arithmetic right shift when negative---- | Bitwise rotate.-bvRotate :: BitVector w -> Int -> BitVector w-bvRotate bvec rot' = leftChunk `bvOr` rightChunk-  where rot = rot' `mod` (bvWidth bvec)-        leftChunk = bvShift bvec rot-        rightChunk = bvShift bvec (rot - bvWidth bvec)---- | Get the width of a 'BitVector'.-bvWidth :: BitVector w -> Int-bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)---- | Test if a particular bit is set.-bvTestBit :: BitVector w -> Int -> Bool-bvTestBit (BV _ x) b = testBit x b---- | Get the number of 1 bits in a 'BitVector'.-bvPopCount :: BitVector w -> Int-bvPopCount (BV _ x) = popCount x--------------------------------------------- BitVector w arithmetic operations (fixed width)---- | Bitwise add.-bvAdd :: BitVector w -> BitVector w -> BitVector w-bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))-  where width = natValue wRepr---- | Bitwise multiply.-bvMul :: BitVector w -> BitVector w -> BitVector w-bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))-  where width = natValue wRepr---- | Bitwise absolute value.-bvAbs :: BitVector w -> BitVector w-bvAbs bvec@(BV wRepr _) = BV wRepr abs_x-  where width = natValue wRepr-        x     = bvIntegerS bvec-        abs_x = truncBits width (abs x) -- this is necessary---- | Bitwise negation.-bvNegate :: BitVector w -> BitVector w-bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))-  where width = fromIntegral (natValue wRepr) :: Integer---- | Get the sign bit as a 'BitVector'.-bvSignum :: BitVector w -> BitVector w-bvSignum bvec@(BV wRepr _) = (bvShift bvec (1 - width)) `bvAnd` (BV wRepr 0x1)-  where width = fromIntegral (natValue wRepr)--------------------------------------------- Width-changing operations---- | Concatenate two bit vectors.------ >>> (bv 0xAA :: BitVector 8) `bvConcat` (bv 0xBCDEF0 :: BitVector 24)--- 0xaabcdef0<32>------ Note that the first argument gets placed in the higher-order bits. The above--- example should be illustrative enough.-bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)-bvConcat (BV hiWRepr hi) (BV loWRepr lo) =-  BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)-  where loWidth = fromIntegral (natValue loWRepr)---- | Infix 'bvConcat'.-(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)-(<:>) = bvConcat--infixl 6 <:>---- | Slice out a smaller bit vector from a larger one. The lowest significant bit is--- given explicitly as an argument of type 'Int', and the length of the slice is--- inferred from a type-level context.------ >>> bvExtract 12 (bv 0xAABCDEF0 :: BitVector 32) :: BitVector 8--- 0xcd<8>------ Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and--- extract bits that aren't present in the input, you will get 0's.-bvExtract :: forall w w' . (KnownNat w')-          => Int-          -> BitVector w-          -> BitVector w'-bvExtract pos bvec = bv xShf-  where (BV _ xShf) = bvShift bvec (- pos)---- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.-bvExtractWithRepr :: NatRepr w'-                  -> Int-                  -> BitVector w-                  -> BitVector w'-bvExtractWithRepr repr pos bvec = BV repr xShf-  where (BV _ xShf) = bvShift bvec (- pos)---- | Zero-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvZext :: forall w w' . KnownNat w'-       => BitVector w-       -> BitVector w'-bvZext (BV _ x) = bv x---- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.-bvZextWithRepr :: NatRepr w'-               -> BitVector w-               -> BitVector w'-bvZextWithRepr repr (BV _ x) = BV repr x---- | Sign-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvSext :: forall w w' . KnownNat w'-       => BitVector w-       -> BitVector w'-bvSext bvec = bv (bvIntegerS bvec)---- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.-bvSextWithRepr :: NatRepr w'-               -> BitVector w-               -> BitVector w'-bvSextWithRepr repr bvec = BV repr (bvIntegerS bvec)--------------------------------------------- Class instances--instance Show (BitVector w) where-  show (BV wRepr val) = prettyHex width val-    where width = natValue wRepr--instance ShowF BitVector--instance Eq (BitVector w) where-  (BV _ x) == (BV _ y) = x == y--instance EqF BitVector where-  (BV _ x) `eqF` (BV _ y) = x == y--instance TestEquality BitVector where-  testEquality (BV wRepr x) (BV wRepr' y) =-    case natValue wRepr == natValue wRepr' && x == y of-      True  -> Just (unsafeCoerce (Refl :: a :~: a))-      False -> Nothing--instance KnownNat w => Bits (BitVector w) where-  (.&.)        = bvAnd-  (.|.)        = bvOr-  xor          = bvXor-  complement   = bvComplement-  shift        = bvShift-  rotate       = bvRotate-  bitSize      = bvWidth-  bitSizeMaybe = Just . bvWidth-  isSigned     = const False-  testBit      = bvTestBit-  bit          = bv . bit-  popCount     = bvPopCount--instance KnownNat w => FiniteBits (BitVector w) where-  finiteBitSize = bvWidth--instance KnownNat w => Num (BitVector w) where-  (+)         = bvAdd-  (*)         = bvMul-  abs         = bvAbs-  signum      = bvSignum-  fromInteger = bv-  negate      = bvNegate--instance KnownNat w => Enum (BitVector w) where-  toEnum   = bv . fromIntegral-  fromEnum = fromIntegral . bvIntegerU--instance KnownNat w => Bounded (BitVector w) where-  minBound = bv 0-  maxBound = bv (-1)--------------------------------------------- UTILITIES--------------------------------------------- Pretty Printing---- | Print an integral value in hex with a leading "0x"-prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String-prettyHex width val = printf format val width-  where numDigits = (width+3) `div` 4-        format = "0x%." ++ show numDigits ++ "x<%d>"--------------------------------------------- Bits---- | Mask for a specified number of lower bits.-lowMask :: (Integral a, Bits b) => a -> b-lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)---- | Truncate to a specified number of lower bits.-truncBits :: (Integral a, Bits b) => a -> b -> b-truncBits width b = b .&. lowMask width
stack.yaml view
@@ -4,4 +4,6 @@ - .  extra-deps:+- containers-0.5.11.0+- lens-4.16 - parameterized-utils-1.0.0