{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.BitVector.Sized.Signed
( SignedBV(..)
, mkSignedBV
) where
import Control.DeepSeq (NFData)
import Data.BitVector.Sized (BV, mkBV)
import qualified Data.BitVector.Sized.Internal as BV
import Data.BitVector.Sized.Panic (panic)
import Data.Parameterized.Classes (Hashable(..))
import Data.Parameterized.NatRepr
import Data.Bits (Bits(..), FiniteBits(..))
import Data.Ix
import GHC.Generics
import GHC.TypeLits (KnownNat)
import Language.Haskell.TH.Lift (Lift)
import Numeric.Natural (Natural)
import System.Random
import System.Random.Stateful
newtype SignedBV w = SignedBV { forall (w :: Natural). SignedBV w -> BV w
asBV :: BV w }
deriving (forall (w :: Natural) x. Rep (SignedBV w) x -> SignedBV w
forall (w :: Natural) x. SignedBV w -> Rep (SignedBV w) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (w :: Natural) x. Rep (SignedBV w) x -> SignedBV w
$cfrom :: forall (w :: Natural) x. SignedBV w -> Rep (SignedBV w) x
Generic, Int -> SignedBV w -> ShowS
forall (w :: Natural). Int -> SignedBV w -> ShowS
forall (w :: Natural). [SignedBV w] -> ShowS
forall (w :: Natural). SignedBV w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SignedBV w] -> ShowS
$cshowList :: forall (w :: Natural). [SignedBV w] -> ShowS
show :: SignedBV w -> String
$cshow :: forall (w :: Natural). SignedBV w -> String
showsPrec :: Int -> SignedBV w -> ShowS
$cshowsPrec :: forall (w :: Natural). Int -> SignedBV w -> ShowS
Show, ReadPrec [SignedBV w]
ReadPrec (SignedBV w)
ReadS [SignedBV w]
forall (w :: Natural). ReadPrec [SignedBV w]
forall (w :: Natural). ReadPrec (SignedBV w)
forall (w :: Natural). Int -> ReadS (SignedBV w)
forall (w :: Natural). ReadS [SignedBV w]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SignedBV w]
$creadListPrec :: forall (w :: Natural). ReadPrec [SignedBV w]
readPrec :: ReadPrec (SignedBV w)
$creadPrec :: forall (w :: Natural). ReadPrec (SignedBV w)
readList :: ReadS [SignedBV w]
$creadList :: forall (w :: Natural). ReadS [SignedBV w]
readsPrec :: Int -> ReadS (SignedBV w)
$creadsPrec :: forall (w :: Natural). Int -> ReadS (SignedBV w)
Read, SignedBV w -> SignedBV w -> Bool
forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SignedBV w -> SignedBV w -> Bool
$c/= :: forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
== :: SignedBV w -> SignedBV w -> Bool
$c== :: forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
Eq, forall (w :: Natural) (m :: * -> *). Quote m => SignedBV w -> m Exp
forall (w :: Natural) (m :: * -> *).
Quote m =>
SignedBV w -> Code m (SignedBV w)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SignedBV w -> m Exp
forall (m :: * -> *). Quote m => SignedBV w -> Code m (SignedBV w)
liftTyped :: forall (m :: * -> *). Quote m => SignedBV w -> Code m (SignedBV w)
$cliftTyped :: forall (w :: Natural) (m :: * -> *).
Quote m =>
SignedBV w -> Code m (SignedBV w)
lift :: forall (m :: * -> *). Quote m => SignedBV w -> m Exp
$clift :: forall (w :: Natural) (m :: * -> *). Quote m => SignedBV w -> m Exp
Lift, forall (w :: Natural). SignedBV w -> ()
forall a. (a -> ()) -> NFData a
rnf :: SignedBV w -> ()
$crnf :: forall (w :: Natural). SignedBV w -> ()
NFData)
instance (KnownNat w, 1 <= w) => Ord (SignedBV w) where
SignedBV BV w
bv1 compare :: SignedBV w -> SignedBV w -> Ordering
`compare` SignedBV BV w
bv2 =
if | BV w
bv1 forall a. Eq a => a -> a -> Bool
== BV w
bv2 -> Ordering
EQ
| forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> Bool
BV.slt forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
bv1 BV w
bv2 -> Ordering
LT
| Bool
otherwise -> Ordering
GT
mkSignedBV :: NatRepr w -> Integer -> SignedBV w
mkSignedBV :: forall (w :: Natural). NatRepr w -> Integer -> SignedBV w
mkSignedBV NatRepr w
w Integer
x = forall (w :: Natural). BV w -> SignedBV w
SignedBV (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
x)
liftUnary :: (BV w -> BV w)
-> SignedBV w
-> SignedBV w
liftUnary :: forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary BV w -> BV w
op (SignedBV BV w
bv) = forall (w :: Natural). BV w -> SignedBV w
SignedBV (BV w -> BV w
op BV w
bv)
liftBinary :: (BV w -> BV w -> BV w)
-> SignedBV w
-> SignedBV w
-> SignedBV w
liftBinary :: forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary BV w -> BV w -> BV w
op (SignedBV BV w
bv1) (SignedBV BV w
bv2) = forall (w :: Natural). BV w -> SignedBV w
SignedBV (BV w -> BV w -> BV w
op BV w
bv1 BV w
bv2)
liftBinaryInt :: (BV w -> Natural -> BV w)
-> SignedBV w
-> Int
-> SignedBV w
liftBinaryInt :: forall (w :: Natural).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt BV w -> Natural -> BV w
op (SignedBV BV w
bv) Int
i = forall (w :: Natural). BV w -> SignedBV w
SignedBV (BV w -> Natural -> BV w
op BV w
bv (Int -> Natural
intToNatural Int
i))
intToNatural :: Int -> Natural
intToNatural :: Int -> Natural
intToNatural = forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance (KnownNat w, 1 <= w) => Bits (SignedBV w) where
.&. :: SignedBV w -> SignedBV w -> SignedBV w
(.&.) = forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary forall (w :: Natural). BV w -> BV w -> BV w
BV.and
.|. :: SignedBV w -> SignedBV w -> SignedBV w
(.|.) = forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary forall (w :: Natural). BV w -> BV w -> BV w
BV.or
xor :: SignedBV w -> SignedBV w -> SignedBV w
xor = forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary forall (w :: Natural). BV w -> BV w -> BV w
BV.xor
complement :: SignedBV w -> SignedBV w
complement = forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.complement forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
shiftL :: SignedBV w -> Int -> SignedBV w
shiftL = forall (w :: Natural).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.shl forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
shiftR :: SignedBV w -> Int -> SignedBV w
shiftR = forall (w :: Natural).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Natural -> BV w
BV.ashr forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
rotateL :: SignedBV w -> Int -> SignedBV w
rotateL = forall (w :: Natural).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.rotateL forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
rotateR :: SignedBV w -> Int -> SignedBV w
rotateR = forall (w :: Natural).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.rotateR forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
bitSize :: SignedBV w -> Int
bitSize SignedBV w
_ = forall (n :: Natural). NatRepr n -> Int
widthVal (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w)
bitSizeMaybe :: SignedBV w -> Maybe Int
bitSizeMaybe SignedBV w
_ = forall a. a -> Maybe a
Just (forall (n :: Natural). NatRepr n -> Int
widthVal (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w))
isSigned :: SignedBV w -> Bool
isSigned = forall a b. a -> b -> a
const Bool
True
testBit :: SignedBV w -> Int -> Bool
testBit (SignedBV BV w
bv) Int
ix = forall (w :: Natural). Natural -> BV w -> Bool
BV.testBit' (Int -> Natural
intToNatural Int
ix) BV w
bv
bit :: Int -> SignedBV w
bit = forall (w :: Natural). BV w -> SignedBV w
SignedBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). NatRepr w -> Natural -> BV w
BV.bit' forall (n :: Natural). KnownNat n => NatRepr n
knownNat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
intToNatural
popCount :: SignedBV w -> Int
popCount (SignedBV BV w
bv) = forall a. Num a => Integer -> a
fromInteger (forall (w :: Natural). BV w -> Integer
BV.asUnsigned (forall (w :: Natural). BV w -> BV w
BV.popCount BV w
bv))
instance (KnownNat w, 1 <= w) => FiniteBits (SignedBV w) where
finiteBitSize :: SignedBV w -> Int
finiteBitSize SignedBV w
_ = forall (n :: Natural). NatRepr n -> Int
widthVal (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w)
countLeadingZeros :: SignedBV w -> Int
countLeadingZeros (SignedBV BV w
bv) = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.clz forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
bv
countTrailingZeros :: SignedBV w -> Int
countTrailingZeros (SignedBV BV w
bv) = forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.ctz forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
bv
instance (KnownNat w, 1 <= w) => Num (SignedBV w) where
+ :: SignedBV w -> SignedBV w -> SignedBV w
(+) = forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.add forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
* :: SignedBV w -> SignedBV w -> SignedBV w
(*) = forall (w :: Natural).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary (forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
BV.mul forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
abs :: SignedBV w -> SignedBV w
abs = forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> BV w
BV.abs forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
signum :: SignedBV w -> SignedBV w
signum (SignedBV BV w
bv) = forall (w :: Natural). NatRepr w -> Integer -> SignedBV w
mkSignedBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
signum forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
bv
fromInteger :: Integer -> SignedBV w
fromInteger = forall (w :: Natural). BV w -> SignedBV w
SignedBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). NatRepr w -> Integer -> BV w
mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat
negate :: SignedBV w -> SignedBV w
negate = forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (forall (w :: Natural). NatRepr w -> BV w -> BV w
BV.negate forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
instance (KnownNat w, 1 <= w) => Enum (SignedBV w) where
toEnum :: Int -> SignedBV w
toEnum = forall (w :: Natural). BV w -> SignedBV w
SignedBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). NatRepr w -> Integer -> BV w
mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
checkInt
where checkInt :: Int -> Integer
checkInt Int
i | Integer
lo forall a. Ord a => a -> a -> Bool
<= forall a. Integral a => a -> Integer
toInteger Int
i Bool -> Bool -> Bool
&& forall a. Integral a => a -> Integer
toInteger Int
i forall a. Ord a => a -> a -> Bool
<= Integer
hi = forall a. Integral a => a -> Integer
toInteger Int
i
| Bool
otherwise = forall a. String -> [String] -> a
panic String
"Data.BitVector.Sized.Signed"
[String
"toEnum: bad argument"]
where lo :: Integer
lo = forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
minSigned (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w)
hi :: Integer
hi = forall (w :: Natural). (1 <= w) => NatRepr w -> Integer
maxSigned (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w)
fromEnum :: SignedBV w -> Int
fromEnum (SignedBV BV w
bv) = forall a. Num a => Integer -> a
fromInteger (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w) BV w
bv)
instance (KnownNat w, 1 <= w) => Ix (SignedBV w) where
range :: (SignedBV w, SignedBV w) -> [SignedBV w]
range (SignedBV BV w
loBV, SignedBV BV w
hiBV) =
(forall (w :: Natural). BV w -> SignedBV w
SignedBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Natural). NatRepr w -> Integer -> BV w
mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
[forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
loBV .. forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
hiBV]
index :: (SignedBV w, SignedBV w) -> SignedBV w -> Int
index (SignedBV BV w
loBV, SignedBV BV w
hiBV) (SignedBV BV w
ixBV) =
forall a. Ix a => (a, a) -> a -> Int
index ( forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
loBV
, forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
hiBV)
(forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
ixBV)
inRange :: (SignedBV w, SignedBV w) -> SignedBV w -> Bool
inRange (SignedBV BV w
loBV, SignedBV BV w
hiBV) (SignedBV BV w
ixBV) =
forall a. Ix a => (a, a) -> a -> Bool
inRange ( forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
loBV
, forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
hiBV)
(forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat BV w
ixBV)
instance (KnownNat w, 1 <= w) => Bounded (SignedBV w) where
minBound :: SignedBV w
minBound = forall (w :: Natural). BV w -> SignedBV w
SignedBV (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
maxBound :: SignedBV w
maxBound = forall (w :: Natural). BV w -> SignedBV w
SignedBV (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.maxSigned forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
instance KnownNat w => Uniform (SignedBV w) where
uniformM :: forall g (m :: * -> *). StatefulGen g m => g -> m (SignedBV w)
uniformM g
g = forall (w :: Natural). BV w -> SignedBV w
SignedBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall g (m :: * -> *) (w :: Natural).
StatefulGen g m =>
NatRepr w -> g -> m (BV w)
BV.uniformM forall (n :: Natural). KnownNat n => NatRepr n
knownNat g
g
instance (KnownNat w, 1 <= w) => UniformRange (SignedBV w) where
uniformRM :: forall g (m :: * -> *).
StatefulGen g m =>
(SignedBV w, SignedBV w) -> g -> m (SignedBV w)
uniformRM (SignedBV BV w
lo, SignedBV BV w
hi) g
g =
forall (w :: Natural). BV w -> SignedBV w
SignedBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall g (m :: * -> *) (w :: Natural).
(StatefulGen g m, 1 <= w) =>
NatRepr w -> (BV w, BV w) -> g -> m (BV w)
BV.sUniformRM forall (n :: Natural). KnownNat n => NatRepr n
knownNat (BV w
lo, BV w
hi) g
g
instance (KnownNat w, 1 <= w) => Random (SignedBV w)
instance Hashable (SignedBV w) where
hashWithSalt :: Int -> SignedBV w -> Int
hashWithSalt Int
salt (SignedBV BV w
b) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt BV w
b