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

  Whereas the output of a Mealy machine depends on /current transition/, the
  output of a Moore machine depends on the /previous state/.

  Moore machines are strictly less expressive, but may impose laxer timing
  requirements.
-}

{-# LANGUAGE Safe #-}

module Clash.Explicit.Moore
  ( -- * Moore machines with explicit clock and reset ports
    moore
  , mooreB
  , medvedev
  , medvedevB
  )
where

import           Clash.Explicit.Signal
  (KnownDomain, Bundle (..), Clock, Reset, Signal, Enable, register)
import           Clash.XException                 (NFDataX)

{- $setup
>>> :set -XDataKinds -XTypeApplications
>>> import Clash.Explicit.Prelude
>>> let macT s (x,y) = x * y + s
>>> let mac clk rst en = moore clk rst en macT id 0
-}

-- | Create a synchronous function from a combinational function describing
-- a moore machine
--
-- @
-- macT
--   :: Int        -- Current state
--   -> (Int,Int)  -- Input
--   -> (Int,Int)  -- Updated state
-- macT s (x,y) = x * y + s
--
-- mac
--   :: 'KnownDomain' dom
--   => 'Clock' dom
--   -> 'Reset' dom
--   -> 'Enable' dom
--   -> 'Signal' dom (Int, Int)
--   -> 'Signal' dom Int
-- mac clk rst en = 'moore' clk rst en macT id 0
-- @
--
-- >>> simulate (mac systemClockGen systemResetGen enableGen) [(0,0),(1,1),(2,2),(3,3),(4,4)]
-- [0,0,1,5,14...
-- ...
--
-- Synchronous sequential functions can be composed just like their
-- combinational counterpart:
--
-- @
-- dualMac
--   :: 'KnownDomain' dom
--   => 'Clock' dom
--   -> 'Reset' dom
--   -> 'Enable' dom
--   -> ('Signal' dom Int, 'Signal' dom Int)
--   -> ('Signal' dom Int, 'Signal' dom Int)
--   -> 'Signal' dom Int
-- dualMac clk rst en (a,b) (x,y) = s1 + s2
--   where
--     s1 = 'moore' clk rst en mac id 0 ('bundle' (a,x))
--     s2 = 'moore' clk rst en mac id 0 ('bundle' (b,y))
-- @
moore
  :: ( KnownDomain dom
     , NFDataX s )
  => Clock dom
  -- ^ 'Clock' to synchronize to
  -> Reset dom
  -> Enable dom
  -> (s -> i -> s)
  -- ^ Transfer function in moore machine form: @state -> input -> newstate@
  -> (s -> o)
  -- ^ Output function in moore machine form: @state -> output@
  -> s
  -- ^ Initial state
  -> (Signal dom i -> Signal dom o)
  -- ^ Synchronous sequential function with input and output matching that
  -- of the moore machine
moore :: Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Signal dom i
-> Signal dom o
moore clk :: Clock dom
clk rst :: Reset dom
rst en :: Enable dom
en ft :: s -> i -> s
ft fo :: s -> o
fo iS :: s
iS =
  \i :: Signal dom i
i -> let s' :: Signal dom s
s' = s -> i -> s
ft (s -> i -> s) -> Signal dom s -> Signal dom (i -> s)
forall (f :: * -> *) 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 :: * -> *) 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
en s
iS Signal dom s
s'
        in s -> o
fo (s -> o) -> Signal dom s -> Signal dom o
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom s
s
{-# INLINABLE moore #-}

-- | Create a synchronous function from a combinational function describing
-- a moore machine without any output logic
medvedev
  :: ( KnownDomain dom
     , NFDataX s )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (s -> i -> s)
  -> s
  -> (Signal dom i -> Signal dom s)
medvedev :: Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> s
-> Signal dom i
-> Signal dom s
medvedev clk :: Clock dom
clk rst :: Reset dom
rst en :: Enable dom
en tr :: s -> i -> s
tr st :: s
st = Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> s)
-> s
-> Signal dom i
-> Signal dom s
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Signal dom i
-> Signal dom o
moore Clock dom
clk Reset dom
rst Enable dom
en s -> i -> s
tr s -> s
forall a. a -> a
id s
st
{-# INLINE medvedev #-}

-- | A version of 'moore' that does automatic 'Bundle'ing
--
-- Given a functions @t@ and @o@ of types:
--
-- @
-- __t__ :: Int -> (Bool, Int) -> Int
-- __o__ :: Int -> (Int, Bool)
-- @
--
-- When we want to make compositions of @t@ and @o@ in @g@ using 'moore', we have to
-- write:
--
-- @
-- g clk rst en a b c = (b1,b2,i2)
--   where
--     (i1,b1) = 'unbundle' (moore clk rst en t o 0 ('bundle' (a,b)))
--     (i2,b2) = 'unbundle' (moore clk rst en t o 3 ('bundle' (c,i1)))
-- @
--
-- Using 'mooreB' however we can write:
--
-- @
-- g clk rst en a b c = (b1,b2,i2)
--   where
--     (i1,b1) = 'mooreB' clk rst en t o 0 (a,b)
--     (i2,b2) = 'mooreB' clk rst en t o 3 (c,i1)
-- @
mooreB
  :: ( KnownDomain dom
     , NFDataX s
     , Bundle i
     , Bundle o )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (s -> i -> s)
  -- ^ Transfer function in moore machine form:
  -- @state -> input -> newstate@
  -> (s -> o)
  -- ^ Output function in moore machine form:
  -- @state -> output@
  -> s
  -- ^ Initial state
  -> (Unbundled dom i -> Unbundled dom o)
  -- ^ Synchronous sequential function with input and output matching that
  -- of the moore machine
mooreB :: Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Unbundled dom i
-> Unbundled dom o
mooreB clk :: Clock dom
clk rst :: Reset dom
rst en :: Enable dom
en ft :: s -> i -> s
ft fo :: s -> o
fo iS :: s
iS i :: Unbundled dom i
i = Signal dom o -> Unbundled dom o
forall a (dom :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Signal dom i
-> Signal dom o
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Signal dom i
-> Signal dom o
moore Clock dom
clk Reset dom
rst Enable dom
en s -> i -> s
ft s -> o
fo s
iS (Unbundled dom i -> Signal dom i
forall a (dom :: Domain).
Bundle a =>
Unbundled dom a -> Signal dom a
bundle Unbundled dom i
i))
{-# INLINE mooreB #-}

-- | A version of 'medvedev' that does automatic 'Bundle'ing
medvedevB
  :: ( KnownDomain dom
     , NFDataX s
     , Bundle i
     , Bundle s )
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (s -> i -> s)
  -> s
  -> (Unbundled dom i -> Unbundled dom s)
medvedevB :: Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> s
-> Unbundled dom i
-> Unbundled dom s
medvedevB clk :: Clock dom
clk rst :: Reset dom
rst en :: Enable dom
en tr :: s -> i -> s
tr st :: s
st = Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> s)
-> s
-> Unbundled dom i
-> Unbundled dom s
forall (dom :: Domain) s i o.
(KnownDomain dom, NFDataX s, Bundle i, Bundle o) =>
Clock dom
-> Reset dom
-> Enable dom
-> (s -> i -> s)
-> (s -> o)
-> s
-> Unbundled dom i
-> Unbundled dom o
mooreB Clock dom
clk Reset dom
rst Enable dom
en s -> i -> s
tr s -> s
forall a. a -> a
id s
st
{-# INLINE medvedevB #-}