{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RoleAnnotations #-}
module Language.Hasmtlib.Type.Bitvec
(
BvEnc(..), SBvEnc(..), KnownBvEnc(..)
, bvEncSing', bvEncSing''
, Bitvec(..)
, bitvecConcat
, asUnsigned, asSigned
, bitvecFromListN, bitvecFromListN'
, _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
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)
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)
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
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
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
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)
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)
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)
_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
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
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
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