module Control.Concurrent.Session.Runtime
( OfferImpls (OfferImplsNil)
, (~||~)
, SessionState (..)
, SessionChain (..)
, sjump
, ssend
, srecv
, soffer
, sselect
, run
, ProgramToMVarsOutgoing (..)
, ProgramCell ()
, Cell ()
) where
import Control.Concurrent.Session.Bool
import Control.Concurrent.Session.List
import Control.Concurrent.Session.SessionType
import Control.Concurrent.Session.Number
import Control.Concurrent.Session.SMonad
import Control.Concurrent
data OfferImpls :: * -> * -> * -> * -> * -> * where
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult
OfferCons :: (SessionChain prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) finalState finalResult) ->
OfferImpls jumps prog prog' finalState finalResult ->
OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult
(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l current currentUX .
( (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 currentUX
, ExpandPids prog currentUX current
) =>
(SessionChain prog prog' (current, outgoing, incoming) finalState finalResult) ->
(OfferImpls jumps prog prog' finalState finalResult) ->
(OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult)
(~||~) chain nxt = OfferCons chain' nxt
where
chain' :: SessionChain prog prog' ((Cons (Jump l) Nil), (Cons (Jump l) Nil), (Cons (Jump l) Nil)) finalState finalResult
chain' = sjump ~>> chain
infixr 5 ~||~
class WalkOfferImpls prog prog' finalState finalResult where
walkOfferImpls :: Int -> OfferImpls jumps prog prog' finalState finalResult -> SessionChain prog prog' from finalState finalResult
instance forall prog prog' finalState finalResult .
WalkOfferImpls prog prog' finalState finalResult where
walkOfferImpls 0 (OfferCons chain _) = SessionChain f
where
f :: forall from .
SessionState prog prog' from ->
IO (finalResult, SessionState prog prog' finalState)
f (SessionState prog prog' outgoingProg incomingProg _ outNotify _ inNotify _)
= runSessionChain chain (SessionState prog prog' outgoingProg incomingProg undefined outNotify undefined inNotify undefined)
walkOfferImpls n (OfferCons _ rest) = walkOfferImpls (n 1) rest
walkOfferImpls _ _ = error "The Truly Impossible Happened."
data Cell :: * -> * where
Cell :: val -> MVar (Cell nxt) -> Cell (Cons val nxt)
SelectCell :: Int -> Cell (Cons (Choice jumps) Nil)
data ProgramCell :: * -> * where
ProgramCell :: MVar a -> MVar (ProgramCell a) -> ProgramCell a
class ProgramToMVarsOutgoing progRef prog mvars | progRef prog -> mvars where
type ProgramToMVarsOutgoingT progRef prog
programToMVarsOutgoing :: progRef -> prog -> IO mvars
instance ProgramToMVarsOutgoing ref Nil Nil where
type ProgramToMVarsOutgoingT ref Nil = Nil
programToMVarsOutgoing _ p = return p
instance ( ProgramToMVarsOutgoing ref nxt nxt'
, TyList nxt
, TyList nxt'
) =>
ProgramToMVarsOutgoing ref (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt') where
type ProgramToMVarsOutgoingT ref (Cons val nxt) = (Cons (MVar (ProgramCell (Cell (Outgoing ref val)))) (ProgramToMVarsOutgoingT ref nxt))
programToMVarsOutgoing ref v
= do { hole <- newEmptyMVar
; rest <- programToMVarsOutgoing ref nxt
; return $ cons hole rest
}
where
nxt = tyTail v
data SessionState :: * -> * -> * -> * where
SessionState :: ( (ProgramToMVarsOutgoingT prog prog) ~ progOut
, (ProgramToMVarsOutgoingT prog' prog') ~ progIn
) =>
prog -> prog' -> progOut -> progIn ->
current ->
MVar (Maybe (Chan ())) ->
(MVar (Cell currentOutgoing)) ->
MVar (Maybe (Chan ())) ->
(MVar (Cell currentIncoming)) ->
SessionState prog prog' (current, currentOutgoing, currentIncoming)
newtype SessionChain prog prog' from to res
= SessionChain { runSessionChain :: (SessionState prog prog' from) ->
IO (res, SessionState prog prog' to)
}
instance SMonad (SessionChain prog prog') where
f ~>> g = SessionChain $
\x ->
do { (_, y) <- runSessionChain f x
; runSessionChain g y
}
f ~>>= g = SessionChain $
\x ->
do { (a, y) <- runSessionChain f x
; runSessionChain (g a) y
}
sreturn a = SessionChain $ \x -> return (a, x)
instance SMonadIO (SessionChain prog prog') where
sliftIO f = SessionChain $
\x ->
do { a <- f
; return (a, x)
}
carefullySwapToNextCell :: MVar (ProgramCell a) -> IO (ProgramCell a)
carefullySwapToNextCell programCellMVar
= do { maybeProgramCell <- tryTakeMVar programCellMVar
; case maybeProgramCell of
Nothing -> do { emptyProgramCell <- newEmptyMVar
; emptyProgramCellMVar <- newEmptyMVar
; let cell = (ProgramCell emptyProgramCell emptyProgramCellMVar)
; didPut <- tryPutMVar programCellMVar cell
; if didPut
then return cell
else takeMVar programCellMVar
}
(Just cell) -> return cell
}
sjump :: forall l prog prog' progOut progIn outgoing incoming current currentUX .
( (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 currentUX
, ExpandPids prog currentUX current
) =>
(SessionChain prog prog') ((Cons (Jump l) Nil), (Cons (Jump l) Nil), (Cons (Jump l) Nil)) (current, outgoing, incoming) ()
sjump = SessionChain f
where
f :: SessionState prog prog' (Cons (Jump l) Nil, (Cons (Jump l) Nil), (Cons (Jump l) Nil)) ->
IO ((), SessionState prog prog' (current, outgoing, incoming))
f (SessionState prog prog' outgoingProg incomingProg _ outNotify _ inNotify _)
= do { (ProgramCell outgoing outProgCellMVar') <- carefullySwapToNextCell outProgCellMVar
; (ProgramCell incoming inProgCellMVar') <- carefullySwapToNextCell inProgCellMVar
; let outgoingProg' = tyListUpdate outgoingProg (undefined :: l) outProgCellMVar'
; let incomingProg' = tyListUpdate incomingProg (undefined :: l) inProgCellMVar'
; return ((), (SessionState prog prog' outgoingProg' incomingProg' current outNotify outgoing inNotify incoming))
}
where
current::current = expandPids prog $ tyListIndex prog (undefined :: l)
outProgCellMVar = tyListIndex outgoingProg (undefined :: l)
inProgCellMVar = tyListIndex incomingProg (undefined :: l)
ssend :: forall t prog prog' nxt nxt' incoming .
t -> (SessionChain prog prog') ((Cons (Send t) nxt), (Cons t nxt'), incoming) (nxt, nxt', incoming) ()
ssend t = SessionChain f
where
f :: SessionState prog prog' ((Cons (Send t) nxt), (Cons t nxt'), incoming) ->
IO ((), SessionState prog prog' (nxt, nxt', incoming))
f (SessionState prog prog' outgoingProg incomingProg current outNotify outMVar inNotify inMVar)
= do { hole <- newEmptyMVar
; outChan <- takeMVar outNotify
; putMVar outMVar (Cell t hole)
; case outChan of
Nothing -> return ()
(Just chan) -> writeChan chan ()
; putMVar outNotify outChan
; return ((), (SessionState prog prog' outgoingProg incomingProg (tyTail current) outNotify hole inNotify inMVar))
}
srecv :: forall t prog prog' nxt nxt' outgoing .
(SessionChain prog prog') ((Cons (Recv t) nxt), outgoing, (Cons t nxt')) (nxt, outgoing, nxt') t
srecv = SessionChain f
where
f :: SessionState prog prog' ((Cons (Recv t) nxt), outgoing, (Cons t nxt')) ->
IO (t, SessionState prog prog' (nxt, outgoing, nxt'))
f (SessionState prog prog' outgoingProg incomingProg current outNotify outMVar inNotify inMVar)
= do { (Cell t nxt') <- takeMVar inMVar
; return (t, (SessionState prog prog' outgoingProg incomingProg (tyTail current) outNotify outMVar inNotify nxt'))
}
soffer :: forall current outgoing incoming finalResult prog prog' jumps .
OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult
-> (SessionChain prog prog') (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResult
soffer implementations = SessionChain f
where
f :: SessionState prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) ->
IO (finalResult, SessionState prog prog' (current, outgoing, incoming))
f (SessionState prog prog' outgoingProg incomingProg _ outNotify _ inNotify inMVar)
= do { (SelectCell n) <- takeMVar inMVar
; runSessionChain (walkOfferImpls n implementations)
(SessionState prog prog' outgoingProg incomingProg undefined outNotify undefined inNotify undefined)
}
sselect :: forall prog prog' progOut progIn label jumps outgoing incoming current currentUX len jumpTarget .
( ProgramToMVarsOutgoingT prog prog ~ progOut
, ProgramToMVarsOutgoingT prog' prog' ~ progIn
, ProgramToMVarsOutgoing prog prog progOut
, ProgramToMVarsOutgoing prog' prog' progIn
, TyListLength jumps len
, SmallerThanBool label len True
, 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
) =>
label -> (SessionChain prog prog') (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()
sselect label = SessionChain f
where
f :: SessionState prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) ->
IO ((), SessionState prog prog' (current, outgoing, incoming))
f (SessionState prog prog' outgoingProg incomingProg _ outNotify outMVar inNotify _)
= do { outChan <- takeMVar outNotify
; putMVar outMVar (SelectCell (tyNumToInt label))
; case outChan of
Nothing -> return ()
(Just chan) -> writeChan chan ()
; putMVar outNotify outChan
; (ProgramCell outgoing outProgCellMVar') <- carefullySwapToNextCell outProgCellMVar
; (ProgramCell incoming inProgCellMVar') <- carefullySwapToNextCell inProgCellMVar
; let outgoingProg' = tyListUpdate outgoingProg (undefined :: jumpTarget) outProgCellMVar'
; let incomingProg' = tyListUpdate incomingProg (undefined :: jumpTarget) inProgCellMVar'
; return ((), (SessionState prog prog' outgoingProg' incomingProg' current outNotify outgoing inNotify incoming))
}
where
current = expandPids prog $ tyListIndex prog (undefined :: jumpTarget)
outProgCellMVar = tyListIndex outgoingProg (undefined :: jumpTarget)
inProgCellMVar = tyListIndex incomingProg (undefined :: jumpTarget)
run :: forall prog prog' progOut progIn init fromO fromI toO toI res res' currentUX currentUX' current current' toCur toCur' .
( 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)))
, DualT prog ~ prog'
, Dual prog prog'
, TyListIndex prog init currentUX
, ExpandPids prog currentUX current
, TyListIndex prog' init currentUX'
, ExpandPids prog' currentUX' current'
) => prog -> init ->
SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res ->
SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' ->
IO (res, res')
run prog _ chain1 chain2
= do { mvarsOut <- programToMVarsOutgoing prog prog
; mvarsIn <- programToMVarsOutgoing prog' prog'
; aDone <- newEmptyMVar
; bDone <- newEmptyMVar
; aNotify <- newMVar Nothing
; bNotify <- newMVar Nothing
; forkIO $ runSessionChain chain1' (SessionState prog prog' mvarsOut mvarsIn undefined aNotify undefined bNotify undefined)
>>= putMVar aDone . fst
; forkIO $ runSessionChain chain2' (SessionState prog' prog mvarsIn mvarsOut undefined bNotify undefined aNotify undefined)
>>= putMVar bDone . fst
; aRes <- takeMVar aDone
; bRes <- takeMVar bDone
; return (aRes, bRes)
}
where
chain1' :: SessionChain prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (toCur, toO, toI) res
chain1' = sjump ~>> chain1
chain2' :: SessionChain prog' prog ((Cons (Jump init) Nil), (Cons (Jump init) Nil), (Cons (Jump init) Nil)) (toCur', toI, toO) res'
chain2' = sjump ~>> chain2
prog' = dual prog