-- {-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE TypeOperators, EmptyDataDecls #-}

module Control.Concurrent.FullSession.Types where

-- |capability -- from the implementation of Pucella and Tov
-- ex. 
-- @
--      Cap Nil (Rec (Send Int (Var Z))) 
--   == Cap (Send Int (Var Z):|:Nil) (Send Int (Var Z)) -- (by `enter' operation)
--
--      Cap (Send Int (Var Z):|:Nil) (Var Z)
--   == Cap (Send Int (Var Z):|:Nil) (Send Int (Var Z)) -- (by `zero' operation)
-- @
data Cap e t

-- session types
-- |no operation
data End
-- |send a value of type v then u
data Send v u -- output
-- |receive a value of type v then u
data Recv v u -- input
-- |send a channel of session type u' then u
data Throw u' u -- throw
-- |receive a channel of session type u' then u
data Catch u' u
-- |recursion binding
data Rec u
-- |recursion variable
data Var n
-- |this channel is (or, will be) owned by maximum two processes
data Bot
-- |send a label i then ui (i in {1,2}) 
data Select u1 u2
-- |receive a label i then ui (i in {1,2})
data Offer u u'