module Control.Concurrent.Session.SessionType where
import Control.Concurrent.Session.List
import Control.Concurrent.Session.Number
data End = End deriving Show
end :: Cons End Nil
end = cons End nil
data Send :: * -> * where
Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double
data Recv :: * -> * where
Recv :: t -> Recv t
RecvInt :: Recv Int
RecvBool :: Recv Bool
RecvChar :: Recv Char
RecvStr :: Recv String
RecvDouble :: Recv Double
data Jump l = Jump l
deriving (Show)
jump :: (TyNum n) => n -> Cons (Jump n) Nil
jump l = cons (Jump l) nil
data Select :: * -> * where
Select :: lstOfLabels -> Select lstOfLabels
select :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil
select lol = cons (Select lol) nil
data Offer :: * -> * where
Offer :: lstOfLabels -> Offer lstOfLabels
offer :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil
offer lol = cons (Offer lol) nil
class Dual a b | a -> b, b -> a where
dual :: a -> b
instance Dual End End where
dual End = End
instance Dual (Jump l) (Jump l) where
dual (Jump l) = Jump l
instance Dual (Send t) (Recv t) where
dual (Send t) = Recv t
dual SendInt = RecvInt
dual SendBool = RecvBool
dual SendChar = RecvChar
dual SendStr = RecvStr
dual SendDouble = RecvDouble
instance Dual (Recv t) (Send t) where
dual (Recv t) = Send t
dual RecvInt = SendInt
dual RecvBool = SendBool
dual RecvChar = SendChar
dual RecvStr = SendStr
dual RecvDouble = SendDouble
instance Dual (Select lst) (Offer lst) where
dual (Select lst) = Offer lst
instance Dual (Offer lst) (Select lst) where
dual (Offer lst) = Select lst
instance Dual Nil Nil where
dual Nil = Nil
instance (Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt') where
dual (Cons val nxt) = Cons (dual val) (dual nxt)
class SListOfJumps lst
instance SListOfJumps Nil
instance (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
class SListOfSessionTypes lstOfLists
instance SListOfSessionTypes Nil
instance (SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)
class SNonTerminal a
instance SNonTerminal (Send t)
instance SNonTerminal (Recv t)
class STerminal a
instance STerminal End
instance (TyNum l) => STerminal (Jump l)
instance (SListOfJumps (Cons val nxt)) => STerminal (Select (Cons val nxt))
instance (SListOfJumps (Cons val nxt)) => STerminal (Offer (Cons val nxt))
class SValidSessionType lst
instance (STerminal a) => SValidSessionType (Cons a Nil)
instance (SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)
infixr 5 ~>
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)
(~>) = cons
infixr 5 ~|~
(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt
(~|~) = cons . jump
class SNoJumpsBeyond s idx
instance SNoJumpsBeyond End idx
instance (SmallerThan l idx) => SNoJumpsBeyond (Jump l) idx
instance SNoJumpsBeyond (Send t) idx
instance SNoJumpsBeyond (Recv t) idx
instance (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Select lol) idx
instance (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Offer lol) idx
instance SNoJumpsBeyond Nil idx
instance (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
class SWellFormedConfig idxA idxB ss
instance ( SListOfSessionTypes ss
, ListLength ss len
, SNoJumpsBeyond ss len
, SmallerThan idxA len
, Elem ss idxA st
, ListLength st len'
, SmallerThan idxB len'
) =>
SWellFormedConfig idxA idxB ss
testWellformed :: (SWellFormedConfig idxA idxB ss) => ss -> idxA -> idxB -> Bool
testWellformed _ _ _ = True
data Choice :: * -> * where
Choice :: lstOfLabels -> Choice lstOfLabels
class OnlyOutgoing a b | a -> b where
onlyOutgoing :: a -> b
instance (OnlyOutgoing nxt nxt') =>
OnlyOutgoing (Cons (Recv t) nxt) nxt' where
onlyOutgoing (Cons _ nxt) = onlyOutgoing nxt
instance OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil) where
onlyOutgoing (Cons (Offer jl) Nil) = Cons (Choice jl) Nil
instance OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil) where
onlyOutgoing (Cons (Select jl) Nil) = Cons (Choice jl) Nil
instance OnlyOutgoing (Cons End Nil) (Cons End Nil) where
onlyOutgoing (Cons End Nil) = (Cons End Nil)
instance OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil) where
onlyOutgoing (Cons (Jump l) Nil) = (Cons (Jump l) Nil)
instance (OnlyOutgoing nxt nxt') =>
OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt') where
onlyOutgoing (Cons (Send t) nxt) = Cons t $ onlyOutgoing nxt
onlyOutgoing (Cons SendInt nxt) = Cons (undefined::Int) $ onlyOutgoing nxt
onlyOutgoing (Cons SendBool nxt) = Cons (undefined::Bool) $ onlyOutgoing nxt
onlyOutgoing (Cons SendChar nxt) = Cons (undefined::Char) $ onlyOutgoing nxt
onlyOutgoing (Cons SendStr nxt) = Cons (undefined::String) $ onlyOutgoing nxt
onlyOutgoing (Cons SendDouble nxt) = Cons (undefined::Double) $ onlyOutgoing nxt