module Control.Concurrent.Session.SessionTypeMonad where
import Control.Concurrent.Session.Base.Bool
import Control.Concurrent.Session.Base.Number
import Control.Concurrent.Session.Base.List
import Control.Concurrent.Session.Base.SMonad
import Control.Concurrent.Session.Types
import Control.Concurrent.Session.SessionType hiding (jump, end, select, offer, (~|~), sendPid, recvPid, sendSession, recvSession, Dual(..))
data TypeState :: * -> * -> * -> * -> * where
TypeState :: nxtLabel -> declareable -> useable -> st ->
TypeState nxtLabel declareable useable st
newtype SessionType f t r = SessionType { buildSessionType :: f -> (r, t) }
instance SMonad SessionType where
a ~>> b = SessionType $ \f -> let (_, f') = buildSessionType a f
in buildSessionType b f'
a ~>>= b = SessionType $ \f -> let (r, f') = buildSessionType a f
in buildSessionType (b r) f'
sreturn r = SessionType $ \f -> (r, f)
newLabel :: ( Succ nxtLabel nxtLabel'
, TyListConsSet nxtLabel declareable declareable'
, TyListConsSet nxtLabel useable useable'
) =>
SessionType (TypeState nxtLabel declareable useable st)
(TypeState nxtLabel' declareable' useable' st) nxtLabel
newLabel = SessionType $ \(TypeState nxtLabel declareable useable st) ->
(nxtLabel, (TypeState (tySucc nxtLabel) (tyListConsSet nxtLabel declareable) (tyListConsSet nxtLabel useable) st))
declareLabel :: ( TyListMember declareable label True
, TyListElem declareable label idx
, TyListDelete declareable idx declareable'
, TyList st
) =>
label -> (SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st))
(TypeState nxtLabel' declareable'' useable' st') a) ->
SessionType (TypeState nxtLabel declareable useable st)
(TypeState nxtLabel' declareable'' useable' st') a
declareLabel label f
= SessionType $ \(TypeState nxtLabel declareable useable st) ->
let idx = tyListElem declareable label
declareable' = tyListDelete idx declareable
in buildSessionType f (TypeState nxtLabel declareable' useable (cons (label, nil) st))
(.=) :: ( TyListMember declareable label True
, TyListElem declareable label idx
, TyListDelete declareable idx declareable'
, TyList st
) =>
label -> (SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st))
(TypeState nxtLabel' declareable'' useable' st') a) ->
SessionType (TypeState nxtLabel declareable useable st)
(TypeState nxtLabel' declareable'' useable' st') a
(.=) = declareLabel
infixl 2 .=
send :: ( TyList f
, TyList fs
) =>
t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, (Cons (Send (SpecialNormal, t)) f)) fs)) ()
send t = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, cons (Send (undefined, t)) f)) id st)))
recv :: ( TyList f
, TyList fs
) =>
t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, (Cons (Recv (SpecialNormal, t)) f)) fs)) ()
recv t = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, cons (Recv (undefined, t)) f)) id st)))
sendPid :: ( TyList f
, TyList fs
, TyListSortNums lst lst'
) =>
lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, (Cons (SendPid False lst') f)) fs)) ()
sendPid lst = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, cons (SendPid FF (tyListSortNums lst)) f)) id st)))
recvPid :: ( TyList f
, TyList fs
, TyListSortNums lst lst'
) =>
lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, (Cons (RecvPid False lst') f)) fs)) ()
recvPid lst = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, cons (RecvPid FF (tyListSortNums lst)) f)) id st)))
sendSession :: ( TyList f
, TyList fs
, TyList fs'
, TyListReverse frag fragRev
, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil)
, TyListDrop (D1 E) fragRev fragTailRev
, TyListReverse fragTailRev fragTail
, TyListAppend fragTail fs fs'
) =>
SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil))
(TypeState nxtLabel' declareable' useable' frag) res ->
SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel' declareable' useable' (Cons (label, (Cons (SendSession False fragHead) f)) fs')) res
sendSession fragST = SessionType $ \(TypeState nxtLabel declareable useable st) ->
let (label, f) = tyHead st
stTail = tyTail st
(res, (TypeState nxtLabel' declareable' useable' frag))
= buildSessionType fragST (TypeState nxtLabel declareable useable (cons (label, nil) nil))
fragRev = tyListReverse frag
(_, fragHead) = tyHead $ tyListTake (D1 E) fragRev
fragTailRev = tyListDrop (D1 E) fragRev
fragTail = tyListReverse fragTailRev
fs' = cons (label, cons (SendSession FF fragHead) f) $ tyListAppend fragTail stTail
in (res, (TypeState nxtLabel' declareable' useable' fs'))
recvSession :: ( TyList f
, TyList fs
, TyList fs'
, TyListReverse frag fragRev
, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil)
, TyListDrop (D1 E) fragRev fragTailRev
, TyListReverse fragTailRev fragTail
, TyListAppend fragTail fs fs'
) =>
SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil))
(TypeState nxtLabel' declareable' useable' frag) res ->
SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel' declareable' useable' (Cons (label, (Cons (RecvSession False fragHead) f)) fs')) res
recvSession fragST = SessionType $ \(TypeState nxtLabel declareable useable st) ->
let (label, f) = tyHead st
stTail = tyTail st
(res, (TypeState nxtLabel' declareable' useable' frag))
= buildSessionType fragST (TypeState nxtLabel declareable useable (cons (label, nil) nil))
fragRev = tyListReverse frag
(_, fragHead) = tyHead $ tyListTake (D1 E) fragRev
fragTailRev = tyListDrop (D1 E) fragRev
fragTail = tyListReverse fragTailRev
fs' = cons (label, cons (RecvSession FF fragHead) f) $ tyListAppend fragTail stTail
in (res, (TypeState nxtLabel' declareable' useable' fs'))
end :: ( TyListReverse (Cons End f) f'
, TyList f
, TyList fs
) =>
SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
end = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, tyListReverse (cons End f))) id st)))
jump :: ( TyListReverse (Cons (Jump jt) f) f'
, TyList f
, TyList fs
, TyListMember useable jt True
) =>
jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs))
(TypeState nxtLabel declareable useable (Cons (label, f') fs)) ()
jump jt = SessionType $ \(TypeState nxtLabel declareable useable st) ->
((), (TypeState nxtLabel declareable useable (modifyCons (\(label, f) -> (label, tyListReverse (cons (Jump jt) f))) id st)))
data BranchesList :: * -> * -> * -> * -> * -> * where
BLNil :: BranchesList Nil Nil z z z
BLCons :: (SessionType (TypeState nxtLabel declareable useable st)
(TypeState nxtLabel' declareable' useable' st') ( (resLst -> Cons res resLst)
, (labs -> Cons (Cons (Jump nxtLabel) Nil) labs))) ->
(BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) ->
(BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st)
((TypeState nxtLabel' declareable' useable' st'), to) finalTo)
(~|~) :: ( Succ label nxtLabel
, TyListConsSet label declareable declareable'
, TyListElem declareable' label idx
, TyListDelete declareable' idx declareable''
, TyListConsSet label useable useable'
, TyList st
, TyListMember declareable' label True
, TyList labs
, TyList resLst
) =>
(SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st))
(TypeState nxtLabel' declareable''' useable'' st') res) ->
(BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo) ->
(BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) ((TypeState nxtLabel' declareable''' useable'' st'), to) finalTo)
(~|~) st lst = BLCons (newLabel ~>>= \l -> declareLabel l st ~>>= \r -> sreturn (cons r, (cons (cons (Jump l) nil)))) lst
infixr 5 ~|~
class BuildBranches bl st where
buildBranches :: bl -> st
instance BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st)
(TypeState nxtLabel declareLabel useable st)
(TypeState nxtLabel declareLabel useable st))
(SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (Nil, Nil)) where
buildBranches (BLNil) = sreturn (nil, nil)
buildBranches _ = error "Monstrously impossible"
instance (BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo)
(SessionType (TypeState nxtLabel' declareable' useable' st') finalTo (resLst, labs))
) =>
BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs)
(TypeState nxtLabel declareable useable st)
((TypeState nxtLabel' declareable' useable' st'), to)
finalTo)
(SessionType (TypeState nxtLabel declareable useable st) finalTo ((Cons res resLst), (Cons (Cons (Jump nxtLabel) Nil) labs))) where
buildBranches (BLCons stm lst) = stm ~>>= \(fR, fL) ->
buildBranches lst ~>>= \(res, labs) ->
sreturn (fR res, fL labs)
buildBranches _ = error "Equally monstrously impossible"
select :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo .
( TyListReverse (Cons (Select listOfJumps) f) f'
, TyList f
, TyList fs
, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo)
(SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))
) =>
(BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) ->
(SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
select bl = SessionType $ \(TypeState nxtLabel declareable useable st) ->
let ((listOfRes, listOfJumps), ts)
= buildSessionType (buildBranches bl) (TypeState nxtLabel declareable useable
((modifyCons (\(label, f) -> (label, tyListReverse (cons (Select listOfJumps) f)))
id st) :: Cons (label, f') fs))
in (listOfRes, ts)
offer :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo .
( TyListReverse (Cons (Offer listOfJumps) f) f'
, TyList f
, TyList fs
, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo)
(SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))
) =>
(BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) ->
(SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes)
offer bl = SessionType $ \(TypeState nxtLabel declareable useable st) ->
let ((listOfRes, listOfJumps), ts)
= buildSessionType (buildBranches bl) (TypeState nxtLabel declareable useable
((modifyCons (\(label, f) -> (label, tyListReverse (cons (Offer listOfJumps) f)))
id st) :: Cons (label, f') fs))
in (listOfRes, ts)
currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) label
currentLabel = SessionType $ \ts@(TypeState _ _ _ st) -> (fst . tyHead $ st, ts)
makeSessionType :: ( TyListSortNums st st'
, TyListSnd st' st''
) =>
SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res)
makeSessionType a = let (res, (TypeState _ _ _ st)) = (buildSessionType a) (TypeState (D0 E) nil nil nil)
in (tyListSnd . tyListSortNums $ st, res)
class TyListSnd lstA lstB | lstA -> lstB where
tyListSnd :: lstA -> lstB
instance TyListSnd Nil Nil where
tyListSnd _ = nil
instance ( TyListSnd nxt nxt'
, TyList nxt
, TyList nxt'
) =>
TyListSnd (Cons (a, b) nxt) (Cons b nxt') where
tyListSnd = modifyCons snd tyListSnd
dual :: True
dual = TT
notDual :: False
notDual = FF