{-# 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
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, 'UnsignedBV', with
instances not provided by 'BV'.
-}

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

-- | Signed bit vector.
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)

-- | Convenience wrapper for 'BV.mkBV'.
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
  -- in this case, negate just means "additive inverse"
  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