{-|
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>
-}

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

#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif

{-# 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
  )
where

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

import Clash.Sized.Vector
  (Vec, dtfold, head, length, repeat, shiftInAt0, singleton)
import Clash.Signal.Delayed.Internal
  (DSignal(..), dfromList, dfromList_lazy, fromSignal, toSignal,
   unsafeFromSignal, antiDelay, feedback)

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
>>> :m -Clash.Prelude
>>> :m -Clash.Prelude.Safe
>>> 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 :: 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
coerce (Signal dom a -> Signal dom a
delaySignal (DSignal dom n a -> Signal dom a
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
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
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 :: 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 (toSignal (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 :: 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
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
. Coercible (DSignal dom n a) (Signal dom a) =>
DSignal dom n a -> Signal dom a
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 (toSignal (delayI2 (-1) enableGen systemClockGen (dfromList [1..])))
-- [-1,-1,1,2,3,4]
--
-- You can also use type application to do the same:
-- >>> sampleN 6 (toSignal (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 :: 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 (toSignal (delayedFold  d1 (-1) (+) enableGen systemClockGen countingSignals))
-- [-1,-2,0,4,8,12]
--
-- >>> printX $ sampleN 8 (toSignal (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 :: 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
forall a. a -> a
id 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 :: 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 (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)