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

module FullSession.SMonad where

import FullSession.Base
import FullSession.Types
import FullSession.Ended

newtype Session t ss tt a = Session { session :: ss -> IO (tt,a) }

(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
(Session m) >>>= f = Session (\ss -> m ss >>= \(tt,x) -> session (f x) tt)

(>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu b
(Session m) >>> (Session n) = Session (\ss -> m ss >>= \(tt,_) -> n tt)


ireturn :: a -> Session t ss ss a
ireturn a = Session (\ss -> return (ss, a))

runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO a
runS s = case s of Session m -> m Nil >>= \(_,a) -> return a

typecheck1
  :: (Length ss l) =>
     (Channel t l -> Session t (ss:>s) ss' a)
     -> Session t (ss:>s) ss' a
typecheck1 = error "ERROR - for type checking purpose only!"

typecheck2
  :: (Length ss l) =>
     (Channel t (S l) -> Channel t l -> Session t (ss:>s1:>s2) ss' a)
     -> Session t (ss:>s1:>s2) ss' a
typecheck2 = error "ERROR - for type checking purpose only!"

inspect1 :: Length tt l => (Channel t l -> Session t ss ss () -> Session t (tt:>t1) tt' a) -> (ss, Session t (tt:>t1) tt' a)
inspect1 = undefined