{-|
Copyright  :  (C) 2013-2016, University of Twente,
                  2017     , Google Inc.
                  2019     , Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

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

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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
  ( -- * 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.Prelude.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, enable, 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
    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 '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 :: (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 :: (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 (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 :: 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
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 (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
enable 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 :: 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 (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
enable 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 :: (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 (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 (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 :: 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 :: 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 :: 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 :: 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
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
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
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
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
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
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 :: 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 :: 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 :: 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 :: 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
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
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
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
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
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
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 :: 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
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
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
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
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
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
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 :: 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
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
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
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
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
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
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 :: 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 :: 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 :: 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
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
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
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
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 :: 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
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
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
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
stepLock)

instance (LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) where
  lockStep :: 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
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 (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 :: 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 (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
stepLock)

allReady :: KnownNat n
         => Bool
         -> Vec n (Vec (n+1) Bool)
         -> Vec n Bool
allReady :: 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)