{-# LANGUAGE FlexibleContexts
           , ScopedTypeVariables
           , PatternSignatures
           , TypeFamilies
           , MultiParamTypeClasses
           , FlexibleInstances
           , UndecidableInstances #-}

{-
    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/>.
-}


-- | 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
    ( withChannel
    , Fork(..)
    , runInterleaved
    , sjumpCh
    , ssendCh
    , srecvCh
    , sofferCh
    , sselectCh
    ) where

import Control.Concurrent.Session.Bool
import Control.Concurrent.Session.Number
import Control.Concurrent.Session.Map
import Control.Concurrent.Session.SessionType
import Control.Concurrent.Session.Runtime
import Control.Concurrent.Session.List
import Control.Concurrent.Session.Pid
import Control.Concurrent
import Control.Monad

-- | 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 prog' (fromO, fromI))
               , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (toO, toI)) (TyMap keyToIdx idxToValue')
               ) =>
    idx -> SessionChain prog prog' (fromO, fromI) (toO, toI) res ->
    InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res
-- pidProg is not necessarily prog as prog could be the dual of pidProg
withChannel idx chain
    = InterleavedChain $
      \p mp -> do { let st = mapLookup mp idx
                  ; (res, st') <- runSessionChain chain st
                  ; let mp' = mapUpdate mp idx st'
                  ; return (res, mp', p)
                  }

-- | Think of this as /spawn/ or /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 and your Pid. The child
-- can go off and do what ever it wants, including creating additional
-- channels. The child starts off knowing with only one open channel
-- which is to the parent.
class Fork invert init sessionsList prog prog'
           sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe
           fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
           keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild where
    fork :: init -> invert -> sessionsList ->
            ((D0 E) -> Pid prog sessionsToIdxMe idxsToPairStructsMe ->
             InterleavedChain (InternalPid prog sessionsToIdxThem idxsToPairStructsThem)
                              (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'')
                              ()) ->
            InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe)
                             (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe')
                             (idxOfChild, Pid prog sessionsToIdxThem idxsToPairStructsThem)

instance forall prog prog' progOut progIn init
    fromO fromI sessionsList
    keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
    keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild''
    idxOfChild sessionsToIdxMe idxsToPairStructsMe sessionsToIdxThem idxsToPairStructsThem .
    ( ProgramToMVarsOutgoing prog prog progOut
    , ProgramToMVarsOutgoing prog' prog' progIn
    , ProgramToMVarsOutgoingT prog prog ~ progOut
    , ProgramToMVarsOutgoingT prog' 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)))
    , BuildPidTyMap prog sessionsList (TyMap sessionsToIdxThem idxsToPairStructsThem)
    , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
    , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
                    (SessionState prog prog' (fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')
    , MapInsert (TyMap Nil Nil) (D0 E)
                    (SessionState prog' prog (fromI, fromO)) (TyMap keyToIdxChild' idxToValueChild')
    , Dual prog prog'
    ) =>
    Fork False init sessionsList prog prog'
         sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe
         fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
         keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild where
             fork _ FF sessionsList child =
                 InterleavedChain $
                     \localPid@(IPid localPPid@(Pid _ prog _) _) mp ->
                         do { let prog' = dual prog
                            ; mvarsOut <- programToMVarsOutgoing prog prog
                            ; mvarsIn <- programToMVarsOutgoing prog' prog'
                            ; ((), (childST :: SessionState prog' prog (fromI, fromO)))
                                <- runSessionChain (sjump :: SessionChain prog' prog
                                                    ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromI, fromO) ())
                                                    (SessionState prog' prog mvarsIn mvarsOut undefined undefined)
                            ; childSessions <- buildPidTyMap prog sessionsList
                            ; let childMap :: TyMap keyToIdxChild' idxToValueChild' = mapInsert (D0 E) childST emptyMap
                                  (localPid', childPid) = makePid localPid childSessions
                            ; forkIO $ runInterleavedChain (child (D0 E) localPPid) childPid childMap >> return ()
                            ; ((), (myST :: SessionState prog prog' (fromO, fromI)))
                                <- runSessionChain (sjump :: SessionChain prog prog'
                                                    ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromO, fromI) ())
                                                    (SessionState prog prog' mvarsOut mvarsIn undefined undefined)
                            ; let idxOfChild :: idxOfChild = mapSize mp
                            ; return ((idxOfChild, iPidToPid childPid), mapInsert idxOfChild myST mp, localPid')
                            }

instance forall prog prog' progOut progIn init
    fromO fromI sessionsList
    keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
    keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild''
    idxOfChild sessionsToIdxMe idxsToPairStructsMe sessionsToIdxThem idxsToPairStructsThem .
    ( ProgramToMVarsOutgoing prog prog progOut
    , ProgramToMVarsOutgoing prog' prog' progIn
    , ProgramToMVarsOutgoingT prog prog ~ progOut
    , ProgramToMVarsOutgoingT prog' 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)))
    , BuildPidTyMap prog sessionsList (TyMap sessionsToIdxThem idxsToPairStructsThem)
    , MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
    , MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
                    (SessionState prog' prog (fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe')
    , MapInsert (TyMap Nil Nil) (D0 E)
                    (SessionState prog prog' (fromO, fromI)) (TyMap keyToIdxChild' idxToValueChild')
    , Dual prog prog'
    ) =>
    Fork True init sessionsList prog prog'
         sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe
         fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
         keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild where
             fork _ TT sessionsList child =
                 InterleavedChain $
                     \localPid@(IPid localPPid@(Pid _ prog _) _) mp ->
                         do { let prog' = dual prog
                            ; mvarsOut <- programToMVarsOutgoing prog prog
                            ; mvarsIn <- programToMVarsOutgoing prog' prog'
                            ; ((), (childST :: SessionState prog prog' (fromO, fromI)))
                                <- runSessionChain (sjump :: SessionChain prog prog'
                                                    ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromO, fromI) ())
                                                    (SessionState prog prog' mvarsOut mvarsIn undefined undefined)
                            ; childSessions <- buildPidTyMap prog sessionsList
                            ; let childMap :: TyMap keyToIdxChild' idxToValueChild' = mapInsert (D0 E) childST emptyMap
                                  (localPid', childPid) = makePid localPid childSessions
                            ; forkIO $ runInterleavedChain (child (D0 E) localPPid) childPid childMap >> return ()
                            ; ((), (myST :: SessionState prog' prog (fromI, fromO)))
                                <- runSessionChain (sjump :: SessionChain prog' prog
                                                    ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) (fromI, fromO) ())
                                                    (SessionState prog' prog mvarsIn mvarsOut undefined undefined)
                            ; let idxOfChild :: idxOfChild = mapSize mp
                            ; return ((idxOfChild, iPidToPid childPid), mapInsert idxOfChild myST mp, localPid')
                            }

-- | Run the root. Use this to start up a family from a single root.
runInterleaved :: (BuildPidTyMap pidProg sessionsList (TyMap sessionsToIdx idxsToPairStructs)) =>
                  sessionsList -> pidProg ->
                  InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs)
                                   (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res ->
                  IO res
runInterleaved sessions pidProg ic
    = do { tyMap <- buildPidTyMap pidProg sessions
         ; runInterleavedChain ic (rootPid tyMap pidProg) emptyMap >>= \(res, _, _) -> return res
         }

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

-- | Convenience combination of 'withChannel' and 'ssend'
ssendCh :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((Cons t nxt), incoming))
           , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, incoming)) (TyMap keyToIdx idxToValue')
           ) =>
    idx -> t -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
ssendCh ch t = withChannel ch (ssend t)

-- | Convenience combination of 'withChannel' and 'srecv'
srecvCh :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (outgoing, (Cons t nxt)))
           , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (outgoing, nxt)) (TyMap keyToIdx idxToValue')
           ) =>
    idx -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t
srecvCh ch = withChannel ch (srecv)

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

-- | Convenience combination of 'withChannel' and 'sselectCh'
sselectCh :: ( ProgramToMVarsOutgoingT prog prog ~ progOut
             , ProgramToMVarsOutgoingT prog' prog' ~ progIn
             , ProgramToMVarsOutgoing prog prog progOut
             , ProgramToMVarsOutgoing prog' prog' progIn
             , MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil))
             , MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (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 (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
sselectCh ch b = withChannel ch (sselect b)