{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RoleAnnotations #-}

{- |
This module provides the type-level length-indexed and MSB-first bitvector 'Bitvec'
built on top of the package @bitvec@ and 'V.Vector'.

It also holds it's type of encoding as a phantom-type via 'BvEnc'.

==== __Examples__

>>> minBound @(Bitvec Unsigned 8)
00000000

>>> maxBound @(Bitvec Signed 8)
01111111

>>> (5 :: Bitvec Unsigned 4) + 10
1111
-}
module Language.Hasmtlib.Type.Bitvec
(
  -- * Bitvector encoding
  BvEnc(..), SBvEnc(..), KnownBvEnc(..)
, bvEncSing', bvEncSing''

  -- * Bitvec type
, Bitvec(..)

  -- * Construction
, bitvecConcat

  -- * Conversion
  -- ** Sign
, asUnsigned, asSigned

  -- ** Lists
, bitvecFromListN, bitvecFromListN'

  -- * Lens
, _signBit
)
where

import Prelude hiding ((&&), (||), not)
import Language.Hasmtlib.Boolean
import Data.GADT.Compare
import Data.Bit
import Data.Bits
import Data.Coerce
import Data.Finite hiding (shift)
import Data.Proxy
import Data.Bifunctor
import Data.Type.Equality
import qualified Data.Vector.Unboxed.Sized as V
import Control.Lens
import GHC.TypeNats

-- | Type of Bitvector encoding - used as promoted type (data-kind).
data BvEnc = Unsigned | Signed deriving (Int -> BvEnc -> ShowS
[BvEnc] -> ShowS
BvEnc -> String
(Int -> BvEnc -> ShowS)
-> (BvEnc -> String) -> ([BvEnc] -> ShowS) -> Show BvEnc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BvEnc -> ShowS
showsPrec :: Int -> BvEnc -> ShowS
$cshow :: BvEnc -> String
show :: BvEnc -> String
$cshowList :: [BvEnc] -> ShowS
showList :: [BvEnc] -> ShowS
Show, BvEnc -> BvEnc -> Bool
(BvEnc -> BvEnc -> Bool) -> (BvEnc -> BvEnc -> Bool) -> Eq BvEnc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BvEnc -> BvEnc -> Bool
== :: BvEnc -> BvEnc -> Bool
$c/= :: BvEnc -> BvEnc -> Bool
/= :: BvEnc -> BvEnc -> Bool
Eq, Eq BvEnc
Eq BvEnc =>
(BvEnc -> BvEnc -> Ordering)
-> (BvEnc -> BvEnc -> Bool)
-> (BvEnc -> BvEnc -> Bool)
-> (BvEnc -> BvEnc -> Bool)
-> (BvEnc -> BvEnc -> Bool)
-> (BvEnc -> BvEnc -> BvEnc)
-> (BvEnc -> BvEnc -> BvEnc)
-> Ord BvEnc
BvEnc -> BvEnc -> Bool
BvEnc -> BvEnc -> Ordering
BvEnc -> BvEnc -> BvEnc
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 :: BvEnc -> BvEnc -> Ordering
compare :: BvEnc -> BvEnc -> Ordering
$c< :: BvEnc -> BvEnc -> Bool
< :: BvEnc -> BvEnc -> Bool
$c<= :: BvEnc -> BvEnc -> Bool
<= :: BvEnc -> BvEnc -> Bool
$c> :: BvEnc -> BvEnc -> Bool
> :: BvEnc -> BvEnc -> Bool
$c>= :: BvEnc -> BvEnc -> Bool
>= :: BvEnc -> BvEnc -> Bool
$cmax :: BvEnc -> BvEnc -> BvEnc
max :: BvEnc -> BvEnc -> BvEnc
$cmin :: BvEnc -> BvEnc -> BvEnc
min :: BvEnc -> BvEnc -> BvEnc
Ord)

-- | Singleton for 'BvEnc'.
data SBvEnc (enc :: BvEnc) where
  SUnsigned :: SBvEnc Unsigned
  SSigned   :: SBvEnc Signed

deriving instance Show (SBvEnc enc)
deriving instance Eq   (SBvEnc enc)
deriving instance Ord  (SBvEnc enc)

-- | Compute singleton 'SBvEnc' from it's promoted type 'BvEnc'.
class KnownBvEnc (enc :: BvEnc) where bvEncSing :: SBvEnc enc
instance KnownBvEnc Unsigned    where bvEncSing :: SBvEnc 'Unsigned
bvEncSing = SBvEnc 'Unsigned
SUnsigned
instance KnownBvEnc Signed      where bvEncSing :: SBvEnc 'Signed
bvEncSing = SBvEnc 'Signed
SSigned

-- | Wrapper for 'bvEncSing' which takes a 'Proxy'.
bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc
bvEncSing' :: forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' prxy enc
_ = forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc

-- | Wrapper for 'bvEncSing' which takes a 'Proxy' and some ballast.
--   This is helpful for singing on values of type 'Bitvec' where the ballst is a 'Nat'.
bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc
bvEncSing'' :: forall {k} (enc :: BvEnc) (a :: k) (prxy :: BvEnc -> k -> *).
KnownBvEnc enc =>
prxy enc a -> SBvEnc enc
bvEncSing'' prxy enc a
_ = forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc

instance GEq SBvEnc where
  geq :: forall (a :: BvEnc) (b :: BvEnc).
SBvEnc a -> SBvEnc b -> Maybe (a :~: b)
geq SBvEnc a
SUnsigned SBvEnc b
SUnsigned = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geq SBvEnc a
SSigned SBvEnc b
SSigned = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  geq SBvEnc a
_ SBvEnc b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance GCompare SBvEnc where
  gcompare :: forall (a :: BvEnc) (b :: BvEnc).
SBvEnc a -> SBvEnc b -> GOrdering a b
gcompare SBvEnc a
SUnsigned SBvEnc b
SUnsigned = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
  gcompare SBvEnc a
SUnsigned SBvEnc b
_  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  gcompare SBvEnc a
_ SBvEnc b
SUnsigned  = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
  gcompare SBvEnc a
SSigned SBvEnc b
SSigned = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
  -- gcompare SSigned _  = GLT
  -- gcompare _ SSigned  = GGT

-- | Length-indexed bitvector ('V.Vector') carrying a phantom type-level 'BvEnc'.
--
--   Most significant bit is first (index 0) for unsigned bitvectors.
--   Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1).
type role Bitvec phantom phantom
newtype Bitvec (enc :: BvEnc) (n :: Nat) = Bitvec { forall (enc :: BvEnc) (n :: Nat). Bitvec enc n -> Vector n Bit
unBitvec :: V.Vector n Bit }
  deriving newtype (Bitvec enc n -> Bitvec enc n -> Bool
(Bitvec enc n -> Bitvec enc n -> Bool)
-> (Bitvec enc n -> Bitvec enc n -> Bool) -> Eq (Bitvec enc n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
$c== :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
== :: Bitvec enc n -> Bitvec enc n -> Bool
$c/= :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
/= :: Bitvec enc n -> Bitvec enc n -> Bool
Eq, Eq (Bitvec enc n)
Eq (Bitvec enc n) =>
(Bitvec enc n -> Bitvec enc n -> Ordering)
-> (Bitvec enc n -> Bitvec enc n -> Bool)
-> (Bitvec enc n -> Bitvec enc n -> Bool)
-> (Bitvec enc n -> Bitvec enc n -> Bool)
-> (Bitvec enc n -> Bitvec enc n -> Bool)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> Ord (Bitvec enc n)
Bitvec enc n -> Bitvec enc n -> Bool
Bitvec enc n -> Bitvec enc n -> Ordering
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
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
forall (enc :: BvEnc) (n :: Nat). Eq (Bitvec enc n)
forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Ordering
forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$ccompare :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Ordering
compare :: Bitvec enc n -> Bitvec enc n -> Ordering
$c< :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
< :: Bitvec enc n -> Bitvec enc n -> Bool
$c<= :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
<= :: Bitvec enc n -> Bitvec enc n -> Bool
$c> :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
> :: Bitvec enc n -> Bitvec enc n -> Bool
$c>= :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bool
>= :: Bitvec enc n -> Bitvec enc n -> Bool
$cmax :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
max :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$cmin :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
min :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
Ord, Bitvec enc n
Bool -> Bitvec enc n
Bitvec enc n -> Bitvec enc n
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
(Bool -> Bitvec enc n)
-> Bitvec enc n
-> Bitvec enc n
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n)
-> Boolean (Bitvec enc n)
forall b.
(Bool -> b)
-> b
-> b
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b)
-> (b -> b -> b)
-> Boolean b
forall (enc :: BvEnc) (n :: Nat). KnownNat n => Bitvec enc n
forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bool -> Bitvec enc n
forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n
forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$cbool :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bool -> Bitvec enc n
bool :: Bool -> Bitvec enc n
$ctrue :: forall (enc :: BvEnc) (n :: Nat). KnownNat n => Bitvec enc n
true :: Bitvec enc n
$cfalse :: forall (enc :: BvEnc) (n :: Nat). KnownNat n => Bitvec enc n
false :: Bitvec enc n
$c&& :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
&& :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$c|| :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
|| :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$c==> :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
==> :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$c<== :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
<== :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$c<==> :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
<==> :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
$cnot :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n
not :: Bitvec enc n -> Bitvec enc n
$cxor :: forall (enc :: BvEnc) (n :: Nat).
KnownNat n =>
Bitvec enc n -> Bitvec enc n -> Bitvec enc n
xor :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
Boolean)

-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Unsigned'.
asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n
asUnsigned :: forall (enc :: BvEnc) (n :: Nat).
Bitvec enc n -> Bitvec 'Unsigned n
asUnsigned = Vector n Bit -> Bitvec 'Unsigned n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec 'Unsigned n)
-> (Bitvec enc n -> Vector n Bit)
-> Bitvec enc n
-> Bitvec 'Unsigned n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Bitvec enc n) @(V.Vector n Bit)

-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Signed'.
asSigned :: forall enc n. Bitvec enc n -> Bitvec Signed n
asSigned :: forall (enc :: BvEnc) (n :: Nat). Bitvec enc n -> Bitvec 'Signed n
asSigned = Vector n Bit -> Bitvec 'Signed n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec 'Signed n)
-> (Bitvec enc n -> Vector n Bit)
-> Bitvec enc n
-> Bitvec 'Signed n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Bitvec enc n) @(V.Vector n Bit)

instance Show (Bitvec enc n) where
  show :: Bitvec enc n -> String
show = Vector n Char -> String
forall a (n :: Nat). Unbox a => Vector n a -> [a]
V.toList (Vector n Char -> String)
-> (Bitvec enc n -> Vector n Char) -> Bitvec enc n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Char) -> Vector n Bit -> Vector n Char
forall a b (n :: Nat).
(Unbox a, Unbox b) =>
(a -> b) -> Vector n a -> Vector n b
V.map (\Bit
b -> if Bit -> Bool
forall a b. Coercible a b => a -> b
coerce Bit
b then Char
'1' else Char
'0') (Vector n Bit -> Vector n Char)
-> (Bitvec enc n -> Vector n Bit) -> Bitvec enc n -> Vector n Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit)
  {-# INLINEABLE show #-}

instance (KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n) where
  .&. :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
(.&.) = Bitvec enc n -> Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b -> b
(&&)
  .|. :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
(.|.) = Bitvec enc n -> Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b -> b
(||)
  xor :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
xor = Bitvec enc n -> Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b -> b
Language.Hasmtlib.Boolean.xor
  complement :: Bitvec enc n -> Bitvec enc n
complement = Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b
not
  shift :: Bitvec enc n -> Int -> Bitvec enc n
shift Bitvec enc n
bv Int
i  = Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Vector n Bit -> Int -> Vector n Bit
forall a. Bits a => a -> Int -> a
shift (forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) Bitvec enc n
bv) (Int -> Int
forall a. Num a => a -> a
negate Int
i)
  rotate :: Bitvec enc n -> Int -> Bitvec enc n
rotate Bitvec enc n
bv Int
i = Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Vector n Bit -> Int -> Vector n Bit
forall a. Bits a => a -> Int -> a
rotate (forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) Bitvec enc n
bv) (Int -> Int
forall a. Num a => a -> a
negate Int
i)
  bitSize :: Bitvec enc n -> Int
bitSize Bitvec enc n
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
  bitSizeMaybe :: Bitvec enc n -> Maybe Int
bitSizeMaybe Bitvec enc n
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
  isSigned :: Bitvec enc n -> Bool
isSigned Bitvec enc n
_ = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Bool
False
    SBvEnc enc
SSigned -> Bool
True
  testBit :: Bitvec enc n -> Int -> Bool
testBit Bitvec enc n
bv = Vector n Bit -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit (Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) Bitvec enc n
bv))
  bit :: Int -> Bitvec enc n
bit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger -> Integer
i) = Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Vector n Bit
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n (Bool -> Bit
Bit Bool
False) Vector n Bit -> [(Finite n, Bit)] -> Vector n Bit
forall a (m :: Nat).
Unbox a =>
Vector m a -> [(Finite m, a)] -> Vector m a
V.// [(Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
finite Integer
i, Bool -> Bit
Bit Bool
True)]
  popCount :: Bitvec enc n -> Int
popCount = Int -> Int
forall a b. Coercible a b => a -> b
coerce (Int -> Int) -> (Bitvec enc n -> Int) -> Bitvec enc n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Bit -> Int
forall a. Bits a => a -> Int
popCount (Vector n Bit -> Int)
-> (Bitvec enc n -> Vector n Bit) -> Bitvec enc n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit)

instance (KnownBvEnc enc, KnownNat n) => Num (Bitvec enc n) where
   fromInteger :: Integer -> Bitvec enc n
fromInteger Integer
x = Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n)
-> (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Bitvec enc n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Finite n -> a) -> Vector n a
V.generate @n (Bool -> Bit
forall a b. Coercible a b => a -> b
coerce (Bool -> Bit) -> (Finite n -> Bool) -> Finite n -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
x (Int -> Bool) -> (Finite n -> Int) -> Finite n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (Finite n -> Integer) -> Finite n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite)
   negate :: Bitvec enc n -> Bitvec enc n
negate        = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Bitvec enc n -> Bitvec enc n
forall a. a -> a
id
    SBvEnc enc
SSigned -> (Bitvec enc n -> Bitvec enc n -> Bitvec enc n
forall a. Num a => a -> a -> a
+Bitvec enc n
1) (Bitvec enc n -> Bitvec enc n)
-> (Bitvec enc n -> Bitvec enc n) -> Bitvec enc n -> Bitvec enc n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b
not
   abs :: Bitvec enc n -> Bitvec enc n
abs Bitvec enc n
x         = if Bitvec enc n -> Bitvec enc n
forall a. Num a => a -> a
signum Bitvec enc n
x Bitvec enc n -> Bitvec enc n -> Bool
forall a. Ord a => a -> a -> Bool
< Bitvec enc n
0 then Bitvec enc n -> Bitvec enc n
forall a. Num a => a -> a
negate Bitvec enc n
x else Bitvec enc n
x
   signum :: Bitvec enc n -> Bitvec enc n
signum Bitvec enc n
x      = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Bitvec enc n
0
    SBvEnc enc
SSigned -> if Bitvec enc n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Bitvec enc n
x Int
0 then -Bitvec enc n
1 else Bitvec enc n
1
   Bitvec enc n
x + :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
+ Bitvec enc n
y = Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec enc n) -> Integer -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
y
   Bitvec enc n
x - :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
- Bitvec enc n
y = Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec enc n) -> Integer -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
y
   Bitvec enc n
x * :: Bitvec enc n -> Bitvec enc n -> Bitvec enc n
* Bitvec enc n
y = Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec enc n) -> Integer -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
y

instance (KnownBvEnc enc, KnownNat n) => Bounded (Bitvec enc n) where
  minBound :: Bitvec enc n
minBound = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n Bit
forall b. Boolean b => b
false
    SBvEnc enc
SSigned -> Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Vector n Bit -> Int -> Vector n Bit
forall a. Bits a => a -> Int -> a
setBit (forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n Bit
forall b. Boolean b => b
false) Int
0
  maxBound :: Bitvec enc n
maxBound = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n Bit
forall b. Boolean b => b
true
    SBvEnc enc
SSigned -> Vector n Bit -> Bitvec enc n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec enc n) -> Vector n Bit -> Bitvec enc n
forall a b. (a -> b) -> a -> b
$ Vector n Bit -> Int -> Vector n Bit
forall a. Bits a => a -> Int -> a
clearBit (forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n Bit
forall b. Boolean b => b
true) Int
0

instance (KnownBvEnc enc, KnownNat n) => Enum (Bitvec enc n) where
  toEnum :: Int -> Bitvec enc n
toEnum     = Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec enc n)
-> (Int -> Integer) -> Int -> Bitvec enc n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
  fromEnum :: Bitvec enc n -> Int
fromEnum Bitvec enc n
x = case forall (enc :: BvEnc). KnownBvEnc enc => SBvEnc enc
bvEncSing @enc of
    SBvEnc enc
SUnsigned -> Vector n Int -> Int
forall a (n :: Nat). (Unbox a, Num a) => Vector n a -> a
V.sum (Vector n Int -> Int)
-> (Vector n Bit -> Vector n Int) -> Vector n Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bit -> Int) -> Vector n Bit -> Vector n Int
forall a b (n :: Nat).
(Unbox a, Unbox b) =>
(Finite n -> a -> b) -> Vector n a -> Vector n b
V.imap (\Finite n
i Bit
b -> if Bit -> Bool
forall a b. Coercible a b => a -> b
coerce Bit
b then Int
2 Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite Finite n
i else Int
0) (Vector n Bit -> Vector n Int)
-> (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Vector n Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector n Bit -> Int) -> Vector n Bit -> Int
forall a b. (a -> b) -> a -> b
$ forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) Bitvec enc n
x
    SBvEnc enc
SSigned -> if Bitvec enc n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Bitvec enc n
x Int
0
          then Int -> Int
forall a. Num a => a -> a
negate (Int -> Int) -> (Vector n Bit -> Int) -> Vector n Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Int) -> (Vector n Bit -> Int) -> Vector n Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Int -> Int
forall a (n :: Nat). (Unbox a, Num a) => Vector n a -> a
V.sum (Vector n Int -> Int)
-> (Vector n Bit -> Vector n Int) -> Vector n Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bit -> Int) -> Vector n Bit -> Vector n Int
forall a b (n :: Nat).
(Unbox a, Unbox b) =>
(Finite n -> a -> b) -> Vector n a -> Vector n b
V.imap (\Finite n
i Bit
b -> if Bit -> Bool
forall a b. Coercible a b => a -> b
coerce Bit
b then Int
2 Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite Finite n
i else Int
0) (Vector n Bit -> Vector n Int)
-> (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Vector n Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector n Bit -> Int) -> Vector n Bit -> Int
forall a b. (a -> b) -> a -> b
$ forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) (Bitvec enc n -> Vector n Bit) -> Bitvec enc n -> Vector n Bit
forall a b. (a -> b) -> a -> b
$ Bitvec enc n -> Bitvec enc n
forall b. Boolean b => b -> b
not Bitvec enc n
x
          else Vector n Int -> Int
forall a (n :: Nat). (Unbox a, Num a) => Vector n a -> a
V.sum (Vector n Int -> Int)
-> (Vector n Bit -> Vector n Int) -> Vector n Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bit -> Int) -> Vector n Bit -> Vector n Int
forall a b (n :: Nat).
(Unbox a, Unbox b) =>
(Finite n -> a -> b) -> Vector n a -> Vector n b
V.imap (\Finite n
i Bit
b -> if Bit -> Bool
forall a b. Coercible a b => a -> b
coerce Bit
b then Int
2 Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite Finite n
i else Int
0) (Vector n Bit -> Vector n Int)
-> (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Vector n Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector n Bit -> Vector n Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector n Bit -> Int) -> Vector n Bit -> Int
forall a b. (a -> b) -> a -> b
$ forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @(V.Vector n Bit) Bitvec enc n
x

instance (KnownBvEnc enc, KnownNat n) => Real (Bitvec enc n) where
  toRational :: Bitvec enc n -> Rational
toRational = Int -> Rational
forall a. Real a => a -> Rational
toRational (Int -> Rational)
-> (Bitvec enc n -> Int) -> Bitvec enc n -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec enc n -> Int
forall a. Enum a => a -> Int
fromEnum

instance (KnownBvEnc enc, KnownNat n) => Integral (Bitvec enc n) where
  toInteger :: Bitvec enc n -> Integer
toInteger = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer)
-> (Bitvec enc n -> Int) -> Bitvec enc n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec enc n -> Int
forall a. Enum a => a -> Int
fromEnum
  quotRem :: Bitvec enc n -> Bitvec enc n -> (Bitvec enc n, Bitvec enc n)
quotRem Bitvec enc n
x Bitvec enc n
y = (Integer -> Bitvec enc n)
-> (Integer -> Bitvec enc n)
-> (Integer, Integer)
-> (Bitvec enc n, Bitvec enc n)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger ((Integer, Integer) -> (Bitvec enc n, Bitvec enc n))
-> (Integer, Integer) -> (Bitvec enc n, Bitvec enc n)
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
x) (Bitvec enc n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec enc n
y)

-- | A Lens on the sign-bit of a signed bitvector.
_signBit :: KnownNat (n + 1) => Lens' (Bitvec Signed (n + 1)) Bit
_signBit :: forall (n :: Nat).
KnownNat (n + 1) =>
Lens' (Bitvec 'Signed (n + 1)) Bit
_signBit = (Bitvec 'Signed (n + 1) -> Bit)
-> (Bitvec 'Signed (n + 1) -> Bit -> Bitvec 'Signed (n + 1))
-> forall {f :: * -> *}.
   Functor f =>
   (Bit -> f Bit)
   -> Bitvec 'Signed (n + 1) -> f (Bitvec 'Signed (n + 1))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\Bitvec 'Signed (n + 1)
bv -> Bool -> Bit
Bit (Bool -> Bit) -> Bool -> Bit
forall a b. (a -> b) -> a -> b
$ Bitvec 'Signed (n + 1) -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Bitvec 'Signed (n + 1)
bv Int
0 )((Bitvec 'Signed (n + 1) -> Bit -> Bitvec 'Signed (n + 1))
 -> forall {f :: * -> *}.
    Functor f =>
    (Bit -> f Bit)
    -> Bitvec 'Signed (n + 1) -> f (Bitvec 'Signed (n + 1)))
-> (Bitvec 'Signed (n + 1) -> Bit -> Bitvec 'Signed (n + 1))
-> forall {f :: * -> *}.
   Functor f =>
   (Bit -> f Bit)
   -> Bitvec 'Signed (n + 1) -> f (Bitvec 'Signed (n + 1))
forall a b. (a -> b) -> a -> b
$
  \Bitvec 'Signed (n + 1)
bv Bit
b -> case Bit
b of
    Bit Bool
False -> Bitvec 'Signed (n + 1) -> Int -> Bitvec 'Signed (n + 1)
forall a. Bits a => a -> Int -> a
clearBit Bitvec 'Signed (n + 1)
bv Int
0
    Bit Bool
True  -> Bitvec 'Signed (n + 1) -> Int -> Bitvec 'Signed (n + 1)
forall a. Bits a => a -> Int -> a
setBit   Bitvec 'Signed (n + 1)
bv Int
0

-- | Concatenation of two bitvectors.
bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
bitvecConcat :: forall (enc :: BvEnc) (n :: Nat) (m :: Nat).
Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
bitvecConcat (Bitvec enc n -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce -> Vector Any Bit
x) (Bitvec enc m -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce -> Vector Any Bit
y) = Vector (Any + Any) Bit -> Bitvec enc (n + m)
forall a b. Coercible a b => a -> b
coerce (Vector (Any + Any) Bit -> Bitvec enc (n + m))
-> Vector (Any + Any) Bit -> Bitvec enc (n + m)
forall a b. (a -> b) -> a -> b
$ Vector Any Bit
x Vector Any Bit -> Vector Any Bit -> Vector (Any + Any) Bit
forall (n :: Nat) (m :: Nat) a.
Unbox a =>
Vector n a -> Vector m a -> Vector (n + m) a
V.++ Vector Any Bit
y

-- | Constructing a bitvector from a list.
bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)
bitvecFromListN :: forall (n :: Nat) (enc :: BvEnc).
KnownNat n =>
[Bit] -> Maybe (Bitvec enc n)
bitvecFromListN = Maybe (Vector n Bit) -> Maybe (Bitvec enc n)
forall a b. Coercible a b => a -> b
coerce (Maybe (Vector n Bit) -> Maybe (Bitvec enc n))
-> ([Bit] -> Maybe (Vector n Bit)) -> [Bit] -> Maybe (Bitvec enc n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a.
(Unbox a, KnownNat n) =>
[a] -> Maybe (Vector n a)
V.fromListN @n

-- | Constructing a bitvector from a list with length given as 'Proxy'.
bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)
bitvecFromListN' :: forall (n :: Nat) (enc :: BvEnc).
KnownNat n =>
Proxy n -> [Bit] -> Maybe (Bitvec enc n)
bitvecFromListN' Proxy n
_ = [Bit] -> Maybe (Bitvec enc n)
forall (n :: Nat) (enc :: BvEnc).
KnownNat n =>
[Bit] -> Maybe (Bitvec enc n)
bitvecFromListN