{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

{-|
Module      : Data.BitVector.Sized.Internal
Copyright   : (c) Galois Inc. 2018
License     : BSD-3
Maintainer  : benselfridge@galois.com
Stability   : experimental
Portability : portable

Internal hidden module containing all definitions for the 'BV' type.
-}

module Data.BitVector.Sized.Internal where

import Data.BitVector.Sized.Panic (panic)

-- Qualified imports
import qualified Data.Bits                  as B
import qualified Data.Bits.Bitwise          as B
import qualified Data.ByteString            as BS
import qualified Numeric                    as N
import qualified Data.Parameterized.NatRepr as P
import qualified Prelude

-- Unqualified imports
import Control.DeepSeq (NFData)
import Data.Char (intToDigit)
import Data.List (genericLength)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Parameterized ( NatRepr
                          , mkNatRepr
                          , natValue
                          , intValue
                          , addNat
                          , ShowF
                          , EqF(..)
                          , Hashable(..)
                          , Some(..)
                          , Pair(..)
                          )
import GHC.Generics (Generic)
import GHC.TypeLits (Nat, type(+), type(<=))
import Language.Haskell.TH.Lift (Lift)
import Numeric.Natural (Natural)
import Prelude hiding (abs, or, and, negate, concat, signum)
import System.Random.Stateful

----------------------------------------
-- Utility functions

-- | Check that a 'NatRepr' is representable as an 'Int'.
checkNatRepr :: NatRepr w -> a -> a
checkNatRepr :: NatRepr w -> a -> a
checkNatRepr = Natural -> a -> a
forall a. Natural -> a -> a
checkNatural (Natural -> a -> a)
-> (NatRepr w -> Natural) -> NatRepr w -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue

-- | Check that a 'Natural' is representable as an 'Int'.
checkNatural :: Natural -> a -> a
checkNatural :: Natural -> a -> a
checkNatural Natural
n a
a = if Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int) :: Natural)
  then String -> [String] -> a
forall a. String -> [String] -> a
panic String
"Data.BitVector.Sized.Internal.checkNatural"
       [Natural -> String
forall a. Show a => a -> String
show Natural
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not representable as Int"]
  else a
a


-- | Unsafe coercion from @Natural@ to @Int@.  We mostly use this to
--   interact with operations from "Data.Bits".  This should only be
--   called when we already know the input @Natural@ is small enough,
--   e.g., because we previously called @checkNatural@.
fromNatural :: Natural -> Int
fromNatural :: Natural -> Int
fromNatural = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral

----------------------------------------
-- BitVector data type definitions

-- | Bitvector datatype, parameterized by width.
newtype BV (w :: Nat) :: Type where
  -- | We store the value as an 'Integer' rather than a 'Natural',
  -- since many of the operations on bitvectors rely on a two's
  -- complement representation. However, an invariant on the value is
  -- that it must always be positive.
  --
  -- Secondly, we maintain the invariant that any constructed BV value
  -- has a width whose value is representable in a Haskell @Int@.
  BV :: Integer -> BV w

  deriving ( (forall x. BV w -> Rep (BV w) x)
-> (forall x. Rep (BV w) x -> BV w) -> Generic (BV w)
forall x. Rep (BV w) x -> BV w
forall x. BV w -> Rep (BV w) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (w :: Nat) x. Rep (BV w) x -> BV w
forall (w :: Nat) x. BV w -> Rep (BV w) x
$cto :: forall (w :: Nat) x. Rep (BV w) x -> BV w
$cfrom :: forall (w :: Nat) x. BV w -> Rep (BV w) x
Generic
           , BV w -> ()
(BV w -> ()) -> NFData (BV w)
forall a. (a -> ()) -> NFData a
forall (w :: Nat). BV w -> ()
rnf :: BV w -> ()
$crnf :: forall (w :: Nat). BV w -> ()
NFData
           , Int -> BV w -> String -> String
[BV w] -> String -> String
BV w -> String
(Int -> BV w -> String -> String)
-> (BV w -> String) -> ([BV w] -> String -> String) -> Show (BV w)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall (w :: Nat). Int -> BV w -> String -> String
forall (w :: Nat). [BV w] -> String -> String
forall (w :: Nat). BV w -> String
showList :: [BV w] -> String -> String
$cshowList :: forall (w :: Nat). [BV w] -> String -> String
show :: BV w -> String
$cshow :: forall (w :: Nat). BV w -> String
showsPrec :: Int -> BV w -> String -> String
$cshowsPrec :: forall (w :: Nat). Int -> BV w -> String -> String
Show
           , ReadPrec [BV w]
ReadPrec (BV w)
Int -> ReadS (BV w)
ReadS [BV w]
(Int -> ReadS (BV w))
-> ReadS [BV w]
-> ReadPrec (BV w)
-> ReadPrec [BV w]
-> Read (BV w)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (w :: Nat). ReadPrec [BV w]
forall (w :: Nat). ReadPrec (BV w)
forall (w :: Nat). Int -> ReadS (BV w)
forall (w :: Nat). ReadS [BV w]
readListPrec :: ReadPrec [BV w]
$creadListPrec :: forall (w :: Nat). ReadPrec [BV w]
readPrec :: ReadPrec (BV w)
$creadPrec :: forall (w :: Nat). ReadPrec (BV w)
readList :: ReadS [BV w]
$creadList :: forall (w :: Nat). ReadS [BV w]
readsPrec :: Int -> ReadS (BV w)
$creadsPrec :: forall (w :: Nat). Int -> ReadS (BV w)
Read
           , BV w -> BV w -> Bool
(BV w -> BV w -> Bool) -> (BV w -> BV w -> Bool) -> Eq (BV w)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (w :: Nat). BV w -> BV w -> Bool
/= :: BV w -> BV w -> Bool
$c/= :: forall (w :: Nat). BV w -> BV w -> Bool
== :: BV w -> BV w -> Bool
$c== :: forall (w :: Nat). BV w -> BV w -> Bool
Eq
           , Ord -- ^ Uses an unsigned ordering, but 'ule' and 'ult' are
                 -- preferred. We provide this instance to allow the use of 'BV'
                 -- in situations where an arbitrary ordering is required (e.g.,
                 -- as the keys in a map)
           , BV w -> Q Exp
BV w -> Q (TExp (BV w))
(BV w -> Q Exp) -> (BV w -> Q (TExp (BV w))) -> Lift (BV w)
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
forall (w :: Nat). BV w -> Q Exp
forall (w :: Nat). BV w -> Q (TExp (BV w))
liftTyped :: BV w -> Q (TExp (BV w))
$cliftTyped :: forall (w :: Nat). BV w -> Q (TExp (BV w))
lift :: BV w -> Q Exp
$clift :: forall (w :: Nat). BV w -> Q Exp
Lift)

instance ShowF BV

instance EqF BV where
  BV Integer
bv eqF :: BV a -> BV a -> Bool
`eqF` BV Integer
bv' = Integer
bv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
bv'

instance Hashable (BV w) where
  hashWithSalt :: Int -> BV w -> Int
hashWithSalt Int
salt (BV Integer
i) = Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt Integer
i

----------------------------------------
-- BV construction
-- | Internal function for masking the input integer *without*
-- checking that the width is representable as an 'Int'. We use this
-- instead of 'mkBV' whenever we already have some guarantee that the
-- width is legal.
mkBV' :: NatRepr w -> Integer -> BV w
mkBV' :: NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
x = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
P.toUnsigned NatRepr w
w Integer
x)

-- | Construct a bitvector with a particular width, where the width is
-- provided as an explicit `NatRepr` argument. The input 'Integer',
-- whether positive or negative, is silently truncated to fit into the
-- number of bits demanded by the return type. The width cannot be
-- arbitrarily large; it must be representable as an 'Int'.
--
-- >>> mkBV (knownNat @4) 10
-- BV 10
-- >>> mkBV (knownNat @2) 10
-- BV 2
-- >>> mkBV (knownNat @4) (-2)
-- BV 14
mkBV :: NatRepr w
     -- ^ Desired bitvector width
     -> Integer
     -- ^ Integer value to truncate to bitvector width
     -> BV w
mkBV :: NatRepr w -> Integer -> BV w
mkBV NatRepr w
w Integer
x = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
x

-- | Return 'Nothing' if the unsigned 'Integer' does not fit in the
-- required number of bits, otherwise return the input.
checkUnsigned :: NatRepr w
              -> Integer
              -> Maybe Integer
checkUnsigned :: NatRepr w -> Integer -> Maybe Integer
checkUnsigned NatRepr w
w Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w
  then Maybe Integer
forall a. Maybe a
Nothing
  else Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i

-- | Like 'mkBV', but returns 'Nothing' if unsigned input integer cannot be
-- represented in @w@ bits.
mkBVUnsigned :: NatRepr w
             -- ^ Desired bitvector width
             -> Integer
             -- ^ Integer value
             -> Maybe (BV w)
mkBVUnsigned :: NatRepr w -> Integer -> Maybe (BV w)
mkBVUnsigned NatRepr w
w Integer
x = NatRepr w -> Maybe (BV w) -> Maybe (BV w)
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (Maybe (BV w) -> Maybe (BV w)) -> Maybe (BV w) -> Maybe (BV w)
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> Maybe Integer -> Maybe (BV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> Integer -> Maybe Integer
forall (w :: Nat). NatRepr w -> Integer -> Maybe Integer
checkUnsigned NatRepr w
w Integer
x

-- | Return 'Nothing if the signed 'Integer' does not fit in the
-- required number of bits, otherwise return an unsigned positive
-- integer that fits in @w@ bits.
signedToUnsigned :: 1 <= w => NatRepr w
                 -- ^ Width of output
                 -> Integer
                 -> Maybe Integer
signedToUnsigned :: NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w Bool -> Bool -> Bool
|| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w
  then Maybe Integer
forall a. Maybe a
Nothing
  else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
i

-- | Like 'mkBV', but returns 'Nothing' if signed input integer cannot
-- be represented in @w@ bits.
mkBVSigned :: 1 <= w => NatRepr w
              -- ^ Desired bitvector width
           -> Integer
           -- ^ Integer value
           -> Maybe (BV w)
mkBVSigned :: NatRepr w -> Integer -> Maybe (BV w)
mkBVSigned NatRepr w
w Integer
x = NatRepr w -> Maybe (BV w) -> Maybe (BV w)
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (Maybe (BV w) -> Maybe (BV w)) -> Maybe (BV w) -> Maybe (BV w)
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> Maybe Integer -> Maybe (BV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> Integer -> Maybe Integer
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w Integer
x

-- | The zero bitvector of any width.
zero :: NatRepr w -> BV w
zero :: NatRepr w -> BV w
zero NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | The bitvector with value 1, of any positive width.
one :: 1 <= w => NatRepr w -> BV w
one :: NatRepr w -> BV w
one NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
1

-- | The bitvector whose value is its own width, of any width.
width :: NatRepr w -> BV w
width :: NatRepr w -> BV w
width NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w)

-- | The minimum unsigned value for bitvector with given width (always 0).
minUnsigned :: NatRepr w -> BV w
minUnsigned :: NatRepr w -> BV w
minUnsigned NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | The maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> BV w
maxUnsigned :: NatRepr w -> BV w
maxUnsigned NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w)

-- | The minimum value for bitvector in two's complement with given width.
minSigned :: 1 <= w => NatRepr w -> BV w
minSigned :: NatRepr w -> BV w
minSigned NatRepr w
w = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
w (NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w)

-- | The maximum value for bitvector in two's complement with given width.
maxSigned :: 1 <= w => NatRepr w -> BV w
maxSigned :: NatRepr w -> BV w
maxSigned NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w)

-- | @unsignedClamp w i@ rounds @i@ to the nearest value between @0@
-- and @2^w - 1@ (inclusive).
unsignedClamp :: NatRepr w -> Integer -> BV w
unsignedClamp :: NatRepr w -> Integer -> BV w
unsignedClamp NatRepr w
w Integer
x = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$
  if | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w -> Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w)
     | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w -> Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w)
     | Bool
otherwise -> Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
x

-- | @signedClamp w i@ rounds @i@ to the nearest value between
-- @-2^(w-1)@ and @2^(w-1) - 1@ (inclusive).
signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w
signedClamp :: NatRepr w -> Integer -> BV w
signedClamp NatRepr w
w Integer
x = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$
  if | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w -> NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w)
     | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w -> Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w)
     | Bool
otherwise -> NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
x

----------------------------------------
-- Construction from fixed-width data types

-- | Construct a 'BV' from a 'Bool'.
bool :: Bool -> BV 1
bool :: Bool -> BV 1
bool Bool
True = Integer -> BV 1
forall (w :: Nat). Integer -> BV w
BV Integer
1
bool Bool
False = Integer -> BV 1
forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | Construct a 'BV' from a 'Word8'.
word8 :: Word8 -> BV 8
word8 :: Word8 -> BV 8
word8 = Integer -> BV 8
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV 8) -> (Word8 -> Integer) -> Word8 -> BV 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word16'.
word16 :: Word16 -> BV 16
word16 :: Word16 -> BV 16
word16 = Integer -> BV 16
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV 16) -> (Word16 -> Integer) -> Word16 -> BV 16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word32'.
word32 :: Word32 -> BV 32
word32 :: Word32 -> BV 32
word32 = Integer -> BV 32
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV 32) -> (Word32 -> Integer) -> Word32 -> BV 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word64'.
word64 :: Word64 -> BV 64
word64 :: Word64 -> BV 64
word64 = Integer -> BV 64
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV 64) -> (Word64 -> Integer) -> Word64 -> BV 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from an 'Int8'.
int8 :: Int8 -> BV 8
int8 :: Int8 -> BV 8
int8 = Word8 -> BV 8
word8 (Word8 -> BV 8) -> (Int8 -> Word8) -> Int8 -> BV 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int8 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int8 -> Word8)

-- | Construct a 'BV' from an 'Int16'.
int16 :: Int16 -> BV 16
int16 :: Int16 -> BV 16
int16 = Word16 -> BV 16
word16 (Word16 -> BV 16) -> (Int16 -> Word16) -> Int16 -> BV 16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int16 -> Word16)

-- | Construct a 'BV' from an 'Int32'.
int32 :: Int32 -> BV 32
int32 :: Int32 -> BV 32
int32 = Word32 -> BV 32
word32 (Word32 -> BV 32) -> (Int32 -> Word32) -> Int32 -> BV 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int32 -> Word32)

-- | Construct a 'BV' from an 'Int64'.
int64 :: Int64 -> BV 64
int64 :: Int64 -> BV 64
int64 = Word64 -> BV 64
word64 (Word64 -> BV 64) -> (Int64 -> Word64) -> Int64 -> BV 64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int64 -> Word64)

-- | Construct a 'BV' from a list of bits, in big endian order (bits
-- with lower value index in the list are mapped to higher order bits
-- in the output bitvector). Return the resulting 'BV' along with its
-- width.
--
-- >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
-- (2,BV 2)
bitsBE :: [Bool] -> Pair NatRepr BV
bitsBE :: [Bool] -> Pair NatRepr BV
bitsBE [Bool]
bs = case Natural -> Some NatRepr
mkNatRepr (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger ([Bool] -> Integer
forall i a. Num i => [a] -> i
genericLength [Bool]
bs)) of
  Some NatRepr x
w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w (Pair NatRepr BV -> Pair NatRepr BV)
-> Pair NatRepr BV -> Pair NatRepr BV
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> Pair NatRepr BV
forall k (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (Integer -> BV x
forall (w :: Nat). Integer -> BV w
BV ([Bool] -> Integer
forall b. Bits b => [Bool] -> b
B.fromListBE [Bool]
bs))

-- | Construct a 'BV' from a list of bits, in little endian order
-- (bits with lower value index in the list are mapped to lower order
-- bits in the output bitvector). Return the resulting 'BV' along
-- with its width.
--
-- >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
-- (2,BV 1)
bitsLE :: [Bool] -> Pair NatRepr BV
bitsLE :: [Bool] -> Pair NatRepr BV
bitsLE [Bool]
bs = case Natural -> Some NatRepr
mkNatRepr (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger ([Bool] -> Integer
forall i a. Num i => [a] -> i
genericLength [Bool]
bs)) of
  Some NatRepr x
w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w (Pair NatRepr BV -> Pair NatRepr BV)
-> Pair NatRepr BV -> Pair NatRepr BV
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> Pair NatRepr BV
forall k (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (Integer -> BV x
forall (w :: Nat). Integer -> BV w
BV ([Bool] -> Integer
forall b. Bits b => [Bool] -> b
B.fromListLE [Bool]
bs))

-- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer'
-- with @8*n@ bits. This function uses a balanced binary fold to
-- achieve /O(n log n)/ total memory allocation and run-time, in
-- contrast to the /O(n^2)/ that would be required by a naive
-- left-fold.
bytestringToIntegerBE :: BS.ByteString -> Integer
bytestringToIntegerBE :: ByteString -> Integer
bytestringToIntegerBE ByteString
bs
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftL` (Int
l2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..|. Integer
x2
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    l2 :: Int
l2 = Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l1
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
bytestringToIntegerBE ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
bytestringToIntegerBE ByteString
bs2

bytestringToIntegerLE :: BS.ByteString -> Integer
bytestringToIntegerLE :: ByteString -> Integer
bytestringToIntegerLE ByteString
bs
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x2 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftL` (Int
l1 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..|. Integer
x1
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
bytestringToIntegerLE ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
bytestringToIntegerLE ByteString
bs2

-- | Construct a 'BV' from a big-endian bytestring.
--
-- >>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
-- (24,BV 257)
bytestringBE :: BS.ByteString -> Pair NatRepr BV
bytestringBE :: ByteString -> Pair NatRepr BV
bytestringBE ByteString
bs = case Natural -> Some NatRepr
mkNatRepr (Natural
8Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
*Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)) of
  Some NatRepr x
w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w (Pair NatRepr BV -> Pair NatRepr BV)
-> Pair NatRepr BV -> Pair NatRepr BV
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> Pair NatRepr BV
forall k (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (Integer -> BV x
forall (w :: Nat). Integer -> BV w
BV (ByteString -> Integer
bytestringToIntegerBE ByteString
bs))

-- | Construct a 'BV' from a little-endian bytestring.
--
-- >>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
-- (24,BV 65792)
bytestringLE :: BS.ByteString -> Pair NatRepr BV
bytestringLE :: ByteString -> Pair NatRepr BV
bytestringLE ByteString
bs = case Natural -> Some NatRepr
mkNatRepr (Natural
8Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
*Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)) of
  Some NatRepr x
w -> NatRepr x -> Pair NatRepr BV -> Pair NatRepr BV
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w (Pair NatRepr BV -> Pair NatRepr BV)
-> Pair NatRepr BV -> Pair NatRepr BV
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> Pair NatRepr BV
forall k (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (Integer -> BV x
forall (w :: Nat). Integer -> BV w
BV (ByteString -> Integer
bytestringToIntegerLE ByteString
bs))

-- | Construct a 'BV' from a list of bytes, in big endian order (bytes
-- with lower value index in the list are mapped to higher order bytes
-- in the output bitvector).
--
-- >>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)
-- (24,BV 257)
bytesBE :: [Word8] -> Pair NatRepr BV
bytesBE :: [Word8] -> Pair NatRepr BV
bytesBE = ByteString -> Pair NatRepr BV
bytestringBE (ByteString -> Pair NatRepr BV)
-> ([Word8] -> ByteString) -> [Word8] -> Pair NatRepr BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack

-- | Construct a 'BV' from a list of bytes, in little endian order
-- (bytes with lower value index in the list are mapped to lower
-- order bytes in the output bitvector).
--
-- >>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)
-- (24,BV 65792)
bytesLE :: [Word8] -> Pair NatRepr BV
bytesLE :: [Word8] -> Pair NatRepr BV
bytesLE = ByteString -> Pair NatRepr BV
bytestringLE (ByteString -> Pair NatRepr BV)
-> ([Word8] -> ByteString) -> [Word8] -> Pair NatRepr BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack

----------------------------------------
-- BitVector -> Integer functions

-- | Unsigned interpretation of a bitvector as a positive Integer.
asUnsigned :: BV w -> Integer
asUnsigned :: BV w -> Integer
asUnsigned (BV Integer
x) = Integer
x

-- | Signed interpretation of a bitvector as an Integer.
asSigned :: (1 <= w) => NatRepr w -> BV w -> Integer
asSigned :: NatRepr w -> BV w -> Integer
asSigned NatRepr w
w (BV Integer
x) =
  -- NB, fromNatural is OK here because we maintain the invariant that
  --  any existing BV value has a representable width
  let wInt :: Int
wInt = Natural -> Int
fromNatural (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w) in
  if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Int
wInt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  then Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Int -> Integer
forall a. Bits a => Int -> a
B.bit Int
wInt
  else Integer
x

-- | Unsigned interpretation of a bitvector as a Natural.
asNatural :: BV w -> Natural
asNatural :: BV w -> Natural
asNatural = (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger :: Integer -> Natural) (Integer -> Natural) -> (BV w -> Integer) -> BV w -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned

-- | Convert a bitvector to a list of bits, in big endian order
-- (higher order bits in the bitvector are mapped to lower indices in
-- the output list).
--
-- >>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
-- [False,True,True,False,True]
asBitsBE :: NatRepr w -> BV w -> [Bool]
asBitsBE :: NatRepr w -> BV w -> [Bool]
asBitsBE NatRepr w
w BV w
bv = [ Natural -> BV w -> Bool
forall (w :: Nat). Natural -> BV w -> Bool
testBit' Natural
i BV w
bv | Natural
i <- Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> [Integer] -> [Natural]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
wi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1, Integer
wi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
2 .. Integer
0] ]
  where wi :: Integer
wi = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w

-- | Convert a bitvector to a list of bits, in little endian order
-- (lower order bits in the bitvector are mapped to lower indices in
-- the output list).
--
-- >>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
-- [True,False,True,True,False]
asBitsLE :: NatRepr w -> BV w -> [Bool]
asBitsLE :: NatRepr w -> BV w -> [Bool]
asBitsLE NatRepr w
w BV w
bv = [ Natural -> BV w -> Bool
forall (w :: Nat). Natural -> BV w -> Bool
testBit' Natural
i BV w
bv | Natural
i <- Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> [Integer] -> [Natural]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 .. Integer
wi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1] ]
  where wi :: Integer
wi = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w

integerToBytesBE :: Natural
                 -- ^ number of bytes
                 -> Integer
                 -> [Word8]
integerToBytesBE :: Natural -> Integer -> [Word8]
integerToBytesBE Natural
n Integer
x =
  [ Integer -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` (Int
8Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
ix)) | Int
ix <- [Int
niInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int
niInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2 .. Int
0] ]
  where ni :: Int
ni = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n

integerToBytesLE :: Natural
                 -- ^ number of bytes
                 -> Integer
                 -> [Word8]
integerToBytesLE :: Natural -> Integer -> [Word8]
integerToBytesLE Natural
n Integer
x =
  [ Integer -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` (Int
8Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
ix)) | Int
ix <- [Int
0 .. Int
niInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
  where ni :: Int
ni = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n

-- | Convert a bitvector to a list of bytes, in big endian order
-- (higher order bytes in the bitvector are mapped to lower indices in
-- the output list). Return 'Nothing' if the width is not a multiple
-- of 8.
--
-- >>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
-- Just [170,187,204,221]
asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]
asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]
asBytesBE NatRepr w
w (BV Integer
x)
  | NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
8 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 = [Word8] -> Maybe [Word8]
forall a. a -> Maybe a
Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> [Word8]
integerToBytesBE (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
8) Integer
x
  | Bool
otherwise = Maybe [Word8]
forall a. Maybe a
Nothing

-- | Convert a bitvector to a list of bytes, in little endian order
-- (lower order bytes in the bitvector are mapped to lower indices in
-- the output list). Return 'Nothing' if the width is not a multiple
-- of 8.
--
-- >>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
-- Just [221,204,187,170]
asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]
asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]
asBytesLE NatRepr w
w (BV Integer
x)
  | NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
8 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 = [Word8] -> Maybe [Word8]
forall a. a -> Maybe a
Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> [Word8]
integerToBytesLE (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
8) Integer
x
  | Bool
otherwise = Maybe [Word8]
forall a. Maybe a
Nothing

-- | 'asBytesBE', but for bytestrings.
asBytestringBE :: NatRepr w -> BV w -> Maybe BS.ByteString
asBytestringBE :: NatRepr w -> BV w -> Maybe ByteString
asBytestringBE NatRepr w
w BV w
bv = [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> Maybe [Word8] -> Maybe ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> BV w -> Maybe [Word8]
forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesBE NatRepr w
w BV w
bv

-- | 'asBytesLE', but for bytestrings.
asBytestringLE :: NatRepr w -> BV w -> Maybe BS.ByteString
asBytestringLE :: NatRepr w -> BV w -> Maybe ByteString
asBytestringLE NatRepr w
w BV w
bv = [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> Maybe [Word8] -> Maybe ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> BV w -> Maybe [Word8]
forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesLE NatRepr w
w BV w
bv

----------------------------------------
-- BV w operations (fixed width)

-- | Bitwise and.
and :: BV w -> BV w -> BV w
and :: BV w -> BV w -> BV w
and (BV Integer
x) (BV Integer
y) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..&. Integer
y)

-- | Bitwise or.
or :: BV w -> BV w -> BV w
or :: BV w -> BV w -> BV w
or (BV Integer
x) (BV Integer
y) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..|. Integer
y)

-- | Bitwise xor.
xor :: BV w -> BV w -> BV w
xor :: BV w -> BV w -> BV w
xor (BV Integer
x) (BV Integer
y) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`B.xor` Integer
y)

-- | Bitwise complement (flip every bit).
complement :: NatRepr w -> BV w -> BV w
complement :: NatRepr w -> BV w -> BV w
complement NatRepr w
w (BV Integer
x) = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer -> Integer
forall a. Bits a => a -> a
B.complement Integer
x)


-- | Clamp shift amounts to the word width and
--   coerce to an @Int@
shiftAmount :: NatRepr w -> Natural -> Int
shiftAmount :: NatRepr w -> Natural -> Int
shiftAmount NatRepr w
w Natural
shf = Natural -> Int
fromNatural (Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
min (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w) Natural
shf)

-- | Left shift by positive 'Natural'.
shl :: NatRepr w -> BV w -> Natural -> BV w
shl :: NatRepr w -> BV w -> Natural -> BV w
shl NatRepr w
w (BV Integer
x) Natural
shf = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftL` NatRepr w -> Natural -> Int
forall (w :: Nat). NatRepr w -> Natural -> Int
shiftAmount NatRepr w
w Natural
shf)

-- | Right arithmetic shift by positive 'Natural'.
ashr :: (1 <= w) => NatRepr w -> BV w -> Natural -> BV w
ashr :: NatRepr w -> BV w -> Natural -> BV w
ashr NatRepr w
w BV w
bv Natural
shf = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` NatRepr w -> Natural -> Int
forall (w :: Nat). NatRepr w -> Natural -> Int
shiftAmount NatRepr w
w Natural
shf)

-- | Right logical shift by positive 'Natural'.
lshr :: NatRepr w -> BV w -> Natural -> BV w
lshr :: NatRepr w -> BV w -> Natural -> BV w
lshr NatRepr w
w (BV Integer
x) Natural
shf =
  -- Shift right (logical by default since the value is positive). No
  -- need to truncate bits, since the result is guaranteed to occupy
  -- no more bits than the input.
  Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` NatRepr w -> Natural -> Int
forall (w :: Nat). NatRepr w -> Natural -> Int
shiftAmount NatRepr w
w Natural
shf)

-- | Bitwise rotate left.
rotateL :: NatRepr w -> BV w -> Natural -> BV w
rotateL :: NatRepr w -> BV w -> Natural -> BV w
rotateL NatRepr w
w BV w
bv Natural
rot' = BV w
leftChunk BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
`or` BV w
rightChunk
  where rot :: Natural
rot = if Natural
wNatural Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 then Natural
0 else Natural
rot' Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
wNatural
        leftChunk :: BV w
leftChunk = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
shl NatRepr w
w BV w
bv Natural
rot
        rightChunk :: BV w
rightChunk = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
lshr NatRepr w
w BV w
bv (Natural
wNatural Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
rot)
        wNatural :: Natural
wNatural = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w

-- | Bitwise rotate right.
rotateR :: NatRepr w -> BV w -> Natural -> BV w
rotateR :: NatRepr w -> BV w -> Natural -> BV w
rotateR NatRepr w
w BV w
bv Natural
rot' = BV w
leftChunk BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
`or` BV w
rightChunk
  where rot :: Natural
rot = if Natural
wNatural Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 then Natural
0 else Natural
rot' Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
wNatural
        rightChunk :: BV w
rightChunk = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
lshr NatRepr w
w BV w
bv Natural
rot
        leftChunk :: BV w
leftChunk = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
shl NatRepr w
w BV w
bv (Natural
wNatural Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
rot)
        wNatural :: Natural
wNatural = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w

-- | The 'BV' that has a particular bit set, and is 0 everywhere
-- else.
bit :: ix+1 <= w
    => NatRepr w
    -- ^ Desired output width
    -> NatRepr ix
    -- ^ Index of bit to set
    -> BV w
bit :: NatRepr w -> NatRepr ix -> BV w
bit NatRepr w
w NatRepr ix
ix =
  NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$
    -- NB fromNatural is OK here because of the (ix+1<w) constraint
    Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix)))

-- | Like 'bit', but without the requirement that the index bit refers
-- to an actual bit in the output 'BV'. If it is out of range, just
-- silently return the zero bitvector.
bit' :: NatRepr w
     -- ^ Desired output width
     -> Natural
     -- ^ Index of bit to set
     -> BV w
bit' :: NatRepr w -> Natural -> BV w
bit' NatRepr w
w Natural
ix
  | Natural
ix Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w = NatRepr w -> BV w -> BV w
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural Natural
ix))
  | Bool
otherwise = NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
zero NatRepr w
w

-- | @setBit bv ix@ is the same as @or bv (bit knownNat ix)@.
setBit :: ix+1 <= w
       => NatRepr ix
       -- ^ Index of bit to set
       -> BV w
       -- ^ Original bitvector
       -> BV w
setBit :: NatRepr ix -> BV w -> BV w
setBit NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of the (ix+1 <= w) constraint
  BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
or BV w
bv (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix))))

-- | Like 'setBit', but without the requirement that the index bit
-- refers to an actual bit in the input 'BV'. If it is out of range,
-- just silently return the original input.
setBit' :: NatRepr w
        -- ^ Desired output width
        -> Natural
        -- ^ Index of bit to set
        -> BV w
        -- ^ Original bitvector
        -> BV w
setBit' :: NatRepr w -> Natural -> BV w -> BV w
setBit' NatRepr w
w Natural
ix BV w
bv
  | Natural
ix Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w = BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
or BV w
bv (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural Natural
ix)))
  | Bool
otherwise = BV w
bv

-- | @clearBit w bv ix@ is the same as @and bv (complement (bit w ix))@.
clearBit :: ix+1 <= w
         => NatRepr w
         -- ^ Desired output width
         -> NatRepr ix
         -- ^ Index of bit to clear
         -> BV w
         -- ^ Original bitvector
         -> BV w
clearBit :: NatRepr w -> NatRepr ix -> BV w -> BV w
clearBit NatRepr w
w NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of the (ix+1<=w) constraint
  BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
and BV w
bv (NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
complement NatRepr w
w (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix)))))


-- | Like 'clearBit', but without the requirement that the index bit
-- refers to an actual bit in the input 'BV'. If it is out of range,
-- just silently return the original input.
clearBit' :: NatRepr w
          -- ^ Desired output width
          -> Natural
          -- ^ Index of bit to clear
          -> BV w
          -- ^ Original bitvector
          -> BV w
clearBit' :: NatRepr w -> Natural -> BV w -> BV w
clearBit' NatRepr w
w Natural
ix BV w
bv
  | Natural
ix Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w = BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
and BV w
bv (NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
complement NatRepr w
w (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural Natural
ix))))
  | Bool
otherwise = BV w
bv

-- | @complementBit bv ix@ is the same as @xor bv (bit knownNat ix)@.
complementBit :: ix+1 <= w
              => NatRepr ix
              -- ^ Index of bit to flip
              -> BV w
              -- ^ Original bitvector
              -> BV w
complementBit :: NatRepr ix -> BV w -> BV w
complementBit NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of (ix+1 <= w) constraint
  BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
xor BV w
bv (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix))))

-- | Like 'complementBit', but without the requirement that the index
-- bit refers to an actual bit in the input 'BV'. If it is out of
-- range, just silently return the original input.
complementBit' :: NatRepr w
               -- ^ Desired output width
               -> Natural
               -- ^ Index of bit to flip
               -> BV w
               -- ^ Original bitvector
               -> BV w
complementBit' :: NatRepr w -> Natural -> BV w -> BV w
complementBit' NatRepr w
w Natural
ix BV w
bv
  | Natural
ix Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w = BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
xor BV w
bv (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural Natural
ix)))
  | Bool
otherwise = BV w
bv

-- | Test if a particular bit is set.
testBit :: ix+1 <= w => NatRepr ix -> BV w -> Bool
testBit :: NatRepr ix -> BV w -> Bool
testBit NatRepr ix
ix (BV Integer
x) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix))

-- | Like 'testBit', but takes a 'Natural' for the bit index. If the
-- index is out of bounds, return 'False'.
testBit' :: Natural -> BV w -> Bool
testBit' :: Natural -> BV w -> Bool
testBit' Natural
ix (BV Integer
x)
  -- NB, If the index is larger than the maximum representable 'Int',
  -- this function should be 'False' by construction of 'BV'.
  | Natural
ix Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int) = Bool
False
  | Bool
otherwise = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Natural -> Int
fromNatural Natural
ix)

-- | Get the number of 1 bits in a 'BV'.
popCount :: BV w -> BV w
popCount :: BV w -> BV w
popCount (BV Integer
x) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Int
forall a. Bits a => a -> Int
B.popCount Integer
x))

-- | Count trailing zeros in a 'BV'.
ctz :: NatRepr w -> BV w -> BV w
ctz :: NatRepr w -> BV w -> BV w
ctz NatRepr w
w (BV Integer
x) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> Integer
go Integer
0)
  where go :: Integer -> Integer
go !Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w Bool -> Bool -> Bool
&&
                Bool -> Bool
not (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)) = Integer -> Integer
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
              | Bool
otherwise = Integer
i

-- | Count leading zeros in a 'BV'.
clz :: NatRepr w -> BV w -> BV w
clz :: NatRepr w -> BV w -> BV w
clz NatRepr w
w (BV Integer
x) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> Integer
go Integer
0)
 where go :: Integer -> Integer
go !Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w Bool -> Bool -> Bool
&&
               Bool -> Bool
not (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))) =
                 Integer -> Integer
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
             | Bool
otherwise = Integer
i

-- | Truncate a bitvector to a particular width given at runtime,
-- while keeping the type-level width constant.
truncBits :: Natural -> BV w -> BV w
truncBits :: Natural -> BV w -> BV w
truncBits Natural
b (BV Integer
x) = Natural -> BV w -> BV w
forall a. Natural -> a -> a
checkNatural Natural
b (BV w -> BV w) -> BV w -> BV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..&. (Int -> Integer
forall a. Bits a => Int -> a
B.bit (Natural -> Int
fromNatural Natural
b) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

----------------------------------------
-- BV w arithmetic operations (fixed width)

-- | Bitvector add.
add :: NatRepr w -> BV w -> BV w -> BV w
add :: NatRepr w -> BV w -> BV w -> BV w
add NatRepr w
w (BV Integer
x) (BV Integer
y) = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)

-- | Bitvector subtract.
sub :: NatRepr w -> BV w -> BV w -> BV w
sub :: NatRepr w -> BV w -> BV w -> BV w
sub NatRepr w
w (BV Integer
x) (BV Integer
y) = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
y)

-- | Bitvector multiply.
mul :: NatRepr w -> BV w -> BV w -> BV w
mul :: NatRepr w -> BV w -> BV w -> BV w
mul NatRepr w
w (BV Integer
x) (BV Integer
y) = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y)

-- | Bitvector division (unsigned). Rounds to zero. Division by zero
-- yields a runtime error.
uquot :: BV w -> BV w -> BV w
uquot :: BV w -> BV w -> BV w
uquot (BV Integer
x) (BV Integer
y) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)

-- | Bitvector remainder after division (unsigned), when rounded to
-- zero. Division by zero yields a runtime error.
urem :: BV w -> BV w -> BV w
urem :: BV w -> BV w -> BV w
urem (BV Integer
x) (BV Integer
y) = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)

-- | 'uquot' and 'urem' returned as a pair.
uquotRem :: BV w -> BV w -> (BV w, BV w)
uquotRem :: BV w -> BV w -> (BV w, BV w)
uquotRem BV w
bv1 BV w
bv2 = (BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
uquot BV w
bv1 BV w
bv2, BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
urem BV w
bv1 BV w
bv2)

-- | Bitvector division (signed). Rounds to zero. Division by zero
-- yields a runtime error.
squot :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
squot :: NatRepr w -> BV w -> BV w -> BV w
squot NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
  where x :: Integer
x = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Bitvector remainder after division (signed), when rounded to
-- zero. Division by zero yields a runtime error.
srem :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
srem :: NatRepr w -> BV w -> BV w -> BV w
srem NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
  where x :: Integer
x = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | 'squot' and 'srem' returned as a pair.
squotRem :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
squotRem :: NatRepr w -> BV w -> BV w -> (BV w, BV w)
squotRem NatRepr w
w BV w
bv1 BV w
bv2 = (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
squot NatRepr w
w BV w
bv1 BV w
bv2, NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
srem NatRepr w
w BV w
bv1 BV w
bv2)

-- | Bitvector division (signed). Rounds to negative infinity. Division
-- by zero yields a runtime error.
sdiv :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
sdiv :: NatRepr w -> BV w -> BV w -> BV w
sdiv NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y)
  where x :: Integer
x = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Bitvector remainder after division (signed), when rounded to
-- negative infinity. Division by zero yields a runtime error.
smod :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smod :: NatRepr w -> BV w -> BV w -> BV w
smod NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
y)
  where x :: Integer
x = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | 'sdiv' and 'smod' returned as a pair.
sdivMod :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
sdivMod :: NatRepr w -> BV w -> BV w -> (BV w, BV w)
sdivMod NatRepr w
w BV w
bv1 BV w
bv2 = (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
sdiv NatRepr w
w BV w
bv1 BV w
bv2, NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smod NatRepr w
w BV w
bv1 BV w
bv2)

-- | Bitvector absolute value.  Returns the 2's complement
--   magnitude of the bitvector.
abs :: (1 <= w) => NatRepr w -> BV w -> BV w
abs :: NatRepr w -> BV w -> BV w
abs NatRepr w
w BV w
bv = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer -> Integer
forall a. Num a => a -> a
Prelude.abs (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv))

-- | 2's complement bitvector negation.
negate :: NatRepr w -> BV w -> BV w
negate :: NatRepr w -> BV w -> BV w
negate NatRepr w
w (BV Integer
x) = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (-Integer
x)

-- | Get the sign bit as a 'BV'.
signBit :: 1 <= w => NatRepr w -> BV w -> BV w
signBit :: NatRepr w -> BV w -> BV w
signBit NatRepr w
w bv :: BV w
bv@(BV Integer
_) = NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
lshr NatRepr w
w BV w
bv (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
`and` Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
1

-- | Return 1 if positive, -1 if negative, and 0 if 0.
signum :: 1 <= w => NatRepr w -> BV w -> BV w
signum :: NatRepr w -> BV w -> BV w
signum NatRepr w
w BV w
bv = NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer -> Integer
forall a. Num a => a -> a
Prelude.signum (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv))

-- | Signed less than.
slt :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
slt :: NatRepr w -> BV w -> BV w -> Bool
slt NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Signed less than or equal.
sle :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
sle :: NatRepr w -> BV w -> BV w -> Bool
sle NatRepr w
w BV w
bv1 BV w
bv2 = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Unsigned less than.
ult :: BV w -> BV w -> Bool
ult :: BV w -> BV w -> Bool
ult BV w
bv1 BV w
bv2 = BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv2

-- | Unsigned less than or equal.
ule :: BV w -> BV w -> Bool
ule :: BV w -> BV w -> Bool
ule BV w
bv1 BV w
bv2 = BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv2

-- | Unsigned minimum of two bitvectors.
umin :: BV w -> BV w -> BV w
umin :: BV w -> BV w -> BV w
umin (BV Integer
x) (BV Integer
y) = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
y then Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
x else Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
y

-- | Unsigned maximum of two bitvectors.
umax :: BV w -> BV w -> BV w
umax :: BV w -> BV w -> BV w
umax (BV Integer
x) (BV Integer
y) = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
y then Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
y else Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV Integer
x

-- | Signed minimum of two bitvectors.
smin :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smin :: NatRepr w -> BV w -> BV w -> BV w
smin NatRepr w
w BV w
bv1 BV w
bv2 = if NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2 then BV w
bv1 else BV w
bv2

-- | Signed maximum of two bitvectors.
smax :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smax :: NatRepr w -> BV w -> BV w -> BV w
smax NatRepr w
w BV w
bv1 BV w
bv2 = if NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2 then BV w
bv2 else BV w
bv1

----------------------------------------
-- Width-changing operations

-- | Concatenate two bitvectors. The first argument gets placed in the
-- higher order bits.
--
-- >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
-- BV 6
-- >>> :type it
-- it :: BV 5
concat :: NatRepr w
       -- ^ Width of higher-order bits
       -> NatRepr w'
       -- ^ Width of lower-order bits
       -> BV w
       -- ^ Higher-order bits
       -> BV w'
       -- ^ Lower-order bits
       -> BV (w+w')
concat :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
concat NatRepr w
w NatRepr w'
w' (BV Integer
hi) (BV Integer
lo) = NatRepr (w + w') -> BV (w + w') -> BV (w + w')
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr (NatRepr w
w NatRepr w -> NatRepr w' -> NatRepr (w + w')
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr w'
w') (BV (w + w') -> BV (w + w')) -> BV (w + w') -> BV (w + w')
forall a b. (a -> b) -> a -> b
$
  Integer -> BV (w + w')
forall (w :: Nat). Integer -> BV w
BV ((Integer
hi Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftL` Natural -> Int
fromNatural (NatRepr w' -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w'
w')) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
B..|. Integer
lo)

-- | Slice out a smaller bitvector from a larger one.
--
-- >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
-- BV 3
-- >>> :type it
-- it :: BV 4
select :: ix + w' <= w
       => NatRepr ix
       -- ^ Index to start selecting from
       -> NatRepr w'
       -- ^ Desired output width
       -> BV w
       -- ^ Bitvector to select from
       -> BV w'
select :: NatRepr ix -> NatRepr w' -> BV w -> BV w'
select NatRepr ix
ix NatRepr w'
w' (BV Integer
x) = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w'
w' Integer
xShf
  -- NB fromNatural is OK because of (ix + w' <= w) constraint
  where xShf :: Integer
xShf = Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` Natural -> Int
fromNatural (NatRepr ix -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr ix
ix)

-- | Like 'select', but takes a 'Natural' as the index to start
-- selecting from. Neither the index nor the output width is checked
-- to ensure the resulting 'BV' lies entirely within the bounds of the
-- original bitvector. Any bits "selected" from beyond the bounds of
-- the input bitvector will be 0.
--
-- >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
-- BV 6
-- >>> :type it
-- it :: BV 4
select' :: Natural
        -- ^ Index to start selecting from
        -> NatRepr w'
        -- ^ Desired output width
        -> BV w
        -- ^ Bitvector to select from
        -> BV w'
select' :: Natural -> NatRepr w' -> BV w -> BV w'
select' Natural
ix NatRepr w'
w' (BV Integer
x)
  | Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
ix Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`B.shiftR` Natural -> Int
fromNatural Natural
ix)
  | Bool
otherwise = NatRepr w' -> BV w'
forall (w :: Nat). NatRepr w -> BV w
zero NatRepr w'
w'

-- | Zero-extend a bitvector to one of strictly greater width.
--
-- >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
-- BV 13
-- >>> :type it
-- it :: BV 8
zext :: w + 1 <= w'
     => NatRepr w'
     -- ^ Desired output width
     -> BV w
     -- ^ Bitvector to extend
     -> BV w'
zext :: NatRepr w' -> BV w -> BV w'
zext NatRepr w'
w (BV Integer
x) = NatRepr w' -> BV w' -> BV w'
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w'
w (BV w' -> BV w') -> BV w' -> BV w'
forall a b. (a -> b) -> a -> b
$ Integer -> BV w'
forall (w :: Nat). Integer -> BV w
BV Integer
x

-- | Sign-extend a bitvector to one of strictly greater width.
sext :: (1 <= w, w + 1 <= w')
     => NatRepr w
     -- ^ Width of input bitvector
     -> NatRepr w'
     -- ^ Desired output width
     -> BV w
     -- ^ Bitvector to extend
     -> BV w'
sext :: NatRepr w -> NatRepr w' -> BV w -> BV w'
sext NatRepr w
w NatRepr w'
w' BV w
bv = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv)

-- | Truncate a bitvector to one of strictly smaller width.
trunc :: w' + 1 <= w
      => NatRepr w'
      -- ^ Desired output width
      -> BV w
      -- ^ Bitvector to truncate
      -> BV w'
trunc :: NatRepr w' -> BV w -> BV w'
trunc NatRepr w'
w' (BV Integer
x) = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w'
w' Integer
x

-- | Like 'trunc', but allows the input width to be greater than or
-- equal to the output width, in which case it just performs a zero
-- extension.
trunc' :: NatRepr w'
       -- ^ Desired output width
       -> BV w
       -- ^ Bitvector to truncate
       -> BV w'
trunc' :: NatRepr w' -> BV w -> BV w'
trunc' NatRepr w'
w' (BV Integer
x) = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' Integer
x
{-# DEPRECATED trunc' "Use zresize instead" #-}

-- | Resizes a bitvector. If @w' > w@, perform a zero extension.
zresize :: NatRepr w'
        -- ^ Desired output width
        -> BV w
        -- ^ Bitvector to resize
        -> BV w'
zresize :: NatRepr w' -> BV w -> BV w'
zresize NatRepr w'
w' (BV Integer
x) = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' Integer
x

-- | Resizes a bitvector. If @w' > w@, perform a signed extension.
sresize :: 1 <= w
        => NatRepr w
        -- ^ Width of input vector
        -> NatRepr w'
        -- ^ Desired output width
        -> BV w
        -- ^ Bitvector to resize
        -> BV w'
sresize :: NatRepr w -> NatRepr w' -> BV w -> BV w'
sresize NatRepr w
w NatRepr w'
w' BV w
bv = NatRepr w' -> Integer -> BV w'
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv)

-- | Wide multiply of two bitvectors.
mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w+w')
mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
mulWide NatRepr w
w NatRepr w'
w' (BV Integer
x) (BV Integer
y) = NatRepr (w + w') -> BV (w + w') -> BV (w + w')
forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr (NatRepr w
w NatRepr w -> NatRepr w' -> NatRepr (w + w')
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr w'
w') (BV (w + w') -> BV (w + w')) -> BV (w + w') -> BV (w + w')
forall a b. (a -> b) -> a -> b
$ Integer -> BV (w + w')
forall (w :: Nat). Integer -> BV w
BV (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y)

----------------------------------------
-- Enum functions

-- | Unsigned successor. @succUnsigned w (maxUnsigned w)@ returns 'Nothing'.
succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
succUnsigned NatRepr w
w (BV Integer
x) =
  if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w
  then Maybe (BV w)
forall a. Maybe a
Nothing
  else BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1))

-- | Signed successor. @succSigned w (maxSigned w)@ returns 'Nothing'.
succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
succSigned :: NatRepr w -> BV w -> Maybe (BV w)
succSigned NatRepr w
w (BV Integer
x) =
  if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w
  then Maybe (BV w)
forall a. Maybe a
Nothing
  else BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1))

-- | Unsigned predecessor. @predUnsigned w zero@ returns 'Nothing'.
predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
predUnsigned NatRepr w
w (BV Integer
x) =
  if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w
  then Maybe (BV w)
forall a. Maybe a
Nothing
  else BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just (Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))

-- | Signed predecessor. @predSigned w (minSigned w)@ returns 'Nothing'.
predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
predSigned :: NatRepr w -> BV w -> Maybe (BV w)
predSigned NatRepr w
w bv :: BV w
bv@(BV Integer
x) =
  if BV w
bv BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
minSigned NatRepr w
w
  then Maybe (BV w)
forall a. Maybe a
Nothing
  else BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))

-- | List of all unsigned bitvectors from a lower to an upper bound,
-- inclusive.
enumFromToUnsigned :: BV w
                   -- ^ Lower bound
                   -> BV w
                   -- ^ Upper bound
                   -> [BV w]
enumFromToUnsigned :: BV w -> BV w -> [BV w]
enumFromToUnsigned BV w
bv1 BV w
bv2 = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> [Integer] -> [BV w]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 .. BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv2]

-- | List of all signed bitvectors from a lower to an upper bound,
-- inclusive.
enumFromToSigned :: 1 <= w => NatRepr w
                 -> BV w
                 -- ^ Lower bound
                 -> BV w
                 -- ^ Upper bound
                 -> [BV w]
enumFromToSigned :: NatRepr w -> BV w -> BV w -> [BV w]
enumFromToSigned NatRepr w
w BV w
bv1 BV w
bv2 =
  Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> (Integer -> Integer) -> Integer -> BV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (Integer -> Maybe Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Integer -> Maybe Integer
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w (Integer -> BV w) -> [Integer] -> [BV w]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 .. NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2]

----------------------------------------
-- Generating random bitvectors

-- | Generates a bitvector uniformly distributed over all possible values for a
-- given width. (See 'System.Random.Stateful.uniformM').
uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)
uniformM :: NatRepr w -> g -> m (BV w)
uniformM NatRepr w
w g
g = Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> m Integer -> m (BV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> g -> m Integer
forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w, NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w) g
g

-- | Generates a bitvector uniformly distributed over the provided range
-- (interpreted as a range of /unsigned/ bitvectors), which is interpreted as
-- inclusive in the lower and upper bound. (See
-- 'System.Random.Stateful.uniformRM').
uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)
uUniformRM :: (BV w, BV w) -> g -> m (BV w)
uUniformRM (BV w
lo, BV w
hi) g
g =
  let loI :: Integer
loI = BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
lo
      hiI :: Integer
hiI = BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
hi
  in Integer -> BV w
forall (w :: Nat). Integer -> BV w
BV (Integer -> BV w) -> m Integer -> m (BV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> g -> m Integer
forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (Integer
loI, Integer
hiI) g
g

-- | Generates a bitvector uniformly distributed over the provided range
-- (interpreted as a range of /signed/ bitvectors), which is interpreted as
-- inclusive in the lower and upper bound. (See
-- 'System.Random.Stateful.uniformRM').
sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)
sUniformRM :: NatRepr w -> (BV w, BV w) -> g -> m (BV w)
sUniformRM NatRepr w
w (BV w
lo, BV w
hi) g
g =
  let loI :: Integer
loI = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
lo
      hiI :: Integer
hiI = NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
hi
  in NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
w (Integer -> BV w) -> m Integer -> m (BV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> g -> m Integer
forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (Integer
loI, Integer
hiI) g
g

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

-- | Pretty print in hex
ppHex :: NatRepr w -> BV w -> String
ppHex :: NatRepr w -> BV w -> String
ppHex NatRepr w
w (BV Integer
x) = String
"0x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
N.showHex Integer
x String
"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in binary
ppBin :: NatRepr w -> BV w -> String
ppBin :: NatRepr w -> BV w -> String
ppBin NatRepr w
w (BV Integer
x) = String
"0b" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> (Int -> Char) -> Integer -> String -> String
forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
N.showIntAtBase Integer
2 Int -> Char
intToDigit Integer
x String
"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in octal
ppOct :: NatRepr w -> BV w -> String
ppOct :: NatRepr w -> BV w -> String
ppOct NatRepr w
w (BV Integer
x) = String
"0o" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
N.showOct Integer
x String
"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in decimal
ppDec :: NatRepr w -> BV w -> String
ppDec :: NatRepr w -> BV w -> String
ppDec NatRepr w
w (BV Integer
x) = Integer -> String
forall a. Show a => a -> String
show Integer
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

ppWidth :: NatRepr w -> String
ppWidth :: NatRepr w -> String
ppWidth NatRepr w
w = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"