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

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

This module defines a wrapper around the 'BV' type, 'SignedBV', with
instances not provided by 'BV'.
-}

module Data.BitVector.Sized.Signed
  ( SignedBV(..)
  , mkSignedBV
  ) where

import           Data.BitVector.Sized (BV, mkBV)
import qualified Data.BitVector.Sized.Internal as BV
import           Data.BitVector.Sized.Panic (panic)
import Data.Parameterized.NatRepr

import Data.Bits (Bits(..), FiniteBits(..))
import Data.Ix
import GHC.Generics
import GHC.TypeLits
import Numeric.Natural
import System.Random
import System.Random.Stateful

-- | Signed bit vector.
newtype SignedBV w = SignedBV { SignedBV w -> BV w
asBV :: BV w }
  deriving ((forall x. SignedBV w -> Rep (SignedBV w) x)
-> (forall x. Rep (SignedBV w) x -> SignedBV w)
-> Generic (SignedBV w)
forall x. Rep (SignedBV w) x -> SignedBV w
forall x. SignedBV w -> Rep (SignedBV w) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (w :: Nat) x. Rep (SignedBV w) x -> SignedBV w
forall (w :: Nat) x. SignedBV w -> Rep (SignedBV w) x
$cto :: forall (w :: Nat) x. Rep (SignedBV w) x -> SignedBV w
$cfrom :: forall (w :: Nat) x. SignedBV w -> Rep (SignedBV w) x
Generic, Int -> SignedBV w -> ShowS
[SignedBV w] -> ShowS
SignedBV w -> String
(Int -> SignedBV w -> ShowS)
-> (SignedBV w -> String)
-> ([SignedBV w] -> ShowS)
-> Show (SignedBV w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (w :: Nat). Int -> SignedBV w -> ShowS
forall (w :: Nat). [SignedBV w] -> ShowS
forall (w :: Nat). SignedBV w -> String
showList :: [SignedBV w] -> ShowS
$cshowList :: forall (w :: Nat). [SignedBV w] -> ShowS
show :: SignedBV w -> String
$cshow :: forall (w :: Nat). SignedBV w -> String
showsPrec :: Int -> SignedBV w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> SignedBV w -> ShowS
Show, ReadPrec [SignedBV w]
ReadPrec (SignedBV w)
Int -> ReadS (SignedBV w)
ReadS [SignedBV w]
(Int -> ReadS (SignedBV w))
-> ReadS [SignedBV w]
-> ReadPrec (SignedBV w)
-> ReadPrec [SignedBV w]
-> Read (SignedBV w)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (w :: Nat). ReadPrec [SignedBV w]
forall (w :: Nat). ReadPrec (SignedBV w)
forall (w :: Nat). Int -> ReadS (SignedBV w)
forall (w :: Nat). ReadS [SignedBV w]
readListPrec :: ReadPrec [SignedBV w]
$creadListPrec :: forall (w :: Nat). ReadPrec [SignedBV w]
readPrec :: ReadPrec (SignedBV w)
$creadPrec :: forall (w :: Nat). ReadPrec (SignedBV w)
readList :: ReadS [SignedBV w]
$creadList :: forall (w :: Nat). ReadS [SignedBV w]
readsPrec :: Int -> ReadS (SignedBV w)
$creadsPrec :: forall (w :: Nat). Int -> ReadS (SignedBV w)
Read, SignedBV w -> SignedBV w -> Bool
(SignedBV w -> SignedBV w -> Bool)
-> (SignedBV w -> SignedBV w -> Bool) -> Eq (SignedBV w)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (w :: Nat). SignedBV w -> SignedBV w -> Bool
/= :: SignedBV w -> SignedBV w -> Bool
$c/= :: forall (w :: Nat). SignedBV w -> SignedBV w -> Bool
== :: SignedBV w -> SignedBV w -> Bool
$c== :: forall (w :: Nat). SignedBV w -> SignedBV w -> Bool
Eq)

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 BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== BV w
bv2              -> Ordering
EQ
       | NatRepr w -> BV w -> BV w -> Bool
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
BV.slt NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
bv1 BV w
bv2 -> Ordering
LT
       | Bool
otherwise               -> Ordering
GT

-- | Convenience wrapper for 'BV.mkBV'.
mkSignedBV :: NatRepr w -> Integer -> SignedBV w
mkSignedBV :: NatRepr w -> Integer -> SignedBV w
mkSignedBV NatRepr w
w Integer
x = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
x)

liftUnary :: (BV w -> BV w)
          -> SignedBV w
          -> SignedBV w
liftUnary :: (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary BV w -> BV w
op (SignedBV BV w
bv) = BV w -> SignedBV w
forall (w :: Nat). 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 :: (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) = BV w -> SignedBV w
forall (w :: Nat). 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 :: (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt BV w -> Natural -> BV w
op (SignedBV BV w
bv) Int
i = BV w -> SignedBV w
forall (w :: Nat). 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 = Int -> Natural
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
(.&.)        = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
forall (w :: Nat).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.and
  .|. :: SignedBV w -> SignedBV w -> SignedBV w
(.|.)        = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
forall (w :: Nat).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.or
  xor :: SignedBV w -> SignedBV w -> SignedBV w
xor          = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
forall (w :: Nat).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Nat). BV w -> BV w -> BV w
BV.xor
  complement :: SignedBV w -> SignedBV w
complement   = (BV w -> BV w) -> SignedBV w -> SignedBV w
forall (w :: Nat). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.complement NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  shiftL :: SignedBV w -> Int -> SignedBV w
shiftL       = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
forall (w :: Nat).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.shl NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  shiftR :: SignedBV w -> Int -> SignedBV w
shiftR       = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
forall (w :: Nat).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Natural -> BV w
BV.ashr NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  rotateL :: SignedBV w -> Int -> SignedBV w
rotateL      = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
forall (w :: Nat).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.rotateL NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  rotateR :: SignedBV w -> Int -> SignedBV w
rotateR      = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
forall (w :: Nat).
(BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w
BV.rotateR NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  bitSize :: SignedBV w -> Int
bitSize SignedBV w
_    = NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w)
  bitSizeMaybe :: SignedBV w -> Maybe Int
bitSizeMaybe SignedBV w
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w))
  isSigned :: SignedBV w -> Bool
isSigned     = Bool -> SignedBV w -> Bool
forall a b. a -> b -> a
const Bool
True
  testBit :: SignedBV w -> Int -> Bool
testBit (SignedBV BV w
bv) Int
ix = Natural -> BV w -> Bool
forall (w :: Nat). Natural -> BV w -> Bool
BV.testBit' (Int -> Natural
intToNatural Int
ix) BV w
bv
  bit :: Int -> SignedBV w
bit          = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> (Int -> BV w) -> Int -> SignedBV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Natural -> BV w
forall (w :: Nat). NatRepr w -> Natural -> BV w
BV.bit' NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Natural -> BV w) -> (Int -> Natural) -> Int -> BV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
intToNatural
  popCount :: SignedBV w -> Int
popCount (SignedBV BV w
bv) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> BV w
forall (w :: Nat). 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
_ = NatRepr w -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w)
  countLeadingZeros :: SignedBV w -> Int
countLeadingZeros  (SignedBV BV w
bv) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> BV w -> Integer
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.clz NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
bv
  countTrailingZeros :: SignedBV w -> Int
countTrailingZeros (SignedBV BV w
bv) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> BV w -> Integer
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.ctz NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
bv

instance (KnownNat w, 1 <= w) => Num (SignedBV w) where
  + :: SignedBV w -> SignedBV w -> SignedBV w
(+)         = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
forall (w :: Nat).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.add NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  * :: SignedBV w -> SignedBV w -> SignedBV w
(*)         = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
forall (w :: Nat).
(BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
liftBinary (NatRepr w -> BV w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
BV.mul NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  abs :: SignedBV w -> SignedBV w
abs         = (BV w -> BV w) -> SignedBV w -> SignedBV w
forall (w :: Nat). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (NatRepr w -> BV w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w
BV.abs NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  signum :: SignedBV w -> SignedBV w
signum (SignedBV BV w
bv) = NatRepr w -> Integer -> SignedBV w
forall (w :: Nat). NatRepr w -> Integer -> SignedBV w
mkSignedBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Integer -> SignedBV w) -> Integer -> SignedBV w
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
signum (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
bv
  fromInteger :: Integer -> SignedBV w
fromInteger = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> (Integer -> BV w) -> Integer -> SignedBV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
  negate :: SignedBV w -> SignedBV w
negate      = (BV w -> BV w) -> SignedBV w -> SignedBV w
forall (w :: Nat). (BV w -> BV w) -> SignedBV w -> SignedBV w
liftUnary (NatRepr w -> BV w -> BV w
forall (w :: Nat). NatRepr w -> BV w -> BV w
BV.negate NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)

instance (KnownNat w, 1 <= w) => Enum (SignedBV w) where
  toEnum :: Int -> SignedBV w
toEnum = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> (Int -> BV w) -> Int -> SignedBV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (Integer -> BV w) -> (Int -> Integer) -> Int -> BV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
checkInt
    where checkInt :: Int -> Integer
checkInt Int
i | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Bool -> Bool -> Bool
&& Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i
                     | Bool
otherwise = String -> [String] -> Integer
forall a. String -> [String] -> a
panic String
"Data.BitVector.Sized.Signed"
                                   [String
"toEnum: bad argument"]
            where lo :: Integer
lo = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
minSigned (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w)
                  hi :: Integer
hi = NatRepr w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w)

  fromEnum :: SignedBV w -> Int
fromEnum (SignedBV BV w
bv) = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (KnownNat w => NatRepr w
forall (n :: Nat). 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) =
    (BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> (Integer -> BV w) -> Integer -> SignedBV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat) (Integer -> SignedBV w) -> [Integer] -> [SignedBV 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
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
loBV .. NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). 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) =
    (Integer, Integer) -> Integer -> Int
forall a. Ix a => (a, a) -> a -> Int
index ( NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
loBV
          , NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
hiBV)
    (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). 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) =
    (Integer, Integer) -> Integer -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange ( NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
loBV
            , NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
hiBV)
    (NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BV w
ixBV)

instance (KnownNat w, 1 <= w) => Bounded (SignedBV w) where
  minBound :: SignedBV w
minBound = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)
  maxBound :: SignedBV w
maxBound = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (NatRepr w -> BV w
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
BV.maxSigned NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)

instance KnownNat w => Uniform (SignedBV w) where
  uniformM :: g -> m (SignedBV w)
uniformM g
g = BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> m (BV w) -> m (SignedBV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> g -> m (BV w)
forall g (m :: * -> *) (w :: Nat).
StatefulGen g m =>
NatRepr w -> g -> m (BV w)
BV.uniformM NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat g
g

instance (KnownNat w, 1 <= w) => UniformRange (SignedBV w) where
  uniformRM :: (SignedBV w, SignedBV w) -> g -> m (SignedBV w)
uniformRM (SignedBV BV w
lo, SignedBV BV w
hi) g
g =
    BV w -> SignedBV w
forall (w :: Nat). BV w -> SignedBV w
SignedBV (BV w -> SignedBV w) -> m (BV w) -> m (SignedBV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> (BV w, BV w) -> g -> m (BV w)
forall g (m :: * -> *) (w :: Nat).
(StatefulGen g m, 1 <= w) =>
NatRepr w -> (BV w, BV w) -> g -> m (BV w)
BV.sUniformRM NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (BV w
lo, BV w
hi) g
g

instance (KnownNat w, 1 <= w) => Random (SignedBV w)