{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
module RWC.Primitives
      ( Identity, ReacT, StateT, Vec, Finite, Proxy (..)
      , rwPrimAdd
      , rwPrimAnd
      , rwPrimBind
      , rwPrimBitIndex
      , rwPrimBitSlice
      , rwPrimBits
      , rwPrimCryptol
      , rwPrimDiv
      , rwPrimEq
      , rwPrimError
      , rwPrimExtern
      , rwPrimExtrude
      , rwPrimGet
      , rwPrimGt
      , rwPrimGtEq
      , rwPrimLAnd
      , rwPrimLNot
      , rwPrimLOr
      , rwPrimLShift
      , rwPrimLift
      , rwPrimLt
      , rwPrimLtEq
      , rwPrimMSBit
      , rwPrimMod
      , rwPrimMul
      , rwPrimNatVal
      , rwPrimNot
      , rwPrimOr
      , rwPrimPow
      , rwPrimPut
      , rwPrimRAnd
      , rwPrimRNAnd
      , rwPrimRNor
      , rwPrimROr
      , rwPrimRShift
      , rwPrimRShiftArith
      , rwPrimRXNor
      , rwPrimRXOr
      , rwPrimResize
      , rwPrimReturn
      , rwPrimSignal
      , rwPrimSub
      , rwPrimFinite
      , rwPrimFiniteMinBound
      , rwPrimFiniteMaxBound
      , rwPrimToFinite
      , rwPrimToFiniteMod
      , rwPrimFromFinite
      -- , rwPrimVecBulkUpdate
      , rwPrimVecConcat
      , rwPrimVecFromList
      , rwPrimVecIndex
      , rwPrimVecIndexProxy
      , rwPrimVecMap
      , rwPrimVecGenerate
      -- , rwPrimVecIterate
      -- , rwPrimVecZip
      , rwPrimVecRSlice
      , rwPrimVecReplicate
      , rwPrimVecReverse
      , rwPrimVecSlice
      , rwPrimXNor
      , rwPrimXOr
      , toIntegerV
      , type (+), type GHC.Monad, type GHC.MonadTrans, KnownNat
      ) where

-- Imports here serve only the GHC implementations (rwc never translates
-- the bodies in this file).
import Prelude ((.),($))
import qualified Prelude                           as GHC
import qualified Control.Monad.Identity            as GHC
import qualified Control.Monad.Resumption.Reactive as GHC
import qualified Control.Monad.State               as GHC
import qualified Data.Bits                         as GHC
import GHC.TypeLits (Nat, type (+), natVal)
import qualified GHC.TypeLits                      as TL
import qualified Data.Finite                       as F
import qualified Data.Vector.Sized                 as V
import qualified Data.Vector                       as VU
import qualified ReWire.BitWord                    as BW

type Identity   = GHC.Identity
type ReacT      = GHC.ReacT
type StateT     = GHC.StateT
type Integer    = GHC.Integer
type String     = GHC.String
type Bool       = GHC.Bool
type Vec        = V.Vector
type KnownNat   = TL.KnownNat
type Finite     = F.Finite

-- ReWire primitives.

-- Primitive types:
-- data (->) a b
-- data ReacT i o m a
-- data StateT s m a
-- data Identity a
-- data Integer
-- data Bool
-- data String
-- data Vec n a
-- data Finite n
-- data Proxy n

-- Also tuples:
-- data () = ()
-- data (a, b) = (a, b)
-- ...

data Proxy (n :: Nat) = Proxy

-- Definitions in this file are never translated by rwc (rwPrim*
-- references compile to built-ins); the bodies are the GHC
-- implementations.

{-# OPAQUE rwPrimError #-}
rwPrimError :: String -> a
rwPrimError :: forall a. String -> a
rwPrimError = String -> a
forall a. HasCallStack => String -> a
GHC.error

-- | The String and list arguments must be literals (after inlining).
{-# OPAQUE rwPrimExtern #-}
rwPrimExtern :: [(String, Integer)] -- ^ Module parameters (name and integer literal value).
             -> String              -- ^ Clock signal name or empty for no clock.
             -> String              -- ^ Reset signal name or empty for no reset.
             -> [(String, Integer)] -- ^ Module inputs (name and integer literal bitwidth).
             -> [(String, Integer)] -- ^ Module outputs (name and integer literal bitwidth).
             -> String              -- ^ Module name.
             -> a                   -- ^ Haskell definition to use when interpreting.
             -> String              -- ^ Reserved: an instance-name hint; currently ignored by the compiler.
             -> a
rwPrimExtern :: forall a.
[(String, Integer)]
-> String
-> String
-> [(String, Integer)]
-> [(String, Integer)]
-> String
-> a
-> String
-> a
rwPrimExtern [(String, Integer)]
_ String
_ String
_ [(String, Integer)]
_ [(String, Integer)]
_ String
_ a
f String
_ = a
f

-- | The String arguments must be literals (after inlining).
{-# OPAQUE rwPrimCryptol #-}
rwPrimCryptol :: String -- ^ Cryptol module file.
              -> String -- ^ Function name.
              -> a      -- ^ Haskell definition to use when running under GHC.
              -> a
rwPrimCryptol :: forall a. String -> String -> a -> a
rwPrimCryptol String
_ String
_ a
f = a
f

{-# OPAQUE rwPrimBind #-}
rwPrimBind :: GHC.Monad m => m a -> (a -> m b) -> m b
rwPrimBind :: forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
rwPrimBind = m a -> (a -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(GHC.>>=)

{-# OPAQUE rwPrimReturn #-}
rwPrimReturn :: GHC.Monad m => a -> m a
rwPrimReturn :: forall (m :: * -> *) a. Monad m => a -> m a
rwPrimReturn = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
GHC.return

{-# OPAQUE rwPrimPut #-}
rwPrimPut :: GHC.Monad m => s -> StateT s m ()
rwPrimPut :: forall (m :: * -> *) s. Monad m => s -> StateT s m ()
rwPrimPut = s -> StateT s m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
GHC.put

{-# OPAQUE rwPrimGet #-}
rwPrimGet :: GHC.Monad m => StateT s m s
rwPrimGet :: forall (m :: * -> *) s. Monad m => StateT s m s
rwPrimGet = StateT s m s
forall s (m :: * -> *). MonadState s m => m s
GHC.get

{-# OPAQUE rwPrimSignal #-}
rwPrimSignal :: GHC.Monad m => o -> ReacT i o m i
rwPrimSignal :: forall (m :: * -> *) o i. Monad m => o -> ReacT i o m i
rwPrimSignal = o -> ReacT i o m i
forall (m :: * -> *) o i. Monad m => o -> ReacT i o m i
GHC.signal

{-# OPAQUE rwPrimLift #-}
rwPrimLift :: (GHC.MonadTrans t, GHC.Monad m) => m a -> t m a
rwPrimLift :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
rwPrimLift = m a -> t m a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
GHC.lift

{-# OPAQUE rwPrimExtrude #-}
rwPrimExtrude :: GHC.Monad m => ReacT i o (StateT s m) a -> s -> ReacT i o m a
rwPrimExtrude :: forall (m :: * -> *) i o s a.
Monad m =>
ReacT i o (StateT s m) a -> s -> ReacT i o m a
rwPrimExtrude (GHC.ReacT (GHC.StateT s -> m (Either a (o, i -> ReacT i o (StateT s m) a), s)
m)) s
s =
   m (Either a (o, i -> ReacT i o m a)) -> ReacT i o m a
forall input output (m :: * -> *) a.
m (Either a (output, input -> ReacT input output m a))
-> ReacT input output m a
GHC.ReacT (m (Either a (o, i -> ReacT i o m a)) -> ReacT i o m a)
-> m (Either a (o, i -> ReacT i o m a)) -> ReacT i o m a
forall a b. (a -> b) -> a -> b
GHC.$
     do (res,s') <- s -> m (Either a (o, i -> ReacT i o (StateT s m) a), s)
m s
s
        case res of
            GHC.Left a
y -> Either a (o, i -> ReacT i o m a)
-> m (Either a (o, i -> ReacT i o m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
GHC.return (a -> Either a (o, i -> ReacT i o m a)
forall a b. a -> Either a b
GHC.Left a
y)
            GHC.Right (o
o,i -> ReacT i o (StateT s m) a
k) -> Either a (o, i -> ReacT i o m a)
-> m (Either a (o, i -> ReacT i o m a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
GHC.return ((o, i -> ReacT i o m a) -> Either a (o, i -> ReacT i o m a)
forall a b. b -> Either a b
GHC.Right (o
o, \ i
i -> ReacT i o (StateT s m) a -> s -> ReacT i o m a
forall (m :: * -> *) i o s a.
Monad m =>
ReacT i o (StateT s m) a -> s -> ReacT i o m a
rwPrimExtrude (i -> ReacT i o (StateT s m) a
k i
i) s
s'))

-- | Convert an Integer into a @'Finite' n@, throws an error if negative or >= @n@.
{-# OPAQUE rwPrimFinite #-}
rwPrimFinite :: KnownNat n => Integer -> Finite n
rwPrimFinite :: forall (n :: Nat). KnownNat n => Integer -> Finite n
rwPrimFinite = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
F.finite

{-# OPAQUE rwPrimFiniteMinBound #-}
rwPrimFiniteMinBound :: KnownNat n => Finite n
rwPrimFiniteMinBound :: forall (n :: Nat). KnownNat n => Finite n
rwPrimFiniteMinBound = Finite n
forall a. Bounded a => a
GHC.minBound

{-# OPAQUE rwPrimFiniteMaxBound #-}
rwPrimFiniteMaxBound :: KnownNat n => Finite n
rwPrimFiniteMaxBound :: forall (n :: Nat). KnownNat n => Finite n
rwPrimFiniteMaxBound = Finite n
forall a. Bounded a => a
GHC.maxBound

{-# OPAQUE rwPrimToFinite #-}
rwPrimToFinite :: KnownNat n => Vec m Bool -> Finite n
rwPrimToFinite :: forall (n :: Nat) (m :: Nat). KnownNat n => Vec m Bool -> Finite n
rwPrimToFinite = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
F.finite (Integer -> Finite n)
-> (Vec m Bool -> Integer) -> Vec m Bool -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec m Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger'

{-# OPAQUE rwPrimToFiniteMod #-}
rwPrimToFiniteMod :: forall m n. KnownNat n => Vec m Bool -> Finite n
rwPrimToFiniteMod :: forall (m :: Nat) (n :: Nat). KnownNat n => Vec m Bool -> Finite n
rwPrimToFiniteMod Vec m Bool
v = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
F.finite (Vec m Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec m Bool
v Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`GHC.mod` (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall (n :: Nat). Proxy n
Proxy :: Proxy n)))

{-# OPAQUE rwPrimFromFinite #-}
rwPrimFromFinite :: KnownNat m => Finite n -> Vec m Bool
rwPrimFromFinite :: forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> Vec m Bool
rwPrimFromFinite = Integer -> Vec m Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec m Bool)
-> (Finite n -> Integer) -> Finite n -> Vec m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
F.getFinite

-- *** Built-in Vec functions. ***

-- | Turns a List literal into a Vec with fixed length. I.e.,
--
--   > [x, y, z] :: Vec 3 a
{-# OPAQUE rwPrimVecFromList #-}
rwPrimVecFromList :: KnownNat n => [a] -> Vec n a
rwPrimVecFromList :: forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList [a]
v = case [a] -> Maybe (Vec n a)
forall (n :: Nat) a. KnownNat n => [a] -> Maybe (Vector n a)
V.fromList [a]
v of
       GHC.Just Vec n a
v' -> Vec n a
v'
       Maybe (Vec n a)
GHC.Nothing -> String -> Vec n a
forall a. HasCallStack => String -> a
GHC.error String
"failed fromList: list is a different length than expected"

{-# OPAQUE rwPrimVecReplicate #-}
rwPrimVecReplicate :: KnownNat n => a -> Vec n a
rwPrimVecReplicate :: forall (n :: Nat) a. KnownNat n => a -> Vec n a
rwPrimVecReplicate = a -> Vector n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
V.replicate

{-# OPAQUE rwPrimVecReverse #-}
rwPrimVecReverse :: Vec n a -> Vec n a
rwPrimVecReverse :: forall (n :: Nat) a. Vec n a -> Vec n a
rwPrimVecReverse = Vector n a -> Vector n a
forall (n :: Nat) a. Vec n a -> Vec n a
V.reverse

{-# OPAQUE rwPrimVecSlice #-}
rwPrimVecSlice :: (KnownNat i, KnownNat n) => Proxy i -> Vec ((i + n) + m) a -> Vec n a
rwPrimVecSlice :: forall (i :: Nat) (n :: Nat) (m :: Nat) a.
(KnownNat i, KnownNat n) =>
Proxy i -> Vec ((i + n) + m) a -> Vec n a
rwPrimVecSlice = Proxy i -> Vector ((i + n) + m) a -> Vector n a
forall (i :: Nat) (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat i, KnownNat n) =>
p i -> Vector ((i + n) + m) a -> Vector n a
V.slice

-- | Slice indexed from the end of the Vec.
{-# OPAQUE rwPrimVecRSlice #-}
rwPrimVecRSlice :: (KnownNat i, KnownNat n) => Proxy i -> Vec ((i + n) + m) a -> Vec n a
rwPrimVecRSlice :: forall (i :: Nat) (n :: Nat) (m :: Nat) a.
(KnownNat i, KnownNat n) =>
Proxy i -> Vec ((i + n) + m) a -> Vec n a
rwPrimVecRSlice Proxy i
i = Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
V.reverse (Vec n a -> Vec n a)
-> (Vector Vector ((i + n) + m) a -> Vec n a)
-> Vector Vector ((i + n) + m) a
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy i -> Vector Vector ((i + n) + m) a -> Vec n a
forall (i :: Nat) (n :: Nat) (m :: Nat) a (p :: Nat -> *).
(KnownNat i, KnownNat n) =>
p i -> Vector ((i + n) + m) a -> Vector n a
V.slice Proxy i
i (Vector Vector ((i + n) + m) a -> Vec n a)
-> (Vector Vector ((i + n) + m) a -> Vector Vector ((i + n) + m) a)
-> Vector Vector ((i + n) + m) a
-> Vec n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Vector ((i + n) + m) a -> Vector Vector ((i + n) + m) a
forall (n :: Nat) a. Vec n a -> Vec n a
V.reverse

{-# OPAQUE rwPrimVecIndex #-}
rwPrimVecIndex :: Vec n a -> Finite n -> a
rwPrimVecIndex :: forall (n :: Nat) a. Vec n a -> Finite n -> a
rwPrimVecIndex = Vector n a -> Finite n -> a
forall (n :: Nat) a. Vec n a -> Finite n -> a
V.index

{-# OPAQUE rwPrimVecIndexProxy #-}
rwPrimVecIndexProxy :: KnownNat n => Vec ((n + m) + 1) a -> Proxy n -> a
rwPrimVecIndexProxy :: forall (n :: Nat) (m :: Nat) a.
KnownNat n =>
Vec ((n + m) + 1) a -> Proxy n -> a
rwPrimVecIndexProxy = Vector ((n + m) + 1) a -> Proxy n -> a
forall (n :: Nat) (m :: Nat) a (p :: Nat -> *).
KnownNat n =>
Vector ((n + m) + 1) a -> p n -> a
V.index'

{-# OPAQUE rwPrimVecMap #-}
rwPrimVecMap :: (a -> b) -> Vec n a -> Vec n b
rwPrimVecMap :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
rwPrimVecMap = (a -> b) -> Vector n a -> Vector n b
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
V.map

-- rwPrimVecZip :: Vec n a -> Vec n b -> Vec n (a , b)
-- rwPrimVecZip = V.zip

{-# OPAQUE rwPrimVecGenerate #-}
rwPrimVecGenerate :: KnownNat n => (Finite n -> a) -> Vec n a
rwPrimVecGenerate :: forall (n :: Nat) a. KnownNat n => (Finite n -> a) -> Vec n a
rwPrimVecGenerate = (Finite n -> a) -> Vector n a
forall (n :: Nat) a. KnownNat n => (Finite n -> a) -> Vec n a
V.generate

-- rwPrimVecIterate :: KnownNat n => Proxy n -> (a -> a) -> a -> Vec n a
-- rwPrimVecIterate = V.iterateN'

-- | Concatenate vectors.
{-# OPAQUE rwPrimVecConcat #-}
rwPrimVecConcat :: Vec n a -> Vec m a -> Vec (n + m) a
rwPrimVecConcat :: forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
rwPrimVecConcat = Vector n a -> Vector m a -> Vector (n + m) a
forall (n :: Nat) (m :: Nat) a.
Vector n a -> Vector m a -> Vector (n + m) a
(V.++)

-- | Materialize an Integer at exactly the result width, reducing mod 2^n
--   (the shared kernel of the arithmetic reference models, exact at any
--   width).
bitsAt :: forall n . KnownNat n => Integer -> Vec n Bool
bitsAt :: forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt = [Bool] -> Vec n Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList ([Bool] -> Vec n Bool)
-> (Integer -> [Bool]) -> Integer -> Vec n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> [Bool]
BW.intToBits' (Integer -> Int
forall a. Enum a => a -> Int
GHC.fromEnum (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall (n :: Nat). Proxy n
Proxy :: Proxy n)))

-- | Interpret an Integer as a bit vector.
{-# OPAQUE rwPrimBits #-}
rwPrimBits :: Integer -> Vec 128 Bool
rwPrimBits :: Integer -> Vec 128 Bool
rwPrimBits = Integer -> Vec 128 Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt

-- | Truncates or zero-pads most significant bits.
{-# OPAQUE rwPrimResize #-}
rwPrimResize :: forall m n . KnownNat m => Vec n Bool -> Vec m Bool
rwPrimResize :: forall (m :: Nat) (n :: Nat).
KnownNat m =>
Vec n Bool -> Vec m Bool
rwPrimResize Vec n Bool
v = [Bool] -> Vec m Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList [Bool]
vs'
    where
      vs :: [Bool]
vs = Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
v
      vs' :: [Bool]
vs' = Int -> [Bool] -> [Bool]
BW.resize' (Integer -> Int
forall a. Enum a => a -> Int
GHC.fromEnum (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m
forall (n :: Nat). Proxy n
Proxy :: Proxy m))) [Bool]
vs

-- Update multiple indices
-- rwPrimVecBulkUpdate :: KnownNat n => Vec n a -> Vec m (Finite n,a) -> Vec n a
-- rwPrimVecBulkUpdate v a = V.update v (V.map (BF.first fromEnum) a)

-- | Produce integer associated with type-level natural.
{-# OPAQUE rwPrimNatVal #-}
rwPrimNatVal :: KnownNat n => Proxy n -> Integer
rwPrimNatVal :: forall (n :: Nat). KnownNat n => Proxy n -> Integer
rwPrimNatVal = Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal

-- | bitSlice a j i returns bits j (most significant) to i (least significant) from a (j >= i).
--   Bits are numbered with the least significant bit at 0 (Verilog convention);
--   the head of the Vec is the most significant bit.
--   The Finite arguments must be known/literals (after inlining).
{-# OPAQUE rwPrimBitSlice #-}
rwPrimBitSlice :: KnownNat m => Vec n Bool -> Finite n -> Finite n -> Vec m Bool
rwPrimBitSlice :: forall (m :: Nat) (n :: Nat).
KnownNat m =>
Vec n Bool -> Finite n -> Finite n -> Vec m Bool
rwPrimBitSlice Vec n Bool
v Finite n
j Finite n
i = case Vector Bool -> Maybe (Vec m Bool)
forall (n :: Nat) a. KnownNat n => Vector a -> Maybe (Vector n a)
V.toSized (Int -> Int -> Vector Bool -> Vector Bool
forall a. Int -> Int -> Vector a -> Vector a
VU.slice Int
start Int
len (Vec n Bool -> Vector Bool
forall (n :: Nat) a. Vector n a -> Vector a
V.fromSized Vec n Bool
v)) of
      Maybe (Vec m Bool)
GHC.Nothing -> String -> Vec m Bool
forall a. HasCallStack => String -> a
GHC.error String
"rwPrimBitSlice: slice size mismatch"
      GHC.Just Vec m Bool
w  -> Vec m Bool
w
      where start :: Int
start = Vector Bool -> Int
forall a. Vector a -> Int
VU.length (Vec n Bool -> Vector Bool
forall (n :: Nat) a. Vector n a -> Vector a
V.fromSized Vec n Bool
v) Int -> Int -> Int
forall a. Num a => a -> a -> a
GHC.- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
GHC.- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
GHC.fromIntegral (Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
F.getFinite Finite n
j)
            len :: Int
len   = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
GHC.fromIntegral (Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
F.getFinite Finite n
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
GHC.- Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
F.getFinite Finite n
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
GHC.+ Integer
1)

-- | bitIndex a i == bitSlice a i i.
--   The Finite argument must be known/literal (after inlining).
{-# OPAQUE rwPrimBitIndex #-}
rwPrimBitIndex :: Vec n Bool -> Finite n -> Bool
rwPrimBitIndex :: forall (n :: Nat). Vec n Bool -> Finite n -> Bool
rwPrimBitIndex Vec n Bool
v Finite n
i = Vec n Bool -> Vector Bool
forall (n :: Nat) a. Vector n a -> Vector a
V.fromSized Vec n Bool
v Vector Bool -> Int -> Bool
forall a. Vector a -> Int -> a
VU.! (Vector Bool -> Int
forall a. Vector a -> Int
VU.length (Vec n Bool -> Vector Bool
forall (n :: Nat) a. Vector n a -> Vector a
V.fromSized Vec n Bool
v) Int -> Int -> Int
forall a. Num a => a -> a -> a
GHC.- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
GHC.- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
GHC.fromIntegral (Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
F.getFinite Finite n
i))

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

-- | Add (wrapping mod 2^n).
{-# OPAQUE rwPrimAdd #-}
rwPrimAdd :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimAdd :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimAdd Vec n Bool
v Vec n Bool
w = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec n Bool) -> Integer -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
GHC.+ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Subtract (wrapping mod 2^n).
{-# OPAQUE rwPrimSub #-}
rwPrimSub :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimSub :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimSub Vec n Bool
v Vec n Bool
w = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec n Bool) -> Integer -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
GHC.- Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Multiply (wrapping mod 2^n).
{-# OPAQUE rwPrimMul #-}
rwPrimMul :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimMul :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimMul Vec n Bool
v Vec n Bool
w = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec n Bool) -> Integer -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
GHC.* Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Unsigned division. Division by zero yields all-ones (2^n - 1),
--   following the SMT-LIB convention implemented by the compiled RTL and
--   the interpreter.
{-# OPAQUE rwPrimDiv #-}
rwPrimDiv :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimDiv :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimDiv Vec n Bool
v Vec n Bool
w
      | Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
GHC.== Integer
0 = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Integer
forall a. Num a => a -> a
GHC.negate Integer
1)
      | Bool
GHC.otherwise            = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec n Bool) -> Integer -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`GHC.div` Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Unsigned modulus. A zero divisor yields the dividend, following the
--   SMT-LIB convention implemented by the compiled RTL and the
--   interpreter.
{-# OPAQUE rwPrimMod #-}
rwPrimMod :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimMod :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimMod Vec n Bool
v Vec n Bool
w
      | Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
GHC.== Integer
0 = Vec n Bool
v
      | Bool
GHC.otherwise            = Integer -> Vec n Bool
forall (n :: Nat). KnownNat n => Integer -> Vec n Bool
bitsAt (Integer -> Vec n Bool) -> Integer -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`GHC.mod` Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Exponentiation.
{-# OPAQUE rwPrimPow #-}
rwPrimPow :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimPow :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimPow Vec n Bool
v Vec n Bool
w = [Bool] -> Vec n Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList ([Bool] -> Vec n Bool) -> [Bool] -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool] -> [Bool]
BW.power' (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
v) (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
w)

-- | Logical and.
{-# OPAQUE rwPrimLAnd #-}
rwPrimLAnd :: Vec n Bool -> Vec n Bool -> Bool
rwPrimLAnd :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimLAnd Vec n Bool
v Vec n Bool
w = Vec n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or Vec n Bool
v Bool -> Bool -> Bool
GHC.&& Vec n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or Vec n Bool
w

-- | Logical or.
{-# OPAQUE rwPrimLOr #-}
rwPrimLOr :: Vec n Bool -> Vec n Bool -> Bool
rwPrimLOr :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimLOr Vec n Bool
v Vec n Bool
w = Vec n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or Vec n Bool
v Bool -> Bool -> Bool
GHC.|| Vec n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or Vec n Bool
w

-- | Logical not.
{-# OPAQUE rwPrimLNot #-}
rwPrimLNot :: Vec n Bool -> Bool
rwPrimLNot :: forall (n :: Nat). Vector n Bool -> Bool
rwPrimLNot Vec n Bool
v = Bool -> Bool
GHC.not (Vec n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or Vec n Bool
v)  -- note that 'or' acts as 'toBool'

-- | Bitwise and.
{-# OPAQUE rwPrimAnd #-}
rwPrimAnd :: Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimAnd :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimAnd = (Bool -> Bool -> Bool)
-> Vector n Bool -> Vector n Bool -> Vector n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bool -> Bool -> Bool
(GHC.&&)

-- | Bitwise or.
{-# OPAQUE rwPrimOr #-}
rwPrimOr :: Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimOr :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimOr = (Bool -> Bool -> Bool)
-> Vector n Bool -> Vector n Bool -> Vector n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bool -> Bool -> Bool
(GHC.||)

-- | Bitwise not.
{-# OPAQUE rwPrimNot #-}
rwPrimNot :: Vec n Bool -> Vec n Bool
rwPrimNot :: forall (n :: Nat). Vec n Bool -> Vec n Bool
rwPrimNot = (Bool -> Bool) -> Vector n Bool -> Vector n Bool
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
V.map Bool -> Bool
GHC.not

-- | Bitwise exclusive or.
{-# OPAQUE rwPrimXOr #-}
rwPrimXOr :: Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimXOr :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimXOr = (Bool -> Bool -> Bool)
-> Vector n Bool -> Vector n Bool -> Vector n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
GHC.xor

-- | Bitwise exclusive nor.
{-# OPAQUE rwPrimXNor #-}
rwPrimXNor :: Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimXNor :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimXNor = (Bool -> Bool -> Bool)
-> Vector n Bool -> Vector n Bool -> Vector n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
V.zipWith (\ Bool
x Bool
y -> Bool -> Bool
GHC.not (Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
GHC.xor Bool
x Bool
y))

-- | Shift left.
{-# OPAQUE rwPrimLShift #-}
rwPrimLShift :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimLShift :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimLShift Vec n Bool
v Vec n Bool
i = [Bool] -> Vec n Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList ([Bool] -> Vec n Bool) -> [Bool] -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool] -> [Bool]
BW.shiftL' (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
v) (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
i)

-- | Shift right.
{-# OPAQUE rwPrimRShift #-}
rwPrimRShift :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimRShift :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimRShift Vec n Bool
v Vec n Bool
i = [Bool] -> Vec n Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList ([Bool] -> Vec n Bool) -> [Bool] -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool] -> [Bool]
BW.shiftR' (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
v) (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
i)

-- | Shift right, sign-extend.
{-# OPAQUE rwPrimRShiftArith #-}
rwPrimRShiftArith :: KnownNat n => Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimRShiftArith :: forall (n :: Nat).
KnownNat n =>
Vec n Bool -> Vec n Bool -> Vec n Bool
rwPrimRShiftArith Vec n Bool
v Vec n Bool
i = [Bool] -> Vec n Bool
forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
rwPrimVecFromList ([Bool] -> Vec n Bool) -> [Bool] -> Vec n Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool] -> [Bool]
BW.arithShiftR' (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
v) (Vec n Bool -> [Bool]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vec n Bool
i)

-- | Equal.
{-# OPAQUE rwPrimEq #-}
rwPrimEq :: Vec n Bool -> Vec n Bool -> Bool
rwPrimEq :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimEq Vec n Bool
v Vec n Bool
w = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
GHC.== Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Greater-than.
{-# OPAQUE rwPrimGt #-}
rwPrimGt :: Vec n Bool -> Vec n Bool -> Bool
rwPrimGt :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimGt Vec n Bool
v Vec n Bool
w = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
GHC.> Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Greater-than or equal.
{-# OPAQUE rwPrimGtEq #-}
rwPrimGtEq :: Vec n Bool -> Vec n Bool -> Bool
rwPrimGtEq :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimGtEq Vec n Bool
v Vec n Bool
w = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
GHC.>= Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Less-than.
{-# OPAQUE rwPrimLt #-}
rwPrimLt :: Vec n Bool -> Vec n Bool -> Bool
rwPrimLt :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimLt Vec n Bool
v Vec n Bool
w = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
GHC.< Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Less-than or equal.
{-# OPAQUE rwPrimLtEq #-}
rwPrimLtEq :: Vec n Bool -> Vec n Bool -> Bool
rwPrimLtEq :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Bool
rwPrimLtEq Vec n Bool
v Vec n Bool
w = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
GHC.<= Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger' Vec n Bool
w

-- | Reduction and.
{-# OPAQUE rwPrimRAnd #-}
rwPrimRAnd :: Vec n Bool -> Bool
rwPrimRAnd :: forall (n :: Nat). Vector n Bool -> Bool
rwPrimRAnd = Vector n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.and

-- | Reduction nand (NOT of the and-reduction, following the Verilog ~& operator).
{-# OPAQUE rwPrimRNAnd #-}
rwPrimRNAnd :: Vec (1 + n) Bool -> Bool
rwPrimRNAnd :: forall (n :: Nat). Vec (1 + n) Bool -> Bool
rwPrimRNAnd = Bool -> Bool
GHC.not (Bool -> Bool)
-> (Vector Vector (1 + n) Bool -> Bool)
-> Vector Vector (1 + n) Bool
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Vector (1 + n) Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.and

-- | Reduction or.
{-# OPAQUE rwPrimROr #-}
rwPrimROr :: Vec n Bool -> Bool
rwPrimROr :: forall (n :: Nat). Vector n Bool -> Bool
rwPrimROr = Vector n Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or

-- | Reduction nor (NOT of the or-reduction, following the Verilog ~| operator).
{-# OPAQUE rwPrimRNor #-}
rwPrimRNor :: Vec (1 + n) Bool -> Bool
rwPrimRNor :: forall (n :: Nat). Vec (1 + n) Bool -> Bool
rwPrimRNor = Bool -> Bool
GHC.not (Bool -> Bool)
-> (Vector Vector (1 + n) Bool -> Bool)
-> Vector Vector (1 + n) Bool
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Vector (1 + n) Bool -> Bool
forall (n :: Nat). Vector n Bool -> Bool
V.or

-- | Reduction xor.
{-# OPAQUE rwPrimRXOr #-}
rwPrimRXOr :: Vec (1 + n) Bool -> Bool
rwPrimRXOr :: forall (n :: Nat). Vec (1 + n) Bool -> Bool
rwPrimRXOr = (Bool -> Bool -> Bool) -> Vector Vector (1 + n) Bool -> Bool
forall a (n :: Nat). (a -> a -> a) -> Vector (1 + n) a -> a
V.foldl1 Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
GHC.xor

-- | Reduction xnor (NOT of the xor-reduction, following the Verilog ~^ operator).
{-# OPAQUE rwPrimRXNor #-}
rwPrimRXNor :: Vec (1 + n) Bool -> Bool
rwPrimRXNor :: forall (n :: Nat). Vec (1 + n) Bool -> Bool
rwPrimRXNor = Bool -> Bool
GHC.not (Bool -> Bool)
-> (Vec (1 + n) Bool -> Bool) -> Vec (1 + n) Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Bool -> Bool) -> Vec (1 + n) Bool -> Bool
forall a (n :: Nat). (a -> a -> a) -> Vector (1 + n) a -> a
V.foldl1 Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
GHC.xor

-- | Most significant bit.
{-# OPAQUE rwPrimMSBit #-}
rwPrimMSBit :: Vec (1 + n) Bool -> Bool
rwPrimMSBit :: forall (n :: Nat). Vec (1 + n) Bool -> Bool
rwPrimMSBit = Vector (1 + n) Bool -> Bool
forall (n :: Nat) a. Vector (1 + n) a -> a
V.head

-- | The unsigned value of a bit vector, as an Integer. Not a primitive:
--   GHC-only simulation support backing ReWire.Bits.toInteger (Integer is
--   a compile-time-literal-only type in the compiled fragment). It lives
--   here because neither front end translates this module's bodies or
--   chases its imports.
{-# OPAQUE toIntegerV #-}
toIntegerV :: Vec n Bool -> Integer
toIntegerV :: forall (n :: Nat). Vec n Bool -> Integer
toIntegerV = Vec n Bool -> Integer
forall (n :: Nat). Vec n Bool -> Integer
BW.toInteger'