package Push(Push(..), apply, tee, pass, passed,
             buffer, buffered,  qbuffer, qbuffered, q1buffer, q1buffered, pipe,
             (»), sink, spew, regToPush, fifoToPush) where

import FIFO

--@ \subsubsection{Push}
--@
--@ \index{Push@\te{Push} (interface type)|textbf}
--@ The {\mbox{\te{Push a}}} interface represents a stream that
--@ consumes values of type ``\te{a}'' only when ``pushed'' by a producer.
--@
--@ Modules with the Push interface can be combined using the function
--@ \te{pipe},
--@ to model computations that comprise several steps,
--@ each of which may be buffered.

--@
infixr 12 »

--@ \begin{libverbatim}
--@ interface Push #(type a);
--@     method Action push(a x1);
--@ endinterface: Push
--@ \end{libverbatim}
interface Push a =
    push :: a -> Action

--@ Apply a function to the data in the stream.
--@ \begin{libverbatim}
--@ function Push#(a) apply(function b f(a x1), Push#(b) dst);
--@ \end{libverbatim}
apply :: (a -> b) -> Push b -> Push a
apply f dst = interface Push { push x = dst.push (f x) }

--@ Allow an action to peek at the stream.
--@ \begin{libverbatim}
--@ function Push#(a) tee(function Action a(a x1), Push#(a) dst);
--@ \end{libverbatim}
tee :: (a -> Action) -> Push a -> Push a
tee a dst = interface Push { push x = action { a x; dst.push x } }

--@ Wrap the stream in a module (without buffering).
--@ \begin{libverbatim}
--@ module pass#(Push#(a) dst)(Push#(a));
--@ \end{libverbatim}
pass :: (IsModule m c) => Push a -> m (Push a)
pass dst =
    module
      interface
        push x = dst.push x

--@ Apply a function to the data in the stream
--@ and wrap the stream in a module (without buffering).
--@ \begin{libverbatim}
--@ module passed#(function b f(a x1), Push#(b))(Push#(a));
--@ \end{libverbatim}
passed :: (IsModule m c) => (a -> b) -> Push b -> m (Push a)
passed f = pass · apply f

--@ Wrap a stream in a module
--@ (with a register buffer initialized to the first argument).
--@ \begin{libverbatim}
--@ module buffer#(a init, Push#(a) dst)(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
buffer :: (IsModule m c, Bits a sa) => a -> Push a -> m (Push a)
buffer init dst =
     module
       r :: Reg a
       r <- mkReg init
       interface
         push x = action { r := x; dst.push r }

--@ Wrap a stream in a module
--@ (with a FIFO buffer).
--@ \begin{libverbatim}
--@ module qbuffer#(Push#(a) dst)(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
qbuffer :: (IsModule m c, Bits a sa) => Push a -> m (Push a)
qbuffer dst =
    module
      q :: FIFO a <- mkFIFO
      rules
        "push": when True ==> action { dst.push q.first; q.deq }
      interface
        push x = action q.enq x



--@ Wrap a stream in a module
--@ with a 1 element (loopy) FIFO buffer.  This saves register elements, but
--@ the push action logic may depend on checking all elements in the pipe.
--@ \begin{libverbatim}
--@ module qbuffer#(Push#(a) dst)(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
q1buffer :: (IsModule m c, Bits a sa) => Push a -> m (Push a)
q1buffer dst =
    module
      q :: FIFO a <- mkLFIFO
      rules
        "push": when True ==> action { dst.push q.first; q.deq }
      interface
        push x = action q.enq x


--@ Apply a function to the data in the stream
--@ and wrap the stream in a module
--@ (with a register buffer initialized to `\US').
--@ \begin{libverbatim}
--@ module buffered#(function b f(a x1))(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
buffered :: (IsModule m c, Bits a sa) => (a -> b) -> Push b -> m (Push a)
buffered f = buffer _ · apply f

--@ Apply a function to the data in the stream
--@ and wrap the stream in a module
--@ (with a loopy FIFO buffer).
--@ \begin{libverbatim}
--@ module q1buffered#(function b f(a x1))(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
q1buffered :: (IsModule m c, Bits a sa) => (a -> b) -> Push b -> m (Push a)
q1buffered f = q1buffer · apply f

--@ Apply a function to the data in the stream
--@ and wrap the stream in a module
--@ (with a FIFO buffer).
--@ \begin{libverbatim}
--@ module qbuffered#(function b f(a x1))(Push#(a))
--@   provisos (Bits#(a, sa));
--@ \end{libverbatim}
qbuffered :: (IsModule m c, Bits a sa) => (a -> b) -> Push b -> m (Push a)
qbuffered f = qbuffer · apply f


--@ A consumer that drops all data.
--@ \begin{libverbatim}
--@ module sink(Push#(a));
--@ \end{libverbatim}
sink :: (IsModule m c) => m (Push a)
sink =
    module
      interface
        push _ = action {}

--@ A producer that always pushes junk on the given stream.
--@ \begin{libverbatim}
--@ module spew#(Push#(a) dst)(Empty);
--@ \end{libverbatim}
spew :: (IsModule m c) => Push a -> m Empty
spew dst =
    module
      rules "spew": when True ==> dst.push _

--@ Combine two streams (e.g., \te{pipe(spew, sink)}).
--@ \begin{libverbatim}
--@ function m#(b) pipe (function m#(b) f(a x1), m#(a) a)
--@   provisos (Monad#(m));
--@ \end{libverbatim}
(») :: (Monad m) => (a -> m b) -> m a -> m b
f » a = a `bind` f

pipe :: (Monad m) => (a -> m b) -> m a -> m b
pipe f a = (f » a)

--@ Wrap a \te{Push} interface around a register.
--@ \begin{libverbatim}
--@ function Push#(a) regToPush(Reg#(a) r);
--@ \end{libverbatim}
regToPush :: Reg a -> Push a
regToPush r =
    interface Push
      push x = r := x

--@ Wrap a \te{Push} interface around a FIFO.
--@ \begin{libverbatim}
--@ function Push#(a) fifoToPush(FIFO#(a) q);
--@ \end{libverbatim}
fifoToPush :: FIFO a -> Push a
fifoToPush q =
    interface Push
      push x = q.enq x