{-# LANGUAGE CPP #-}
{-# 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 x. UnsignedBV w -> Rep (UnsignedBV w) x)
-> (forall x. Rep (UnsignedBV w) x -> UnsignedBV w)
-> Generic (UnsignedBV w)
forall (w :: Natural) x. Rep (UnsignedBV w) x -> UnsignedBV w
forall (w :: Natural) x. UnsignedBV w -> Rep (UnsignedBV w) x
forall x. Rep (UnsignedBV w) x -> UnsignedBV w
forall x. UnsignedBV w -> Rep (UnsignedBV w) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (w :: Natural) x. UnsignedBV w -> Rep (UnsignedBV w) x
from :: forall x. UnsignedBV w -> Rep (UnsignedBV w) x
$cto :: forall (w :: Natural) x. Rep (UnsignedBV w) x -> UnsignedBV w
to :: forall x. Rep (UnsignedBV w) x -> UnsignedBV w
Generic, Int -> UnsignedBV w -> ShowS
[UnsignedBV w] -> ShowS
UnsignedBV w -> String
(Int -> UnsignedBV w -> ShowS)
-> (UnsignedBV w -> String)
-> ([UnsignedBV w] -> ShowS)
-> Show (UnsignedBV w)
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
$cshowsPrec :: forall (w :: Natural). Int -> UnsignedBV w -> ShowS
showsPrec :: Int -> UnsignedBV w -> ShowS
$cshow :: forall (w :: Natural). UnsignedBV w -> String
show :: UnsignedBV w -> String
$cshowList :: forall (w :: Natural). [UnsignedBV w] -> ShowS
showList :: [UnsignedBV w] -> ShowS
Show, ReadPrec [UnsignedBV w]
ReadPrec (UnsignedBV w)
Int -> ReadS (UnsignedBV w)
ReadS [UnsignedBV w]
(Int -> ReadS (UnsignedBV w))
-> ReadS [UnsignedBV w]
-> ReadPrec (UnsignedBV w)
-> ReadPrec [UnsignedBV w]
-> Read (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
$creadsPrec :: forall (w :: Natural). Int -> ReadS (UnsignedBV w)
readsPrec :: Int -> ReadS (UnsignedBV w)
$creadList :: forall (w :: Natural). ReadS [UnsignedBV w]
readList :: ReadS [UnsignedBV w]
$creadPrec :: forall (w :: Natural). ReadPrec (UnsignedBV w)
readPrec :: ReadPrec (UnsignedBV w)
$creadListPrec :: forall (w :: Natural). ReadPrec [UnsignedBV w]
readListPrec :: ReadPrec [UnsignedBV w]
Read, UnsignedBV w -> UnsignedBV w -> Bool
(UnsignedBV w -> UnsignedBV w -> Bool)
-> (UnsignedBV w -> UnsignedBV w -> Bool) -> Eq (UnsignedBV w)
forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
Eq, Eq (UnsignedBV w)
Eq (UnsignedBV w) =>
(UnsignedBV w -> UnsignedBV w -> Ordering)
-> (UnsignedBV w -> UnsignedBV w -> Bool)
-> (UnsignedBV w -> UnsignedBV w -> Bool)
-> (UnsignedBV w -> UnsignedBV w -> Bool)
-> (UnsignedBV w -> UnsignedBV w -> Bool)
-> (UnsignedBV w -> UnsignedBV w -> UnsignedBV w)
-> (UnsignedBV w -> UnsignedBV w -> UnsignedBV w)
-> Ord (UnsignedBV w)
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
$ccompare :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Ordering
compare :: UnsignedBV w -> UnsignedBV w -> Ordering
$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
>= :: UnsignedBV w -> UnsignedBV w -> Bool
$cmax :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> UnsignedBV w
max :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
$cmin :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> UnsignedBV w
min :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
Ord, (forall (m :: * -> *). Quote m => UnsignedBV w -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    UnsignedBV w -> Code m (UnsignedBV w))
-> Lift (UnsignedBV w)
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)
$clift :: forall (w :: Natural) (m :: * -> *).
Quote m =>
UnsignedBV w -> m Exp
lift :: forall (m :: * -> *). Quote m => UnsignedBV w -> m Exp
$cliftTyped :: forall (w :: Natural) (m :: * -> *).
Quote m =>
UnsignedBV w -> Code m (UnsignedBV w)
liftTyped :: forall (m :: * -> *).
Quote m =>
UnsignedBV w -> Code m (UnsignedBV w)
Lift, UnsignedBV w -> ()
(UnsignedBV w -> ()) -> NFData (UnsignedBV w)
forall (w :: Natural). UnsignedBV w -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (w :: Natural). UnsignedBV w -> ()
rnf :: 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 = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (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)
          -> 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) = BV w -> UnsignedBV w
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) = BV w -> UnsignedBV w
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 = BV w -> UnsignedBV w
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 = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance KnownNat w => Bits (UnsignedBV w) where
  .&. :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
(.&.)        = (BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.and
  .|. :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
(.|.)        = (BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.or
  xor :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
xor          = (BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
liftBinary BV w -> BV w -> BV w
forall (w :: Natural). BV w -> BV w -> BV w
BV.xor
  complement :: UnsignedBV w -> UnsignedBV w
complement   = (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w) -> UnsignedBV w -> UnsignedBV 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 :: UnsignedBV w -> Int -> UnsignedBV w
shiftL       = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
forall (w :: Natural).
(BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV 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 :: UnsignedBV w -> Int -> UnsignedBV w
shiftR       = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
forall (w :: Natural).
(BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
BV.lshr NatRepr w
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
  rotateL :: UnsignedBV w -> Int -> UnsignedBV w
rotateL      = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
forall (w :: Natural).
(BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV 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 :: UnsignedBV w -> Int -> UnsignedBV w
rotateR      = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
forall (w :: Natural).
(BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV 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 :: UnsignedBV w -> Int
bitSize UnsignedBV w
_    = NatRepr w -> Int
forall (n :: Natural). NatRepr n -> Int
widthVal (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w)
  bitSizeMaybe :: UnsignedBV w -> Maybe Int
bitSizeMaybe UnsignedBV 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 :: UnsignedBV w -> Bool
isSigned     = Bool -> UnsignedBV w -> Bool
forall a b. a -> b -> a
const Bool
False
  testBit :: UnsignedBV w -> Int -> Bool
testBit (UnsignedBV 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 -> UnsignedBV w
bit          = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w) -> (Int -> BV w) -> Int -> UnsignedBV 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 :: UnsignedBV w -> Int
popCount (UnsignedBV 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 => FiniteBits (UnsignedBV w) where
  finiteBitSize :: UnsignedBV w -> Int
finiteBitSize UnsignedBV w
_ = NatRepr w -> Int
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) = 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 :: UnsignedBV w -> Int
countTrailingZeros (UnsignedBV 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 => Num (UnsignedBV w) where
  + :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
(+)         = (BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV 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)
  * :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
(*)         = (BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w -> BV w)
-> UnsignedBV w -> UnsignedBV w -> UnsignedBV 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 :: UnsignedBV w -> UnsignedBV w
abs         = UnsignedBV w -> UnsignedBV w
forall a. a -> a
id
  signum :: UnsignedBV w -> UnsignedBV w
signum (UnsignedBV BV w
bv) = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w) -> BV w -> UnsignedBV w
forall a b. (a -> b) -> a -> b
$ Integer -> BV w
forall (w :: Natural). Integer -> BV w
BV.BV (Integer -> BV w) -> Integer -> BV 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
$ BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
bv
  fromInteger :: Integer -> UnsignedBV w
fromInteger = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w)
-> (Integer -> BV w) -> Integer -> UnsignedBV 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
  -- in this case, negate just means "additive inverse"
  negate :: UnsignedBV w -> UnsignedBV w
negate      = (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
forall (w :: Natural).
(BV w -> BV w) -> UnsignedBV w -> UnsignedBV 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 => Enum (UnsignedBV w) where
  toEnum :: Int -> UnsignedBV w
toEnum = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w) -> (Int -> BV w) -> Int -> UnsignedBV 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 | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 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
<= NatRepr w -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @w) = 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.Unsigned"
                                   [String
"toEnum: bad argument"]

  fromEnum :: UnsignedBV w -> Int
fromEnum (UnsignedBV 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)

instance KnownNat w => Ix (UnsignedBV w) where
  range :: (UnsignedBV w, UnsignedBV w) -> [UnsignedBV w]
range (UnsignedBV BV w
loBV, UnsignedBV BV w
hiBV) =
    BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w)
-> (Integer -> BV w) -> Integer -> UnsignedBV 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 -> UnsignedBV w) -> [Integer] -> [UnsignedBV w]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
loBV .. BV w -> Integer
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) =
    (Integer, Integer) -> Integer -> Int
forall a. Ix a => (a, a) -> a -> Int
index ( BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
loBV,
            BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
hiBV)
    (BV w -> Integer
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) =
    (Integer, Integer) -> Integer -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange ( BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
loBV
            , BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
hiBV)
    (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
ixBV)

instance KnownNat w => Bounded (UnsignedBV w) where
  minBound :: UnsignedBV w
minBound = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.minUnsigned NatRepr w
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
  maxBound :: UnsignedBV w
maxBound = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
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 = BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w) -> m (BV w) -> m (UnsignedBV 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 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 =
    BV w -> UnsignedBV w
forall (w :: Natural). BV w -> UnsignedBV w
UnsignedBV (BV w -> UnsignedBV w) -> m (BV w) -> m (UnsignedBV w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BV w, BV w) -> g -> m (BV w)
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
#if MIN_VERSION_random(1,3,0)
  isInRange :: (UnsignedBV w, UnsignedBV w) -> UnsignedBV w -> Bool
isInRange (UnsignedBV w
lo, UnsignedBV w
hi) UnsignedBV w
x =
    UnsignedBV w
lo UnsignedBV w -> UnsignedBV w -> Bool
forall a. Ord a => a -> a -> Bool
<= UnsignedBV w
x Bool -> Bool -> Bool
&& UnsignedBV w
x UnsignedBV w -> UnsignedBV w -> Bool
forall a. Ord a => a -> a -> Bool
<= UnsignedBV w
hi
#endif

instance KnownNat w => Random (UnsignedBV w)

instance Hashable (UnsignedBV w) where
  hashWithSalt :: Int -> UnsignedBV w -> Int
hashWithSalt Int
salt (UnsignedBV BV w
b) = Int -> BV w -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt BV w
b