{- Interleaving.hs Copyright 2008 Matthew Sackman 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 . -} {-# 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)