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
withChannel :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, fromO, fromI))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current', toO, toI)) (TyMap keyToIdx idxToValue')
) =>
idx -> SessionChain prog prog' (current, fromO, fromI) (current', toO, toI) res ->
InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res
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)
}
class Fork invert init sessionsList prog prog'
sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe
fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe'
keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild
current current' currentUX currentUX' 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 sessionsListSorted current current' currentUX currentUX'
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)))
, TyListIndex prog init currentUX
, TyListIndex prog' init currentUX'
, ExpandPids prog currentUX current
, ExpandPids prog' currentUX' current'
, BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem)
, TyListSortNums sessionsList sessionsListSorted
, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
(SessionState prog prog' (current, fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')
, MapInsert (TyMap Nil Nil) (D0 E)
(SessionState prog' prog (current', 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
current current' currentUX currentUX' 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 (current', fromI, fromO)))
<- runSessionChain (sjump :: SessionChain prog' prog
((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (current', fromI, fromO) ())
(SessionState prog' prog mvarsIn mvarsOut undefined undefined undefined)
; childSessions <- buildPidTyMap prog (tyListSortNums 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' (current, fromO, fromI)))
<- runSessionChain (sjump :: SessionChain prog prog'
((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (current, fromO, fromI) ())
(SessionState prog prog' mvarsOut mvarsIn undefined 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 sessionsListSorted current current' currentUX currentUX'
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)))
, TyListIndex prog init currentUX
, TyListIndex prog' init currentUX'
, ExpandPids prog currentUX current
, ExpandPids prog' currentUX' current'
, BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem)
, TyListSortNums sessionsList sessionsListSorted
, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild
, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild
(SessionState prog' prog (current', fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe')
, MapInsert (TyMap Nil Nil) (D0 E)
(SessionState prog prog' (current, 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
current current' currentUX currentUX' 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' (current, fromO, fromI)))
<- runSessionChain (sjump :: SessionChain prog prog'
((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (current, fromO, fromI) ())
(SessionState prog prog' mvarsOut mvarsIn undefined undefined undefined)
; childSessions <- buildPidTyMap prog (tyListSortNums 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 (current', fromI, fromO)))
<- runSessionChain (sjump :: SessionChain prog' prog
((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (current', fromI, fromO) ())
(SessionState prog' prog mvarsIn mvarsOut undefined undefined undefined)
; let idxOfChild :: idxOfChild = mapSize mp
; return ((idxOfChild, iPidToPid childPid), mapInsert idxOfChild myST mp, localPid')
}
runInterleaved :: ( BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdx idxsToPairStructs)
, TyListSortNums sessionsList sessionsListSorted
) =>
sessionsList -> prog ->
InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs)
(TyMap Nil Nil) (TyMap keyToIdx idxToValue) res ->
IO res
runInterleaved sessions prog ic
= do { tyMap <- buildPidTyMap prog (tyListSortNums sessions)
; runInterleavedChain ic (rootPid tyMap prog) emptyMap >>= \(res, _, _) -> return res
}
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)))
, TyListIndex prog l current'
, ExpandPids prog current' current
, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((Cons (Jump l) Nil), (Cons (Jump l) Nil), (Cons (Jump l) Nil)))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')
) =>
idx -> InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
sjumpCh ch = withChannel ch sjump
ssendCh :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((Cons (Send t) nxt), (Cons t nxt'), incoming))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, 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)
srecvCh :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((Cons (Recv t) nxt), outgoing, (Cons t nxt')))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, outgoing, nxt')) (TyMap keyToIdx idxToValue')
) =>
idx -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t
srecvCh ch = withChannel ch (srecv)
sofferCh :: ( MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' ((Cons (Offer jumps) Nil), Cons (Choice jumps) Nil, Cons (Choice jumps) Nil))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')
) =>
idx -> OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult ->
InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') finalResult
sofferCh ch offerImpls = withChannel ch (soffer offerImpls)
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 (Select jumps) Nil), Cons (Choice jumps) Nil, Cons (Choice jumps) Nil))
, MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, 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)))
, TyListIndex prog jumpTarget currentUX
, ExpandPids prog currentUX current
) =>
idx -> label -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()
sselectCh ch b = withChannel ch (sselect b)