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
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')
}
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
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)
}
runInterleaved :: InterleavedChain (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res -> IO res
runInterleaved ic = liftM fst $ runSChain ic emptyMap
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
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)
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)
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)
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)