-----------------------------------------------------------------------------
-- |
-- Module      :  ForSyDe.Shallow.DataflowLib
-- Copyright   :  (c) SAM Group, KTH/ICT/ECS 2007-2008
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  forsyde-dev@ict.kth.se
-- Stability   :  experimental
-- Portability :  portable
--
-- The dataflow library defines data types, process constructors and
-- functions to model dataflow process networks, as described by Lee and
-- Parks in Dataflow process networks, IEEE Proceedings, 1995 ([LeeParks95]).
--
-- Each process is defined by a set of firing rules and corresponding
-- actions. A process fires, if the incoming signals match a firing
-- rule. Then the process consumes the matched tokens and executes the
-- action corresponding to the firing rule.
--
-----------------------------------------------------------------------------

module ForSyDe.Shallow.DataflowLib
    (
      -- * Data Types           
      -- | The data type @FiringToken@ defines the data type for tokens. The
      --   constructor @Wild@ constructs a token wildcard, the constructor
      --   @Value a@ constructs a token with value @a@.
      -- 
      -- A sequence (pattern) matches a signal, if the sequence is a prefix of
      -- the signal. The following list illustrates the firing rules:
      -- 
      --   * [⊥] matches always  (/NullS/ in ForSyDe)
      --
      --   * [*] matches signal with at least one token (/[Wild]/ in ForSyDe)
      --
      --   * [v] matches signal with v as its first value (/[Value v]/ in ForSyDe)
      --
      --   * [*,*] matches signals with at least two tokens (/[Wild,Wild]/ in ForSyDe) 
      -- 
      FiringToken(Wild, Value),
      -- * Combinational Process Constructors 
      -- | Combinatorial processes
      -- do not have an internal state. This means, that the output
      -- signal only depends on the input signals.
      --
      -- To illustrate the concept of data flow processes, we create a process that selects tokens from two inputs according to a control signal. 
      --
      -- The process has the following firing rules [LeeParks95]:
      --
      -- 
      --   * R1 = {[*], ⊥, [T]}
      --
      --   * R2 = {⊥, [*], [F]}
      -- 
      --
      -- The corresponding ForSyDe formulation of the firing rules is:
      --
      -- @
      --  selectRules = [ ([Wild], [], [Value True]),
      --                  ([], [Wild], [Value False]) ]
      -- @
      --
      -- For the output we formulate the following set of output functions:
      -- 
      -- @
      --  selectOutput xs ys _	= [ [headS xs], [headS ys] ]
      -- @
      -- 
      -- The select process /selectDF/ is then defined by:
      --
      -- @
      --  selectDF :: Eq a => Signal a -> Signal a 
      --                   -> Signal Bool -> Signal a
      --  selectDF =  zipWith3DF selectRules selectOutput
      -- @
      --
      -- Given the signals /s1/, /s2/ and /s3/
      --
      -- @
      --  s1 = signal [1,2,3,4,5,6]
      --  s2 = signal [7,8,9,10,11,12]
      --  s3 = signal [True, True, False, False, True, True]
      -- @
      --
      -- the executed process gives the following results:
      --
      -- @ 
      --  DataflowLib> selectDF s1 s2 s3
      --  {1,2,7,8,3,4} :: Signal Integer
      -- @
      --
      -- The library contains the following combinational process constructors:
      mapDF, zipWithDF, zipWith3DF, 
      -- * Sequential Process Constructors 
      -- | Sequential processes have
      -- an internal state. This means, that the output signal may
      -- depend internal state and on the input signal. 
      --     
      -- As an example we can view a process calculating the running sum
      -- of the input tokens. It has only one firing rule, which is
      -- illustrated below.
      --
      -- @
      --  Firing Rule    Next State    Output
      --  ------------------------------------
      --  (*,[*])        state + x     {state}
      -- @
      --
      -- A dataflow process using these firing rules and the initial state 0 can be formulated in ForSyDe as 
      --
      -- @
      --  rs xs = mealyDF firingRule nextState output initState xs
      --     where 
      --        firingRule	  = [(Wild, [Wild])]
      --        nextState state xs = [(state + headS xs)]
      --        output state _	  = [[state]]
      --        initState	  = 0
      -- @
      --
      -- Execution of the process gives
      --
      -- @     
      --  DataflowLib> rs (signal[1,2,3,4,5,6])
      --    {0,1,3,6,10,15} :: Signal Integer
      -- @
      -- 
      -- Another 'running sum' process /rs2/ takes two tokens, pushes
      -- them into a queue of five elements and calculates the sum as
      -- output.
      --
      -- @
      --  rs2 = mealyDF fs ns o init
      --     where 
      --        init	    = [0,0,0,0,0]
      --        fs	    = [(Wild, ([Wild, Wild]))]
      --        ns state xs = [drop 2 state ++ fromSignal (takeS 2 xs)]
      --        o state _   = [[(sum state)]]
      -- @
      -- 
      -- Execution of the process gives
      --
      -- @
      --  DataflowLib>rs2 (signal [1,2,3,4,5,6,7,8,9,10])
      --  {0,3,10,20,30} :: Signal Integer
      -- @
      scanlDF, mooreDF, mealyDF
    ) where

import ForSyDe.Shallow.CoreLib 


------------------------------------------------------------------------
--
-- DATA TYPES
--
------------------------------------------------------------------------

data FiringToken a = Wild
                   | Value a deriving (Eq, Show)


------------------------------------------------------------------------
--
-- COMBINATIONAL PROCESS CONSTRUCTORS
--
------------------------------------------------------------------------

-- |The process constructor @mapDF@ takes a list of firing rules, a list of corresponding output functions and generates a data flow process with one input and one output signal.
mapDF			:: Eq a => [[FiringToken a]] 
			   -> (Signal a -> [[b]]) -> Signal a -> Signal b

mapDF _  _  NullS		=  NullS   
mapDF rs as xs			=  output +-+ mapDF rs as xs'
   where
	   xs'			=  if matchedRule < 0 then
				      NullS
				   else
				      consumeDF rule xs
	   matchedRule		=  (matchDF rs xs)
	   rule			=  rs !! matchedRule
	   output		=  if matchedRule < 0 then
				      NullS
				   else
				      signal ((as xs) !! matchedRule)
-- |The process constructors @zipWithDF@ takes a list of firing rules, a list of corresponding output functions to generate a data flow process with two input signals and one output signal.
zipWithDF	        :: (Eq a, Eq b) => 
			   [([FiringToken b], [FiringToken a])] 
			   -> (Signal b -> Signal a -> [[c]]) -> Signal b 
			   -> Signal a -> Signal c

zipWithDF _  _  NullS NullS  = NullS
zipWithDF rs as xs	ys     = output +-+ zipWithDF rs as xs' ys'
   where 
	  (xs', ys')	       = if matchedRule < 0 then
				    (NullS, NullS)
				 else
				    consume2DF rule xs ys
	  matchedRule	       = (match2DF rs xs ys)
	  rule		       = rs !! matchedRule
	  output	       = if matchedRule < 0 then
				    NullS
				 else
				    signal ((as xs ys) !! matchedRule)

-- |The process constructors @zipWith3DF@ takes a list of firing rules, a list of corresponding output functions to generate a data flow process with three input signals and one output signal.
zipWith3DF		:: (Eq a, Eq b, Eq c) => 
			   [([FiringToken a],[FiringToken b],[FiringToken c])] 
			   -> (Signal a -> Signal b -> Signal c -> [[d]]) 
			   -> Signal a -> Signal b -> Signal c -> Signal d
zipWith3DF _  _  NullS NullS NullS = NullS
zipWith3DF rs as xs ys zs	= output +-+ zipWith3DF rs as xs' ys' zs'
   where 
         (xs', ys', zs')	= if matchedRule < 0 then
				     (NullS, NullS, NullS)
				  else
	 			    consume3DF rule xs ys zs
	 matchedRule		= (match3DF rs xs ys zs)
	 rule			= rs !! matchedRule
	 output			= if matchedRule < 0 then
				     NullS
		     	          else
				     signal ((as xs ys zs) !! matchedRule)


------------------------------------------------------------------------
--
-- SEQUENTIAL PROCESS CONSTRUCTORS
--
------------------------------------------------------------------------
-- | The process constructor @scanlDF@ implements a finite state machine without output decoder in the ForSyDe methodology. It takes a set of firing rules and a set of corresponding next state functions as arguments. A firing rule is a tuple. The first value is a pattern for the state, the second value corresponds to an input pattern. When a pattern matches, the process fires, the corresponding next state is executed, and the tokens matching the pattern are consumed.
scanlDF			  :: (Eq a, Eq b) => [(FiringToken b,[FiringToken a])]		
			     -> (b -> Signal a -> [b]) 
			     -> b -> Signal a -> Signal b
scanlDF _  _  _	    NullS	= NullS
scanlDF fs ns state xs		= (unitS state) 
				  +-+ scanlDF fs ns state' xs'
   where 
	   xs'			= if matchedRule < 0 then
				     NullS
				  else
				     consumeDF rule xs
	   matchedRule		= matchStDF fs state xs
	   rule			= snd (fs !! matchedRule)
	   state'		= if matchedRule < 0 then
				     error "No rule matches the pattern!"
				  else
				     (ns state xs) !! matchedRule

-- | The process constructor @mooreDF@ implements a Moore finite state machine in the ForSyDe methodology. It takes a set of firing rules, a set of corresponding next state functions and a set of output functions as argument. A firing rule is a tuple. The first value is a pattern for the state, the second value corresponds to an input pattern. When a pattern matches, the process fires, the corresponding next state and output functions are executed, and the tokens matching the pattern are consumed.
mooreDF			  :: (Eq a, Eq b) => [(FiringToken b,[FiringToken a])] 
			     -> (b -> Signal a -> [b]) -> (b -> [c]) 
			     -> b -> Signal a -> Signal c
mooreDF _  _  _ _     NullS	= NullS
mooreDF fs ns o state xs	= output +-+ mooreDF fs ns o state' xs'
   where 
	   xs'			= if matchedRule < 0 then
				     NullS
				  else
				     consumeDF rule xs
	   matchedRule		= matchStDF fs state xs
	   rule			= snd (fs !! matchedRule)
	   output		= signal (o state)
	   state'		= if matchedRule < 0 then
				     error "No rule matches the pattern!"
				  else
				     (ns state xs) !! matchedRule 


-- | The process constructor @mealyDF@ implements the most general state machine in the ForSyDe methodology. It takes a set of firing rules, a set of corresponding next state functions and a set of output functions as argument. A firing rule is a tuple. The first value is a pattern for the state, the second value corresponds to an input pattern. When a pattern matches, the process fires, the corresponding next state and output functions are executed, and the tokens matching the pattern are consumed.
mealyDF	:: (Eq a, Eq b) => [(FiringToken b,[FiringToken a])] 
	-> (b -> Signal a -> [b]) -> (b -> Signal a -> [[c]]) 
	-> b -> Signal a -> Signal c
mealyDF _  _  _ _     NullS	= NullS
mealyDF fs ns o state xs	= output +-+ mealyDF fs ns o state' xs'
   where 
	   xs'			= if matchedRule < 0 then
				     NullS
				  else
				     consumeDF rule xs
	   matchedRule		= matchStDF fs state xs
	   rule			= snd (fs !! matchedRule)
	   output		= signal ((o state xs) !! matchedRule)
	   state'		= if matchedRule < 0 then
				     error "No rule matches the pattern!"
				  else
				     (ns state xs) !! matchedRule  


------------------------------------------------------------------------
--
-- SUPPORTING FUNCTIONS
--
------------------------------------------------------------------------

-- The function 'prefixDF' takes a pattern and a signal and returns
-- 'True', if the pattern is a prefix from the signal.
prefixDF			:: Eq a => [FiringToken a] -> Signal a -> Bool
prefixDF []	        _	=  True
prefixDF _	        NullS	=  False
prefixDF (Wild:ps)      (_:-xs)	=  prefixDF ps xs
prefixDF ((Value p):ps) (x:-xs) =  if p == x then
				      prefixDF ps xs
				   else
				      False

-- The function 'consumeDF' takes a pattern and a signal and consumes
-- the pattern from the signal. The functions 'consume2DF' and
-- 'consume3DF' work in the same way as 'consumeDF', but with two and
-- three input signals.
consumeDF			:: Eq a => [FiringToken a] 
				   -> Signal a -> Signal a
consumeDF _	       NullS	=  NullS			   
consumeDF []	       xs       =  xs
consumeDF (Wild:ts)    (_:-xs)  =  consumeDF ts xs	       
consumeDF (Value t:ts) (x:-xs)  =  if t == x then
				      consumeDF ts xs
				   else
				      error "Tokens not correct"

consume2DF			 :: (Eq a, Eq b) => 
				    ([FiringToken a], [FiringToken b]) 
				    -> Signal a -> Signal b -> (Signal a, Signal b)
consume2DF (px, py) xs ys	 =  (consumeDF px xs,
				     consumeDF py ys)

consume3DF			 :: (Eq a, Eq b, Eq c) => 
				    ([FiringToken a], [FiringToken b], [FiringToken c]) 
				     -> Signal a -> Signal b -> Signal c 
				     -> (Signal a,Signal b,Signal c)
consume3DF (px, py, pz) xs ys zs = (consumeDF px xs,
				    consumeDF py ys,
				    consumeDF pz zs)

-- The function 'matchDF' checks, which firing rule, starting from 0, is
-- matched by the input signal. If no firing rule matches, the output is
-- '-1'. The functions 'maptch2S' and 'match3DF' work in the same way
-- for two and three inputs.
matchDF				:: (Num a, Eq b) => 
				   [[FiringToken b]] -> Signal b -> a
matchDF rs xs			=  matchDF' 0 rs xs
   where matchDF' _ []     _ 	=  -1
	 matchDF' n (r:rs) xs	=  if prefixDF r xs then
				      n
				   else
				      matchDF' (n+1) rs xs

match2DF			:: (Num a, Eq b, Eq c) => 
				   [([FiringToken b], [FiringToken c])]
				   -> Signal b -> Signal c -> a
match2DF rs xs ys		=  match2DF' 0 rs xs ys
   where match2DF' _ [] _ _	=  -1
         match2DF' n ((rx, ry):rs) xs ys
				=  if prefixDF rx xs &&
				     prefixDF ry ys 
				   then
				     n
				   else
				     match2DF' (n+1) rs xs ys

match3DF			:: (Num a, Eq b, Eq c, Eq d) => 
				   [([FiringToken b], [FiringToken d], [FiringToken c])]
				    -> Signal b -> Signal d -> Signal c -> a
match3DF rs xs ys zs		= match3DF' 0 rs xs ys zs
   where match3DF' _ [] _ _ _	= -1 
	 match3DF' n ((rx, ry, rz):rs) xs ys zs 
				=  if prefixDF rx xs &&
				      prefixDF ry ys &&
				      prefixDF rz zs 
				   then
				      n
				   else
				      match3DF' (n+1) rs xs ys zs  

-- The function 'matchStDF' works in the same way as 'matchDF', but it looks on patterns that include the state.
matchStDF			:: (Num a, Eq b, Eq c) => 
				   [(FiringToken c,[FiringToken b])] 
				   -> c -> Signal b -> a
matchStDF rs state xs		= matchStDF' 0 rs state xs
  where matchStDF' _ [] _ _	=  -1
	matchStDF' n (r:rs) state xs	
				=  if prefixDF (snd r) xs && 
				      matchState (fst r) state
				   then
				      n
				   else
				      matchStDF' (n+1) rs state xs	
		
matchState			:: Eq a => FiringToken a -> a -> Bool
matchState Wild      _		= True
matchState (Value v) x		= x == v 



------------------------------------------------------------------------
--
-- CODE FOR TESTING
--
------------------------------------------------------------------------


selectRules = [ ([Wild], [], [Value True]),
 		   ([], [Wild], [Value False]) ]


selectOutput xs ys _ =  [ [headS xs], [headS ys] ]

selectDF			:: Eq a => Signal a -> Signal a 
				   -> Signal Bool -> Signal a
selectDF			=  zipWith3DF selectRules selectOutput



s1 = signal [1,2,3,4,5,6]
s2 = signal [7,8,9,10,11,12]
s3 = signal [True, True, False, False, True, True]

rs xs			        = mealyDF firingRule nextState output initState xs
   where firingRule	        = [(Wild, [Wild])]
	 nextState state xs	= [(state + headS xs)]
	 output state _		= [[state]]
	 initState		= 0

rs2			   = mealyDF fs ns o init
   where init		   = [0,0,0,0,0]
	 fs		   = [(Wild, ([Wild, Wild]))]
	 ns state xs	   = [drop 2 state ++ fromSignal (takeS 2 xs)]
	 o state _	   = [[(sum state)]]