{-# LANGUAGE TypeOperators, KindSignatures, ScopedTypeVariables, EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}

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)