    {-|
    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 Bool -> Vec n Bool -> Vec (n + 1) Bool
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :>)) (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 Bool -> Vec n Bool -> Vec (n + 1) Bool
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :>)) (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 Bool -> Vec n Bool -> Vec (n + 1) Bool
    forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a
    :>) (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 (l :: Nat). SNat l -> 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 (l :: Nat). SNat l -> a -> b) -> Vec k a -> Vec k b
    smap ((Vec (n + 1) Bool -> SNat l -> Vec (n + 1) Bool)
    -> SNat l -> Vec (n + 1) Bool -> Vec (n + 1) Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Vec (n + 1) Bool -> SNat l -> 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)