--
--  Control.Concurrent.Session :: Session Types for Haskell
--  Copyright (C) 2007  Matthew Sackman (matthew@wellquite.org)
--
--  This library is free software; you can redistribute it and/or
--  modify it under the terms of the GNU Lesser General Public
--  License as published by the Free Software Foundation; either
--  version 2.1 of the License, or (at your option) any later version.
--
--  This library is distributed in the hope that it will be useful,
--  but WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
--  Lesser General Public License for more details.
--
--  You should have received a copy of the GNU Lesser General Public
--  License along with this library; if not, write to the Free Software
--  Foundation, Inc., 59 Temple Place, Suite 330, Boston,
--  MA  02111-1307  USA
--
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-}

module Control.Concurrent.Session.Runtime
    where

import Control.Concurrent.Session.Loop
import Control.Concurrent.Session.BaseClasses
import Control.Concurrent.Session.BaseTypes
import Control.Concurrent.Session.List
import Control.Concurrent.Session.State
import Control.Concurrent.MVar
import Control.Concurrent

-- all that's necessary is that the first type to BuildReductionList *can't* be LoopT
instance forall a alist b.
    (BuildReductionList () (SessionSpec a) alist,
     MatchAnyChoice alist (SessionSpec b)) =>
    ZeroOrMoreSteps (SessionSpec a) (SessionSpec b) where
        stepN = findAnyMatch . findReduction ()
instance ZeroOrMoreSteps (SessionSpec a) (SessionSpec a) where
    stepN = id

mkState :: (JustSendsRecvs (SessionSpec spec) (SessionSpec outgoing) (SessionSpec incoming),
            JustSendsRecvs (SessionSpec spec') (SessionSpec incoming) (SessionSpec outgoing),
            DualT (SessionSpec spec) (SessionSpec spec')) =>
           (SessionSpec spec) ->
           IO (SessionState (SessionSpec spec) outgoing incoming,
               SessionState (SessionSpec spec') incoming outgoing)
mkState _ = do { outgoing <- newEmptyMVar
               ; incoming <- newEmptyMVar
               ; lock <- newEmptyMVar
               ; let s1 = SessionState outgoing incoming
               ; let s2 = SessionState incoming outgoing
               ; return (s1, s2)
               }

runSessionWithProcs :: (JustSendsRecvs (SessionSpec spec) (SessionSpec outgoing) (SessionSpec incoming),
                        JustSendsRecvs (SessionSpec specD) (SessionSpec incoming) (SessionSpec outgoing),
                        DualT (SessionSpec spec) (SessionSpec specD),
                        JustSendsRecvs (SessionSpec spec') (SessionSpec outgoing') (SessionSpec incoming'),
                        JustSendsRecvs (SessionSpec specD') (SessionSpec incoming') (SessionSpec outgoing'),
                        ZeroOrMoreSteps (SessionSpec spec) (SessionSpec spec'),
                        ZeroOrMoreSteps (SessionSpec specD) (SessionSpec specD')
                       ) =>
                       (SessionSpec spec)
                    -> Proc () (SessionSpec spec) (SessionSpec spec') outgoing outgoing' incoming incoming'
                    -> Proc () (SessionSpec specD) (SessionSpec specD') incoming incoming' outgoing outgoing'
                    -> IO (SessionSpec spec')
runSessionWithProcs spec (Proc p1) (Proc p2)
    = do { (s1, s2) <- mkState spec
         ; t1Term <- newEmptyMVar
         ; t2Term <- newEmptyMVar
         ; let f1 = (p1 s1) >>= writeTerminal t1Term
         ; let f2 = (p2 s2) >>= writeTerminal t2Term
         ; tid1 <- forkIO f1
         ; tid2 <- forkIO f2
         ; takeMVar t1Term
         ; takeMVar t2Term
         ; return (stepN spec)
         }
    where
      writeTerminal :: MVar () -> ((), SessionState s o i) -> IO ()
      writeTerminal termCell ((), someState) = putMVar termCell ()

send :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
         NextOp (SessionSpec (SessT t o)) (SessionSpec o),
         ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
         JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
        t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i ->
        IO ((), SessionState (SessionSpec s) o i)
send val (SessionState o i) = do { newEmpty <- newEmptyMVar
                                 ; putMVar o (Cell val newEmpty)
                                 ; return ((), SessionState newEmpty i)
                                 }

recv :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
         NextOp (SessionSpec (SessT t i)) (SessionSpec i),
         ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
         JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
        SessionState (SessionSpec (RecvT t s)) o (SessT t i) ->
        IO (t, SessionState (SessionSpec s) o i)
recv (SessionState o i) = do { (Cell val next) <- takeMVar i
                             ; return (val, SessionState o next)
                             }

-- log through stdout and send
sendLog :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
            ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
            JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
            Show t) =>
           t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i
             -> IO ((), SessionState (SessionSpec s) o i)
sendLog v = sliftIO (putStrLn $ "Sending '" ++ (show v) ++ "'")
            >~> send v

-- receive and log through stdout
recvLog :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
            ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
            JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
            ZeroOrMoreSteps (SessionSpec s) (SessionSpec s),
            Show t) =>
           SessionState (SessionSpec (RecvT t s)) o (SessT t i)
               -> IO (t, SessionState (SessionSpec s) o i)
recvLog = recv
          >~>= (\r -> sliftIO (putStrLn $ "Received '" ++ (show r) ++ "'")
                >~> returnS r)

infixl 1 >~>
infixl 1 >~>=

-- (>>) :: (Monad m) => m b -> m c -> m c
-- (>~>) serves the same purpose as (>>). So it's basically
-- on the lines of Session-from-a-to-b-with-type-n ->
--                 Session-from-b-to-c-with-type-m ->
--                 Session-from-a-to-c-with-type-m
(>~>) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
          JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
          JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
          ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
          ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
         ((SessionState (SessionSpec a) o i) ->
          IO (r, (SessionState (SessionSpec b) o' i'))) ->
         ((SessionState (SessionSpec b) o' i') ->
          IO (r', (SessionState (SessionSpec c) o'' i''))) ->
         ((SessionState (SessionSpec a) o i) ->
          IO (r', (SessionState (SessionSpec c) o'' i'')))
f >~> g = \s -> f s >>= \(_, s') -> g s'

-- (>>=) :: (Monad m) => m b -> (b -> m c) -> m c
-- (>~>=) serves the same purpose as (>>=). So it's basically
-- on the lines of Session-from-a-to-b-with-type-n ->
--                 (n -> Session-from-b-to-c-with-type-m) ->
--                 Session-from-a-to-c-with-type-m
(>~>=) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
           JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
           JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
           ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
           ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
           ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
          ((SessionState (SessionSpec a) o i) ->
           IO (r, (SessionState (SessionSpec b) o' i'))) ->
          (r -> (SessionState (SessionSpec b) o' i') ->
           IO (r', (SessionState (SessionSpec c) o'' i''))) ->
          ((SessionState (SessionSpec a) o i) ->
           IO (r', (SessionState (SessionSpec c) o'' i'')))
f >~>= g = \s -> f s >>= \(r, s') -> g r s'

-- return :: (Monad m) => a -> m a
-- returnS is pretty much the some as return, lifting a value into a session
-- returnS :: r -> Session-from-a-to-a-with-type-r
returnS :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
           r -> (SessionState (SessionSpec a) o i) ->
           IO (r, (SessionState (SessionSpec a) o i))
returnS v s = return (v, s)

end :: r -> (SessionState (SessionSpec EndT) EndT EndT) ->
       IO (r, (SessionState (SessionSpec EndT) EndT EndT))
end r state = return (r, state)

-- lifting just lift an IO straight in:
-- sliftIO :: IO r -> Session-from-a-to-a-with-type-r
sliftIO :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
           IO r -> ((SessionState (SessionSpec a) o i) ->
                    IO (r, (SessionState (SessionSpec a) o i)))
sliftIO f = \s -> f >>= \r -> returnS r s

-- for when the inner function wants to grab a value from outside...
-- sliftIO' :: (m -> IO n) -> (m -> Session-from-a-to-a-with-type n)
sliftIO' :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
             ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
            (r -> IO r') -> (r -> (SessionState (SessionSpec a) o i) ->
                             IO (r', (SessionState (SessionSpec a) o i)))
sliftIO' f = \r -> sliftIO (f r)