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

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE NoImplicitPrelude #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# LANGUAGE Trustworthy #-}

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

    module Clash.Explicit.Signal.Delayed
      ( DSignal
        -- * Delay-annotated synchronous signals
      , delayed
      , delayedI
      , delayN
      , delayI
      , delayedFold
      , feedback
        -- * Signal \<-\> DSignal conversion
      , fromSignal
      , toSignal
        -- * List \<-\> DSignal conversion (not synthesizable)
      , dfromList
        -- ** lazy versions
      , dfromList_lazy
        -- * Experimental
      , unsafeFromSignal
      , antiDelay
      , forward
      )
    where

    import Prelude                    ((.), (<$>), (<*>), id, Num(..))

    import Data.Coerce                (coerce)
    import Data.Kind                  (Type)
    import Data.Proxy                 (Proxy (..))
    import Data.Singletons            (Apply, TyFun, type (@@))
    import GHC.TypeLits               (KnownNat, Nat, type (+), type (^), type (*))

    import Clash.Sized.Vector
    import Clash.Signal.Delayed.Internal
      (DSignal(..), dfromList, dfromList_lazy, fromSignal, toSignal,
       unsafeFromSignal, antiDelay, feedback, forward)

    import Clash.Explicit.Signal
      (KnownDomain, Clock, Domain, Reset, Signal, Enable, register, delay, bundle, unbundle)
    import Clash.Promoted.Nat         (SNat (..), snatToInteger)
    import Clash.XException           (NFDataX)

    {- $setup
    >>> :set -XDataKinds
    >>> :set -XTypeOperators
    >>> import Clash.Explicit.Prelude
    >>> let delay3 clk rst en = delayed clk rst en (-1 :> -1 :> -1 :> Nil)
    >>> let delay2 clk rst en = (delayedI clk rst en :: Int -> DSignal System n Int -> DSignal System (n + 2) Int)
    >>> let delayN2 = delayN d2
    >>> let delayI2 = delayI :: KnownDomain dom => Int -> Enable dom -> Clock dom -> DSignal dom n Int -> DSignal dom (n + 2) Int
    >>> let countingSignals = Clash.Prelude.repeat (dfromList [0..]) :: Vec 4 (DSignal dom 0 Int)
    >>> :{
    let mac :: Clock System
            -> Reset System
            -> Enable System
            -> DSignal System 0 Int -> DSignal System 0 Int
            -> DSignal System 0 Int
        mac clk rst en x y = feedback (mac' x y)
          where
            mac' :: DSignal System 0 Int -> DSignal System 0 Int
                 -> DSignal System 0 Int
                 -> (DSignal System 0 Int, DSignal System 1 Int)
            mac' a b acc = let acc' = a * b + acc
                           in  (acc, delayed clk rst en (singleton 0) acc')
    :}

    -}

    -- TODO: Reimplement with dtfold
    -- | Delay a 'DSignal' for @d@ periods.
    --
    -- @
    -- delay3
    --   :: KnownDomain dom
    --   => Clock dom
    --   -> Reset dom
    --   -> Enable dom
    --   -> 'DSignal' dom n Int
    --   -> 'DSignal' dom (n + 3) Int
    -- delay3 clk rst en = 'delayed' clk rst en (-1 ':>' -1 ':>' -1 ':>' 'Nil')
    -- @
    --
    -- >>> sampleN 7 (delay3 systemClockGen resetGen enableGen (dfromList [0..]))
    -- [-1,-1,-1,-1,1,2,3]
    delayed
      :: forall dom  a n d
       . ( KnownDomain dom
         , KnownNat d
         , NFDataX a )
      => Clock dom
      -> Reset dom
      -> Enable dom
      -> Vec d a
      -- ^ Initial values
      -> DSignal dom n a
      -> DSignal dom (n + d) a
    delayed :: forall (dom :: Domain) a (n :: Nat) (d :: Nat).
    (KnownDomain dom, KnownNat d, NFDataX a) =>
    Clock dom
    -> Reset dom
    -> Enable dom
    -> Vec d a
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayed Clock dom
    clk Reset dom
    rst Enable dom
    en Vec d a
    m DSignal dom n a
    ds = Signal dom a -> DSignal dom (n + d) a
    forall a b. Coercible a b => a -> b
    coerce (Signal dom a -> Signal dom a
    delaySignal (DSignal dom n a -> Signal dom a
    forall a b. Coercible a b => a -> b
    coerce DSignal dom n a
    ds))
      where
        delaySignal :: Signal dom a -> Signal dom a
        delaySignal :: Signal dom a -> Signal dom a
    delaySignal Signal dom a
    s = case Vec d a -> Int
    forall (n :: Nat) a. KnownNat n => Vec n a -> Int
    length Vec d a
    m of
          Int
    0 -> Signal dom a
    s
          Int
    _ -> let (Vec d (Signal dom a)
    r',Vec 1 (Signal dom a)
    o) = Vec d (Signal dom a)
    -> Vec 1 (Signal dom a)
    -> (Vec d (Signal dom a), Vec 1 (Signal dom a))
    forall (n :: Nat) a (m :: Nat).
    KnownNat n =>
    Vec n a -> Vec m a -> (Vec n a, Vec m a)
    shiftInAt0 (Signal dom (Vec d a) -> Unbundled dom (Vec d a)
    forall a (dom :: Domain).
    Bundle a =>
    Signal dom a -> Unbundled dom a
    forall (dom :: Domain).
    Signal dom (Vec d a) -> Unbundled dom (Vec d a)
    unbundle Signal dom (Vec d a)
    r) (Signal dom a -> Vec 1 (Signal dom a)
    forall a. a -> Vec 1 a
    singleton Signal dom a
    s)
                   r :: Signal dom (Vec d a)
    r      = Clock dom
    -> Reset dom
    -> Enable dom
    -> Vec d a
    -> Signal dom (Vec d a)
    -> Signal dom (Vec d a)
    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
    en Vec d a
    m (Unbundled dom (Vec d a) -> Signal dom (Vec d a)
    forall a (dom :: Domain).
    Bundle a =>
    Unbundled dom a -> Signal dom a
    forall (dom :: Domain).
    Unbundled dom (Vec d a) -> Signal dom (Vec d a)
    bundle Vec d (Signal dom a)
    Unbundled dom (Vec d a)
    r')
               in  Vec (0 + 1) (Signal dom a) -> Signal dom a
    forall (n :: Nat) a. Vec (n + 1) a -> a
    head Vec 1 (Signal dom a)
    Vec (0 + 1) (Signal dom a)
    o

    -- | Delay a 'DSignal' for @d@ periods, where @d@ is derived from the
    -- context.
    --
    -- @
    -- delay2
    --   :: KnownDomain dom
    --   => Clock dom
    --   -> Reset dom
    --   -> Enable dom
    --   -> Int
    --   -> 'DSignal' dom n Int
    --   -> 'DSignal' dom (n + 2) Int
    -- delay2 = 'delayedI'
    -- @
    --
    -- >>> sampleN 7 (delay2 systemClockGen resetGen enableGen (-1) (dfromList ([0..])))
    -- [-1,-1,-1,1,2,3,4]
    --
    -- @d@ can also be specified using type application:
    --
    -- >>> :t delayedI @3
    -- delayedI @3
    --   :: ... =>
    --      Clock dom
    --      -> Reset dom
    --      -> Enable dom
    --      -> a
    --      -> DSignal dom n a
    --      -> DSignal dom (n + 3) a
    delayedI
      :: ( KnownNat d
         , KnownDomain dom
         , NFDataX a )
      => Clock dom
      -> Reset dom
      -> Enable dom
      -> a
      -- ^ Initial value
      -> DSignal dom n a
      -> DSignal dom (n + d) a
    delayedI :: forall (d :: Nat) (dom :: Domain) a (n :: Nat).
    (KnownNat d, KnownDomain dom, NFDataX a) =>
    Clock dom
    -> Reset dom
    -> Enable dom
    -> a
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayedI Clock dom
    clk Reset dom
    rst Enable dom
    en a
    dflt = Clock dom
    -> Reset dom
    -> Enable dom
    -> Vec d a
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    forall (dom :: Domain) a (n :: Nat) (d :: Nat).
    (KnownDomain dom, KnownNat d, NFDataX a) =>
    Clock dom
    -> Reset dom
    -> Enable dom
    -> Vec d a
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayed Clock dom
    clk Reset dom
    rst Enable dom
    en (a -> Vec d a
    forall (n :: Nat) a. KnownNat n => a -> Vec n a
    repeat a
    dflt)

    -- | Delay a 'DSignal' for @d@ cycles, the value at time 0..d-1 is /a/.
    --
    -- @
    -- delayN2
    --   :: 'KnownDomain' dom
    --   => Int
    --   -> 'Enable' dom
    --   -> 'Clock' dom
    --   -> 'DSignal' dom n Int
    --   -> 'DSignal' dom (n + 2) Int
    -- delayN2 = 'delayN' d2
    -- @
    --
    -- >>> printX $ sampleN 6 (delayN2 (-1) enableGen systemClockGen (dfromList [1..]))
    -- [-1,-1,1,2,3,4]
    delayN
      :: forall dom a d n
       . ( KnownDomain dom
         , NFDataX a )
      => SNat d
      -> a
      -- ^ Initial value
      -> Enable dom
      -> Clock dom
      -> DSignal dom n a
      -> DSignal dom (n+d) a
    delayN :: forall (dom :: Domain) a (d :: Nat) (n :: Nat).
    (KnownDomain dom, NFDataX a) =>
    SNat d
    -> a
    -> Enable dom
    -> Clock dom
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayN SNat d
    d a
    dflt Enable dom
    ena Clock dom
    clk = Signal dom a -> DSignal dom (n + d) a
    forall a b. Coercible a b => a -> b
    coerce (Signal dom a -> DSignal dom (n + d) a)
    -> (DSignal dom n a -> Signal dom a)
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Signal dom a -> Signal dom a
    go (SNat d -> Integer
    forall (n :: Nat). SNat n -> Integer
    snatToInteger SNat d
    d) (Signal dom a -> Signal dom a)
    -> (DSignal dom n a -> Signal dom a)
    -> DSignal dom n a
    -> Signal dom a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall a b. Coercible a b => a -> b
    forall a b. Coercible a b => a -> b
    coerce @_ @(Signal dom a)
      where
        go :: Integer -> Signal dom a -> Signal dom a
    go Integer
    0 = Signal dom a -> Signal dom a
    forall a. a -> a
    id
        go Integer
    i = Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    forall (dom :: Domain) a.
    (KnownDomain dom, NFDataX a) =>
    Clock dom -> Enable dom -> a -> Signal dom a -> Signal dom a
    delay Clock dom
    clk Enable dom
    ena a
    dflt (Signal dom a -> Signal dom a)
    -> (Signal dom a -> Signal dom a) -> Signal dom a -> Signal dom a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Signal dom a -> Signal dom a
    go (Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)

    -- | Delay a 'DSignal' for @d@ cycles, where @d@ is derived from the context.
    -- The value at time 0..d-1 is a default value.
    --
    -- @
    -- delayI2
    --   :: 'KnownDomain' dom
    --   => Int
    --   -> 'Enable' dom
    --   -> 'Clock' dom
    --   -> 'DSignal' dom n Int
    --   -> 'DSignal' dom (n + 2) Int
    -- delayI2 = 'delayI'
    -- @
    --
    -- >>> sampleN 6 (delayI2 (-1) enableGen systemClockGen (dfromList [1..]))
    -- [-1,-1,1,2,3,4]
    --
    -- You can also use type application to do the same:
    --
    -- >>> sampleN 6 (delayI @2 (-1) enableGen systemClockGen (dfromList [1..]))
    -- [-1,-1,1,2,3,4]
    delayI
      :: forall d n a dom
       . ( NFDataX a
         , KnownDomain dom
         , KnownNat d )
      => a
      -- ^ Initial value
      -> Enable dom
      -> Clock dom
      -> DSignal dom n a
      -> DSignal dom (n+d) a
    delayI :: forall (d :: Nat) (n :: Nat) a (dom :: Domain).
    (NFDataX a, KnownDomain dom, KnownNat d) =>
    a
    -> Enable dom
    -> Clock dom
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayI a
    dflt = SNat d
    -> a
    -> Enable dom
    -> Clock dom
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    forall (dom :: Domain) a (d :: Nat) (n :: Nat).
    (KnownDomain dom, NFDataX a) =>
    SNat d
    -> a
    -> Enable dom
    -> Clock dom
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayN (SNat d
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: SNat d) a
    dflt

    data DelayedFold (dom :: Domain) (n :: Nat) (delay :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
    type instance Apply (DelayedFold dom n delay a) k = DSignal dom (n + (delay*k)) a

    -- | Tree fold over a 'Vec' of 'DSignal's with a combinatorial function,
    -- and delaying @delay@ cycles after each application.
    -- Values at times 0..(delay*k)-1 are set to a default.
    --
    -- @
    -- countingSignals :: Vec 4 (DSignal dom 0 Int)
    -- countingSignals = repeat (dfromList [0..])
    -- @
    --
    -- >>> printX $ sampleN 6 (delayedFold  d1 (-1) (+) enableGen systemClockGen countingSignals)
    -- [-1,-2,0,4,8,12]
    --
    -- >>> printX $ sampleN 8 (delayedFold d2 (-1) (*) enableGen systemClockGen countingSignals)
    -- [-1,-1,1,1,0,1,16,81]
    delayedFold
      :: forall dom  n delay k a
       . ( NFDataX a
         , KnownDomain dom
         , KnownNat delay
         , KnownNat k )
      => SNat delay
      -- ^ Delay applied after each step
      -> a
      -- ^ Initial value
      -> (a -> a -> a)
      -- ^ Fold operation to apply
      -> Enable dom
      -> Clock dom
      -> Vec (2^k) (DSignal dom n a)
      -- ^ Vector input of size 2^k
      -> DSignal dom (n + (delay * k)) a
      -- ^ Output Signal delayed by (delay * k)
    delayedFold :: forall (dom :: Domain) (n :: Nat) (delay :: Nat) (k :: Nat) a.
    (NFDataX a, KnownDomain dom, KnownNat delay, KnownNat k) =>
    SNat delay
    -> a
    -> (a -> a -> a)
    -> Enable dom
    -> Clock dom
    -> Vec (2 ^ k) (DSignal dom n a)
    -> DSignal dom (n + (delay * k)) a
    delayedFold SNat delay
    _ a
    dflt a -> a -> a
    op Enable dom
    ena Clock dom
    clk = Proxy (DelayedFold dom n delay a)
    -> (DSignal dom n a -> DelayedFold dom n delay a @@ 0)
    -> (forall (l :: Nat).
        SNat l
        -> (DelayedFold dom n delay a @@ l)
        -> (DelayedFold dom n delay a @@ l)
        -> DelayedFold dom n delay a @@ (l + 1))
    -> Vec (2 ^ k) (DSignal dom n a)
    -> DelayedFold dom n delay a @@ k
    forall (p :: TyFun Nat Type -> Type) (k :: Nat) a.
    KnownNat k =>
    Proxy p
    -> (a -> p @@ 0)
    -> (forall (l :: Nat).
        SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1))
    -> Vec (2 ^ k) a
    -> p @@ k
    dtfold (Proxy (DelayedFold dom n delay a)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (DelayedFold dom n delay a)) DSignal dom n a -> DelayedFold dom n delay a @@ 0
    DSignal dom n a -> DSignal dom n a
    forall a. a -> a
    id SNat l
    -> (DelayedFold dom n delay a @@ l)
    -> (DelayedFold dom n delay a @@ l)
    -> DelayedFold dom n delay a @@ (l + 1)
    forall (l :: Nat).
    SNat l
    -> (DelayedFold dom n delay a @@ l)
    -> (DelayedFold dom n delay a @@ l)
    -> DelayedFold dom n delay a @@ (l + 1)
    go
      where
        go :: SNat l
           -> DelayedFold dom n delay a @@ l
           -> DelayedFold dom n delay a @@ l
           -> DelayedFold dom n delay a @@ (l+1)
        go :: forall (l :: Nat).
    SNat l
    -> (DelayedFold dom n delay a @@ l)
    -> (DelayedFold dom n delay a @@ l)
    -> DelayedFold dom n delay a @@ (l + 1)
    go SNat l
    SNat DelayedFold dom n delay a @@ l
    x DelayedFold dom n delay a @@ l
    y = a
    -> Enable dom
    -> Clock dom
    -> DSignal dom (n + (delay * l)) a
    -> DSignal dom ((n + (delay * l)) + delay) a
    forall (d :: Nat) (n :: Nat) a (dom :: Domain).
    (NFDataX a, KnownDomain dom, KnownNat d) =>
    a
    -> Enable dom
    -> Clock dom
    -> DSignal dom n a
    -> DSignal dom (n + d) a
    delayI a
    dflt Enable dom
    ena Clock dom
    clk (a -> a -> a
    op (a -> a -> a)
    -> DSignal dom (n + (delay * l)) a
    -> DSignal dom (n + (delay * l)) (a -> a)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> DelayedFold dom n delay a @@ l
    DSignal dom (n + (delay * l)) a
    x DSignal dom (n + (delay * l)) (a -> a)
    -> DSignal dom (n + (delay * l)) a
    -> DSignal dom (n + (delay * l)) a
    forall a b.
    DSignal dom (n + (delay * l)) (a -> b)
    -> DSignal dom (n + (delay * l)) a
    -> DSignal dom (n + (delay * l)) b
    forall (f :: Type -> Type) a b.
    Applicative f =>
    f (a -> b) -> f a -> f b
    <*> DelayedFold dom n delay a @@ l
    DSignal dom (n + (delay * l)) a
    y)