module FullSession.Types where
import FullSession.Base
data Bot = Bot
data Send v u = Send (v -> IO ()) u
data Recv v u = Recv (IO v) u
data Throw u' u = Throw (u' -> IO ()) u
data Catch u' u = Catch (IO u') u
data Select u1 u2 = Select (Bool -> IO ()) u1 u2
data Offer u1 u2 = Offer (IO Bool) u1 u2
data End = End
data Rec m r = Rec m r deriving Show
data Var n = Var n deriving Show
data Close = Close (IO ())
data SelectN u1 u2 = SelectN u1 u2
data OfferN u1 u2 = OfferN (IO (Maybe Bool)) u1 u2
newtype Channel t n = C n
class Diff xx yy zz | xx yy -> zz where
diff :: Either xx yy -> zz
instance (Length xx lx, Length yy ly, Diff' (SubT lx ly) xx yy zz, Sub lx ly) => Diff xx yy zz where
diff e = (\sub_ diff' ->
case e of
Left xx -> fst (diff' (sub_ (Left (len_ xx)))) xx
Right yy -> snd (diff' (sub_ (Right (len_ yy)))) yy
) sub_ diff'
class Diff' n xx yy zz | n xx yy -> zz where
diff' :: n -> (xx -> zz, yy -> zz)
instance (xx ~ zz, yy ~ zz) => Diff' Z xx yy zz where
diff' _ = (id, id)
instance (Diff' n xx' yy zz', xx ~ (xx' :> End), zz ~ (zz' :> End)) => Diff' (S n) xx yy zz where
diff' (S n) = (\f -> (\(xx' :> End) -> fst f xx' :> End, \yy -> snd f yy :> End)) (diff' n)
instance (Diff' n xx yy' zz', yy ~ (yy' :> End), zz ~ (zz' :> End)) => Diff' (P n) xx yy zz where
diff' (P n) = (\f -> (\xx -> fst f xx :> End, \(yy' :> End) -> snd f yy' :> End)) (diff' n)