{-# OPTIONS_GHC -funbox-strict-fields #-}

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}

-- NOTE: defined(MIN_VERSION_integer_gmp) == package configured with -fgmp

#if defined(MIN_VERSION_integer_gmp)
{-# LANGUAGE MagicHash #-}
#endif

-- |
-- Module    : Data.BitVector
-- Copyright : (c) 2012-2016 Iago Abal
--             (c) 2012-2013 HASLab & University of Minho
-- License   : BSD3
-- Maintainer: Iago Abal <mail@iagoabal.eu>
--
-- Bit-vector arithmetic inspired by SMT-LIB <http://smt-lib.org/>
-- and Cryptol <http://cryptol.net/>.
--
-- Bit-vectors are represented as a pair /size/ and /value/,
-- where sizes are of type 'Int' and values are 'Integer'.
--
-- * Bit-vectors are interpreted as unsigned integers
--   (i.e. natural numbers) except for some specific /signed/ operations.
--
-- * Most operations are in some way /size-polymorphic/ and, if required,
--   will perform padding to adjust the size of input bit-vectors.
--
-- For documentation purposes we will write @[n]k@ to denote a bit-vector
-- of size @n@ representing the natural number @k@.
module Data.BitVector
  ( -- * Bit-vectors
    BitVector
  , BV
  , size, width
  , nat, uint, int
    -- * Creation
  , nil
  , bitVec
  , bitVecs
  , ones, zeros
    -- * Test
  , isNat
  , isPos
    -- * Comparison
  , (==.), (/=.)
  , (<.), (<=.), (>.), (>=.)
  , slt, sle, sgt, sge
    -- * Indexing
  , (@.), index
  , (@@), extract
  , (@:)
  , (!.)
  , least, most
  , msb, lsb, msb1, lsb1
  -- * Arithmetic
  , signumI
  , pow
  , sdiv, srem, smod
  , lg2
  -- * List-like operations
  , (#), cat, append, concat
  , zeroExtend, signExtend
  , foldl, foldl_
  , foldr, foldr_
  , reverse, reverse_
  , replicate, replicate_
  , and, and_
  , or, or_
  , split
  , group, group_
  , join
  -- * Bitwise operations
  , module Data.Bits
  , not, not_
  , nand, nor, xnor
  , (<<.), shl, (>>.), shr, ashr
  , (<<<.), rol, (>>>.), ror
  -- * Conversion
  , fromBool
  , fromBits
  , toBits
  -- * Pretty-printing
  , showBin
  , showOct
  , showHex
  ) where

import           Control.Monad ( Monad(..), when )
import           Control.Exception ( assert )

import           Data.Bits
import           Data.Bool ( Bool(..), otherwise, (&&), (||))
import qualified Data.Bool as Bool
import           Data.Data ( Data )
import qualified Data.List as List
import           Data.Monoid ( Monoid(..) )
import           Data.Ord
#ifdef __GLASGOW_HASKELL__
import qualified Text.Read as R
#endif
import           Data.Typeable ( Typeable )

#if defined(MIN_VERSION_integer_gmp)
import qualified GHC.Integer.Logarithms as I
import           GHC.Prim ( (+#) )
import           GHC.Types ( Int(..) )
#else
import           Data.Int ( Int )
#endif

import           Prelude
  ( Char
  , Eq(..)
  , Enum(..), Num(..)
  , Integral(..), Integer
  , Maybe(..)
  , Real(..)
#if MIN_VERSION_base(4,11,0)
  , Semigroup(..)
#endif
  , Show(..), String
  , const
  , error
  , flip, fromIntegral
  , maxBound
  , snd
  , undefined
  , ($), (.), (^), (++)
  )

{-# DEPRECATED foldl_, foldr_, reverse_, replicate_, and_, or_, group_, not_ "Use corresponding versions without underscore" #-}
{-# DEPRECATED cat "Use (#) or append instead" #-}

----------------------------------------------------------------------
--- Bit-vectors

-- | Big-endian /pseudo size-polymorphic/ bit-vectors.
data BV
    = BV {
      BV -> Int
size :: !Int      -- ^ The /size/ of a bit-vector.
    , BV -> Integer
nat  :: !Integer  -- ^ The value of a bit-vector, as a natural number.
    }
  deriving (Typeable BV
Typeable BV =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BV -> c BV)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BV)
-> (BV -> Constr)
-> (BV -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BV))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BV))
-> ((forall b. Data b => b -> b) -> BV -> BV)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r)
-> (forall u. (forall d. Data d => d -> u) -> BV -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BV -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BV -> m BV)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BV -> m BV)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BV -> m BV)
-> Data BV
BV -> Constr
BV -> DataType
(forall b. Data b => b -> b) -> BV -> BV
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BV -> u
forall u. (forall d. Data d => d -> u) -> BV -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BV -> m BV
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BV -> m BV
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BV
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BV -> c BV
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BV)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BV)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BV -> c BV
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BV -> c BV
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BV
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BV
$ctoConstr :: BV -> Constr
toConstr :: BV -> Constr
$cdataTypeOf :: BV -> DataType
dataTypeOf :: BV -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BV)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BV)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BV)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BV)
$cgmapT :: (forall b. Data b => b -> b) -> BV -> BV
gmapT :: (forall b. Data b => b -> b) -> BV -> BV
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BV -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BV -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BV -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BV -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BV -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BV -> m BV
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BV -> m BV
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BV -> m BV
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BV -> m BV
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BV -> m BV
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BV -> m BV
Data,Typeable)

-- | An alias for 'BV'.
type BitVector = BV

-- | An alias for 'size'.
width :: BV -> Int
width :: BV -> Int
width = BV -> Int
size
{-# INLINE width #-}

-- | An alias for 'nat'.
uint :: BV -> Integer
uint :: BV -> Integer
uint = BV -> Integer
nat
{-# INLINE uint #-}

-- | 2's complement value of a bit-vector.
--
-- >>> int [2]3
-- -1
--
-- >>> int [4]12
-- -4
int :: BV -> Integer
int :: BV -> Integer
int BV
u | BV -> Bool
msb BV
u     = - BV -> Integer
nat(-BV
u)
      | Bool
otherwise = BV -> Integer
nat BV
u
{-# INLINE int #-}

instance Show BV where
  show :: BV -> String
show (BV Int
n Integer
a) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
a

#ifdef __GLASGOW_HASKELL__
instance R.Read BV where
  readPrec :: ReadPrec BV
readPrec = do
    R.Punc "[" <- ReadPrec Lexeme
R.lexP
    n <- R.step R.readPrec
    when (n < 0) R.pfail
    R.Punc "]" <- R.lexP
    a <- R.step R.readPrec
    when (a < 0) R.pfail
    return (bitVec (n::Int) (a::Integer))
#endif

----------------------------------------------------------------------
--- Safety checking & Errors

checkBounds :: Bool
#if CHECK_BOUNDS
checkBounds :: Bool
checkBounds = Bool
True
#else
checkBounds = False
#endif

check :: Bool -> Bool
check :: Bool -> Bool
check Bool
c = Bool
checkBounds Bool -> Bool -> Bool
&& Bool
c
{-# INLINE check #-}

----------------------------------------------------------------------
--- Construction

-- | The /empty/ bit-vector, ie. @[0]0@.
nil :: BV
nil :: BV
nil = Int -> Integer -> BV
BV Int
0 Integer
0
{-# INLINE nil #-}

-- | Create 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
bitVec :: Integral a => Int -> a -> BV
bitVec :: forall a. Integral a => Int -> a -> BV
bitVec Int
n a
a | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.bitVec: negative size"
           | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0    = Int -> Integer -> BV
BV Int
n (Integer
a' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n)
           | Bool
otherwise = BV -> BV
forall a. Num a => a -> a
negate (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> BV
BV Int
n ((-Integer
a') Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n)
  where a' :: Integer
a' = a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a
{-# INLINE bitVec #-}

-- | List of bit-vector literals of the same size
--
-- When a list of integer literals is interpreted as a list of bit-vectors,
-- 'fromInteger' is applied to each element invidually:
--
-- >>> [1,3,5] :: [BV]
-- [ [1]1, [2]3, [3]5 ]
--
-- Sometimes 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 ]
bitVecs :: Integral a => Int -> [a] -> [BV]
bitVecs :: forall a. Integral a => Int -> [a] -> [BV]
bitVecs = (a -> BV) -> [a] -> [BV]
forall a b. (a -> b) -> [a] -> [b]
List.map ((a -> BV) -> [a] -> [BV])
-> (Int -> a -> BV) -> Int -> [a] -> [BV]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> BV
forall a. Integral a => Int -> a -> BV
bitVec
{-# INLINE bitVecs #-}

-- | Create a mask of ones.
ones :: Int -> BV
ones :: Int -> BV
ones Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.ones: negative size"
       | Bool
otherwise = Int -> Integer -> BV
BV Int
n (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
{-# INLINE ones #-}

-- | Create a mask of zeros.
zeros :: Int -> BV
zeros :: Int -> BV
zeros Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.zeros: negative size"
        | Bool
otherwise = Int -> Integer -> BV
BV Int
n Integer
0
{-# INLINE zeros #-}

----------------------------------------------------------------------
--- Test

-- | Test if the signed value of a bit-vector is a natural number.
isNat :: BV -> Bool
isNat :: BV -> Bool
isNat = Bool -> Bool
Bool.not (Bool -> Bool) -> (BV -> Bool) -> BV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Bool
msb
{-# INLINE isNat #-}

-- | Test if the signed value of a bit-vector is a positive number.
isPos :: BV -> Bool
isPos :: BV -> Bool
isPos BV
a = BV -> Integer
int(BV
a) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
{-# INLINE isPos #-}

----------------------------------------------------------------------
--- Comparison

infix 4 ==., /=., <., <=., >., >=.
infix 4 `slt`, `sle`, `sgt`, `sge`

instance Eq BV where
  (BV Int
_ Integer
a) == :: BV -> BV -> Bool
== (BV Int
_ Integer
b) = Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
  {-# INLINE (==) #-}

instance Ord BV where
  compare :: BV -> BV -> Ordering
compare = (BV -> Integer) -> BV -> BV -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing BV -> Integer
nat
  {-# INLINE compare #-}

-- | Fixed-size equality.
--
-- In contrast with '==', which is /size-polymorphic/, this equality
-- requires both bit-vectors to be of equal size.
--
-- >>> [n]k ==. [m]k
-- False
--
-- >>> [n]k ==. [n]k
-- True
(==.) :: BV -> BV -> Bool
(BV Int
n Integer
a) ==. :: BV -> BV -> Bool
==. (BV Int
m Integer
b) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
{-# INLINE (==.) #-}

-- | Fixed-size inequality.
--
-- The negated version of '==.'.
(/=.) :: BV -> BV -> Bool
BV
u /=. :: BV -> BV -> Bool
/=. BV
v = Bool -> Bool
Bool.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ BV
u BV -> BV -> Bool
==. BV
v
{-# INLINE (/=.) #-}

-- | Fixed-size /less-than/.
(<.) :: BV -> BV -> Bool
(BV Int
n Integer
a) <. :: BV -> BV -> Bool
<. (BV Int
m Integer
b) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b
{-# INLINE (<.) #-}

-- | Fixed-size /less-than-or-equals/.
(<=.) :: BV -> BV -> Bool
(BV Int
n Integer
a) <=. :: BV -> BV -> Bool
<=. (BV Int
m Integer
b) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
{-# INLINE (<=.) #-}

-- | Fixed-size /greater-than/.
(>.) :: BV -> BV -> Bool
(BV Int
n Integer
a) >. :: BV -> BV -> Bool
>. (BV Int
m Integer
b) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
b
{-# INLINE (>.) #-}

-- | Fixed-size /greater-than-or-equals/.
(>=.) :: BV -> BV -> Bool
(BV Int
n Integer
a) >=. :: BV -> BV -> Bool
>=. (BV Int
m Integer
b) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
b
{-# INLINE (>=.) #-}

-- | Fixed-size signed /less-than/.
slt :: BV -> BV -> Bool
u :: BV
u@BV{size :: BV -> Int
size=Int
n} slt :: BV -> BV -> Bool
`slt` v :: BV
v@BV{size :: BV -> Int
size=Int
m} = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& BV -> Integer
int BV
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< BV -> Integer
int BV
v
{-# INLINE slt #-}

-- | Fixed-size signed /less-than-or-equals/.
sle :: BV -> BV -> Bool
u :: BV
u@BV{size :: BV -> Int
size=Int
n} sle :: BV -> BV -> Bool
`sle` v :: BV
v@BV{size :: BV -> Int
size=Int
m} = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& BV -> Integer
int BV
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= BV -> Integer
int BV
v
{-# INLINE sle #-}

-- | Fixed-size signed /greater-than/.
sgt :: BV -> BV -> Bool
u :: BV
u@BV{size :: BV -> Int
size=Int
n} sgt :: BV -> BV -> Bool
`sgt` v :: BV
v@BV{size :: BV -> Int
size=Int
m} = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& BV -> Integer
int BV
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> BV -> Integer
int BV
v
{-# INLINE sgt #-}

-- | Fixed-size signed /greater-than-or-equals/.
sge :: BV -> BV -> Bool
u :: BV
u@BV{size :: BV -> Int
size=Int
n} sge :: BV -> BV -> Bool
`sge` v :: BV
v@BV{size :: BV -> Int
size=Int
m} = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& BV -> Integer
int BV
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= BV -> Integer
int BV
v
{-# INLINE sge #-}

----------------------------------------------------------------------
--- Indexing

infixl 9 @., @@, @:, !.

-- | Bit indexing.
--
-- @u \@. i@ stands for the /i/-th bit of /u/.
--
-- >>> [4]2 @. 0
-- False
--
-- >>> [4]2 @. 1
-- True
(@.) :: Integral ix => BV -> ix -> Bool
(BV Int
n Integer
a) @. :: forall ix. Integral ix => BV -> ix -> Bool
@. ix
i | Bool -> Bool
check(Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i') = String -> Bool
forall a. HasCallStack => String -> a
error String
"Data.BitVector.(@.): index of out bounds"
              | Bool
otherwise                = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i'
  where i' :: Int
i' = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ix
i
{-# INLINE (@.) #-}

-- | @index i a == a \@. i@
index :: Integral ix => ix -> BV -> Bool
index :: forall ix. Integral ix => ix -> BV -> Bool
index = (BV -> ix -> Bool) -> ix -> BV -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip BV -> ix -> Bool
forall ix. Integral ix => BV -> ix -> Bool
(@.)
{-# INLINE index #-}

-- | Bit-string extraction.
--
-- @u \@\@ (j,i) == fromBits (map (u \@.) [j,j-1..i])@
--
-- >>> [4]7 @@ (3,1)
-- [3]3
(@@) :: Integral ix => BV -> (ix,ix) -> BV
(BV Int
_ Integer
a) @@ :: forall ix. Integral ix => BV -> (ix, ix) -> BV
@@ (ix
j,ix
i) | Bool -> Bool
check(ix
i ix -> ix -> Bool
forall a. Ord a => a -> a -> Bool
< ix
0 Bool -> Bool -> Bool
|| ix
j ix -> ix -> Bool
forall a. Ord a => a -> a -> Bool
< ix
i) = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.(@@): invalid range"
                  | Bool
otherwise             = Int -> Integer -> BV
BV Int
m (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
i') Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
m
  where i' :: Int
i' = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ix
i
        m :: Int
m  = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ix -> Int) -> ix -> Int
forall a b. (a -> b) -> a -> b
$ ix
j ix -> ix -> ix
forall a. Num a => a -> a -> a
- ix
i ix -> ix -> ix
forall a. Num a => a -> a -> a
+ ix
1
{-# INLINE (@@) #-}

-- | @extract j i a == a \@\@ (j,i)@
extract :: Integral ix => ix -> ix -> BV -> BV
extract :: forall ix. Integral ix => ix -> ix -> BV -> BV
extract ix
j ix
i = (BV -> (ix, ix) -> BV
forall ix. Integral ix => BV -> (ix, ix) -> BV
@@ (ix
j,ix
i))
{-# INLINE extract #-}

-- | Bit list indexing.
--
-- prop> u @: is ==. fromBits $ List.map (u @.) is
(@:) :: Integral ix => BV -> [ix] -> BV
(BV Int
n Integer
a) @: :: forall ix. Integral ix => BV -> [ix] -> BV
@: [ix]
is = [Bool] -> BV
fromBits ([Bool] -> BV) -> [Bool] -> BV
forall a b. (a -> b) -> a -> b
$ (ix -> Bool) -> [ix] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
List.map ix -> Bool
forall {p}. Integral p => p -> Bool
testBitAux [ix]
is
  -- NB: Failing _late_ (the bounds check is done by 'testBitAux') avoids
  -- duplicating calls to 'fromIntegral' **and** this code should allow GHC
  -- to fuse 'fodlr' (from inlining 'frombits') with 'map'.
  where testBitAux :: p -> Bool
testBitAux p
i
          | Bool -> Bool
check(Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i') = String -> Bool
forall a. HasCallStack => String -> a
error String
"Data.BitVector.(@:): index out of bounds"
          | Bool
otherwise                = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i'
          where i' :: Int
i' = p -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
i
{-# INLINE (@:) #-}

-- | Reverse bit-indexing.
--
-- Index starting from the most significant bit.
--
-- @u !. i == u \@. (size u - i - 1) @
--
-- >>> [3]3 !. 0
-- False
(!.) :: Integral ix => BV -> ix -> Bool
(BV Int
n Integer
a) !. :: forall ix. Integral ix => BV -> ix -> Bool
!. ix
i | Bool -> Bool
check(Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i') = String -> Bool
forall a. HasCallStack => String -> a
error String
"Data.BitVector.(!.): index out of bounds"
              | Bool
otherwise                = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i'Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
  where i' :: Int
i' = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ix
i
{-# INLINE (!.) #-}

-- | Take least significant bits.
--
-- @least m u == u \@\@ (m-1,0)@
least :: Integral ix => ix -> BV -> BV
least :: forall ix. Integral ix => ix -> BV -> BV
least ix
m (BV Int
_ Integer
a) | Bool -> Bool
check(Int
m' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1) = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.least: non-positive index"
                 | Bool
otherwise     = Int -> Integer -> BV
BV Int
m' (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> ix -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ix
m
  where m' :: Int
m' = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ix
m
{-# INLINE least #-}

-- | Take most significant bits.
--
-- @most m u == u \@\@ (n-1,n-m)@
most :: Integral ix => ix -> BV -> BV
most :: forall ix. Integral ix => ix -> BV -> BV
most ix
m (BV Int
n Integer
a) | Bool -> Bool
check(Int
m' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1) = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.most: non-positive index"
                | Bool -> Bool
check(Int
m' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n) = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.most: index out of bounds"
                | Bool
otherwise     = Int -> Integer -> BV
BV Int
m' (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m')
  where m' :: Int
m' = ix -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ix
m
{-# INLINE most #-}

-- | Most significant bit.
--
-- @msb u == u !. 0@
msb :: BV -> Bool
msb :: BV -> Bool
msb = (BV -> Int -> Bool
forall ix. Integral ix => BV -> ix -> Bool
!. (Int
0::Int))
{-# INLINE msb #-}

-- | Least significant bit.
--
-- @lsb u == u \@. 0@
lsb :: BV -> Bool
lsb :: BV -> Bool
lsb = (BV -> Int -> Bool
forall ix. Integral ix => BV -> ix -> Bool
@. (Int
0::Int))
{-# INLINE lsb #-}

-- | Most significant 1-bit.
--
-- /Pre/: input must be non-zero.
--
-- >>> msb1 [4]2
-- 1
--
-- >>> msb1 [4]4
-- 2
msb1 :: BV -> Int
msb1 :: BV -> Int
msb1 (BV Int
_ Integer
0) = String -> Int
forall a. HasCallStack => String -> a
error String
"Data.BitVector.msb1: zero bit-vector"
msb1 (BV Int
n Integer
a) = Int -> Int
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
  where go :: Int -> Int
go Int
i | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i = Int
i
             | Bool
otherwise   = Int -> Int
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

-- | Least significant 1-bit.
--
-- /Pre/: input must be non-zero.
--
-- >>> msb1 [4]3
-- 0
--
-- >>> msb1 [4]6
-- 1
lsb1 :: BV -> Int
lsb1 :: BV -> Int
lsb1 (BV Int
_ Integer
0) = String -> Int
forall a. HasCallStack => String -> a
error String
"Data.BitVector.lsb1: zero bit-vector"
lsb1 (BV Int
_ Integer
a) = Int -> Int
go Int
0
  where go :: Int -> Int
go Int
i | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i = Int
i
             | Bool
otherwise   = Int -> Int
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

----------------------------------------------------------------------
--- Arithmetic

instance Num BV where
  (BV Int
n1 Integer
a) + :: BV -> BV -> BV
+ (BV Int
n2 Integer
b) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
  {-# INLINE (+) #-}
  (BV Int
n1 Integer
a) * :: BV -> BV -> BV
* (BV Int
n2 Integer
b) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
  {-# INLINE (*) #-}
  negate :: BV -> BV
negate u :: BV
u@(BV Int
_ Integer
0) = BV
u
  negate   (BV Int
n Integer
a) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
a
  {-# INLINE negate #-}
  abs :: BV -> BV
abs BV
u | BV -> Bool
msb BV
u     = BV -> BV
forall a. Num a => a -> a
negate BV
u
        | Bool
otherwise = BV
u
  {-# INLINE abs #-}
  signum :: BV -> BV
signum BV
u = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
2 (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
signum (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ BV -> Integer
int BV
u
  {-# INLINE signum #-}
  fromInteger :: Integer -> BV
fromInteger !Integer
i = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
n Integer
i
    where !n :: Int
n = if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer -> Int
integerWidth Integer
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 else Integer -> Int
integerWidth Integer
i
  {-# INLINE fromInteger #-}

-- | Bit-vector 'signum' as an 'Integral'.
signumI :: Integral a => BV -> a
signumI :: forall a. Integral a => BV -> a
signumI = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (BV -> Integer) -> BV -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum (Integer -> Integer) -> (BV -> Integer) -> BV -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
int

instance Real BV where
  toRational :: BV -> Rational
toRational = Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational) -> (BV -> Integer) -> BV -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
nat

instance Enum BV where
  toEnum :: Int -> BV
toEnum = Int -> BV
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  fromEnum :: BV -> Int
fromEnum (BV Int
_ Integer
a) = Bool -> Int -> Int
forall a. HasCallStack => Bool -> a -> a
assert (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
max_int) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
a
    where max_int :: Integer
max_int = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound::Int)

instance Integral BV where
  quotRem :: BV -> BV -> (BV, BV)
quotRem (BV Int
n1 Integer
a) (BV Int
n2 Integer
b) = (Int -> Integer -> BV
BV Int
n Integer
q,Int -> Integer -> BV
BV Int
n Integer
r)
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
          (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
a Integer
b
  {-# INLINE quotRem #-}
  divMod :: BV -> BV -> (BV, BV)
divMod = BV -> BV -> (BV, BV)
forall a. Integral a => a -> a -> (a, a)
quotRem
  {-# INLINE divMod #-}
  toInteger :: BV -> Integer
toInteger = BV -> Integer
int
  {-# INLINE toInteger #-}

-- | Bit-vector exponentiation.
--
-- @pow [n]k e@ computes @k@ raised to @e@ modulo @n@.
--
-- This is faster than Haskell's (^) operator because it performs
-- modulo division just once. Besides, @a^0 == [1]0@ !!!
pow :: Integral exp => BV -> exp -> BV
pow :: forall exp. Integral exp => BV -> exp -> BV
pow (BV Int
n Integer
a) exp
e = Int -> Integer -> BV
BV Int
n (Integer
aInteger -> exp -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^exp
e Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)
  where m :: Integer
m = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
{-# INLINE pow #-}

-- | 2's complement signed division.
sdiv :: BV -> BV -> BV
sdiv :: BV -> BV -> BV
sdiv u :: BV
u@(BV Int
n1 Integer
_) v :: BV
v@(BV Int
n2 Integer
_) = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
n Integer
q
  where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
        q :: Integer
q = BV -> Integer
int BV
u Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` BV -> Integer
int BV
v
{-# INLINE sdiv #-}

-- | 2's complement signed remainder (sign follows dividend).
srem :: BV -> BV -> BV
srem :: BV -> BV -> BV
srem u :: BV
u@(BV Int
n1 Integer
_) v :: BV
v@(BV Int
n2 Integer
_) = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
n Integer
r
  where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
        r :: Integer
r = BV -> Integer
int BV
u Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` BV -> Integer
int BV
v
{-# INLINE srem #-}

-- | 2's complement signed remainder (sign follows divisor).
smod :: BV -> BV -> BV
smod :: BV -> BV -> BV
smod u :: BV
u@(BV Int
n1 Integer
_) v :: BV
v@(BV Int
n2 Integer
_) = Int -> Integer -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
n Integer
r
  where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
        r :: Integer
r = BV -> Integer
int BV
u Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` BV -> Integer
int BV
v
{-# INLINE smod #-}

-- | Ceiling logarithm base 2.
--
-- /Pre/: input bit-vector must be non-zero.
lg2 :: BV -> BV
lg2 :: BV -> BV
lg2 (BV Int
_ Integer
0) = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.lg2: zero bit-vector"
lg2 (BV Int
n Integer
1) = Int -> Integer -> BV
BV Int
n Integer
0
#if defined(MIN_VERSION_integer_gmp)
lg2 (BV Int
n Integer
a) = Int -> Integer -> BV
BV Int
n (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
a')
  where a' :: Int
a' = Int# -> Int
I# (Integer -> Int#
I.integerLog2# Integer
a)
#else
lg2 (BV n a) = BV n $ go 0 1
  where go !k !b | b == a    = k
                 | b > a     = k-1
                 | otherwise = go (k+1) (2*b)
#endif
{-# INLINE lg2 #-}

----------------------------------------------------------------------
--- List-like operations

infixr 5 #

-- | Concatenation of two bit-vectors.
(#), cat, append :: BV -> BV -> BV
(BV Int
n Integer
a) # :: BV -> BV -> BV
# (BV Int
m Integer
b) = Int -> Integer -> BV
BV (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) ((Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
m) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)
{-# INLINE (#) #-}

cat :: BV -> BV -> BV
cat = BV -> BV -> BV
(#)
{-# INLINE cat #-}

append :: BV -> BV -> BV
append = BV -> BV -> BV
(#)
{-# INLINE append #-}

-- | An alias for 'join'.
concat :: [BV] -> BV
concat :: [BV] -> BV
concat = [BV] -> BV
join

-- This is the most sensible monoid instance until we have size types!

instance Monoid BV where
  mempty :: BV
mempty  = BV
nil
  {-# INLINE mempty #-}
  mconcat :: [BV] -> BV
mconcat = [BV] -> BV
join
  {-# INLINE mconcat #-}
#if !MIN_VERSION_base(4,11,0)
  mappend = (#)
  {-# INLINE mappend #-}
#else

instance Semigroup BV where
  <> :: BV -> BV -> BV
(<>) = BV -> BV -> BV
(#)
  {-# INLINE (<>) #-}
#endif

-- | Logical extension.
--
-- >>> zeroExtend 3 [1]1
-- [4]1
zeroExtend :: Integral size => size -> BV -> BV
zeroExtend :: forall ix. Integral ix => ix -> BV -> BV
zeroExtend size
d (BV Int
n Integer
a) = Int -> Integer -> BV
BV (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
d') Integer
a
  where d' :: Int
d' = size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral size
d
{-# INLINE zeroExtend #-}

-- | Arithmetic extension.
--
-- >>> signExtend 2 [2]1
-- [4]1
--
-- >>> signExtend 2 [2]3
-- [4]15
signExtend :: Integral size => size -> BV -> BV
signExtend :: forall ix. Integral ix => ix -> BV -> BV
signExtend size
d (BV Int
n Integer
a)
  | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) = Int -> Integer -> BV
BV (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
d') (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (size -> Integer
forall a. Integral a => a -> Integer
maxNat size
d Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
a
  | Bool
otherwise       = Int -> Integer -> BV
BV (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
d') Integer
a
  where d' :: Int
d' = size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral size
d
{-# INLINE 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, foldl_ :: (a -> Bool -> a) -> a -> BV -> a
foldl :: forall a. (a -> Bool -> a) -> a -> BV -> a
foldl a -> Bool -> a
f a
e (BV Int
n Integer
a) = Int -> a -> a
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
e
  where go :: Int -> a -> a
go Int
i !a
x | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0    = let !b :: Bool
b = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i in Int -> a -> a
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a -> Bool -> a
f a
x Bool
b
                | Bool
otherwise = a
x
foldl_ :: forall a. (a -> Bool -> a) -> a -> BV -> a
foldl_ = (a -> Bool -> a) -> a -> BV -> a
forall a. (a -> Bool -> a) -> a -> BV -> a
foldl
{-# INLINE foldl #-}

-- |
-- @foldr f z (fromBits [un, ..., u1, u0]) == un \`f\` (... \`f\` (u1 \`f\` (u0 \`f\` z)))@
--
-- @foldr f e = fromBits . foldr f e . toBits@
foldr, foldr_ :: (Bool -> a -> a) -> a -> BV -> a
foldr :: forall a. (Bool -> a -> a) -> a -> BV -> a
foldr Bool -> a -> a
f a
e (BV Int
n Integer
a) = Int -> a -> a
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
e
 where go :: Int -> a -> a
go Int
i !a
x | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0    = let !b :: Bool
b = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i in Bool -> a -> a
f Bool
b (Int -> a -> a
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
x)
               | Bool
otherwise = a
x
foldr_ :: forall a. (Bool -> a -> a) -> a -> BV -> a
foldr_ = (Bool -> a -> a) -> a -> BV -> a
forall a. (Bool -> a -> a) -> a -> BV -> a
foldr
{-# INLINE foldr #-}

-- |
-- @reverse == fromBits . reverse . toBits@
reverse, reverse_ :: BV -> BV
reverse :: BV -> BV
reverse bv :: BV
bv@(BV Int
n Integer
_) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd ((Integer, Integer) -> Integer) -> (Integer, Integer) -> Integer
forall a b. (a -> b) -> a -> b
$ ((Integer, Integer) -> Bool -> (Integer, Integer))
-> (Integer, Integer) -> BV -> (Integer, Integer)
forall a. (a -> Bool -> a) -> a -> BV -> a
foldl (Integer, Integer) -> Bool -> (Integer, Integer)
forall {b}. Num b => (b, b) -> Bool -> (b, b)
go (Integer
1,Integer
0) BV
bv
  where go :: (b, b) -> Bool -> (b, b)
go (b
v,b
acc) Bool
b | Bool
b         = (b
v',b
accb -> b -> b
forall a. Num a => a -> a -> a
+b
v)
                     | Bool
otherwise = (b
v',b
acc)
          where v' :: b
v' = b
2b -> b -> b
forall a. Num a => a -> a -> a
*b
v
reverse_ :: BV -> BV
reverse_ = BV -> BV
reverse
{-# INLINE reverse #-}

-- |
-- /Pre/: if @replicate_ n u@ then @n > 0@ must hold.
--
-- @replicate_ n == fromBits . concat . replicate n . toBits @
replicate, replicate_ :: Integral size => size -> BV -> BV
replicate :: forall ix. Integral ix => ix -> BV -> BV
replicate size
0 BV
_ = String -> BV
forall a. HasCallStack => String -> a
error String
"Data.BitVector.replicate: cannot replicate 0-times"
replicate size
n BV
u = size -> BV -> BV
forall {t}. (Eq t, Num t) => t -> BV -> BV
go (size
nsize -> size -> size
forall a. Num a => a -> a -> a
-size
1) BV
u
  where go :: t -> BV -> BV
go t
0 !BV
acc = BV
acc
        go t
k !BV
acc = t -> BV -> BV
go (t
kt -> t -> t
forall a. Num a => a -> a -> a
-t
1) (BV
u BV -> BV -> BV
# BV
acc)
replicate_ :: forall ix. Integral ix => ix -> BV -> BV
replicate_ = size -> BV -> BV
forall ix. Integral ix => ix -> BV -> BV
replicate
{-# INLINE replicate #-}

-- | Conjunction.
--
-- Essentially, @and == foldr1 (.&.)@.
--
-- Returns @[1]1@ if the input list is empty.
and, and_ :: [BV] -> BV
and :: [BV] -> BV
and [] = Int -> BV
ones Int
1
and [BV]
ws = Int -> Integer -> BV
BV Int
n' (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
List.foldl1' Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.) ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (BV -> Integer) -> [BV] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
List.map BV -> Integer
nat [BV]
ws
  where n' :: Int
n' = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (BV -> Int) -> [BV] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
List.map BV -> Int
size [BV]
ws
and_ :: [BV] -> BV
and_ = [BV] -> BV
and
{-# INLINE and #-}

-- | Disjunction.
--
-- Essentially, @or == foldr1 (.|.)@.
--
-- Returns @[1]0@ if the input list is empty.
or, or_ :: [BV] -> BV
or :: [BV] -> BV
or [] = Int -> BV
zeros Int
1
or [BV]
ws = Int -> Integer -> BV
BV Int
n' (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
List.foldl1' Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.) ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (BV -> Integer) -> [BV] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
List.map BV -> Integer
nat [BV]
ws
  where n' :: Int
n' = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (BV -> Int) -> [BV] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
List.map BV -> Int
size [BV]
ws
or_ :: [BV] -> BV
or_ = [BV] -> BV
or
{-# 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 :: forall times. Integral times => times -> BV -> [BV]
split times
k (BV Int
n Integer
a) | times
k times -> times -> Bool
forall a. Ord a => a -> a -> Bool
<= times
0    = String -> [BV]
forall a. HasCallStack => String -> a
error String
"Data.BitVector.split: non-positive splits"
                 | Bool
otherwise = (Integer -> BV) -> [Integer] -> [BV]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> Integer -> BV
BV Int
s) ([Integer] -> [BV]) -> [Integer] -> [BV]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Integer -> [Integer]
forall size times.
(Integral size, Integral times) =>
size -> times -> Integer -> [Integer]
splitInteger Int
s Int
k' Integer
a
  where k' :: Int
k' = times -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral times
k
        (Int
q,Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
n Int
k'
        s :: Int
s = Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int
forall a. Num a => a -> a
signum Int
r
{-# INLINE split #-}

-- | Split a bit-vector into /n/-wide pieces.
--
-- >>> group 3 [4]15
-- [[3]1,[3]7]
group, group_ :: Integral size => size -> BV -> [BV]
group :: forall times. Integral times => times -> BV -> [BV]
group size
s (BV Int
n Integer
a) | size
s size -> size -> Bool
forall a. Ord a => a -> a -> Bool
<= size
0    = String -> [BV]
forall a. HasCallStack => String -> a
error String
"Data.BitVector.group: non-positive size"
                 | Bool
otherwise = (Integer -> BV) -> [Integer] -> [BV]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> Integer -> BV
BV Int
s') ([Integer] -> [BV]) -> [Integer] -> [BV]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Integer -> [Integer]
forall size times.
(Integral size, Integral times) =>
size -> times -> Integer -> [Integer]
splitInteger Int
s' Int
k Integer
a
  where s' :: Int
s' = size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral size
s
        (Int
q,Int
r) = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
n Int
s'
        k :: Int
k = Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int
forall a. Num a => a -> a
signum Int
r
group_ :: forall times. Integral times => times -> BV -> [BV]
group_ = size -> BV -> [BV]
forall times. Integral times => times -> BV -> [BV]
group
{-# INLINE group #-}

splitInteger :: (Integral size, Integral times) =>
                    size -> times -> Integer -> [Integer]
splitInteger :: forall size times.
(Integral size, Integral times) =>
size -> times -> Integer -> [Integer]
splitInteger size
n = [Integer] -> times -> Integer -> [Integer]
forall {t} {t}.
(Bits t, Integral t, Num t, Eq t) =>
[t] -> t -> t -> [t]
go []
  where n' :: Int
n' = size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral size
n
        go :: [t] -> t -> t -> [t]
go [t]
acc t
0 t
_ = [t]
acc
        go [t]
acc t
k t
a = [t] -> t -> t -> [t]
go (t
vt -> [t] -> [t]
forall a. a -> [a] -> [a]
:[t]
acc) (t
kt -> t -> t
forall a. Num a => a -> a -> a
-t
1) t
a'
          where v :: t
v  = t
a t -> t -> t
forall a. Integral a => a -> a -> a
`mod` t
2t -> size -> t
forall a b. (Num a, Integral b) => a -> b -> a
^size
n
                a' :: t
a' = t
a t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
n'
{-# INLINE splitInteger #-}

-- | Concatenate a (possibly empty) list of bit-vectors.
--
-- >>> join [[2]3,[2]2]
-- [4]14
join :: [BV] -> BV
join :: [BV] -> BV
join = (BV -> BV -> BV) -> BV -> [BV] -> BV
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' BV -> BV -> BV
(#) BV
nil
{-# INLINE join #-}

----------------------------------------------------------------------
--- Bitwise operations

infixl 8 <<., `shl`, >>., `shr`, `ashr`, <<<., `rol`, >>>., `ror`

instance Bits BV where
  (BV Int
n1 Integer
a) .&. :: BV -> BV -> BV
.&. (BV Int
n2 Integer
b) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
  {-# INLINE (.&.) #-}
  (BV Int
n1 Integer
a) .|. :: BV -> BV -> BV
.|. (BV Int
n2 Integer
b) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
  {-# INLINE (.|.) #-}
  (BV Int
n1 Integer
a) xor :: BV -> BV -> BV
`xor` (BV Int
n2 Integer
b) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b
    where n :: Int
n = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n1 Int
n2
  {-# INLINE xor #-}
  complement :: BV -> BV
complement (BV Int
n Integer
a) = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
a
  {-# INLINE complement #-}
#if MIN_VERSION_base(4,7,0)
  zeroBits :: BV
zeroBits = Int -> Integer -> BV
BV Int
1 Integer
0
  {-# INLINE zeroBits #-}
#endif
  bit :: Int -> BV
bit Int
i = Int -> Integer -> BV
BV (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
i)
  {-# INLINE bit #-}
  testBit :: BV -> Int -> Bool
testBit (BV Int
n Integer
a) Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n     = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
i
                     | Bool
otherwise = Bool
False
  {-# INLINE testBit #-}
  bitSize :: BV -> Int
bitSize = BV -> Int
forall a. HasCallStack => a
undefined
#if MIN_VERSION_base(4,7,0)
  bitSizeMaybe :: BV -> Maybe Int
bitSizeMaybe = Maybe Int -> BV -> Maybe Int
forall a b. a -> b -> a
const Maybe Int
forall a. Maybe a
Nothing
#endif
  isSigned :: BV -> Bool
isSigned = Bool -> BV -> Bool
forall a b. a -> b -> a
const Bool
False
  shiftL :: BV -> Int -> BV
shiftL (BV Int
n Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n     = Int -> Integer -> BV
BV Int
n Integer
0
    | Bool
otherwise = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
a Int
k Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
  {-# INLINE shiftL #-}
  shiftR :: BV -> Int -> BV
shiftR (BV Int
n Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n     = Int -> Integer -> BV
BV Int
n Integer
0
    | Bool
otherwise = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
a Int
k
  {-# INLINE shiftR #-}
  rotateL :: BV -> Int -> BV
rotateL BV
bv       Int
0 = BV
bv
  rotateL (BV Int
n Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n    = Int -> Integer -> BV
BV Int
n Integer
a
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n     = BV -> Int -> BV
forall a. Bits a => a -> Int -> a
rotateL (Int -> Integer -> BV
BV Int
n Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
h Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
l
    where s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
          l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s
          h :: Integer
h = (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
  {-# INLINE rotateL #-}
  rotateR :: BV -> Int -> BV
rotateR BV
bv       Int
0 = BV
bv
  rotateR (BV Int
n Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n    = Int -> Integer -> BV
BV Int
n Integer
a
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n     = BV -> Int -> BV
forall a. Bits a => a -> Int -> a
rotateR (Int -> Integer -> BV
BV Int
n Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Int -> Integer -> BV
BV Int
n (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
h Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
l
    where s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
          l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k
          h :: Integer
h = (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n
  {-# INLINE rotateR #-}
  popCount :: BV -> Int
popCount (BV Int
_ Integer
a) = Bool -> Int -> Int
forall a. HasCallStack => Bool -> a -> a
assert (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
a
  {-# INLINE popCount #-}

-- | An alias for 'complement'.
not, not_ :: BV -> BV
not :: BV -> BV
not = BV -> BV
forall a. Bits a => a -> a
complement
not_ :: BV -> BV
not_ = BV -> BV
not
{-# INLINE not #-}

-- | Negated '.&.'.
nand :: BV -> BV -> BV
nand :: BV -> BV -> BV
nand BV
u BV
v = BV -> BV
not (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV
u BV -> BV -> BV
forall a. Bits a => a -> a -> a
.&. BV
v
{-# INLINE nand #-}

-- | Negated '.|.'.
nor :: BV -> BV -> BV
nor :: BV -> BV -> BV
nor BV
u BV
v = BV -> BV
not (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV
u BV -> BV -> BV
forall a. Bits a => a -> a -> a
.|. BV
v
{-# INLINE nor #-}

-- | Negated 'xor'.
xnor :: BV -> BV -> BV
xnor :: BV -> BV -> BV
xnor BV
u BV
v = BV -> BV
not (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV
u BV -> BV -> BV
forall a. Bits a => a -> a -> a
`xor` BV
v
{-# INLINE xnor #-}

-- | Left shift.
(<<.), shl :: BV -> BV -> BV
bv :: BV
bv@BV{size :: BV -> Int
size=Int
n} <<. :: BV -> BV -> BV
<<. (BV Int
_ Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n  = Int -> Integer -> BV
BV Int
n Integer
0
  | Bool
otherwise            = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`shiftL` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
k)
{-# INLINE (<<.) #-}

shl :: BV -> BV -> BV
shl = BV -> BV -> BV
(<<.)
{-# INLINE shl #-}

-- | Logical right shift.
(>>.), shr :: BV -> BV -> BV
bv :: BV
bv@BV{size :: BV -> Int
size=Int
n} >>. :: BV -> BV -> BV
>>. (BV Int
_ Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n  = Int -> Integer -> BV
BV Int
n Integer
0
  | Bool
otherwise            = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
k)
{-# INLINE (>>.) #-}

shr :: BV -> BV -> BV
shr = BV -> BV -> BV
(>>.)
{-# INLINE shr #-}

-- | Arithmetic right shift
ashr :: BV -> BV -> BV
ashr :: BV -> BV -> BV
ashr BV
u BV
v | BV -> Bool
msb BV
u     = BV -> BV
not ((BV -> BV
not BV
u) BV -> BV -> BV
>>. BV
v)
         | Bool
otherwise = BV
u BV -> BV -> BV
>>. BV
v

-- | Rotate left.
(<<<.), rol :: BV -> BV -> BV

bv :: BV
bv@BV{size :: BV -> Int
size=Int
n} <<<. :: BV -> BV -> BV
<<<. (BV Int
_ Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n'   = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`rotateL` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
k Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n')
  | Bool
otherwise = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`rotateL` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
k)
  where n' :: Integer
n' = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
{-# INLINE (<<<.) #-}

rol :: BV -> BV -> BV
rol = BV -> BV -> BV
(<<<.)
{-# INLINE rol #-}

-- | Rotate right.
(>>>.), ror :: BV -> BV -> BV

bv :: BV
bv@BV{size :: BV -> Int
size=Int
n} >>>. :: BV -> BV -> BV
>>>. (BV Int
_ Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n'   = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`rotateR` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
k Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n')
  | Bool
otherwise = BV
bv BV -> Int -> BV
forall a. Bits a => a -> Int -> a
`rotateR` (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
k)
  where n' :: Integer
n' = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
{-# INLINE (>>>.) #-}

ror :: BV -> BV -> BV
ror = BV -> BV -> BV
(>>>.)
{-# INLINE ror #-}

----------------------------------------------------------------------
--- Conversion

-- | Create a bit-vector from a single bit.
fromBool :: Bool -> BV
fromBool :: Bool -> BV
fromBool Bool
False = Int -> Integer -> BV
BV Int
1 Integer
0
fromBool Bool
True  = Int -> Integer -> BV
BV Int
1 Integer
1
{-# INLINE fromBool #-}

-- | Create a bit-vector from a big-endian list of bits.
--
-- >>> fromBits [False, False, True]
-- [3]1
fromBits :: [Bool] -> BV
fromBits :: [Bool] -> BV
fromBits [Bool]
bs =
  let (Int
n,Integer
k) = (Bool -> (Int, Integer) -> (Int, Integer))
-> (Int, Integer) -> [Bool] -> (Int, Integer)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr Bool -> (Int, Integer) -> (Int, Integer)
forall {b}. Bits b => Bool -> (Int, b) -> (Int, b)
go (Int
0,Integer
0) [Bool]
bs in
  Int -> Integer -> BV
BV Int
n Integer
k
  -- NB: 'setBit' is a GMP function, faster than regular addition.
  where go :: Bool -> (Int, b) -> (Int, b)
go Bool
b (!Int
i,!b
v) | Bool
b         = (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,b -> Int -> b
forall a. Bits a => a -> Int -> a
setBit b
v Int
i)
                     | Bool
otherwise = (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,b
v)
{-# INLINE fromBits #-}

-- | Create a big-endian list of bits from a bit-vector.
--
-- >>> toBits [4]11
-- [True, False, True, True]
toBits :: BV -> [Bool]
toBits :: BV -> [Bool]
toBits (BV Int
n Integer
a) = (Int -> Bool) -> [Int] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
List.map (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a) [Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2..Int
0]
{-# INLINE toBits #-}

----------------------------------------------------------------------
--- Pretty-printing

-- | Show a bit-vector in binary form.
showBin :: BV -> String
showBin :: BV -> String
showBin = (String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (BV -> String) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Char) -> [Bool] -> String
forall a b. (a -> b) -> [a] -> [b]
List.map Bool -> Char
showBit ([Bool] -> String) -> (BV -> [Bool]) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> [Bool]
toBits
  where showBit :: Bool -> Char
showBit Bool
True  = Char
'1'
        showBit Bool
False = Char
'0'

hexChar :: Integral a => a -> Char
hexChar :: forall a. Integral a => a -> Char
hexChar a
0 = Char
'0'
hexChar a
1 = Char
'1'
hexChar a
2 = Char
'2'
hexChar a
3 = Char
'3'
hexChar a
4 = Char
'4'
hexChar a
5 = Char
'5'
hexChar a
6 = Char
'6'
hexChar a
7 = Char
'7'
hexChar a
8 = Char
'8'
hexChar a
9 = Char
'9'
hexChar a
10 = Char
'a'
hexChar a
11 = Char
'b'
hexChar a
12 = Char
'c'
hexChar a
13 = Char
'd'
hexChar a
14 = Char
'e'
hexChar a
15 = Char
'f'
hexChar a
_  = String -> Char
forall a. HasCallStack => String -> a
error String
"Data.BitVector.hexChar: invalid input"

-- | Show a bit-vector in octal form.
showOct :: BV -> String
showOct :: BV -> String
showOct = (String
"0o" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (BV -> String) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BV -> Char) -> [BV] -> String
forall a b. (a -> b) -> [a] -> [b]
List.map (Integer -> Char
forall a. Integral a => a -> Char
hexChar (Integer -> Char) -> (BV -> Integer) -> BV -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
nat) ([BV] -> String) -> (BV -> [BV]) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> BV -> [BV]
forall times. Integral times => times -> BV -> [BV]
group (Int
3::Int)

-- | Show a bit-vector in hexadecimal form.
showHex :: BV -> String
showHex :: BV -> String
showHex = (String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (BV -> String) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BV -> Char) -> [BV] -> String
forall a b. (a -> b) -> [a] -> [b]
List.map (Integer -> Char
forall a. Integral a => a -> Char
hexChar (Integer -> Char) -> (BV -> Integer) -> BV -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
nat) ([BV] -> String) -> (BV -> [BV]) -> BV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> BV -> [BV]
forall times. Integral times => times -> BV -> [BV]
group (Int
4::Int)

----------------------------------------------------------------------
--- Utilities

-- | Greatest natural number representable with /n/ bits.
maxNat :: Integral size => size -> Integer
maxNat :: forall a. Integral a => a -> Integer
maxNat size
n = Integer
2Integer -> size -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^size
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
{-# INLINE maxNat #-}

-- | Minimum width of a bit-vector to represent a given integer number.
--
-- >>> integerWidth 4
-- 3
--
-- >>> integerWidth (-4)
-- 4
integerWidth :: Integer -> Int
#if defined(MIN_VERSION_integer_gmp)
integerWidth :: Integer -> Int
integerWidth !Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Int# -> Int
I# (Integer -> Int#
I.integerLog2# Integer
n Int# -> Int# -> Int#
+# Int#
1#)
  | Bool
otherwise = Int# -> Int
I# (Integer -> Int#
I.integerLog2# (-Integer
n) Int# -> Int# -> Int#
+# Int#
2#)
#else
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)
#endif
{-# INLINE integerWidth #-}