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