{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2017     , Google Inc.
                  2019     , Myrtle Software Ltd,
                  2021     , QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

Self-synchronizing circuits based on data-flow principles.
-}

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoGeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE Safe #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}
{-# OPTIONS_HADDOCK show-extensions #-}

module Clash.Prelude.DataFlow {-# DEPRECATED "Module will be removed in Clash 1.10 in favor of clash-protocols. See: https://github.com/clash-lang/clash-protocols/." #-}
  ( -- * Data types
    DataFlow (..)
    -- * Creating DataFlow circuits
  , liftDF
  , pureDF
  , mealyDF
  , mooreDF
  , fifoDF
    -- * Composition combinators
  , idDF
  , seqDF
  , firstDF
  , swapDF
  , secondDF
  , parDF
  , parNDF
  , loopDF
  , loopDF_nobuf
    -- * Lock-Step operation
  , LockStep (..)
  )
where

import GHC.TypeLits           (KnownNat, type (+), type (^))
import Prelude
  hiding ((++), (!!), length, map, repeat, tail, unzip3, zip3, zipWith)

import Clash.Class.BitPack    (boolToBV)
import Clash.Class.Resize     (truncateB)
import Clash.Class.BitPack.BitIndex (msb)
import Clash.Explicit.Mealy   (mealyB)
import Clash.Promoted.Nat     (SNat)
import Clash.Signal           (KnownDomain, (.&&.))
import Clash.Signal.Bundle    (Bundle (..))
import Clash.Explicit.Signal  (Clock, Reset, Signal, Enable, andEnable, register)
import Clash.Sized.BitVector  (BitVector)
import Clash.Sized.Vector
import Clash.XException       (errorX, NFDataX)

{- | Dataflow circuit with bidirectional synchronization channels.

In the /forward/ direction we assert /validity/ of the data. In the /backward/
direction we assert that the circuit is /ready/ to receive new data. A circuit
adhering to the 'DataFlow' type should:

 * Not consume data when validity is deasserted.
 * Only update its output when readiness is asserted.

The 'DataFlow' type is defined as:

@
newtype DataFlow' dom iEn oEn i o
  = DF
  { df :: 'Signal' dom i     -- Incoming data
       -> 'Signal' dom iEn   -- Flagged with \/valid\/ bits \@iEn\@.
       -> 'Signal' dom oEn   -- Incoming back-pressure, \/ready\/ edge.
       -> ( 'Signal' dom o   -- Outgoing data.
          , 'Signal' dom oEn -- Flagged with \/valid\/ bits \@oEn\@.
          , 'Signal' dom iEn -- Outgoing back-pressure, \/ready\/ edge.
          )
  }
@

where:

 * @dom@ is the domain to which the circuit is synchronized.
 * @iEn@ is the type of the bidirectional incoming synchronization channel.
 * @oEn@ is the type of the bidirectional outgoing synchronization channel.
 * @i@ is the incoming data type.
 * @o@ is the outgoing data type.

We define several composition operators for our 'DataFlow' circuits:

 * 'seqDF' sequential composition.
 * 'parDF' parallel composition.
 * 'loopDF' add a feedback arc.
 * 'lockStep' proceed in lock-step.

When you look at the types of the above operators it becomes clear why we
parametrize in the types of the synchronization channels.
-}
newtype DataFlow dom iEn oEn i o
  = DF
  { -- | Create an ordinary circuit from a 'DataFlow' circuit
    forall (dom :: Domain) iEn oEn i o.
DataFlow dom iEn oEn i o
-> Signal dom i
-> Signal dom iEn
-> Signal dom oEn
-> (Signal dom o, Signal dom oEn, Signal dom iEn)
df :: Signal dom i     -- Incoming data
       -> Signal dom iEn   -- Flagged with /valid/ bits @iEn@.
       -> Signal dom oEn   -- Incoming back-pressure, /ready/ edge.
       -> ( Signal dom o   -- Outgoing data.
          , Signal dom oEn -- Flagged with /valid/ bits @oEn@.
          , Signal dom iEn -- Outgoing back-pressure, /ready/ edge.
          )
  }

-- | Dataflow circuit synchronized to the 'Clash.Signal.systemClockGen'.
-- type DataFlow iEn oEn i o = DataFlow' systemClockGen iEn oEn i o

-- | Create a 'DataFlow' circuit from a circuit description with the appropriate
-- type:
--
-- @
-- 'Signal' dom i        -- Incoming data.
-- -> 'Signal' dom Bool  -- Flagged with a single \/valid\/ bit.
-- -> 'Signal' dom Bool  -- Incoming back-pressure, \/ready\/ bit.
-- -> ( 'Signal' dom o   -- Outgoing data.
--    , 'Signal' dom oEn -- Flagged with a single \/valid\/ bit.
--    , 'Signal' dom iEn -- Outgoing back-pressure, \/ready\/ bit.
--    )
-- @
--
-- A circuit adhering to the 'DataFlow' type should:
--
--  * Not consume data when validity is deasserted.
--  * Only update its output when readiness is asserted.
liftDF
  :: ( Signal dom i
    -> Signal dom Bool
    -> Signal dom Bool
    -> (Signal dom o, Signal dom Bool, Signal dom Bool))
  -> DataFlow dom Bool Bool i o
liftDF :: forall (dom :: Domain) i o.
(Signal dom i
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom o, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool i o
liftDF = (Signal dom i
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom o, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool i o
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF

-- | Create a 'DataFlow' circuit where the given function @f@ operates on the
-- data, and the synchronization channels are passed unaltered.
pureDF
  :: (i -> o)
  -> DataFlow dom Bool Bool i o
pureDF :: forall i o (dom :: Domain). (i -> o) -> DataFlow dom Bool Bool i o
pureDF i -> o
f = (Signal dom i
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom o, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool i o
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom i
i Signal dom Bool
iV Signal dom Bool
oR -> ((i -> o) -> Signal dom i -> Signal dom o
forall a b. (a -> b) -> Signal dom a -> Signal dom b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap i -> o
f Signal dom i
i,Signal dom Bool
iV,Signal dom Bool
oR))

-- | Create a 'DataFlow' circuit from a Mealy machine description as those of
-- "Clash.Prelude.Mealy"
mealyDF
  :: ( KnownDomain dom
     , NFDataX s )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (s -> i -> (s,o))
  -> s
  -> DataFlow dom Bool Bool i o
mealyDF :: forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s, o))
-> s
-> DataFlow dom Bool Bool i o
mealyDF Clock dom
clk Reset dom
rst Enable dom
gen s -> i -> (s, o)
f s
iS =
  (Signal dom i
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom o, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool i o
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom i
i Signal dom Bool
iV Signal dom Bool
oR -> let en :: Signal dom Bool
en     = Signal dom Bool
iV Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
oR
                      (Signal dom s
s',Signal dom o
o) = Signal dom (s, o) -> Unbundled dom (s, o)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain). Signal dom (s, o) -> Unbundled dom (s, o)
unbundle (s -> i -> (s, o)
f (s -> i -> (s, o)) -> Signal dom s -> Signal dom (i -> (s, o))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom s
s Signal dom (i -> (s, o)) -> Signal dom i -> Signal dom (s, o)
forall a b. Signal dom (a -> b) -> Signal dom a -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom i
i)
                      s :: Signal dom s
s      = Clock dom
-> Reset dom -> Enable dom -> s -> Signal dom s -> Signal dom s
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom
clk Reset dom
rst (Enable dom -> Signal dom Bool -> Enable dom
forall (dom :: Domain). Enable dom -> Signal dom Bool -> Enable dom
andEnable Enable dom
gen Signal dom Bool
en) s
iS Signal dom s
s'
                  in  (Signal dom o
o,Signal dom Bool
iV,Signal dom Bool
oR))

-- | Create a 'DataFlow' circuit from a Moore machine description as those of
-- "Clash.Prelude.Moore"
mooreDF
  :: ( KnownDomain dom
     , NFDataX s )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (s -> i -> s)
  -> (s -> o)
  -> s
  -> DataFlow dom Bool Bool i o
mooreDF :: forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> DataFlow dom Bool Bool i o
mooreDF Clock dom
clk Reset dom
rst Enable dom
gen s -> i -> s
ft s -> o
fo s
iS =
  (Signal dom i
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom o, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool i o
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom i
i Signal dom Bool
iV Signal dom Bool
oR -> let en :: Signal dom Bool
en  = Signal dom Bool
iV Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
oR
                      s' :: Signal dom s
s'  = s -> i -> s
ft (s -> i -> s) -> Signal dom s -> Signal dom (i -> s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom s
s Signal dom (i -> s) -> Signal dom i -> Signal dom s
forall a b. Signal dom (a -> b) -> Signal dom a -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Signal dom i
i
                      s :: Signal dom s
s   = Clock dom
-> Reset dom -> Enable dom -> s -> Signal dom s -> Signal dom s
forall (dom :: Domain) a.
(KnownDomain dom, NFDataX a) =>
Clock dom
-> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom a
register Clock dom
clk Reset dom
rst (Enable dom -> Signal dom Bool -> Enable dom
forall (dom :: Domain). Enable dom -> Signal dom Bool -> Enable dom
andEnable Enable dom
gen Signal dom Bool
en) s
iS Signal dom s
s'
                      o :: Signal dom o
o   = s -> o
fo (s -> o) -> Signal dom s -> Signal dom o
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom s
s
                  in  (Signal dom o
o,Signal dom Bool
iV,Signal dom Bool
oR))

fifoDF_mealy
  :: forall addrSize a
   . KnownNat addrSize
  => (Vec (2^addrSize) a, BitVector (addrSize + 1), BitVector (addrSize + 1))
  -> (a, Bool, Bool)
  -> ((Vec (2^addrSize) a, BitVector (addrSize + 1), BitVector (addrSize + 1))
     ,(a, Bool, Bool))
fifoDF_mealy :: forall (addrSize :: Nat) a.
KnownNat addrSize =>
(Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
 BitVector (addrSize + 1))
-> (a, Bool, Bool)
-> ((Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
     BitVector (addrSize + 1)),
    (a, Bool, Bool))
fifoDF_mealy (Vec (2 ^ addrSize) a
mem,BitVector (addrSize + 1)
rptr,BitVector (addrSize + 1)
wptr) (a
wdata,Bool
winc,Bool
rinc) =
  let raddr :: BitVector addrSize
raddr = BitVector (addrSize + 1) -> BitVector addrSize
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB BitVector (addrSize + 1)
rptr :: BitVector addrSize
      waddr :: BitVector addrSize
waddr = BitVector (addrSize + 1) -> BitVector addrSize
forall (a :: Nat) (b :: Nat).
KnownNat a =>
BitVector (a + b) -> BitVector a
forall (f :: Nat -> Type) (a :: Nat) (b :: Nat).
(Resize f, KnownNat a) =>
f (a + b) -> f a
truncateB BitVector (addrSize + 1)
wptr :: BitVector addrSize

      mem' :: Vec (2 ^ addrSize) a
mem' | Bool
winc Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
full = BitVector addrSize
-> a -> Vec (2 ^ addrSize) a -> Vec (2 ^ addrSize) a
forall (n :: Nat) i a.
(KnownNat n, Enum i) =>
i -> a -> Vec n a -> Vec n a
replace BitVector addrSize
waddr a
wdata Vec (2 ^ addrSize) a
mem
           | Bool
otherwise        = Vec (2 ^ addrSize) a
mem

      rdata :: a
rdata = Vec (2 ^ addrSize) a
mem Vec (2 ^ addrSize) a -> BitVector addrSize -> a
forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
!! BitVector addrSize
raddr

      rptr' :: BitVector (addrSize + 1)
rptr' = BitVector (addrSize + 1)
rptr BitVector (addrSize + 1)
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1)
forall a. Num a => a -> a -> a
+ Bool -> BitVector (addrSize + 1)
forall (n :: Nat). KnownNat n => Bool -> BitVector (n + 1)
boolToBV (Bool
rinc Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
empty)
      wptr' :: BitVector (addrSize + 1)
wptr' = BitVector (addrSize + 1)
wptr BitVector (addrSize + 1)
-> BitVector (addrSize + 1) -> BitVector (addrSize + 1)
forall a. Num a => a -> a -> a
+ Bool -> BitVector (addrSize + 1)
forall (n :: Nat). KnownNat n => Bool -> BitVector (n + 1)
boolToBV (Bool
winc Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
full)
      empty :: Bool
empty = BitVector (addrSize + 1)
rptr BitVector (addrSize + 1) -> BitVector (addrSize + 1) -> Bool
forall a. Eq a => a -> a -> Bool
== BitVector (addrSize + 1)
wptr
      full :: Bool
full  = BitVector (addrSize + 1) -> Bit
forall a. BitPack a => a -> Bit
msb BitVector (addrSize + 1)
rptr Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
/= BitVector (addrSize + 1) -> Bit
forall a. BitPack a => a -> Bit
msb BitVector (addrSize + 1)
wptr Bool -> Bool -> Bool
&& BitVector addrSize
raddr BitVector addrSize -> BitVector addrSize -> Bool
forall a. Eq a => a -> a -> Bool
== BitVector addrSize
waddr
  in  ((Vec (2 ^ addrSize) a
mem',BitVector (addrSize + 1)
rptr',BitVector (addrSize + 1)
wptr'), (a
rdata,Bool
empty,Bool
full))

-- | Create a FIFO buffer adhering to the 'DataFlow' protocol. Can be filled
-- with initial content.
--
-- To create a FIFO of size 4, with two initial values 2 and 3 you would write:
--
-- @
-- fifo4 = 'fifoDF' d4 (2 :> 3 :> Nil)
-- @
fifoDF
  :: forall addrSize m n a dom
   . ( KnownDomain dom
     , NFDataX a
     , KnownNat addrSize
     , KnownNat n
     , KnownNat m
     , (m + n) ~ (2 ^ addrSize) )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> SNat (m + n) -- ^ Depth of the FIFO buffer. Must be a power of two.
  -> Vec m a      -- ^ Initial content. Can be smaller than the size of the
                  -- FIFO. Empty spaces are initialized with 'undefined'.
  -> DataFlow dom Bool Bool a a
fifoDF :: forall (addrSize :: Nat) (m :: Nat) (n :: Nat) a (dom :: Domain).
(KnownDomain dom, NFDataX a, KnownNat addrSize, KnownNat n,
 KnownNat m, (m + n) ~ (2 ^ addrSize)) =>
Clock dom
-> Reset dom
-> Enable dom
-> SNat (m + n)
-> Vec m a
-> DataFlow dom Bool Bool a a
fifoDF Clock dom
clk Reset dom
rst Enable dom
en SNat (m + n)
_ Vec m a
iS = (Signal dom a
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom a, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool a a
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF ((Signal dom a
  -> Signal dom Bool
  -> Signal dom Bool
  -> (Signal dom a, Signal dom Bool, Signal dom Bool))
 -> DataFlow dom Bool Bool a a)
-> (Signal dom a
    -> Signal dom Bool
    -> Signal dom Bool
    -> (Signal dom a, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool a a
forall a b. (a -> b) -> a -> b
$ \Signal dom a
i Signal dom Bool
iV Signal dom Bool
oR ->
  let initRdPtr :: BitVector (addrSize + 1)
initRdPtr      = BitVector (addrSize + 1)
0
      initWrPtr :: BitVector (addrSize + 1)
initWrPtr      = Int -> BitVector (addrSize + 1)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vec m a -> Int
forall (n :: Nat) a. KnownNat n => Vec n a -> Int
length Vec m a
iS)
      initMem :: Vec (m + n) a
initMem        = Vec m a
iS Vec m a -> Vec n a -> Vec (m + n) a
forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
++ a -> Vec n a
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat  (String -> a
forall a. HasCallStack => String -> a
errorX String
"fifoDF: undefined") :: Vec (m + n) a
      initS :: (Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
 BitVector (addrSize + 1))
initS          = (Vec (m + n) a
Vec (2 ^ addrSize) a
initMem,BitVector (addrSize + 1)
initRdPtr,BitVector (addrSize + 1)
initWrPtr)
      (Signal dom a
o,Signal dom Bool
empty,Signal dom Bool
full) = Clock dom
-> Reset dom
-> Enable dom
-> ((Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
     BitVector (addrSize + 1))
    -> (a, Bool, Bool)
    -> ((Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
         BitVector (addrSize + 1)),
        (a, Bool, Bool)))
-> (Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
    BitVector (addrSize + 1))
-> Unbundled dom (a, Bool, Bool)
-> Unbundled dom (a, Bool, Bool)
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s, Bundle i, Bundle o) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> (s, o))
-> s
-> Unbundled dom i
-> Unbundled dom o
mealyB Clock dom
clk Reset dom
rst Enable dom
en (Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
 BitVector (addrSize + 1))
-> (a, Bool, Bool)
-> ((Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
     BitVector (addrSize + 1)),
    (a, Bool, Bool))
forall (addrSize :: Nat) a.
KnownNat addrSize =>
(Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
 BitVector (addrSize + 1))
-> (a, Bool, Bool)
-> ((Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
     BitVector (addrSize + 1)),
    (a, Bool, Bool))
fifoDF_mealy (Vec (2 ^ addrSize) a, BitVector (addrSize + 1),
 BitVector (addrSize + 1))
initS (Signal dom a
i,Signal dom Bool
iV,Signal dom Bool
oR)
  in  (Signal dom a
o,Bool -> Bool
not (Bool -> Bool) -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom Bool
empty, Bool -> Bool
not (Bool -> Bool) -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom Bool
full)

-- | Identity circuit
--
-- <<doc/idDF.svg>>
idDF :: DataFlow dom en en a a
idDF :: forall (dom :: Domain) en a. DataFlow dom en en a a
idDF = (Signal dom a
 -> Signal dom en
 -> Signal dom en
 -> (Signal dom a, Signal dom en, Signal dom en))
-> DataFlow dom en en a a
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom a
a Signal dom en
val Signal dom en
rdy -> (Signal dom a
a,Signal dom en
val,Signal dom en
rdy))

-- | Sequential composition of two 'DataFlow' circuits.
--
-- <<doc/seqDF.svg>>
seqDF
  :: DataFlow dom aEn bEn a b
  -> DataFlow dom bEn cEn b c
  -> DataFlow dom aEn cEn a c
(DF Signal dom a
-> Signal dom aEn
-> Signal dom bEn
-> (Signal dom b, Signal dom bEn, Signal dom aEn)
f) seqDF :: forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` (DF Signal dom b
-> Signal dom bEn
-> Signal dom cEn
-> (Signal dom c, Signal dom cEn, Signal dom bEn)
g) = (Signal dom a
 -> Signal dom aEn
 -> Signal dom cEn
 -> (Signal dom c, Signal dom cEn, Signal dom aEn))
-> DataFlow dom aEn cEn a c
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom a
a Signal dom aEn
aVal Signal dom cEn
cRdy -> let (Signal dom b
b,Signal dom bEn
bVal,Signal dom aEn
aRdy) = Signal dom a
-> Signal dom aEn
-> Signal dom bEn
-> (Signal dom b, Signal dom bEn, Signal dom aEn)
f Signal dom a
a Signal dom aEn
aVal Signal dom bEn
bRdy
                                                (Signal dom c
c,Signal dom cEn
cVal,Signal dom bEn
bRdy) = Signal dom b
-> Signal dom bEn
-> Signal dom cEn
-> (Signal dom c, Signal dom cEn, Signal dom bEn)
g Signal dom b
b Signal dom bEn
bVal Signal dom cEn
cRdy
                                            in  (Signal dom c
c,Signal dom cEn
cVal,Signal dom aEn
aRdy))

-- | Apply the circuit to the first halve of the communication channels, leave
-- the second halve unchanged.
--
-- <<doc/firstDF.svg>>
firstDF
  :: DataFlow dom aEn bEn a b
  -> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
firstDF :: forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
firstDF (DF Signal dom a
-> Signal dom aEn
-> Signal dom bEn
-> (Signal dom b, Signal dom bEn, Signal dom aEn)
f) = (Signal dom (a, c)
 -> Signal dom (aEn, cEn)
 -> Signal dom (bEn, cEn)
 -> (Signal dom (b, c), Signal dom (bEn, cEn),
     Signal dom (aEn, cEn)))
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (a, c)
ac Signal dom (aEn, cEn)
acV Signal dom (bEn, cEn)
bcR -> let (Signal dom a
a,Signal dom c
c)     = Signal dom (a, c) -> Unbundled dom (a, c)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain). Signal dom (a, c) -> Unbundled dom (a, c)
unbundle Signal dom (a, c)
ac
                                        (Signal dom aEn
aV,Signal dom cEn
cV)   = Signal dom (aEn, cEn) -> Unbundled dom (aEn, cEn)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (aEn, cEn) -> Unbundled dom (aEn, cEn)
unbundle Signal dom (aEn, cEn)
acV
                                        (Signal dom bEn
bR,Signal dom cEn
cR)   = Signal dom (bEn, cEn) -> Unbundled dom (bEn, cEn)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (bEn, cEn) -> Unbundled dom (bEn, cEn)
unbundle Signal dom (bEn, cEn)
bcR
                                        (Signal dom b
b,Signal dom bEn
bV,Signal dom aEn
aR) = Signal dom a
-> Signal dom aEn
-> Signal dom bEn
-> (Signal dom b, Signal dom bEn, Signal dom aEn)
f Signal dom a
a Signal dom aEn
aV Signal dom bEn
bR
                                        bc :: Signal dom (b, c)
bc        = Unbundled dom (b, c) -> Signal dom (b, c)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain). Unbundled dom (b, c) -> Signal dom (b, c)
bundle (Signal dom b
b,Signal dom c
c)
                                        bcV :: Signal dom (bEn, cEn)
bcV       = Unbundled dom (bEn, cEn) -> Signal dom (bEn, cEn)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (bEn, cEn) -> Signal dom (bEn, cEn)
bundle (Signal dom bEn
bV,Signal dom cEn
cV)
                                        acR :: Signal dom (aEn, cEn)
acR       = Unbundled dom (aEn, cEn) -> Signal dom (aEn, cEn)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (aEn, cEn) -> Signal dom (aEn, cEn)
bundle (Signal dom aEn
aR,Signal dom cEn
cR)
                                    in  (Signal dom (b, c)
bc,Signal dom (bEn, cEn)
bcV,Signal dom (aEn, cEn)
acR)
                    )

-- | Swap the two communication channels.
--
-- <<doc/swapDF.svg>>
swapDF :: DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
swapDF :: forall (dom :: Domain) aEn bEn a b.
DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
swapDF = (Signal dom (a, b)
 -> Signal dom (aEn, bEn)
 -> Signal dom (bEn, aEn)
 -> (Signal dom (b, a), Signal dom (bEn, aEn),
     Signal dom (aEn, bEn)))
-> DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (a, b)
ab Signal dom (aEn, bEn)
abV Signal dom (bEn, aEn)
baR -> ((a, b) -> (b, a)
forall {b} {a}. (b, a) -> (a, b)
swap ((a, b) -> (b, a)) -> Signal dom (a, b) -> Signal dom (b, a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (a, b)
ab, (aEn, bEn) -> (bEn, aEn)
forall {b} {a}. (b, a) -> (a, b)
swap ((aEn, bEn) -> (bEn, aEn))
-> Signal dom (aEn, bEn) -> Signal dom (bEn, aEn)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (aEn, bEn)
abV, (bEn, aEn) -> (aEn, bEn)
forall {b} {a}. (b, a) -> (a, b)
swap ((bEn, aEn) -> (aEn, bEn))
-> Signal dom (bEn, aEn) -> Signal dom (aEn, bEn)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (bEn, aEn)
baR))
  where
    swap :: (b, a) -> (a, b)
swap ~(b
a,a
b) = (a
b,b
a)

-- | Apply the circuit to the second halve of the communication channels, leave
-- the first halve unchanged.
--
-- <<doc/secondDF.svg>>
secondDF
  :: DataFlow dom aEn bEn a b
  -> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)
secondDF :: forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)
secondDF DataFlow dom aEn bEn a b
f = DataFlow dom (cEn, aEn) (aEn, cEn) (c, a) (a, c)
forall (dom :: Domain) aEn bEn a b.
DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
swapDF DataFlow dom (cEn, aEn) (aEn, cEn) (c, a) (a, c)
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
-> DataFlow dom (cEn, aEn) (bEn, cEn) (c, a) (b, c)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` DataFlow dom aEn bEn a b
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
firstDF DataFlow dom aEn bEn a b
f DataFlow dom (cEn, aEn) (bEn, cEn) (c, a) (b, c)
-> DataFlow dom (bEn, cEn) (cEn, bEn) (b, c) (c, b)
-> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` DataFlow dom (bEn, cEn) (cEn, bEn) (b, c) (c, b)
forall (dom :: Domain) aEn bEn a b.
DataFlow dom (aEn, bEn) (bEn, aEn) (a, b) (b, a)
swapDF

-- | Compose two 'DataFlow' circuits in parallel.
--
-- <<doc/parDF.svg>>
parDF
  :: DataFlow dom aEn bEn a b
  -> DataFlow dom cEn dEn c d
  -> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
DataFlow dom aEn bEn a b
f parDF :: forall (dom :: Domain) aEn bEn a b cEn dEn c d.
DataFlow dom aEn bEn a b
-> DataFlow dom cEn dEn c d
-> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
`parDF` DataFlow dom cEn dEn c d
g = DataFlow dom aEn bEn a b
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
firstDF DataFlow dom aEn bEn a b
f DataFlow dom (aEn, cEn) (bEn, cEn) (a, c) (b, c)
-> DataFlow dom (bEn, cEn) (bEn, dEn) (b, c) (b, d)
-> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` DataFlow dom cEn dEn c d
-> DataFlow dom (bEn, cEn) (bEn, dEn) (b, c) (b, d)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom (cEn, aEn) (cEn, bEn) (c, a) (c, b)
secondDF DataFlow dom cEn dEn c d
g

-- | Compose /n/ 'DataFlow' circuits in parallel.
parNDF
  :: KnownNat n
  => Vec n (DataFlow dom aEn bEn a b)
  -> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
parNDF :: forall (n :: Nat) (dom :: Domain) aEn bEn a b.
KnownNat n =>
Vec n (DataFlow dom aEn bEn a b)
-> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
parNDF Vec n (DataFlow dom aEn bEn a b)
fs =
  (Signal dom (Vec n a)
 -> Signal dom (Vec n aEn)
 -> Signal dom (Vec n bEn)
 -> (Signal dom (Vec n b), Signal dom (Vec n bEn),
     Signal dom (Vec n aEn)))
-> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (Vec n a)
as Signal dom (Vec n aEn)
aVs Signal dom (Vec n bEn)
bRs ->
        let as' :: Unbundled dom (Vec n a)
as'  = Signal dom (Vec n a) -> Unbundled dom (Vec n a)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Vec n a) -> Unbundled dom (Vec n a)
unbundle Signal dom (Vec n a)
as
            aVs' :: Unbundled dom (Vec n aEn)
aVs' = Signal dom (Vec n aEn) -> Unbundled dom (Vec n aEn)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Vec n aEn) -> Unbundled dom (Vec n aEn)
unbundle Signal dom (Vec n aEn)
aVs
            bRs' :: Unbundled dom (Vec n bEn)
bRs' = Signal dom (Vec n bEn) -> Unbundled dom (Vec n bEn)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Vec n bEn) -> Unbundled dom (Vec n bEn)
unbundle Signal dom (Vec n bEn)
bRs
            (Vec n (Signal dom b)
bs,Vec n (Signal dom bEn)
bVs,Vec n (Signal dom aEn)
aRs) = Vec n (Signal dom b, Signal dom bEn, Signal dom aEn)
-> (Vec n (Signal dom b), Vec n (Signal dom bEn),
    Vec n (Signal dom aEn))
forall (n :: Nat) a b c.
Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
unzip3 ((DataFlow dom aEn bEn a b
 -> (Signal dom a, Signal dom aEn, Signal dom bEn)
 -> (Signal dom b, Signal dom bEn, Signal dom aEn))
-> Vec n (DataFlow dom aEn bEn a b)
-> Vec n (Signal dom a, Signal dom aEn, Signal dom bEn)
-> Vec n (Signal dom b, Signal dom bEn, Signal dom aEn)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\DataFlow dom aEn bEn a b
k (Signal dom a
a,Signal dom aEn
b,Signal dom bEn
r) -> DataFlow dom aEn bEn a b
-> Signal dom a
-> Signal dom aEn
-> Signal dom bEn
-> (Signal dom b, Signal dom bEn, Signal dom aEn)
forall (dom :: Domain) iEn oEn i o.
DataFlow dom iEn oEn i o
-> Signal dom i
-> Signal dom iEn
-> Signal dom oEn
-> (Signal dom o, Signal dom oEn, Signal dom iEn)
df DataFlow dom aEn bEn a b
k Signal dom a
a Signal dom aEn
b Signal dom bEn
r) Vec n (DataFlow dom aEn bEn a b)
fs
                                  (Vec n (Signal dom a)
-> Vec n (Signal dom aEn)
-> Vec n (Signal dom bEn)
-> Vec n (Signal dom a, Signal dom aEn, Signal dom bEn)
forall (n :: Nat) a b c.
Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
zip3 (Vec n (Signal dom a) -> Vec n (Signal dom a)
forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
lazyV Vec n (Signal dom a)
Unbundled dom (Vec n a)
as') (Vec n (Signal dom aEn) -> Vec n (Signal dom aEn)
forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
lazyV Vec n (Signal dom aEn)
Unbundled dom (Vec n aEn)
aVs') Vec n (Signal dom bEn)
Unbundled dom (Vec n bEn)
bRs'))
        in  (Unbundled dom (Vec n b) -> Signal dom (Vec n b)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Vec n b) -> Signal dom (Vec n b)
bundle Vec n (Signal dom b)
Unbundled dom (Vec n b)
bs,Unbundled dom (Vec n bEn) -> Signal dom (Vec n bEn)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Vec n bEn) -> Signal dom (Vec n bEn)
bundle Vec n (Signal dom bEn)
Unbundled dom (Vec n bEn)
bVs, Unbundled dom (Vec n aEn) -> Signal dom (Vec n aEn)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Vec n aEn) -> Signal dom (Vec n aEn)
bundle Vec n (Signal dom aEn)
Unbundled dom (Vec n aEn)
aRs)
     )

-- | Feed back the second halve of the communication channel. The feedback loop
-- is buffered by a 'fifoDF' circuit.
--
-- So given a circuit /h/ with two synchronization channels:
--
-- @
-- __h__ :: 'DataFlow' (Bool,Bool) (Bool,Bool) (a,d) (b,d)
-- @
--
-- Feeding back the /d/ part (including its synchronization channels) results
-- in:
--
-- @
-- 'loopDF' d4 Nil h
-- @
--
-- <<doc/loopDF.svg>>
--
-- When you have a circuit @h'@, with only a single synchronization channel:
--
-- @
-- __h'__ :: 'DataFlow' Bool Bool (a,d) (b,d)
-- @
--
-- and you want to compose /h'/ in a feedback loop, the following will not work:
--
-- @
-- f \`@'seqDF'@\` ('loopDF' d4 Nil h') \`@'seqDF'@\` g
-- @
--
-- The circuits @f@, @h@, and @g@, must operate in /lock-step/ because the /h'/
-- circuit only has a single synchronization channel. Consequently, there
-- should only be progress when all three circuits are producing /valid/ data
-- and all three circuits are /ready/ to receive new data. We need to compose
-- /h'/ with the 'lockStep' and 'stepLock' functions to achieve the /lock-step/
-- operation.
--
-- @
-- f \`@'seqDF'@\` ('lockStep' \`@'seqDF'@\` 'loopDF' d4 Nil h' \`@'seqDF'@\` 'stepLock') \`@'seqDF'@\` g
-- @
--
-- <<doc/loopDF_sync.svg>>
loopDF
  :: ( KnownDomain dom
     , NFDataX d
     , KnownNat m
     , KnownNat n
     , KnownNat addrSize
     , (m+n) ~ (2^addrSize) )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> SNat (m + n)
  -- ^ Depth of the FIFO buffer. Must be a power of two
  -> Vec m d
  -- ^ Initial content of the FIFO buffer. Can be smaller than the size of the
  -- FIFO. Empty spaces are initialized with 'undefined'.
  -> DataFlow dom (Bool,Bool) (Bool,Bool) (a,d) (b,d)
  -> DataFlow dom Bool Bool   a           b
loopDF :: forall (dom :: Domain) d (m :: Nat) (n :: Nat) (addrSize :: Nat) a
       b.
(KnownDomain dom, NFDataX d, KnownNat m, KnownNat n,
 KnownNat addrSize, (m + n) ~ (2 ^ addrSize)) =>
Clock dom
-> Reset dom
-> Enable dom
-> SNat (m + n)
-> Vec m d
-> DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d)
-> DataFlow dom Bool Bool a b
loopDF Clock dom
clk Reset dom
rst Enable dom
en SNat (m + n)
sz Vec m d
is (DF Signal dom (a, d)
-> Signal dom (Bool, Bool)
-> Signal dom (Bool, Bool)
-> (Signal dom (b, d), Signal dom (Bool, Bool),
    Signal dom (Bool, Bool))
f) =
  (Signal dom a
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom b, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool a b
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom a
a Signal dom Bool
aV Signal dom Bool
bR -> let (Signal dom (b, d)
bd,Signal dom (Bool, Bool)
bdV,Signal dom (Bool, Bool)
adR) = Signal dom (a, d)
-> Signal dom (Bool, Bool)
-> Signal dom (Bool, Bool)
-> (Signal dom (b, d), Signal dom (Bool, Bool),
    Signal dom (Bool, Bool))
f Signal dom (a, d)
ad Signal dom (Bool, Bool)
adV Signal dom (Bool, Bool)
bdR
                      (Signal dom b
b,Signal dom d
d)        = Signal dom (b, d) -> Unbundled dom (b, d)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain). Signal dom (b, d) -> Unbundled dom (b, d)
unbundle Signal dom (b, d)
bd
                      (Signal dom Bool
bV,Signal dom Bool
dV)      = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
bdV
                      (Signal dom Bool
aR,Signal dom Bool
dR)      = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
adR
                      (Signal dom d
d_buf,Signal dom Bool
dV_buf,Signal dom Bool
dR_buf) = DataFlow dom Bool Bool d d
-> Signal dom d
-> Signal dom Bool
-> Signal dom Bool
-> (Signal dom d, Signal dom Bool, Signal dom Bool)
forall (dom :: Domain) iEn oEn i o.
DataFlow dom iEn oEn i o
-> Signal dom i
-> Signal dom iEn
-> Signal dom oEn
-> (Signal dom o, Signal dom oEn, Signal dom iEn)
df (Clock dom
-> Reset dom
-> Enable dom
-> SNat (m + n)
-> Vec m d
-> DataFlow dom Bool Bool d d
forall (addrSize :: Nat) (m :: Nat) (n :: Nat) a (dom :: Domain).
(KnownDomain dom, NFDataX a, KnownNat addrSize, KnownNat n,
 KnownNat m, (m + n) ~ (2 ^ addrSize)) =>
Clock dom
-> Reset dom
-> Enable dom
-> SNat (m + n)
-> Vec m a
-> DataFlow dom Bool Bool a a
fifoDF Clock dom
clk Reset dom
rst Enable dom
en SNat (m + n)
sz Vec m d
is) Signal dom d
d Signal dom Bool
dV Signal dom Bool
dR

                      ad :: Signal dom (a, d)
ad  = Unbundled dom (a, d) -> Signal dom (a, d)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain). Unbundled dom (a, d) -> Signal dom (a, d)
bundle (Signal dom a
a,Signal dom d
d_buf)
                      adV :: Signal dom (Bool, Bool)
adV = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
aV,Signal dom Bool
dV_buf)
                      bdR :: Signal dom (Bool, Bool)
bdR = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
bR,Signal dom Bool
dR_buf)
                  in  (Signal dom b
b,Signal dom Bool
bV,Signal dom Bool
aR)
     )

-- | Feed back the second halve of the communication channel. Unlike 'loopDF',
-- the feedback loop is /not/ buffered.
loopDF_nobuf :: DataFlow dom (Bool,Bool) (Bool,Bool) (a,d) (b,d)
             -> DataFlow dom Bool Bool   a           b
loopDF_nobuf :: forall (dom :: Domain) a d b.
DataFlow dom (Bool, Bool) (Bool, Bool) (a, d) (b, d)
-> DataFlow dom Bool Bool a b
loopDF_nobuf (DF Signal dom (a, d)
-> Signal dom (Bool, Bool)
-> Signal dom (Bool, Bool)
-> (Signal dom (b, d), Signal dom (Bool, Bool),
    Signal dom (Bool, Bool))
f) = (Signal dom a
 -> Signal dom Bool
 -> Signal dom Bool
 -> (Signal dom b, Signal dom Bool, Signal dom Bool))
-> DataFlow dom Bool Bool a b
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom a
a Signal dom Bool
aV Signal dom Bool
bR -> let (Signal dom (b, d)
bd,Signal dom (Bool, Bool)
bdV,Signal dom (Bool, Bool)
adR) = Signal dom (a, d)
-> Signal dom (Bool, Bool)
-> Signal dom (Bool, Bool)
-> (Signal dom (b, d), Signal dom (Bool, Bool),
    Signal dom (Bool, Bool))
f Signal dom (a, d)
ad Signal dom (Bool, Bool)
adV Signal dom (Bool, Bool)
bdR
                                          (Signal dom b
b,Signal dom d
d)        = Signal dom (b, d) -> Unbundled dom (b, d)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain). Signal dom (b, d) -> Unbundled dom (b, d)
unbundle Signal dom (b, d)
bd
                                          (Signal dom Bool
bV,Signal dom Bool
dV)      = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
bdV
                                          (Signal dom Bool
aR,Signal dom Bool
dR)      = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
adR
                                          ad :: Signal dom (a, d)
ad           = Unbundled dom (a, d) -> Signal dom (a, d)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain). Unbundled dom (a, d) -> Signal dom (a, d)
bundle (Signal dom a
a,Signal dom d
d)
                                          adV :: Signal dom (Bool, Bool)
adV          = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
aV,Signal dom Bool
dV)
                                          bdR :: Signal dom (Bool, Bool)
bdR          = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
bR,Signal dom Bool
dR)
                                      in  (Signal dom b
b,Signal dom Bool
bV,Signal dom Bool
aR)
                         )

-- | Reduce or extend the synchronization granularity of parallel compositions.
class LockStep a b where
  -- | Reduce the synchronization granularity to a single 'Bool'ean value.
  --
  -- Given:
  --
  -- @
  -- __f__ :: 'DataFlow' Bool Bool a b
  -- __g__ :: 'DataFlow' Bool Bool c d
  -- __h__ :: 'DataFlow' Bool Bool (b,d) (p,q)
  -- @
  --
  -- We /cannot/ simply write:
  --
  -- @
  -- (f \`@'parDF'@\` g) \`@'seqDF'@\` h
  -- @
  --
  -- because, @f \`parDF\` g@, has type, @'DataFlow' (Bool,Bool) (Bool,Bool) (a,c) (b,d)@,
  -- which does not match the expected synchronization granularity of @h@. We
  -- need a circuit in between that has the type:
  --
  -- @
  -- 'DataFlow' (Bool,Bool) Bool (b,d) (b,d)
  -- @
  --
  -- Simply '&&'-ing the /valid/ signals in the forward direction, and
  -- duplicating the /ready/ signal in the backward direction is however not
  -- enough. We also need to make sure that @f@ does not update its output when
  -- @g@'s output is invalid and visa versa, as @h@ can only consume its input
  -- when both @f@ and @g@ are producing valid data. @g@'s /ready/ port is hence
  -- only asserted when @h@ is ready and @f@ is producing /valid/ data. And @f@'s
  -- ready port is only asserted when @h@ is ready and @g@ is producing valid
  -- data. @f@ and @g@ will hence be proceeding in /lock-step/.
  --
  -- The 'lockStep' function ensures that all synchronization signals are
  -- properly connected:
  --
  -- @
  -- (f \`@'parDF'@\` g) \`@'seqDF'@\` 'lockStep' \`@'seqDF'@\` h
  -- @
  --
  -- <<doc/lockStep.svg>>
  --
  -- __Note 1__: ensure that the components that you are synchronizing have
  -- buffered/delayed @ready@ and @valid@ signals, or 'lockStep' has the
  -- potential to introduce combinational loops. You can do this by placing
  -- 'fifoDF's on the parallel channels. Extending the above example, you would
  -- write:
  --
  -- @
  -- ((f \`@'seqDF'@\` 'fifoDF' d4 Nil) \`@'parDF'@\` (g \`@'seqDF'@\` 'fifoDF' d4 Nil)) \`@'seqDF'@\` 'lockStep' \`@'seqDF'@\` h
  -- @
  --
  -- __Note 2__: 'lockStep' works for arbitrarily nested tuples. That is:
  --
  -- @
  -- p :: 'DataFlow' Bool Bool ((b,d),d) z
  --
  -- q :: 'DataFlow' ((Bool,Bool),Bool) ((Bool,Bool),Bool) ((a,c),c) ((b,d),d)
  -- q = f \`@'parDF'@\` g \`@'parDF'@\` g
  --
  -- r = q \`@'seqDF'@\` 'lockStep' \`@'seqDF'@\` p
  -- @
  --
  -- Does the right thing.
  lockStep :: DataFlow dom a Bool b b

  -- | Extend the synchronization granularity from a single 'Bool'ean value.
  --
  -- Given:
  --
  -- @
  -- __f__ :: 'DataFlow' Bool Bool a b
  -- __g__ :: 'DataFlow' Bool Bool c d
  -- __h__ :: 'DataFlow' Bool Bool (p,q) (a,c)
  -- @
  --
  -- We /cannot/ simply write:
  --
  -- @
  -- h \`@'seqDF'@\` (f \`@'parDF'@\` g)
  -- @
  --
  -- because, @f \`parDF\` g@, has type, @'DataFlow' (Bool,Bool) (Bool,Bool) (a,c) (b,d)@,
  -- which does not match the expected synchronization granularity of @h@. We
  -- need a circuit in between that has the type:
  --
  -- @
  -- 'DataFlow' Bool (Bool,Bool) (a,c) (a,c)
  -- @
  --
  -- Simply '&&'-ing the /ready/ signals in the backward direction, and
  -- duplicating the /valid/ signal in the forward direction is however not
  -- enough. We need to make sure that @f@ does not consume values when @g@ is
  -- not /ready/ and visa versa, because @h@ cannot update the values of its
  -- output tuple independently. @f@'s /valid/ port is hence only asserted when
  -- @h@ is valid and @g@ is ready to receive new values. @g@'s /valid/ port is
  -- only asserted when @h@ is valid and @f@ is ready to receive new values.
  -- @f@ and @g@ will hence be proceeding in /lock-step/.
  --
  -- The 'stepLock' function ensures that all synchronization signals are
  -- properly connected:
  --
  -- @
  -- h \`@'seqDF'@\` 'stepLock' \`@'seqDF'@\` (f \`@'parDF'@\` g)
  -- @
  --
  -- <<doc/stepLock.svg>>
  --
  -- __Note 1__: ensure that the components that you are synchronizing have
  -- buffered/delayed @ready@ and @valid@ signals, or 'stepLock' has the
  -- potential to introduce combinational loops. You can do this by placing
  -- 'fifoDF's on the parallel channels. Extending the above example, you would
  -- write:
  --
  -- @
  -- h \`@'seqDF'@\` 'stepLock' \`@'seqDF'@\` ((`fifoDF` d4 Nil \`@'seqDF'@\` f) \`@'parDF'@\` (`fifoDF` d4 Nil \`@'seqDF'@\` g))
  -- @
  --
  -- __Note 2__: 'stepLock' works for arbitrarily nested tuples. That is:
  --
  -- @
  -- p :: 'DataFlow' Bool Bool z ((a,c),c)
  --
  -- q :: 'DataFlow' ((Bool,Bool),Bool) ((Bool,Bool),Bool) ((a,c),c) ((b,d),d)
  -- q = f \`@'parDF'@\` g \`@'parDF'@\` g
  --
  -- r = p \`@'seqDF'@\` 'stepLock' \`@'seqDF'@\` q
  -- @
  --
  -- Does the right thing.
  stepLock :: DataFlow dom Bool a b b

instance LockStep Bool c where
  lockStep :: forall (dom :: Domain). DataFlow dom Bool Bool c c
lockStep = DataFlow dom Bool Bool c c
forall (dom :: Domain) en a. DataFlow dom en en a a
idDF
  stepLock :: forall (dom :: Domain). DataFlow dom Bool Bool c c
stepLock = DataFlow dom Bool Bool c c
forall (dom :: Domain) en a. DataFlow dom en en a a
idDF

instance (LockStep a x, LockStep b y) => LockStep (a,b) (x,y) where
  lockStep :: forall (dom :: Domain). DataFlow dom (a, b) Bool (x, y) (x, y)
lockStep = (DataFlow dom a Bool x x
forall a b (dom :: Domain). LockStep a b => DataFlow dom a Bool b b
forall (dom :: Domain). DataFlow dom a Bool x x
lockStep DataFlow dom a Bool x x
-> DataFlow dom b Bool y y
-> DataFlow dom (a, b) (Bool, Bool) (x, y) (x, y)
forall (dom :: Domain) aEn bEn a b cEn dEn c d.
DataFlow dom aEn bEn a b
-> DataFlow dom cEn dEn c d
-> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
`parDF` DataFlow dom b Bool y y
forall a b (dom :: Domain). LockStep a b => DataFlow dom a Bool b b
forall (dom :: Domain). DataFlow dom b Bool y y
lockStep) DataFlow dom (a, b) (Bool, Bool) (x, y) (x, y)
-> DataFlow dom (Bool, Bool) Bool (x, y) (x, y)
-> DataFlow dom (a, b) Bool (x, y) (x, y)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF`
                ((Signal dom (x, y)
 -> Signal dom (Bool, Bool)
 -> Signal dom Bool
 -> (Signal dom (x, y), Signal dom Bool, Signal dom (Bool, Bool)))
-> DataFlow dom (Bool, Bool) Bool (x, y) (x, y)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (x, y)
xy Signal dom (Bool, Bool)
xyV Signal dom Bool
rdy -> let (Signal dom Bool
xV,Signal dom Bool
yV)   = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
xyV
                                        val :: Signal dom Bool
val       = Signal dom Bool
xV Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
yV
                                        xR :: Signal dom Bool
xR        = Signal dom Bool
yV Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
rdy
                                        yR :: Signal dom Bool
yR        = Signal dom Bool
xV Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
rdy
                                        xyR :: Signal dom (Bool, Bool)
xyR       = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
xR,Signal dom Bool
yR)
                                    in  (Signal dom (x, y)
xy,Signal dom Bool
val,Signal dom (Bool, Bool)
xyR)))

  stepLock :: forall (dom :: Domain). DataFlow dom Bool (a, b) (x, y) (x, y)
stepLock = ((Signal dom (x, y)
 -> Signal dom Bool
 -> Signal dom (Bool, Bool)
 -> (Signal dom (x, y), Signal dom (Bool, Bool), Signal dom Bool))
-> DataFlow dom Bool (Bool, Bool) (x, y) (x, y)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (x, y)
xy Signal dom Bool
val Signal dom (Bool, Bool)
xyR -> let (Signal dom Bool
xR,Signal dom Bool
yR) = Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Bool, Bool) -> Unbundled dom (Bool, Bool)
unbundle Signal dom (Bool, Bool)
xyR
                                     rdy :: Signal dom Bool
rdy     = Signal dom Bool
xR  Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
yR
                                     xV :: Signal dom Bool
xV      = Signal dom Bool
val Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
yR
                                     yV :: Signal dom Bool
yV      = Signal dom Bool
val Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Signal dom Bool
xR
                                     xyV :: Signal dom (Bool, Bool)
xyV     = Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
forall (dom :: Domain).
Unbundled dom (Bool, Bool) -> Signal dom (Bool, Bool)
bundle (Signal dom Bool
xV,Signal dom Bool
yV)
                                 in  (Signal dom (x, y)
xy,Signal dom (Bool, Bool)
xyV,Signal dom Bool
rdy))) DataFlow dom Bool (Bool, Bool) (x, y) (x, y)
-> DataFlow dom (Bool, Bool) (a, b) (x, y) (x, y)
-> DataFlow dom Bool (a, b) (x, y) (x, y)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` (DataFlow dom Bool a x x
forall a b (dom :: Domain). LockStep a b => DataFlow dom Bool a b b
forall (dom :: Domain). DataFlow dom Bool a x x
stepLock DataFlow dom Bool a x x
-> DataFlow dom Bool b y y
-> DataFlow dom (Bool, Bool) (a, b) (x, y) (x, y)
forall (dom :: Domain) aEn bEn a b cEn dEn c d.
DataFlow dom aEn bEn a b
-> DataFlow dom cEn dEn c d
-> DataFlow dom (aEn, cEn) (bEn, dEn) (a, c) (b, d)
`parDF` DataFlow dom Bool b y y
forall a b (dom :: Domain). LockStep a b => DataFlow dom Bool a b b
forall (dom :: Domain). DataFlow dom Bool b y y
stepLock)

instance (LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) where
  lockStep :: forall (dom :: Domain).
DataFlow dom (Vec n en) Bool (Vec n a) (Vec n a)
lockStep = Vec n (DataFlow dom en Bool a a)
-> DataFlow dom (Vec n en) (Vec n Bool) (Vec n a) (Vec n a)
forall (n :: Nat) (dom :: Domain) aEn bEn a b.
KnownNat n =>
Vec n (DataFlow dom aEn bEn a b)
-> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
parNDF (DataFlow dom en Bool a a -> Vec n (DataFlow dom en Bool a a)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat DataFlow dom en Bool a a
forall a b (dom :: Domain). LockStep a b => DataFlow dom a Bool b b
forall (dom :: Domain). DataFlow dom en Bool a a
lockStep) DataFlow dom (Vec n en) (Vec n Bool) (Vec n a) (Vec n a)
-> DataFlow dom (Vec n Bool) Bool (Vec n a) (Vec n a)
-> DataFlow dom (Vec n en) Bool (Vec n a) (Vec n a)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF`
    (Signal dom (Vec n a)
 -> Signal dom (Vec n Bool)
 -> Signal dom Bool
 -> (Signal dom (Vec n a), Signal dom Bool,
     Signal dom (Vec n Bool)))
-> DataFlow dom (Vec n Bool) Bool (Vec n a) (Vec n a)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (Vec n a)
xs Signal dom (Vec n Bool)
vals Signal dom Bool
rdy ->
          let val :: Signal dom Bool
val  = (Vec (n + 1) Bool -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and (Vec (n + 1) Bool -> Bool)
-> (Vec n Bool -> Vec (n + 1) Bool) -> Vec n Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
True :>)) (Vec n Bool -> Bool) -> Signal dom (Vec n Bool) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Vec n Bool)
vals
              rdys :: Signal dom (Vec n Bool)
rdys = Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool
forall (n :: Nat).
KnownNat n =>
Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool
allReady (Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool)
-> Signal dom Bool
-> Signal dom (Vec n (Vec (n + 1) Bool) -> Vec n Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom Bool
rdy Signal dom (Vec n (Vec (n + 1) Bool) -> Vec n Bool)
-> Signal dom (Vec n (Vec (n + 1) Bool)) -> Signal dom (Vec n Bool)
forall a b. Signal dom (a -> b) -> Signal dom a -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Vec (n + 1) Bool -> Vec n (Vec (n + 1) Bool)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat (Vec (n + 1) Bool -> Vec n (Vec (n + 1) Bool))
-> (Vec n Bool -> Vec (n + 1) Bool)
-> Vec n Bool
-> Vec n (Vec (n + 1) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n Bool -> Bool -> Vec (n + 1) Bool
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< Bool
True) (Vec n Bool -> Vec n (Vec (n + 1) Bool))
-> Signal dom (Vec n Bool) -> Signal dom (Vec n (Vec (n + 1) Bool))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Vec n Bool)
vals)
          in  (Signal dom (Vec n a)
xs,Signal dom Bool
val,Signal dom (Vec n Bool)
rdys)
       )
  stepLock :: forall (dom :: Domain).
DataFlow dom Bool (Vec n en) (Vec n a) (Vec n a)
stepLock =
    (Signal dom (Vec n a)
 -> Signal dom Bool
 -> Signal dom (Vec n Bool)
 -> (Signal dom (Vec n a), Signal dom (Vec n Bool),
     Signal dom Bool))
-> DataFlow dom Bool (Vec n Bool) (Vec n a) (Vec n a)
forall (dom :: Domain) iEn oEn i o.
(Signal dom i
 -> Signal dom iEn
 -> Signal dom oEn
 -> (Signal dom o, Signal dom oEn, Signal dom iEn))
-> DataFlow dom iEn oEn i o
DF (\Signal dom (Vec n a)
xs Signal dom Bool
val Signal dom (Vec n Bool)
rdys ->
          let rdy :: Signal dom Bool
rdy  = (Vec (n + 1) Bool -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and (Vec (n + 1) Bool -> Bool)
-> (Vec n Bool -> Vec (n + 1) Bool) -> Vec n Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
True :>)) (Vec n Bool -> Bool) -> Signal dom (Vec n Bool) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Vec n Bool)
rdys
              vals :: Signal dom (Vec n Bool)
vals = Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool
forall (n :: Nat).
KnownNat n =>
Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool
allReady (Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool)
-> Signal dom Bool
-> Signal dom (Vec n (Vec (n + 1) Bool) -> Vec n Bool)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom Bool
val Signal dom (Vec n (Vec (n + 1) Bool) -> Vec n Bool)
-> Signal dom (Vec n (Vec (n + 1) Bool)) -> Signal dom (Vec n Bool)
forall a b. Signal dom (a -> b) -> Signal dom a -> Signal dom b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Vec (n + 1) Bool -> Vec n (Vec (n + 1) Bool)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat (Vec (n + 1) Bool -> Vec n (Vec (n + 1) Bool))
-> (Vec n Bool -> Vec (n + 1) Bool)
-> Vec n Bool
-> Vec n (Vec (n + 1) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n Bool -> Bool -> Vec (n + 1) Bool
forall (n :: Nat) a. Vec n a -> a -> Vec (n + 1) a
:< Bool
True) (Vec n Bool -> Vec n (Vec (n + 1) Bool))
-> Signal dom (Vec n Bool) -> Signal dom (Vec n (Vec (n + 1) Bool))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Vec n Bool)
rdys)
          in  (Signal dom (Vec n a)
xs,Signal dom (Vec n Bool)
vals,Signal dom Bool
rdy)
       ) DataFlow dom Bool (Vec n Bool) (Vec n a) (Vec n a)
-> DataFlow dom (Vec n Bool) (Vec n en) (Vec n a) (Vec n a)
-> DataFlow dom Bool (Vec n en) (Vec n a) (Vec n a)
forall (dom :: Domain) aEn bEn a b cEn c.
DataFlow dom aEn bEn a b
-> DataFlow dom bEn cEn b c -> DataFlow dom aEn cEn a c
`seqDF` Vec n (DataFlow dom Bool en a a)
-> DataFlow dom (Vec n Bool) (Vec n en) (Vec n a) (Vec n a)
forall (n :: Nat) (dom :: Domain) aEn bEn a b.
KnownNat n =>
Vec n (DataFlow dom aEn bEn a b)
-> DataFlow dom (Vec n aEn) (Vec n bEn) (Vec n a) (Vec n b)
parNDF (DataFlow dom Bool en a a -> Vec n (DataFlow dom Bool en a a)
forall (n :: Nat) a. KnownNat n => a -> Vec n a
repeat DataFlow dom Bool en a a
forall a b (dom :: Domain). LockStep a b => DataFlow dom Bool a b b
forall (dom :: Domain). DataFlow dom Bool en a a
stepLock)

allReady :: KnownNat n
         => Bool
         -> Vec n (Vec (n+1) Bool)
         -> Vec n Bool
allReady :: forall (n :: Nat).
KnownNat n =>
Bool -> Vec n (Vec (n + 1) Bool) -> Vec n Bool
allReady Bool
b Vec n (Vec (n + 1) Bool)
vs = (Vec (n + 1) Bool -> Bool)
-> Vec n (Vec (n + 1) Bool) -> Vec n Bool
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map (Vec (n + 1) Bool -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and (Vec (n + 1) Bool -> Bool)
-> (Vec (n + 1) Bool -> Vec (n + 1) Bool)
-> Vec (n + 1) Bool
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
b :>) (Vec n Bool -> Vec (n + 1) Bool)
-> (Vec (n + 1) Bool -> Vec n Bool)
-> Vec (n + 1) Bool
-> Vec (n + 1) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (n + 1) Bool -> Vec n Bool
forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
tail) ((forall (n :: Nat). SNat n -> Vec (n + 1) Bool -> Vec (n + 1) Bool)
-> Vec n (Vec (n + 1) Bool) -> Vec n (Vec (n + 1) Bool)
forall (k :: Nat) a b.
KnownNat k =>
(forall (n :: Nat). SNat n -> a -> b) -> Vec k a -> Vec k b
smap ((Vec (n + 1) Bool -> SNat n -> Vec (n + 1) Bool)
-> SNat n -> Vec (n + 1) Bool -> Vec (n + 1) Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Vec (n + 1) Bool -> SNat n -> Vec (n + 1) Bool
forall (n :: Nat) a (d :: Nat).
KnownNat n =>
Vec n a -> SNat d -> Vec n a
rotateLeftS) Vec n (Vec (n + 1) Bool)
vs)