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

module Language.Hasmtlib.Internal.Bitvec where

import Language.Hasmtlib.Boolean
import Language.Hasmtlib.Internal.Render
import Data.ByteString.Builder
import Data.Bit
import Data.Bits
import Data.Coerce
import Data.Finite
import Data.Proxy
import Data.Ratio ((%))
import Data.Bifunctor
import qualified Data.Vector.Unboxed.Sized as V
import GHC.TypeNats

-- | Unsigned and length-indexed bitvector with MSB first.
newtype Bitvec (n :: Nat) = Bitvec { forall (n :: Nat). Bitvec n -> Vector n Bit
unBitvec :: V.Vector n Bit }
  deriving stock (Bitvec n -> Bitvec n -> Bool
(Bitvec n -> Bitvec n -> Bool)
-> (Bitvec n -> Bitvec n -> Bool) -> Eq (Bitvec n)
forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
== :: Bitvec n -> Bitvec n -> Bool
$c/= :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
/= :: Bitvec n -> Bitvec n -> Bool
Eq, Eq (Bitvec n)
Eq (Bitvec n) =>
(Bitvec n -> Bitvec n -> Ordering)
-> (Bitvec n -> Bitvec n -> Bool)
-> (Bitvec n -> Bitvec n -> Bool)
-> (Bitvec n -> Bitvec n -> Bool)
-> (Bitvec n -> Bitvec n -> Bool)
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> Ord (Bitvec n)
Bitvec n -> Bitvec n -> Bool
Bitvec n -> Bitvec n -> Ordering
Bitvec n -> Bitvec n -> Bitvec n
forall (n :: Nat). Eq (Bitvec n)
forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
forall (n :: Nat). Bitvec n -> Bitvec n -> Ordering
forall (n :: Nat). Bitvec n -> Bitvec n -> Bitvec 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
$ccompare :: forall (n :: Nat). Bitvec n -> Bitvec n -> Ordering
compare :: Bitvec n -> Bitvec n -> Ordering
$c< :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
< :: Bitvec n -> Bitvec n -> Bool
$c<= :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
<= :: Bitvec n -> Bitvec n -> Bool
$c> :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
> :: Bitvec n -> Bitvec n -> Bool
$c>= :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bool
>= :: Bitvec n -> Bitvec n -> Bool
$cmax :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bitvec n
max :: Bitvec n -> Bitvec n -> Bitvec n
$cmin :: forall (n :: Nat). Bitvec n -> Bitvec n -> Bitvec n
min :: Bitvec n -> Bitvec n -> Bitvec n
Ord)
  deriving newtype (Bitvec n
Bool -> Bitvec n
Bitvec n -> Bitvec n
Bitvec n -> Bitvec n -> Bitvec n
(Bool -> Bitvec n)
-> Bitvec n
-> Bitvec n
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n -> Bitvec n)
-> Boolean (Bitvec n)
forall (n :: Nat). KnownNat n => Bitvec n
forall (n :: Nat). KnownNat n => Bool -> Bitvec n
forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n
forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n -> Bitvec n
forall b.
(Bool -> b)
-> b
-> b
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b -> b)
-> (b -> b)
-> (b -> b -> b)
-> Boolean b
$cbool :: forall (n :: Nat). KnownNat n => Bool -> Bitvec n
bool :: Bool -> Bitvec n
$ctrue :: forall (n :: Nat). KnownNat n => Bitvec n
true :: Bitvec n
$cfalse :: forall (n :: Nat). KnownNat n => Bitvec n
false :: Bitvec n
$c&& :: forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n -> Bitvec n
&& :: Bitvec n -> Bitvec n -> Bitvec n
$c|| :: forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n -> Bitvec n
|| :: Bitvec n -> Bitvec n -> Bitvec n
$c==> :: forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n -> Bitvec n
==> :: Bitvec n -> Bitvec n -> Bitvec n
$cnot :: forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n
not :: Bitvec n -> Bitvec n
$cxor :: forall (n :: Nat). KnownNat n => Bitvec n -> Bitvec n -> Bitvec n
xor :: Bitvec n -> Bitvec n -> Bitvec n
Boolean)

instance Show (Bitvec n) where
  show :: Bitvec n -> String
show = Vector n Char -> String
forall a (n :: Nat). Unbox a => Vector n a -> [a]
V.toList (Vector n Char -> String)
-> (Bitvec n -> Vector n Char) -> Bitvec 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 n -> Vector n Bit) -> Bitvec 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)

instance Render (Bitvec n) where
  render :: Bitvec n -> Builder
render = String -> Builder
stringUtf8 (String -> Builder) -> (Bitvec n -> String) -> Bitvec n -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> String
forall a. Show a => a -> String
show
  {-# INLINEABLE render #-}

instance KnownNat n => Num (Bitvec n) where
   fromInteger :: Integer -> Bitvec n
fromInteger Integer
x = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n)
-> (Vector n Bit -> Vector n Bit) -> Vector n Bit -> Bitvec 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 n) -> Vector n Bit -> Bitvec 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 n -> Bitvec n
negate        = Bitvec n -> Bitvec n
forall a. a -> a
id
   abs :: Bitvec n -> Bitvec n
abs           = Bitvec n -> Bitvec n
forall a. a -> a
id
   signum :: Bitvec n -> Bitvec n
signum Bitvec n
_      = Bitvec n
0
   (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
x) + :: Bitvec n -> Bitvec n -> Bitvec n
+ (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
y) = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(V.Vector n Bit) (Vector n Bit -> Bitvec n) -> Vector n Bit -> Bitvec n
forall a b. (a -> b) -> a -> b
$ Vector n Bit
x Vector n Bit -> Vector n Bit -> Vector n Bit
forall a. Num a => a -> a -> a
+ Vector n Bit
y
   (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
x) - :: Bitvec n -> Bitvec n -> Bitvec n
- (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
y) = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(V.Vector n Bit) (Vector n Bit -> Bitvec n) -> Vector n Bit -> Bitvec n
forall a b. (a -> b) -> a -> b
$ Vector n Bit
x Vector n Bit -> Vector n Bit -> Vector n Bit
forall a. Num a => a -> a -> a
- Vector n Bit
y
   (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
x) * :: Bitvec n -> Bitvec n -> Bitvec n
* (Bitvec n -> Vector n Bit
forall a b. Coercible a b => a -> b
coerce -> Vector n Bit
y) = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(V.Vector n Bit) (Vector n Bit -> Bitvec n) -> Vector n Bit -> Bitvec n
forall a b. (a -> b) -> a -> b
$ Vector n Bit
x Vector n Bit -> Vector n Bit -> Vector n Bit
forall a. Num a => a -> a -> a
* Vector n Bit
y     
     
instance KnownNat n => Bounded (Bitvec n) where
  minBound :: Bitvec n
minBound = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n) -> Vector n Bit -> Bitvec 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     
  maxBound :: Bitvec n
maxBound = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n) -> Vector n Bit -> Bitvec 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     

instance KnownNat n => Enum (Bitvec n) where
  succ :: Bitvec n -> Bitvec n
succ Bitvec n
x   = Bitvec n
x Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
+ Bitvec n
1
  pred :: Bitvec n -> Bitvec n
pred Bitvec n
x   = Bitvec n
x Bitvec n -> Bitvec n -> Bitvec n
forall a. Num a => a -> a -> a
- Bitvec n
1
  toEnum :: Int -> Bitvec n
toEnum   = Integer -> Bitvec n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec n) -> (Int -> Integer) -> Int -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
  fromEnum :: Bitvec n -> Int
fromEnum = Vector n Int -> Int
forall a (n :: Nat). (Unbox a, Num a) => Vector n a -> a
V.sum (Vector n Int -> Int)
-> (Bitvec n -> Vector n Int) -> Bitvec n -> 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)
-> (Bitvec n -> Vector n Bit) -> Bitvec n -> 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 -> Vector n Bit)
-> (Bitvec n -> Vector n Bit) -> Bitvec n -> Vector n Bit
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 KnownNat n => Real (Bitvec n) where
  toRational :: Bitvec n -> Rational
toRational Bitvec n
x = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Bitvec n -> Int
forall a. Enum a => a -> Int
fromEnum Bitvec n
x) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

instance KnownNat n => Integral (Bitvec n) where
  toInteger :: Bitvec n -> Integer
toInteger = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Bitvec n -> Int) -> Bitvec n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Int
forall a. Enum a => a -> Int
fromEnum
  quotRem :: Bitvec n -> Bitvec n -> (Bitvec n, Bitvec n)
quotRem Bitvec n
x Bitvec n
y = (Integer -> Bitvec n)
-> (Integer -> Bitvec n)
-> (Integer, Integer)
-> (Bitvec n, Bitvec 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 n
forall a. Num a => Integer -> a
fromInteger Integer -> Bitvec n
forall a. Num a => Integer -> a
fromInteger ((Integer, Integer) -> (Bitvec n, Bitvec n))
-> (Integer, Integer) -> (Bitvec n, Bitvec n)
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (Bitvec n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec n
x) (Bitvec n -> Integer
forall a. Integral a => a -> Integer
toInteger Bitvec n
y)

bvReverse :: Bitvec n -> Bitvec n
bvReverse :: forall (n :: Nat). Bitvec n -> Bitvec n
bvReverse = Vector Any Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector Any Bit -> Bitvec n)
-> (Bitvec n -> Vector Any Bit) -> Bitvec n -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Any Bit -> Vector Any Bit
forall a (n :: Nat). Unbox a => Vector n a -> Vector n a
V.reverse (Vector Any Bit -> Vector Any Bit)
-> (Bitvec n -> Vector Any Bit) -> Bitvec n -> Vector Any Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce

bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n
bvReplicate :: forall (n :: Nat). KnownNat n => Bit -> Bitvec n
bvReplicate = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n)
-> (Bit -> Vector n Bit) -> Bit -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a. (KnownNat n, Unbox a) => a -> Vector n a
V.replicate @n

bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n
bvReplicate' :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bit -> Bitvec n
bvReplicate' proxy n
_ = Bit -> Bitvec n
forall (n :: Nat). KnownNat n => Bit -> Bitvec n
bvReplicate

bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n
bvGenerate :: forall (n :: Nat). KnownNat n => (Finite n -> Bit) -> Bitvec n
bvGenerate = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n)
-> ((Finite n -> Bit) -> Vector n Bit)
-> (Finite n -> Bit)
-> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Finite n -> a) -> Vector n a
V.generate @n ((Finite n -> Bit) -> Vector n Bit)
-> ((Finite n -> Bit) -> Finite n -> Bit)
-> (Finite n -> Bit)
-> Vector n Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bit) -> Finite n -> Bit
forall a b. Coercible a b => a -> b
coerce

bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m)
bvConcat :: forall (n :: Nat) (m :: Nat).
Bitvec n -> Bitvec m -> Bitvec (n + m)
bvConcat (Bitvec n -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce -> Vector Any Bit
x) (Bitvec m -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce -> Vector Any Bit
y) = Vector (Any + Any) Bit -> Bitvec (n + m)
forall a b. Coercible a b => a -> b
coerce (Vector (Any + Any) Bit -> Bitvec (n + m))
-> Vector (Any + Any) Bit -> Bitvec (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

bvTake' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec n
bvTake' :: forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bitvec (n + m) -> Bitvec n
bvTake' proxy n
p = Vector n Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector n Bit -> Bitvec n)
-> (Bitvec (n + m) -> Vector n Bit) -> Bitvec (n + m) -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Vector (n + Any) Bit -> Vector n Bit
forall (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat n, Unbox a) =>
p n -> Vector (n + m) a -> Vector n a
V.take' proxy n
p (Vector (n + Any) Bit -> Vector n Bit)
-> (Bitvec (n + m) -> Vector (n + Any) Bit)
-> Bitvec (n + m)
-> Vector n Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec (n + m) -> Vector (n + Any) Bit
forall a b. Coercible a b => a -> b
coerce

bvDrop' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec m
bvDrop' :: forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bitvec (n + m) -> Bitvec m
bvDrop' proxy n
p = Vector Any Bit -> Bitvec m
forall a b. Coercible a b => a -> b
coerce (Vector Any Bit -> Bitvec m)
-> (Bitvec (n + m) -> Vector Any Bit) -> Bitvec (n + m) -> Bitvec m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Vector (n + Any) Bit -> Vector Any Bit
forall (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat n, Unbox a) =>
p n -> Vector (n + m) a -> Vector m a
V.drop' proxy n
p (Vector (n + Any) Bit -> Vector Any Bit)
-> (Bitvec (n + m) -> Vector (n + Any) Bit)
-> Bitvec (n + m)
-> Vector Any Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec (n + m) -> Vector (n + Any) Bit
forall a b. Coercible a b => a -> b
coerce

bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n+m) -> (Bitvec n, Bitvec m)
bvSplitAt' :: forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bitvec (n + m) -> (Bitvec n, Bitvec m)
bvSplitAt' proxy n
p = (Vector n Bit, Vector Any Bit) -> (Bitvec n, Bitvec m)
forall a b. Coercible a b => a -> b
coerce ((Vector n Bit, Vector Any Bit) -> (Bitvec n, Bitvec m))
-> (Bitvec (n + m) -> (Vector n Bit, Vector Any Bit))
-> Bitvec (n + m)
-> (Bitvec n, Bitvec m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Vector (n + Any) Bit -> (Vector n Bit, Vector Any Bit)
forall (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat n, Unbox a) =>
p n -> Vector (n + m) a -> (Vector n a, Vector m a)
V.splitAt' proxy n
p (Vector (n + Any) Bit -> (Vector n Bit, Vector Any Bit))
-> (Bitvec (n + m) -> Vector (n + Any) Bit)
-> Bitvec (n + m)
-> (Vector n Bit, Vector Any Bit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec (n + m) -> Vector (n + Any) Bit
forall a b. Coercible a b => a -> b
coerce

bvToList :: Bitvec n -> [Bit]
bvToList :: forall (n :: Nat). Bitvec n -> [Bit]
bvToList = Vector Any Bit -> [Bit]
forall a (n :: Nat). Unbox a => Vector n a -> [a]
V.toList (Vector Any Bit -> [Bit])
-> (Bitvec n -> Vector Any Bit) -> Bitvec n -> [Bit]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Vector Any Bit
forall a b. Coercible a b => a -> b
coerce

bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN :: forall (n :: Nat). KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN = Maybe (Vector n Bit) -> Maybe (Bitvec n)
forall a b. Coercible a b => a -> b
coerce (Maybe (Vector n Bit) -> Maybe (Bitvec n))
-> ([Bit] -> Maybe (Vector n Bit)) -> [Bit] -> Maybe (Bitvec 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

bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n)
bvFromListN' :: forall (n :: Nat).
KnownNat n =>
Proxy n -> [Bit] -> Maybe (Bitvec n)
bvFromListN' Proxy n
_ = [Bit] -> Maybe (Bitvec n)
forall (n :: Nat). KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN

bvRotL :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n
bvRotL :: forall (n :: Nat) (i :: Nat).
KnownNat (Mod i n) =>
Proxy i -> Bitvec n -> Bitvec n
bvRotL Proxy i
_ (Bitvec n -> Vector (Mod i n + Any) Bit
forall a b. Coercible a b => a -> b
coerce -> Vector (Mod i n + Any) Bit
x) = Vector (Any + Mod i n) Bit -> Bitvec n
forall a b. Coercible a b => a -> b
coerce (Vector (Any + Mod i n) Bit -> Bitvec n)
-> Vector (Any + Mod i n) Bit -> Bitvec n
forall a b. (a -> b) -> a -> b
$ Vector Any Bit
r Vector Any Bit
-> Vector (Mod i n) Bit -> Vector (Any + Mod i n) Bit
forall (n :: Nat) (m :: Nat) a.
Unbox a =>
Vector n a -> Vector m a -> Vector (n + m) a
V.++ Vector (Mod i n) Bit
l
  where
    (Vector (Mod i n) Bit
l, Vector Any Bit
r) = Proxy (Mod i n)
-> Vector (Mod i n + Any) Bit
-> (Vector (Mod i n) Bit, Vector Any Bit)
forall (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat n, Unbox a) =>
p n -> Vector (n + m) a -> (Vector n a, Vector m a)
V.splitAt' (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Mod i n)) Vector (Mod i n + Any) Bit
x

bvRotR :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n
bvRotR :: forall (n :: Nat) (i :: Nat).
KnownNat (Mod i n) =>
Proxy i -> Bitvec n -> Bitvec n
bvRotR Proxy i
p = Bitvec n -> Bitvec n
forall (n :: Nat). Bitvec n -> Bitvec n
bvReverse (Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n) -> Bitvec n -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy i -> Bitvec n -> Bitvec n
forall (n :: Nat) (i :: Nat).
KnownNat (Mod i n) =>
Proxy i -> Bitvec n -> Bitvec n
bvRotL Proxy i
p (Bitvec n -> Bitvec n)
-> (Bitvec n -> Bitvec n) -> Bitvec n -> Bitvec n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Bitvec n
forall (n :: Nat). Bitvec n -> Bitvec n
bvReverse

bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvShL :: forall (n :: Nat).
KnownNat n =>
Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvShL Bitvec n
x Bitvec n
y = [Bit] -> Maybe (Bitvec n)
forall (n :: Nat). KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN ([Bit] -> Maybe (Bitvec n)) -> [Bit] -> Maybe (Bitvec n)
forall a b. (a -> b) -> a -> b
$ ([Bit] -> [Bit] -> [Bit]
forall a. [a] -> [a] -> [a]
++ Int -> Bit -> [Bit]
forall a. Int -> a -> [a]
replicate Int
i Bit
forall b. Boolean b => b
false) ([Bit] -> [Bit]) -> [Bit] -> [Bit]
forall a b. (a -> b) -> a -> b
$ Int -> [Bit] -> [Bit]
forall a. Int -> [a] -> [a]
drop Int
i ([Bit] -> [Bit]) -> [Bit] -> [Bit]
forall a b. (a -> b) -> a -> b
$ Bitvec n -> [Bit]
forall (n :: Nat). Bitvec n -> [Bit]
bvToList Bitvec n
x
  where 
    i :: Int
i = Bitvec n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Bitvec n
y 
    
bvLShR :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvLShR :: forall (n :: Nat).
KnownNat n =>
Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvLShR Bitvec n
x Bitvec n
y = (Bitvec n -> Bitvec n) -> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bitvec n -> Bitvec n
forall (n :: Nat). Bitvec n -> Bitvec n
bvReverse (Maybe (Bitvec n) -> Maybe (Bitvec n))
-> Maybe (Bitvec n) -> Maybe (Bitvec n)
forall a b. (a -> b) -> a -> b
$ [Bit] -> Maybe (Bitvec n)
forall (n :: Nat). KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN ([Bit] -> Maybe (Bitvec n)) -> [Bit] -> Maybe (Bitvec n)
forall a b. (a -> b) -> a -> b
$ ([Bit] -> [Bit] -> [Bit]
forall a. [a] -> [a] -> [a]
++ Int -> Bit -> [Bit]
forall a. Int -> a -> [a]
replicate Int
i Bit
forall b. Boolean b => b
false) ([Bit] -> [Bit]) -> [Bit] -> [Bit]
forall a b. (a -> b) -> a -> b
$ Int -> [Bit] -> [Bit]
forall a. Int -> [a] -> [a]
drop Int
i ([Bit] -> [Bit]) -> [Bit] -> [Bit]
forall a b. (a -> b) -> a -> b
$ Bitvec n -> [Bit]
forall (n :: Nat). Bitvec n -> [Bit]
bvToList (Bitvec n -> [Bit]) -> Bitvec n -> [Bit]
forall a b. (a -> b) -> a -> b
$ Bitvec n -> Bitvec n
forall (n :: Nat). Bitvec n -> Bitvec n
bvReverse Bitvec n
x
  where 
    i :: Int
i = Bitvec n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Bitvec n
y 
  
bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n+i)
bvZeroExtend :: forall (i :: Nat) (n :: Nat).
KnownNat i =>
Proxy i -> Bitvec n -> Bitvec (n + i)
bvZeroExtend Proxy i
p Bitvec n
x = Bitvec n -> Bitvec i -> Bitvec (n + i)
forall (n :: Nat) (m :: Nat).
Bitvec n -> Bitvec m -> Bitvec (n + m)
bvConcat Bitvec n
x (Bitvec i -> Bitvec (n + i)) -> Bitvec i -> Bitvec (n + i)
forall a b. (a -> b) -> a -> b
$ Proxy i -> Bit -> Bitvec i
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bit -> Bitvec n
bvReplicate' Proxy i
p Bit
forall b. Boolean b => b
false 
  
bvExtract :: forall n i j. 
  ( KnownNat i, KnownNat ((j - i) + 1)
  , (i+(n-i)) ~ n
  , (((j - i) + 1) + ((n - i)-((j - i) + 1))) ~ (n - i)
  ) => Proxy i -> Proxy j -> Bitvec n -> Bitvec (( j - i ) + 1)
bvExtract :: forall (n :: Nat) (i :: Nat) (j :: Nat).
(KnownNat i, KnownNat ((j - i) + 1), (i + (n - i)) ~ n,
 (((j - i) + 1) + ((n - i) - ((j - i) + 1))) ~ (n - i)) =>
Proxy i -> Proxy j -> Bitvec n -> Bitvec ((j - i) + 1)
bvExtract Proxy i
pri Proxy j
_ Bitvec n
x = forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bitvec (n + m) -> Bitvec n
bvTake' @_ @((n-i)-((j-i)+1)) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @((j-i)+1)) Bitvec (((j - i) + 1) + ((n - i) - ((j - i) + 1)))
Bitvec (n - i)
x'
  where
    Bitvec (n - i)
x' :: Bitvec (n-i) = Proxy i -> Bitvec (i + (n - i)) -> Bitvec (n - i)
forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Bitvec (n + m) -> Bitvec m
bvDrop' Proxy i
pri Bitvec n
Bitvec (i + (n - i))
x