-----------------------------------------------------------------------------
-- |
-- Module      :  ForSyDe.Shallow.MoC.Synchronous.Process
-- Copyright   :  (c) ForSyDe Group, KTH 2007-2008
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  forsyde-dev@ict.kth.se
-- Stability   :  experimental
-- Portability :  portable
--
-- The synchronous process library defines processes for the
-- synchronous computational model. It is based on the synchronous
-- library "ForSyDe.Shallow.MoC.Synchronous".
-----------------------------------------------------------------------------
module ForSyDe.Shallow.MoC.Synchronous.Process (
  fifoDelaySY, finiteFifoDelaySY,
  memorySY, mergeSY, groupSY, counterSY
  ) where

import ForSyDe.Shallow.MoC.Synchronous.Lib
import ForSyDe.Shallow.Core
import ForSyDe.Shallow.Utility.Queue
import ForSyDe.Shallow.Utility.Memory

-- | The process 'fifoDelaySY' implements a synchronous model of a
-- FIFO with infinite size. The FIFOs take a list of values at each
-- event cycle and output one value. There is a delay of one cycle.
fifoDelaySY     :: Signal [a] -> Signal (AbstExt a)

-- | The process 'finiteFifoDelaySY' implements a FIFO with finite
-- size. The FIFOs take a list of values at each event cycle and
-- output one value. There is a delay of one cycle.
finiteFifoDelaySY   :: Int -> Signal [a] -> Signal (AbstExt a)

-- | The process 'memorySY' implements a synchronous memory. It uses
-- access functions of the type 'Read adr' and 'Write adr value'.
memorySY        :: Int -> Signal (Access a) -> Signal (AbstExt a) 

-- | The process 'mergeSY' merges two input signals into a single
-- signal. The process has an internal buffer in order to prevent loss
-- of data. The process is deterministic and outputs events according
-- to their time tag. If there are two valid values at on both
-- signals. The value of the first signal is output first.
mergeSY         :: Signal (AbstExt a) -> Signal (AbstExt a) 
           -> Signal (AbstExt a)

-- | The process 'counterSY' implements a counter, that counts from
--   min to max. The process 'counterSY' has no input and its output is
--   an infinite signal.
counterSY       :: (Enum a, Ord a) => a -> a -> Signal a

-- | The function 'groupSY' groups values into a vector of size n,
-- which takes n cycles. While the grouping takes place the output
-- from this process consists of absent values.
groupSY :: Int -> Signal a -> Signal (AbstExt (Vector a))

fifoDelaySY :: Signal [a] -> Signal (AbstExt a)
fifoDelaySY Signal [a]
xs =  (Queue a -> [a] -> Queue a)
-> (Queue a -> AbstExt a)
-> Queue a
-> Signal [a]
-> Signal (AbstExt a)
forall a b c.
(a -> b -> a) -> (a -> c) -> a -> Signal b -> Signal c
mooreSY Queue a -> [a] -> Queue a
forall a. Queue a -> [a] -> Queue a
fifoState Queue a -> AbstExt a
forall a. Queue a -> AbstExt a
fifoOutput ([a] -> Queue a
forall a. [a] -> Queue a
queue []) Signal [a]
xs

fifoState :: Queue a -> [a] -> Queue a
fifoState :: Queue a -> [a] -> Queue a
fifoState (Q []) [a]
xs =  ([a] -> Queue a
forall a. [a] -> Queue a
Q [a]
xs)
fifoState Queue a
q [a]
xs      =  (Queue a, AbstExt a) -> Queue a
forall a b. (a, b) -> a
fst (Queue a -> (Queue a, AbstExt a)
forall a. Queue a -> (Queue a, AbstExt a)
popQ (Queue a -> [a] -> Queue a
forall a. Queue a -> [a] -> Queue a
pushListQ Queue a
q [a]
xs))

fifoOutput :: Queue a -> AbstExt a
fifoOutput :: Queue a -> AbstExt a
fifoOutput (Q [])    = AbstExt a
forall a. AbstExt a
Abst
fifoOutput (Q (a
x:[a]
_)) = a -> AbstExt a
forall a. a -> AbstExt a
Prst a
x

finiteFifoDelaySY :: Int -> Signal [a] -> Signal (AbstExt a)
finiteFifoDelaySY Int
n Signal [a]
xs 
  = (FiniteQueue a -> [a] -> FiniteQueue a)
-> (FiniteQueue a -> AbstExt a)
-> FiniteQueue a
-> Signal [a]
-> Signal (AbstExt a)
forall a b c.
(a -> b -> a) -> (a -> c) -> a -> Signal b -> Signal c
mooreSY FiniteQueue a -> [a] -> FiniteQueue a
forall a. FiniteQueue a -> [a] -> FiniteQueue a
fifoStateFQ FiniteQueue a -> AbstExt a
forall a. FiniteQueue a -> AbstExt a
fifoOutputFQ (Int -> [a] -> FiniteQueue a
forall a. Int -> [a] -> FiniteQueue a
finiteQueue Int
n []) Signal [a]
xs

fifoStateFQ :: FiniteQueue a -> [a] -> FiniteQueue a
fifoStateFQ :: FiniteQueue a -> [a] -> FiniteQueue a
fifoStateFQ (FQ Int
n []) [a]
xs = (Int -> [a] -> FiniteQueue a
forall a. Int -> [a] -> FiniteQueue a
FQ Int
n [a]
xs)
fifoStateFQ FiniteQueue a
q         [a]
xs = (FiniteQueue a, AbstExt a) -> FiniteQueue a
forall a b. (a, b) -> a
fst (FiniteQueue a -> (FiniteQueue a, AbstExt a)
forall a. FiniteQueue a -> (FiniteQueue a, AbstExt a)
popFQ (FiniteQueue a -> [a] -> FiniteQueue a
forall a. FiniteQueue a -> [a] -> FiniteQueue a
pushListFQ FiniteQueue a
q [a]
xs))

fifoOutputFQ :: FiniteQueue a -> AbstExt a
fifoOutputFQ :: FiniteQueue a -> AbstExt a
fifoOutputFQ (FQ Int
_ [])    = AbstExt a
forall a. AbstExt a
Abst
fifoOutputFQ (FQ Int
_ (a
x:[a]
_)) = a -> AbstExt a
forall a. a -> AbstExt a
Prst a
x

memorySY :: Int -> Signal (Access a) -> Signal (AbstExt a)
memorySY Int
size Signal (Access a)
xs       = (Memory a -> Access a -> Memory a)
-> (Memory a -> Access a -> AbstExt a)
-> Memory a
-> Signal (Access a)
-> Signal (AbstExt a)
forall a b c.
(a -> b -> a) -> (a -> b -> c) -> a -> Signal b -> Signal c
mealySY Memory a -> Access a -> Memory a
forall a. Memory a -> Access a -> Memory a
ns Memory a -> Access a -> AbstExt a
forall a. Memory a -> Access a -> AbstExt a
o (Int -> Memory a
forall a. Int -> Memory a
newMem Int
size) Signal (Access a)
xs
  where 
    ns :: Memory a -> Access a -> Memory a
ns Memory a
mem (Read Int
x)    = Memory a -> Access a -> Memory a
forall a. Memory a -> Access a -> Memory a
memState Memory a
mem (Int -> Access a
forall a. Int -> Access a
Read Int
x)
    ns Memory a
mem (Write Int
x a
v) = Memory a -> Access a -> Memory a
forall a. Memory a -> Access a -> Memory a
memState Memory a
mem (Int -> a -> Access a
forall a. Int -> a -> Access a
Write Int
x a
v)
    o :: Memory a -> Access a -> AbstExt a
o  Memory a
mem (Read Int
x)    = Memory a -> Access a -> AbstExt a
forall a. Memory a -> Access a -> AbstExt a
memOutput Memory a
mem (Int -> Access a
forall a. Int -> Access a
Read Int
x)
    o  Memory a
mem (Write Int
x a
v) = Memory a -> Access a -> AbstExt a
forall a. Memory a -> Access a -> AbstExt a
memOutput Memory a
mem (Int -> a -> Access a
forall a. Int -> a -> Access a
Write Int
x a
v)


mergeSY :: Signal (AbstExt a) -> Signal (AbstExt a) -> Signal (AbstExt a)
mergeSY Signal (AbstExt a)
xs Signal (AbstExt a)
ys                           = ([a] -> AbstExt a -> AbstExt a -> [a])
-> ([a] -> AbstExt a)
-> [a]
-> Signal (AbstExt a)
-> Signal (AbstExt a)
-> Signal (AbstExt a)
forall a b c d.
(a -> b -> c -> a)
-> (a -> d) -> a -> Signal b -> Signal c -> Signal d
moore2SY [a] -> AbstExt a -> AbstExt a -> [a]
forall a. [a] -> AbstExt a -> AbstExt a -> [a]
mergeState [a] -> AbstExt a
forall a. [a] -> AbstExt a
mergeOutput [] Signal (AbstExt a)
xs Signal (AbstExt a)
ys
  where 
    mergeState :: [a] -> AbstExt a -> AbstExt a -> [a]
mergeState []     AbstExt a
Abst     AbstExt a
Abst     = []
    mergeState []     AbstExt a
Abst     (Prst a
y) = [a
y]
    mergeState []     (Prst a
x) AbstExt a
Abst     = [a
x]
    mergeState []     (Prst a
x) (Prst a
y) = [a
x, a
y]
    mergeState (a
_:[a]
us) AbstExt a
Abst     AbstExt a
Abst     = [a]
us
    mergeState (a
_:[a]
us) AbstExt a
Abst     (Prst a
y) = [a]
us [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
y]
    mergeState (a
_:[a]
us) (Prst a
x) AbstExt a
Abst     = [a]
us [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x]
    mergeState (a
_:[a]
us) (Prst a
x) (Prst a
y) = [a]
us [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x, a
y]
    mergeOutput :: [a] -> AbstExt a
mergeOutput []    = AbstExt a
forall a. AbstExt a
Abst
    mergeOutput (a
u:[a]
_) = a -> AbstExt a
forall a. a -> AbstExt a
Prst a
u 

groupSY :: Int -> Signal a -> Signal (AbstExt (Vector a))
groupSY Int
k                      = (Vector a -> a -> Vector a)
-> (Vector a -> a -> AbstExt (Vector a))
-> Vector a
-> Signal a
-> Signal (AbstExt (Vector a))
forall a b c.
(a -> b -> a) -> (a -> b -> c) -> a -> Signal b -> Signal c
mealySY Vector a -> a -> Vector a
forall a. Vector a -> a -> Vector a
f Vector a -> a -> AbstExt (Vector a)
forall a. Vector a -> a -> AbstExt (Vector a)
g Vector a
forall a. Vector a
s0 
  where
    s0 :: Vector a
s0                         = Vector a
forall a. Vector a
NullV
    f :: Vector a -> a -> Vector a
f Vector a
v a
x | (Vector a -> Int
forall a. Vector a -> Int
lengthV Vector a
v) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0   = a -> Vector a
forall a. a -> Vector a
unitV a
x
          | (Vector a -> Int
forall a. Vector a -> Int
lengthV Vector a
v) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k   = a -> Vector a
forall a. a -> Vector a
unitV a
x 
          | Bool
otherwise          = Vector a
v Vector a -> a -> Vector a
forall a. Vector a -> a -> Vector a
<: a
x
    g :: Vector a -> a -> AbstExt (Vector a)
g Vector a
v a
_ | (Vector a -> Int
forall a. Vector a -> Int
lengthV Vector a
v) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0   = AbstExt (Vector a)
forall a. AbstExt a
Abst
    g Vector a
v a
x | (Vector a -> Int
forall a. Vector a -> Int
lengthV Vector a
v) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1 = Vector a -> AbstExt (Vector a)
forall a. a -> AbstExt a
Prst (Vector a
vVector a -> a -> Vector a
forall a. Vector a -> a -> Vector a
<:a
x)
    g Vector a
_ a
_ | Bool
otherwise          = AbstExt (Vector a)
forall a. AbstExt a
Abst
 
counterSY :: a -> a -> Signal a
counterSY a
m a
n = (a -> a) -> a -> Signal a
forall a. (a -> a) -> a -> Signal a
sourceSY a -> a
f a
m
  where 
    f :: a -> a
f a
x | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
n    = a
m
        | Bool
otherwise = a -> a
forall a. Enum a => a -> a
succ a
x