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

-- | 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 = 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