module Control.Concurrent.Session.Pid
( Pid (..)
, InternalPid (..)
, makePid
, rootPid
, iPidToPid
, myPid
, InterleavedChain (..)
, BuildPidTyMap (..)
, CreateSession (..)
, PidEq (..)
) where
import Control.Concurrent.Session.Bool
import Control.Concurrent.Session.Number
import Control.Concurrent.Session.Map
import Control.Concurrent.Session.List
import Control.Concurrent.Session.SessionType
import Control.Concurrent.Session.SMonad
import Control.Concurrent.Session.Runtime
import Control.Concurrent
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
type RawPid = [Int]
data Pid :: * -> * -> * -> * where
Pid :: RawPid -> prog -> TyMap sessionsToIdx idxsToPairStructs ->
Pid prog sessionsToIdx idxsToPairStructs
data InternalPid :: * -> * -> * -> * where
IPid :: Pid prog sessionsToIdx idxsToPairStructs -> [RawPid] ->
InternalPid prog sessionsToIdx idxsToPairStructs
pidToRawPid :: Pid prog sessionsToIdx idxsToPairStructs -> RawPid
pidToRawPid (Pid p _ _) = p
iPidToPid :: InternalPid prog sessionsToIdx idxsToPairStructs ->
Pid prog sessionsToIdx idxsToPairStructs
iPidToPid (IPid p _) = p
instance Show (Pid prog sessionsToIdx idxsToPairStructs) where
show = (:) '<' . (:) '.' . foldr (\c a -> shows c ('.':a)) ">" . reverse . pidToRawPid
instance Eq (Pid prog sessionsToIdx idxsToPairStructs) where
(==) a b = (==) (pidToRawPid a) (pidToRawPid b)
instance Ord (Pid prog sessionsToIdx idxsToPairStructs) where
compare a b = compare (pidToRawPid a) (pidToRawPid b)
instance Eq (InternalPid prog sessionsToIdx idxsToPairStructs) where
(==) a b = (==) (iPidToPid a) (iPidToPid b)
instance Ord (InternalPid prog sessionsToIdx idxsToPairStructs) where
compare a b = compare (iPidToPid a) (iPidToPid b)
class PidEq a b where
(=~=) :: a -> b -> Bool
instance PidEq (Pid progA sessionsToIdxA idxsToPairStructsA) (Pid progB sessionsToIdxB idxsToPairStructsB) where
(=~=) a b = (==) (pidToRawPid a) (pidToRawPid b)
makePid :: InternalPid prog sessionsToIdxO idxsToPairStructsO ->
TyMap sessionsToIdxN idxsToPairStructsN ->
(InternalPid prog sessionsToIdxO idxsToPairStructsO,
InternalPid prog sessionsToIdxN idxsToPairStructsN)
makePid (IPid orig@(Pid _ prog _) (p:ps)) childTM = ((IPid orig ps), child)
where
child = IPid (Pid p prog childTM) [x:p | x <- [0..]]
makePid (IPid _ []) _ = error "Out of pids. Interesting."
rootPid :: TyMap sessionsToIdx idxsToPairStructs -> prog ->
InternalPid prog sessionsToIdx idxsToPairStructs
rootPid tm prog = IPid (Pid [0] prog tm) [[x,0] | x <- [0..]]
newtype InterleavedChain internalPid from to res
= InterleavedChain { runInterleavedChain :: internalPid ->
from ->
IO (res, to, internalPid)
}
myPid :: InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) from from (Pid prog sessionsToIdx idxsToPairStructs)
myPid = InterleavedChain $ \p x -> return (iPidToPid p, x, p)
instance SMonad (InterleavedChain internalPid) where
f ~>> g = InterleavedChain $
\p x -> do { (_, y, p') <- runInterleavedChain f p x
; runInterleavedChain g p' y
}
f ~>>= g = InterleavedChain $
\p x -> do { (a, y, p') <- runInterleavedChain f p x
; runInterleavedChain (g a) p' y
}
sreturn a = InterleavedChain $
\p x -> return (a, x, p)
instance SMonadIO (InterleavedChain internalPid) where
sliftIO f = InterleavedChain $
\p x -> do { a <- f
; return (a, x, p)
}
class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where
type BuildPidTyMapT prog stlst
buildPidTyMap :: prog -> stlst -> IO tymap
instance (BuildPidTyMap' prog stlst (TyMap Nil Nil) tymap) =>
BuildPidTyMap prog stlst tymap where
type BuildPidTyMapT prog stlst = BuildPidTyMapT' prog stlst (TyMap Nil Nil)
buildPidTyMap prog stlst = buildPidTyMap' prog stlst emptyMap
class BuildPidTyMap' prog stlist tymap1 tymap2 | prog stlist tymap1 -> tymap2 where
type BuildPidTyMapT' prog stlist tymap1
buildPidTyMap' :: prog -> stlist -> tymap1 -> IO tymap2
instance BuildPidTyMap' prog Nil acc acc where
type BuildPidTyMapT' prog Nil acc = acc
buildPidTyMap' _ _ m = return m
instance ( BuildPidTyMap' prog nxt
(TyMap keyToIdx' idxToValue') (TyMap keyToIdx'' idxToValue'')
, MapInsert (TyMap keyToIdx idxToValue) init
(MVar (Map (RawPid, RawPid)
(MVar (PairStruct init prog prog' (fromO, fromI)))))
(TyMap keyToIdx' idxToValue')
, TyList nxt
) =>
BuildPidTyMap' prog (Cons (init, False) nxt) (TyMap keyToIdx idxToValue)
(TyMap keyToIdx'' idxToValue'') where
type BuildPidTyMapT' prog (Cons (init, False) nxt) (TyMap keyToIdx idxToValue)
= BuildPidTyMapT' prog nxt (TyMap (Cons init keyToIdx)
(Cons ((MVar (Map (RawPid, RawPid)
(MVar (PairStruct init prog (DualT prog)
((Cons (Jump init) Nil), (Cons (Jump init) Nil)))))))
idxToValue))
buildPidTyMap' prog lst m
= do { mvar <- newMVar Map.empty
; buildPidTyMap' prog nxt (m' mvar)
}
where
(init, FF) = tyHead lst
nxt = tyTail lst
m' :: (MVar (Map (RawPid, RawPid)
(MVar (PairStruct init prog prog' (fromO, fromI))))) ->
TyMap keyToIdx' idxToValue'
m' mvar = mapInsert init mvar m
instance ( BuildPidTyMap' prog nxt (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue')
, TyList nxt
) =>
BuildPidTyMap' prog (Cons (init, True) nxt) (TyMap keyToIdx idxToValue)
(TyMap keyToIdx' idxToValue') where
type BuildPidTyMapT' prog (Cons (init, True) nxt) (TyMap keyToIdx idxToValue) = BuildPidTyMapT' prog nxt (TyMap keyToIdx idxToValue)
buildPidTyMap' prog lst m = buildPidTyMap' prog (tyTail lst) m
type instance Outgoing prog (Cons (RecvPid t) nxt) = Outgoing prog nxt
type instance Outgoing prog (Cons (SendPid t) nxt) = Cons (Pid prog (LHS (BuildPidTyMapT prog t)) (RHS (BuildPidTyMapT prog t))) (Outgoing prog nxt)
type family LHS thing
type instance LHS (TyMap sessionsToIdx idxsToPairStructs) = sessionsToIdx
type family RHS thing
type instance RHS (TyMap sessionsToIdx idxsToPairStructs) = idxsToPairStructs
data PairStruct :: * -> * -> * -> * -> * where
PS ::RawPid ->
(SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ()) ->
PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil))
instance Eq (PairStruct init prog prog' start) where
(==) (PS x _) (PS y _) = x == y
instance Ord (PairStruct init prog prog' start) where
compare (PS x _) (PS y _) = compare x y
class CreateSession invert init prog prog' fromO fromI progOut progIn
sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem
keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where
createSession :: init -> invert -> Pid prog sessionsToIdxThem idxsToPairStructsThem ->
InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe)
(TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem
instance forall init prog prog' fromO fromI progOut progIn
sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem
keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem .
( ProgramToMVarsOutgoingT prog prog ~ progOut
, ProgramToMVarsOutgoingT prog' prog' ~ progIn
, ProgramToMVarsOutgoing prog prog progOut
, ProgramToMVarsOutgoing 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)))
, MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init
(MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil))))))
, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem
, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem
(SessionState prog prog' (fromO, fromI)) (TyMap keyToIdxMe' idxToValueMe')
) =>
CreateSession False init prog prog' fromO fromI progOut progIn
sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem
keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where
createSession init FF (Pid remotePid _ _) =
InterleavedChain $
\ipid@(IPid (Pid localPid _ localSTMap) _) mp ->
do { let pidFuncMapMVar :: MVar (Map (RawPid, RawPid)
(MVar (PairStruct init prog prog'
((Cons (Jump init) Nil), (Cons (Jump init) Nil)))))
= mapLookup localSTMap init
; pidFuncMap <- takeMVar pidFuncMapMVar
; emptyMVar :: MVar (TyMap keyToIdxMe' idxToValueMe') <- newEmptyMVar
; psMVar :: MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)))
<- case Map.lookup (localPid, remotePid) pidFuncMap of
Nothing
-> do { empty <- newEmptyMVar
; putMVar pidFuncMapMVar (Map.insert (localPid, remotePid) empty pidFuncMap)
; return empty
}
(Just mv)
-> do { putMVar pidFuncMapMVar pidFuncMap
; return mv
}
; let idxOfThem :: idxOfThem = mapSize mp
ps :: PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil))
= PS localPid (f idxOfThem mp emptyMVar)
; putMVar psMVar ps
; mp' <- takeMVar emptyMVar
; return (idxOfThem, mp', ipid)
}
where
f :: idxOfThem -> (TyMap keyToIdxMe idxToValueMe) ->
MVar (TyMap keyToIdxMe' idxToValueMe') ->
SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) ->
IO ()
f idxOfThem mp mv localST
= do { ((), localST') <- runSessionChain sjump localST
; putMVar mv (mapInsert idxOfThem localST' mp)
}
instance forall init prog prog' fromO fromI progOut progIn
sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem
keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem .
( ProgramToMVarsOutgoingT prog prog ~ progOut
, ProgramToMVarsOutgoingT prog' prog' ~ progIn
, ProgramToMVarsOutgoing prog prog progOut
, ProgramToMVarsOutgoing 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)))
, MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init
(MVar (Map (RawPid, RawPid) (MVar (PairStruct init prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil))))))
, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem
, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem
(SessionState prog' prog (fromI, fromO)) (TyMap keyToIdxMe' idxToValueMe')
, Dual prog prog'
) =>
CreateSession True init prog prog' fromO fromI progOut progIn
sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem
keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem where
createSession init TT (Pid remotePid prog remoteSTMap) =
InterleavedChain $
\ipid@(IPid (Pid localPid _ _) _) mp ->
do { let pidFuncMapMVar :: MVar (Map (RawPid, RawPid)
(MVar (PairStruct init prog prog'
((Cons (Jump init) Nil), (Cons (Jump init) Nil)))))
= mapLookup remoteSTMap init
prog' = dual prog
; pidFuncMap <- takeMVar pidFuncMapMVar
; mvarsOut <- programToMVarsOutgoing prog prog
; mvarsIn <- programToMVarsOutgoing prog' prog'
; let (theirST :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)))
= SessionState prog prog' mvarsOut mvarsIn undefined undefined
(myST :: SessionState prog' prog ((Cons (Jump init) Nil), (Cons (Jump init) Nil)))
= SessionState prog' prog mvarsIn mvarsOut undefined undefined
idxOfThem :: idxOfThem = mapSize mp
; case Map.lookup (remotePid, localPid) pidFuncMap of
Nothing
-> do { newEmptyMVar <- newEmptyMVar
; putMVar pidFuncMapMVar (Map.insert (remotePid, localPid) newEmptyMVar pidFuncMap)
; ps <- takeMVar newEmptyMVar
; modifyMVar_ pidFuncMapMVar (return . Map.delete (remotePid, localPid))
; case ps of
(PS _ (f :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ()))
-> f theirST
}
(Just fullMVar)
-> do { ps <- takeMVar fullMVar
; putMVar pidFuncMapMVar (Map.delete (remotePid, localPid) pidFuncMap)
; case ps of
(PS _ (f :: SessionState prog prog' ((Cons (Jump init) Nil), (Cons (Jump init) Nil)) -> IO ()))
-> f theirST
}
; ((), myST') <- runSessionChain sjump myST
; return (idxOfThem, mapInsert idxOfThem myST' mp, ipid)
}