{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module ReWire.Bits where

import ReWire
import ReWire.Finite
import Prelude hiding (head, (<>), (==), (-), (^), (&&), (||))

type Lit = W 128

zero :: Bit
zero :: Bit
zero = Bit
False

one :: Bit
one :: Bit
one = Bit
True

{-# INLINE bit #-}
bit :: W 1 -> Bit
bit :: W 1 -> Bit
bit = W 1 -> Bit
W (1 + 0) -> Bit
forall (n :: Natural). W (1 + n) -> Bit
msbit

-- | The unsigned value of a bit vector, as an Integer. A GHC-only
--   convenience for simulation and testing: rwc does not compile uses of
--   this function (Integer is a compile-time-literal-only type in the
--   compiled fragment).
{-# INLINE toInteger #-}
toInteger :: W n -> Integer
toInteger :: forall (n :: Natural). W n -> Integer
toInteger = Vec n Bit -> Integer
forall (n :: Natural). W n -> Integer
toIntegerV

-- | Project range of bits.
--   a @@ (j, i) returns bits j (most significant) to i (least significant) from a (j >= i).
--   The Integer arguments must be non-negative integer literals (after inlining).
{-# INLINE (@@) #-}
(@@) :: (KnownNat n,KnownNat m) => W n -> (Integer, Integer) -> W m
W n
a @@ :: forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) =>
W n -> (Integer, Integer) -> W m
@@ (Integer
j, Integer
i) = W n -> Integer -> Integer -> W m
forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) =>
W n -> Integer -> Integer -> W m
bitSlice W n
a Integer
j Integer
i

-- | Project single bit.
--   The Integer argument must be a non-negative integer literal (after inlining).
{-# INLINE (@.) #-}
(@.) :: KnownNat n => W n -> Integer -> Bit
W n
a @. :: forall (n :: Natural). KnownNat n => W n -> Integer -> Bit
@. Integer
i = W n -> Integer -> Bit
forall (n :: Natural). KnownNat n => W n -> Integer -> Bit
bitIndex W n
a Integer
i

-- infixr 9 @., @@

-- *** Primitive bitwise operations based on Verilog operators.

infixr 9 **
infixl 8  *, /, %
infixl 7  +, -
infixl 6  <<., >>., >>>
infixl 6  >, >=, <, <=
infixr 6  <>
infixl 5  .&.
infixl 4  ^, ~^, `xor`
infixl 3  .|.
infixr 2  &&., &&&
infixr 1  ||., |||

-- | Interpret an Integer literal into a bit vector. Truncates most significant
--   bits or zero-pads to make it fit.
{-# INLINE lit #-}
lit :: KnownNat n => Integer -> W n
lit :: forall (n :: Natural). KnownNat n => Integer -> W n
lit Integer
i = Vec 128 Bit -> Vec n Bit
forall (m :: Natural) (n :: Natural).
KnownNat m =>
Vec n Bit -> Vec m Bit
rwPrimResize (Integer -> Vec 128 Bit
rwPrimBits Integer
i :: Lit)

-- | Resize bitvector, truncating or zero padding most significant bits.
{-# INLINE resize #-}
resize :: KnownNat m => W n -> W m
resize :: forall (m :: Natural) (n :: Natural).
KnownNat m =>
Vec n Bit -> Vec m Bit
resize = Vec n Bit -> Vec m Bit
forall (m :: Natural) (n :: Natural).
KnownNat m =>
Vec n Bit -> Vec m Bit
rwPrimResize

-- | Sign-extend a bitvector by @m@ bits (the result width is inferred
--   from the use site). Compiles to the idiomatic replicated-msb
--   concatenation.
{-# INLINE sext #-}
sext :: KnownNat m => W (1 + n) -> W (m + (1 + n))
sext :: forall (m :: Natural) (n :: Natural).
KnownNat m =>
W (1 + n) -> W (m + (1 + n))
sext W (1 + n)
w = Bit -> Vec m Bit
forall (n :: Natural) a. KnownNat n => a -> Vec n a
rwPrimVecReplicate (W (1 + n) -> Bit
forall (n :: Natural). W (1 + n) -> Bit
msbit W (1 + n)
w) Vec m Bit -> W (1 + n) -> Vector Vector (m + (1 + n)) Bit
forall (n :: Natural) a (m :: Natural).
Vec n a -> Vec m a -> Vec (n + m) a
`rwPrimVecConcat` W (1 + n)
w

{-# INLINE bitSlice #-}
bitSlice :: (KnownNat n, KnownNat m) => W n -> Integer -> Integer -> W m
bitSlice :: forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) =>
W n -> Integer -> Integer -> W m
bitSlice W n
v Integer
j Integer
i = W n -> Finite n -> Finite n -> W m
forall (m :: Natural) (n :: Natural).
KnownNat m =>
W n -> Finite n -> Finite n -> W m
finBitSlice W n
v (Integer -> Finite n
forall (n :: Natural). KnownNat n => Integer -> Finite n
finite Integer
j) (Integer -> Finite n
forall (n :: Natural). KnownNat n => Integer -> Finite n
finite Integer
i)

{-# INLINE bitIndex #-}
bitIndex :: KnownNat n => W n -> Integer -> Bit
bitIndex :: forall (n :: Natural). KnownNat n => W n -> Integer -> Bit
bitIndex W n
v Integer
i = W n -> Finite n -> Bit
forall (n :: Natural). W n -> Finite n -> Bit
finBitIndex W n
v (Integer -> Finite n
forall (n :: Natural). KnownNat n => Integer -> Finite n
finite Integer
i)

{-# INLINE finBitSlice #-}
finBitSlice :: KnownNat m => W n -> Finite n -> Finite n -> W m
finBitSlice :: forall (m :: Natural) (n :: Natural).
KnownNat m =>
W n -> Finite n -> Finite n -> W m
finBitSlice = Vec n Bit -> Finite n -> Finite n -> Vec m Bit
forall (m :: Natural) (n :: Natural).
KnownNat m =>
W n -> Finite n -> Finite n -> W m
rwPrimBitSlice

{-# INLINE finBitIndex #-}
finBitIndex :: W n -> Finite n -> Bit
finBitIndex :: forall (n :: Natural). W n -> Finite n -> Bit
finBitIndex = Vec n Bit -> Finite n -> Bit
forall (n :: Natural). W n -> Finite n -> Bit
rwPrimBitIndex

-- | Add.
{-# INLINE (+) #-}
(+) :: KnownNat n => W n -> W n -> W n
+ :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(+) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimAdd

-- | Subtract.
{-# INLINE (-) #-}
(-) :: KnownNat n => W n -> W n -> W n
(-) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimSub

-- | Multiply.
{-# INLINE (*) #-}
(*) :: KnownNat n => W n -> W n -> W n
* :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(*) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimMul

-- | Unsigned division. Division by zero yields all-ones (2^n - 1),
--   following the SMT-LIB convention (compiled RTL, the interpreter, and
--   the GHC implementation agree).
{-# INLINE (/) #-}
(/) :: KnownNat n => W n -> W n -> W n
/ :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(/) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimDiv

-- | Unsigned modulus. A zero divisor yields the dividend, following the
--   SMT-LIB convention (compiled RTL, the interpreter, and the GHC
--   implementation agree).
{-# INLINE (%) #-}
(%) :: KnownNat n => W n -> W n -> W n
% :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(%) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimMod

-- | Exponentiation.
{-# INLINE (**) #-}
(**) :: KnownNat n => W n -> W n -> W n
** :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(**) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimPow

-- | Prelude (&&), but using built-ins.
{-# INLINE (&&&) #-}
(&&&) :: Bool -> Bool -> Bool
&&& :: Bit -> Bit -> Bit
(&&&) Bit
a Bit
b = W 1 -> Bit
bit (W 1 -> Bit) -> W 1 -> Bit
forall a b. (a -> b) -> a -> b
$ ([Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
a] :: W 1) W 1 -> W 1 -> W 1
forall (n :: Natural). W n -> W n -> W n
.&. ([Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
b] :: W 1)

-- | Prelude (||), but using built-ins.
{-# INLINE (|||) #-}
(|||) :: Bool -> Bool -> Bool
||| :: Bit -> Bit -> Bit
(|||) Bit
a Bit
b = W 1 -> Bit
bit (W 1 -> Bit) -> W 1 -> Bit
forall a b. (a -> b) -> a -> b
$ ([Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
a] :: W 1) W 1 -> W 1 -> W 1
forall (n :: Natural). W n -> W n -> W n
.|. ([Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
b] :: W 1)

-- | Logical and.
{-# INLINE (&&.) #-}
(&&.) :: W n -> W n -> Bool
&&. :: forall (n :: Natural). W n -> W n -> Bit
(&&.) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimLAnd

-- | Logical or.
{-# INLINE (||.) #-}
(||.) :: W n -> W n -> Bool
||. :: forall (n :: Natural). W n -> W n -> Bit
(||.) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimLOr

-- | Logical not.
{-# INLINE lnot #-}
lnot :: W n -> Bit
lnot :: forall (n :: Natural). W n -> Bit
lnot = Vec n Bit -> Bit
forall (n :: Natural). W n -> Bit
rwPrimLNot

-- | Bitwise and.
{-# INLINE (.&.) #-}
(.&.) :: W n -> W n -> W n
.&. :: forall (n :: Natural). W n -> W n -> W n
(.&.) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). W n -> W n -> W n
rwPrimAnd

-- | Bitwise or.
{-# INLINE (.|.) #-}
(.|.) :: W n -> W n -> W n
.|. :: forall (n :: Natural). W n -> W n -> W n
(.|.) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). W n -> W n -> W n
rwPrimOr

-- | Bitwise not.
{-# INLINE bnot #-}
bnot :: W n -> W n
bnot :: forall (n :: Natural). W n -> W n
bnot = Vec n Bit -> Vec n Bit
forall (n :: Natural). W n -> W n
rwPrimNot

-- | Bitwise exclusive or.
{-# INLINE (^) #-}
(^) :: W n -> W n -> W n
^ :: forall (n :: Natural). W n -> W n -> W n
(^) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). W n -> W n -> W n
rwPrimXOr

-- | Logical xor, for Bit/Bool (using the built-in operator).
{-# INLINE xor #-}
xor :: Bool -> Bool -> Bool
xor :: Bit -> Bit -> Bit
xor Bit
a Bit
b = W 1 -> Bit
bit (W 1 -> Bit) -> W 1 -> Bit
forall a b. (a -> b) -> a -> b
$ [Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
a] W 1 -> W 1 -> W 1
forall (n :: Natural). W n -> W n -> W n
^ [Bit] -> W 1
forall (n :: Natural) a. KnownNat n => [a] -> Vec n a
fromList [Bit
b]

-- | Bitwise exclusive nor.
{-# INLINE (~^) #-}
(~^) :: W n -> W n -> W n
~^ :: forall (n :: Natural). W n -> W n -> W n
(~^) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). W n -> W n -> W n
rwPrimXNor

-- | Shift left.
{-# INLINE (<<.) #-}
(<<.) :: KnownNat n => W n -> W n -> W n
<<. :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(<<.) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimLShift

-- | Shift right.
{-# INLINE (>>.) #-}
(>>.) :: KnownNat n => W n -> W n -> W n
>>. :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(>>.) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimRShift

-- | Shift right, sign-extend.
{-# INLINE (>>>) #-}
(>>>) :: KnownNat n => W n -> W n -> W n
>>> :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
(>>>) = Vec n Bit -> Vec n Bit -> Vec n Bit
forall (n :: Natural). KnownNat n => W n -> W n -> W n
rwPrimRShiftArith

-- Could implement on Vec (m + n)? Could also reimplement Lshift/Rshift to use Proxy?
-- | Rotate right
{-# INLINE rotR #-}
rotR :: KnownNat m => W m -> W m -> W m
rotR :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
rotR W m
n W m
w = (W m
w W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
>>. W m
n) W m -> W m -> W m
forall (n :: Natural). W n -> W n -> W n
.|. (W m
w W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
<<. (Integer -> W m
forall (n :: Natural). KnownNat n => Integer -> W n
lit (W m -> Integer
forall (n :: Natural) a. KnownNat n => Vec n a -> Integer
len W m
w) W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
- W m
n))

-- | Rotate left
{-# INLINE rotL #-}
rotL :: KnownNat m => W m -> W m -> W m
rotL :: forall (n :: Natural). KnownNat n => W n -> W n -> W n
rotL W m
n W m
w = (W m
w W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
<<. W m
n) W m -> W m -> W m
forall (n :: Natural). W n -> W n -> W n
.|. (W m
w W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
>>. (Integer -> W m
forall (n :: Natural). KnownNat n => Integer -> W n
lit (W m -> Integer
forall (n :: Natural) a. KnownNat n => Vec n a -> Integer
len W m
w) W m -> W m -> W m
forall (n :: Natural). KnownNat n => W n -> W n -> W n
- W m
n))

-- | Equal.
{-# INLINE (==) #-}
(==) :: W n -> W n -> Bool
== :: forall (n :: Natural). W n -> W n -> Bit
(==) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimEq

-- | Not equal.
{-# INLINE (/=) #-}
(/=) :: W n -> W n -> Bool
/= :: forall (n :: Natural). W n -> W n -> Bit
(/=) W n
a W n
b = Bit -> Bit
not (W n
a W n -> W n -> Bit
forall (n :: Natural). W n -> W n -> Bit
== W n
b)

-- | Greater-than.
{-# INLINE (>) #-}
(>) :: W n -> W n -> Bool
> :: forall (n :: Natural). W n -> W n -> Bit
(>) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimGt

-- | Greater-than or equal.
{-# INLINE (>=) #-}
(>=) :: W n -> W n -> Bool
>= :: forall (n :: Natural). W n -> W n -> Bit
(>=) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimGtEq

-- | Less-than.
{-# INLINE (<) #-}
(<) :: W n -> W n -> Bool
< :: forall (n :: Natural). W n -> W n -> Bit
(<) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimLt

-- | Less-than or equal.
{-# INLINE (<=) #-}
(<=) :: W n -> W n -> Bool
<= :: forall (n :: Natural). W n -> W n -> Bit
(<=) = Vec n Bit -> Vec n Bit -> Bit
forall (n :: Natural). W n -> W n -> Bit
rwPrimLtEq

-- | Concatenate.
{-# INLINE (<>) #-}
(<>) :: W n -> W m -> W (n + m)
<> :: forall (n :: Natural) (m :: Natural). W n -> W m -> W (n + m)
(<>) = Vec n Bit -> Vec m Bit -> Vec (n + m) Bit
forall (n :: Natural) a (m :: Natural).
Vec n a -> Vec m a -> Vec (n + m) a
rwPrimVecConcat

-- | Reduction and.
{-# INLINE rAnd #-}
rAnd :: W n -> Bit
rAnd :: forall (n :: Natural). W n -> Bit
rAnd = Vec n Bit -> Bit
forall (n :: Natural). W n -> Bit
rwPrimRAnd

-- | Reduction nand.
{-# INLINE rNAnd #-}
rNAnd :: W (1 + n) -> Bit
rNAnd :: forall (n :: Natural). W (1 + n) -> Bit
rNAnd = Vec (1 + n) Bit -> Bit
forall (n :: Natural). W (1 + n) -> Bit
rwPrimRNAnd

-- | Reduction or.
{-# INLINE rOr #-}
rOr :: W n -> Bit
rOr :: forall (n :: Natural). W n -> Bit
rOr = Vec n Bit -> Bit
forall (n :: Natural). W n -> Bit
rwPrimROr

-- | Reduction nor.
{-# INLINE rNor #-}
rNor :: W (1 + n) -> Bit
rNor :: forall (n :: Natural). W (1 + n) -> Bit
rNor = Vec (1 + n) Bit -> Bit
forall (n :: Natural). W (1 + n) -> Bit
rwPrimRNor

-- | Reduction xor.
{-# INLINE rXOr #-}
rXOr :: W (1 + n) -> Bit
rXOr :: forall (n :: Natural). W (1 + n) -> Bit
rXOr = Vec (1 + n) Bit -> Bit
forall (n :: Natural). W (1 + n) -> Bit
rwPrimRXOr

-- | Reduction xnor.
{-# INLINE rXNor #-}
rXNor :: W (1 + n) -> Bit
rXNor :: forall (n :: Natural). W (1 + n) -> Bit
rXNor = Vec (1 + n) Bit -> Bit
forall (n :: Natural). W (1 + n) -> Bit
rwPrimRXNor

-- | Most significant bit.
{-# INLINE msbit #-}
msbit :: W (1 + n) -> Bit
msbit :: forall (n :: Natural). W (1 + n) -> Bit
msbit = Vec (1 + n) Bit -> Bit
forall (n :: Natural). W (1 + n) -> Bit
rwPrimMSBit

-- | Least significant bit.
{-# INLINE odd #-}
odd :: W (1 + n) -> Bool
odd :: forall (n :: Natural). W (1 + n) -> Bit
odd W (1 + n)
b = W 1 -> Bit
bit (W (1 + n) -> W 1
forall (m :: Natural) (n :: Natural).
KnownNat m =>
Vec n Bit -> Vec m Bit
resize W (1 + n)
b :: W 1)

-- | Negation of the least significant bit.
{-# INLINE even #-}
even :: W (1 + n) -> Bool
even :: forall (n :: Natural). W (1 + n) -> Bit
even W (1 + n)
b = Bit -> Bit
not (W 1 -> Bit
bit (W (1 + n) -> W 1
forall (m :: Natural) (n :: Natural).
KnownNat m =>
Vec n Bit -> Vec m Bit
resize W (1 + n)
b :: W 1))