    {-# 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
    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 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

    -- | Signed bit vector.
    newtype SignedBV w = SignedBV { forall (w :: Natural). 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 (w :: Natural) x. Rep (SignedBV w) x -> SignedBV w
    forall (w :: Natural) x. SignedBV w -> Rep (SignedBV w) x
    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
    $cfrom :: forall (w :: Natural) x. SignedBV w -> Rep (SignedBV w) x
    from :: forall x. SignedBV w -> Rep (SignedBV w) x
    $cto :: forall (w :: Natural) x. Rep (SignedBV w) x -> SignedBV w
    to :: forall x. Rep (SignedBV w) x -> SignedBV w
    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 (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
    $cshowsPrec :: forall (w :: Natural). Int -> SignedBV w -> ShowS
    showsPrec :: Int -> SignedBV w -> ShowS
    $cshow :: forall (w :: Natural). SignedBV w -> String
    show :: SignedBV w -> String
    $cshowList :: forall (w :: Natural). [SignedBV w] -> ShowS
    showList :: [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 (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
    $creadsPrec :: forall (w :: Natural). Int -> ReadS (SignedBV w)
    readsPrec :: Int -> ReadS (SignedBV w)
    $creadList :: forall (w :: Natural). ReadS [SignedBV w]
    readList :: ReadS [SignedBV w]
    $creadPrec :: forall (w :: Natural). ReadPrec (SignedBV w)
    readPrec :: ReadPrec (SignedBV w)
    $creadListPrec :: forall (w :: Natural). ReadPrec [SignedBV w]
    readListPrec :: ReadPrec [SignedBV w]
    Read, SignedBV w -> SignedBV w -> Bool
    (SignedBV w -> SignedBV w -> Bool)
    -> (SignedBV w -> SignedBV w -> Bool) -> Eq (SignedBV w)
    forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
    == :: SignedBV w -> SignedBV w -> Bool
    $c/= :: forall (w :: Natural). SignedBV w -> SignedBV w -> Bool
    /= :: SignedBV w -> SignedBV w -> Bool
    Eq, (forall (m :: * -> *). Quote m => SignedBV w -> m Exp)
    -> (forall (m :: * -> *).
        Quote m =>
        SignedBV w -> Code m (SignedBV w))
    -> Lift (SignedBV w)
    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)
    $clift :: forall (w :: Natural) (m :: * -> *). Quote m => SignedBV w -> m Exp
    lift :: forall (m :: * -> *). Quote m => SignedBV w -> m Exp
    $cliftTyped :: forall (w :: Natural) (m :: * -> *).
    Quote m =>
    SignedBV w -> Code m (SignedBV w)
    liftTyped :: forall (m :: * -> *). Quote m => SignedBV w -> Code m (SignedBV w)
    Lift, SignedBV w -> ()
    (SignedBV w -> ()) -> NFData (SignedBV w)
    forall (w :: Natural). SignedBV w -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall (w :: Natural). SignedBV w -> ()
    rnf :: 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 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 :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> BV w -> Bool
    BV.slt NatRepr w
    forall (n :: Natural). 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 :: forall (w :: Natural). NatRepr w -> Integer -> SignedBV w
    mkSignedBV NatRepr w
    w Integer
    x = BV w -> SignedBV w
    forall (w :: Natural). BV w -> SignedBV w
    SignedBV (NatRepr w -> Integer -> BV w
    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) = BV w -> SignedBV w
    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) = BV w -> SignedBV w
    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 = BV w -> SignedBV w
    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 = 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 :: Natural).
    (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). 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 :: Natural).
    (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). 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 :: Natural).
    (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    BV.xor
      complement :: SignedBV w -> SignedBV w
    complement   = (BV w -> BV w) -> SignedBV w -> SignedBV w
    forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
    liftUnary (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.complement NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      shiftL :: SignedBV w -> Int -> SignedBV w
    shiftL       = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.shl NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      shiftR :: SignedBV w -> Int -> SignedBV w
    shiftR       = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> Natural -> BV w
    BV.ashr NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      rotateL :: SignedBV w -> Int -> SignedBV w
    rotateL      = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.rotateL NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      rotateR :: SignedBV w -> Int -> SignedBV w
    rotateR      = (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> SignedBV w -> Int -> SignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.rotateR NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      bitSize :: SignedBV w -> Int
    bitSize SignedBV w
    _    = NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal (forall (n :: Natural). 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 :: Natural). NatRepr n -> Int
    widthVal (forall (n :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). NatRepr w -> Natural -> BV w
    BV.bit' NatRepr w
    forall (n :: Natural). 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 :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> BV w
    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
    _ = NatRepr w -> Int
    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) = 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 :: Natural). 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 :: Natural). NatRepr w -> BV w -> BV w
    BV.clz NatRepr w
    forall (n :: Natural). 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 :: Natural). 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 :: Natural). NatRepr w -> BV w -> BV w
    BV.ctz NatRepr w
    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
    (+)         = (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    liftBinary (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    BV.add NatRepr w
    forall (n :: Natural). 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 :: Natural).
    (BV w -> BV w -> BV w) -> SignedBV w -> SignedBV w -> SignedBV w
    liftBinary (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    BV.mul NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      abs :: SignedBV w -> SignedBV w
    abs         = (BV w -> BV w) -> SignedBV w -> SignedBV w
    forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
    liftUnary (NatRepr w -> BV w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> BV w
    BV.abs NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      signum :: SignedBV w -> SignedBV w
    signum (SignedBV BV w
    bv) = NatRepr w -> Integer -> SignedBV w
    forall (w :: Natural). NatRepr w -> Integer -> SignedBV w
    mkSignedBV NatRepr w
    forall (n :: Natural). 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 :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    bv
      fromInteger :: Integer -> SignedBV w
    fromInteger = BV w -> SignedBV w
    forall (w :: Natural). 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 :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat
      negate :: SignedBV w -> SignedBV w
    negate      = (BV w -> BV w) -> SignedBV w -> SignedBV w
    forall (w :: Natural). (BV w -> BV w) -> SignedBV w -> SignedBV w
    liftUnary (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.negate NatRepr w
    forall (n :: Natural). 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 :: Natural). 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 :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). 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 :: Natural). (1 <= w) => NatRepr w -> Integer
    minSigned (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @w)
                      hi :: Integer
    hi = NatRepr w -> Integer
    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) = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (NatRepr w -> BV w -> Integer
    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) =
        (BV w -> SignedBV w
    forall (w :: Natural). 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 :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). 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 :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    loBV .. NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    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) =
        (Integer, Integer) -> Integer -> Int
    forall a. Ix a => (a, a) -> a -> Int
    index ( NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    loBV
              , NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    hiBV)
        (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    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) =
        (Integer, Integer) -> Integer -> Bool
    forall a. Ix a => (a, a) -> a -> Bool
    inRange ( NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    loBV
                , NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    hiBV)
        (NatRepr w -> BV w -> Integer
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
    BV.asSigned NatRepr w
    forall (n :: Natural). 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 :: Natural). BV w -> SignedBV w
    SignedBV (NatRepr w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.minSigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      maxBound :: SignedBV w
    maxBound = BV w -> SignedBV w
    forall (w :: Natural). BV w -> SignedBV w
    SignedBV (NatRepr w -> BV w
    forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
    BV.maxSigned NatRepr w
    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 = BV w -> SignedBV w
    forall (w :: Natural). 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 :: Natural).
    StatefulGen g m =>
    NatRepr w -> g -> m (BV w)
    BV.uniformM NatRepr w
    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 =
        BV w -> SignedBV w
    forall (w :: Natural). 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 :: Natural).
    (StatefulGen g m, 1 <= w) =>
    NatRepr w -> (BV w, BV w) -> g -> m (BV w)
    BV.sUniformRM NatRepr w
    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) = Int -> BV w -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    salt BV w
    b