{-
    Interleaving.hs
        Copyright 2008 Matthew Sackman <matthew@wellquite.org>

    This file is part of Session Types for Haskell.

    Session Types for Haskell is free software: you can redistribute it
    and/or modify it under the terms of the GNU General Public License
    as published by the Free Software Foundation, either version 3 of
    the License, or (at your option) any later version.

    Session Types for Haskell 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 General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with Session Types for Haskell.
    If not, see <http://www.gnu.org/licenses/>.
-}

{-# LANGUAGE FlexibleContexts, ExistentialQuantification, ScopedTypeVariables, PatternSignatures #-}

-- | A single thread should be able to have multiple concurrent
-- conversations with other threads. So this module places
-- 'InterleavedChain' as an instance of 'SMonad', and equipts it with
-- the capability to manage and modify a mapping of channels to other
-- threads. Note there is some danger in here. Deadlocks can start to
-- appear if you're silly or deliberately mean. However, this is
-- starting to get towards the Actor / Erlang model of message
-- passing.

module Control.Concurrent.Session.Interleaving
    ( InterleavedChain ()
    , withChannel
    , createChannel
    , createChannel'
    , runInterleaved
    , sjumpCh
    , ssendCh
    , srecvCh
    , sofferCh
    , sselectCh
    ) where

import Control.Concurrent.Session.Number
import Control.Concurrent.Session.Map
import Control.Concurrent.Session.SMonad
import Control.Concurrent.Session.SessionType
import Control.Concurrent.Session.Runtime
import Control.Concurrent.Session.List
import Control.Concurrent
import Control.Monad

type InterleavedChain f t res = SChain IO f t res

-- | Perform the given actions on the given channel. Note that the
-- value emitted by the actions will be passed out.
withChannel :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (fromO, fromI))
               , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (toO, toI)) (TyMap keyToIdx idxToValue')
               ) =>
    idx -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res ->
    InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res
withChannel idx chain
    = SChain $ \mp -> do { st <- mapLookup mp idx
                         ; (res, st') <- runSessionChain chain st
                         ; mp' <- mapUpdate mp idx st'
                         ; return (res, mp')
                         }

-- | This is a sane wrapper around 'createChannel''. The difference is
-- that this version ensures the child starts off only knowing about
-- the parent, which is clearly the sanest idea.
createChannel :: forall prog prog' progOut progIn init fromO fromI
                 keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
                 keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild''
                 idxOfChild .
    ( Dual prog prog', Dual prog' prog
    , ProgramToMVarsOutgoing prog progOut
    , ProgramToMVarsOutgoing prog' progIn
    , SWellFormedConfig init (D0 E) prog
    , SWellFormedConfig init (D0 E) prog'
    , TyListIndex progOut init (MVar (ProgramCell (Cell fromO)))
    , TyListIndex progIn init (MVar (ProgramCell (Cell fromI)))
    , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
    , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
                    (SessionState prog progOut progIn (fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')
    , MapInsert (TyMap Nil Nil) (D0 E)
                    (SessionState prog' progIn progOut (fromI, fromO)) (TyMap keyToIdxChild' idxToValueChild')
    ) =>
    prog -> init ->
    ((D0 E) -> InterleavedChain (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'') ()) ->
    InterleavedChain (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfChild
createChannel prog init child = createChannel' prog init emptyMap child

-- | Think of this as /spawn/ of /fork/ - it creates a child thread
-- which must be prepared to communicate with you. You get a channel
-- set up to the child which is emitted by this function. The child is
-- first told about the channel back to you. The child can go off and
-- do what ever it wants, including creating additional channels. The
-- child starts off with the childMap you supply, extended with the
-- new channel from you to the child. Note that you're asking for
-- trouble if you try creating a child without an 'emptyMap' as
-- channels (and sessions in general) are not in any way designed to
-- be shared between /more/ than two parties at a time.
createChannel' :: forall prog prog' progOut progIn init fromO fromI
                 keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
                 keyToIdxChild idxToValueChild keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild''
                 idxOfChild idxOfMe .
    ( Dual prog prog', Dual prog' prog
    , ProgramToMVarsOutgoing prog progOut
    , ProgramToMVarsOutgoing prog' progIn
    , SWellFormedConfig init (D0 E) prog
    , SWellFormedConfig init (D0 E) prog'
    , TyListIndex progOut init (MVar (ProgramCell (Cell fromO)))
    , TyListIndex progIn init (MVar (ProgramCell (Cell fromI)))
    , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
    , MapSize (TyMap keyToIdxChild idxToValueChild) idxOfMe
    , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
                    (SessionState prog progOut progIn (fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')
    , MapInsert (TyMap keyToIdxChild idxToValueChild) idxOfMe
                    (SessionState prog' progIn progOut (fromI, fromO)) (TyMap keyToIdxChild' idxToValueChild')
    ) =>
    prog -> init -> (TyMap keyToIdxChild idxToValueChild) ->
    (idxOfMe -> InterleavedChain (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'') ()) ->
    InterleavedChain (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfChild
createChannel' prog _ childMap child
    = SChain $ \mp -> do { mvarsOut <- programToMVarsOutgoing prog
                         ; mvarsIn <- programToMVarsOutgoing (dual prog)
                         ; ((), (childST :: SessionState prog' progIn progOut (fromI, fromO)))
                             <- runSessionChain (sjump :: SessionChain prog' progIn progOut
                                                          ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromI, fromO) ())
                                                (SessionState (dual prog) mvarsIn mvarsOut undefined undefined)
                         ; let idxOfMe :: idxOfMe = mapSize childMap
                         ; let childMap' :: TyMap keyToIdxChild' idxToValueChild' = mapInsert idxOfMe childST childMap
                         ; forkIO $ runSChain (child idxOfMe) childMap' >> return ()
                         ; ((), (myST :: SessionState prog progOut progIn (fromO, fromI)))
                             <- runSessionChain (sjump :: SessionChain prog progOut progIn
                                                          ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromO, fromI) ())
                                                (SessionState prog mvarsOut mvarsIn undefined undefined)
                         ; let idxOfChild :: idxOfChild = mapSize mp
                         ; return (idxOfChild, mapInsert idxOfChild myST mp)
                         }

-- | Run the root. Use this to start up a family from a single root.
runInterleaved :: InterleavedChain (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res -> IO res
runInterleaved ic = liftM fst $ runSChain ic emptyMap

-- | Convenience combination of 'withChannel' and 'sjump'
sjumpCh :: ( Dual prog prog'
           , ProgramToMVarsOutgoing prog progOut
           , ProgramToMVarsOutgoing prog' progIn
           , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil))
           , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (outgoing, incoming)) (TyMap keyToIdx idxToValue')
           , SWellFormedConfig l (D0 E) prog
           , SWellFormedConfig l (D0 E) prog'
           , TyListIndex progOut l (MVar (ProgramCell (Cell outgoing)))
           , TyListIndex progIn l (MVar (ProgramCell (Cell incoming)))
           ) =>
    idx -> InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
sjumpCh ch = withChannel ch sjump

-- | Convenience combination of 'withChannel' and 'ssend'
ssendCh :: ( Dual prog prog'
           , ProgramToMVarsOutgoing prog progOut
           , ProgramToMVarsOutgoing prog' progIn
           , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn ((Cons t nxt), incoming))
           , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (nxt, incoming)) (TyMap keyToIdx idxToValue')
           ) =>
    idx -> t -> InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
ssendCh ch t = withChannel ch (ssend t)

-- | Convenience combination of 'withChannel' and 'srecv'
srecvCh :: ( Dual prog prog'
           , ProgramToMVarsOutgoing prog progOut
           , ProgramToMVarsOutgoing prog' progIn
           , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (outgoing, (Cons t nxt)))
           , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (outgoing, nxt)) (TyMap keyToIdx idxToValue')
           ) =>
    idx -> InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t
srecvCh ch = withChannel ch (srecv)

-- | Convenience combination of 'withChannel' and 'soffer'
sofferCh :: ( Dual prog prog'
            , ProgramToMVarsOutgoing prog progOut
            , ProgramToMVarsOutgoing prog' progIn
            , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil))
            , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (outgoing, incoming)) (TyMap keyToIdx idxToValue')
            ) =>
    idx -> OfferImpls jumps prog progOut progIn (outgoing, incoming) finalResult ->
    InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') finalResult
sofferCh ch offerImpls = withChannel ch (soffer offerImpls)

-- | Convenience combination of 'withChannel' and 'sselectCh'
sselectCh :: ( Dual prog prog'
             , ProgramToMVarsOutgoing prog progOut
             , ProgramToMVarsOutgoing prog' progIn
             , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil))
             , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog progOut progIn (outgoing, incoming)) (TyMap keyToIdx idxToValue')
             , TyListLength jumps len
             , SmallerThan label len
             , TypeNumberToInt label
             , TyListIndex jumps label (Cons (Jump jumpTarget) Nil)
             , SWellFormedConfig jumpTarget (D0 E) prog
             , SWellFormedConfig jumpTarget (D0 E) prog'
             , TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing)))
             , TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming)))
             ) =>
    idx -> label -> InterleavedChain (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
sselectCh ch b = withChannel ch (sselect b)