-- {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances -fallow-incoherent-instances #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE IncoherentInstances #-} -- for CompList

module Control.Concurrent.FullSession.Session where

import Prelude hiding (catch, succ)
import qualified Control.Concurrent (forkOS, forkIO, ThreadId)
import Control.Concurrent.FullSession.Misc
import Control.Concurrent.FullSession.UChan
import Control.Concurrent.FullSession.Types
-- import Control.Monad.Indexed -- from category-extras

-- |Session monad.
-- t is an `index' (like in the ST monad),
-- ss is the precondition of the computation,
-- tt is the postcondition of the computation,
-- and a is the return value
newtype Session t ss tt a = Session (IO a)

-- |return the value computed by a session. The forall ensures that internal channels 
-- used by the session is inaccessible to the rest of the program
runS :: (IsEnded ss T, Ended l ss, Length ss l) => (forall t. Session t Nil ss a) -> IO a
runS m = case m of Session io -> io

{-
instance IxFunctor (Session t) where
  imap f (Session m) = Session (fmap f m)
instance IxPointed (Session t) where
  ireturn = Session . return
instance IxApplicative (Session t) where
  iap (Session f) (Session a) = Session (f >>= \f' -> a >>= \a' -> return (f' a'))
instance IxMonad (Session t) where
  f `ibind` (Session m) = Session (m >>= \a -> case f a of Session n -> n)
-}

-- |bind for indexed monad
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
Session m >>>= f = Session $ m >>= \x -> case f x of Session n -> n
infixr 1 >>>=

-- |bind, discarding the result of the computation on LHS
m >>> n = m >>>= \_ -> n
infixr 8 >>>


-- |return for indexed monad
ireturn :: a -> Session t ss ss a
ireturn a = Session $ return a


-- |run a computation of type IO a
io :: IO a -> Session t ss ss a
io m = Session m

-- |create a channel
new :: Length ss l => Session t ss (Cap Nil Bot:|:ss) (Channel t l)
new = Session newUChan

-- |output on a channel
send :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Send v s)) (Cap e s) ss tt) => Channel t n -> v -> Session t ss tt ()
send c v = Session $ outUChan c v

-- |input on a channel
recv :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Recv v s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt v
recv c = Session $ inUChan c

-- |output a label `1'
sel1 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select s x)) (Cap e s) ss tt) => Channel t n -> Session t ss tt () 
sel1 c = Session $ outUChan c True

-- |output a label `2'
sel2 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select x s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt () 
sel2 c = Session $ outUChan c False

-- |output a label
select :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Select x y)) (Cap e x) uu ss, Update n' (Cap e (Select x y)) (Cap e y) uu tt) => 
         Channel t n -> Bool -> Session t ss xx () -> Session t tt xx () -> Session t uu xx ()
select c b (Session m) (Session n) = Session $ outUChan c b >> if b then m else n

-- |input a label i
offer :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Offer x y)) (Cap e x) uu ss, Update n' (Cap e (Offer x y)) (Cap e y) uu tt) => 
         Channel t n -> Session t ss xx a -> Session t tt xx a -> Session t uu xx a
offer c (Session m) (Session n) = Session $ inUChan c >>= \b -> if b then m else n

-- |output a channel
sendS :: (Length ss l, Length tt l, Sub l (S n) n', Sub l (S m) m', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt', Update m' (Cap e' u') (Cap e' End) tt' tt) => 
         Channel t n -> Channel t m -> Session t ss tt ()
sendS c c' = Session $ outUChan c c'

-- |input a channel
recvS :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Catch u' u)) (Cap e u) ss tt) => 
         Channel t n -> Session t ss (Cap Nil u':|:tt) (Channel t l)
recvS c = Session $ inUChan c

-- |create a channel, then pass it to other process
sendS_new :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt, Comp2 u' u'') => 
         Channel t n -> Session t ss (Cap Nil u'':|:tt) (Channel t l)
sendS_new c = Session $ newUChan >>= \c' -> outUChan c c' >> return c'

-- |start a new thread
forkIO :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' Control.Concurrent.ThreadId
forkIO (Session m) = Session (Control.Concurrent.forkIO m)

-- |start a new OS thread
forkOS :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' Control.Concurrent.ThreadId
forkOS (Session m) = Session (Control.Concurrent.forkOS m)

forkOS_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()
forkOS_ m = forkOS m >>> ireturn ()

forkIO_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()
forkIO_ m = forkIO m >>> ireturn ()


-- |expand a (Rec u) to u (from Pucella and Tov)
enter :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Rec r)) (Cap (r:|:e) r) ss tt) => Channel t n -> Session t ss tt ()
enter c = Session (return ())

-- |replace (Var Z) with recursion body (from Pucella and Tov)
zero :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r:|:e) (Var Z)) (Cap (r:|:e) r) ss tt) => Channel t n -> Session t ss tt ()
zero c = Session (return ())

-- |(from Pucella and Tov)
suc :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r:|:e) (Var (S v))) (Cap e (Var v)) ss tt) => Channel t n -> Session t ss tt ()
suc c = Session (return ())

-- |recursion
recur :: (Sub l2 l d, AppendEnd d ss ss', Sub l2 (S n) n', EndedWithout n' l2 x ss', Length ss l, Length ss' l2, IsEnded tt' T, Length tt' l2, Ended l2 tt') => 
         (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt' ()
recur f c = case f c of Session m -> Session m
--recur :: (Length ss' l2, Sub l2 l d, AppendEnd d ss ss', Sub l (S n) n', EndedWithout n' l ss, Length ss l, IsEnded tt' T, Length tt' l, Ended l tt') => 
--         (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt' ()

-- integrated with recur
--extend :: (Length ss l, Length ss' l2, Sub l2 l d, AppendEnd d ss ss') => Session t ss tt a -> Session t ss' tt a
--extend :: Session t ss tt a -> Session t ss tt a
--extend (Session m) = Session m



-- |T if the all elements of ss are Cap Nil End
class IsEnded ss b | ss -> b
instance (IsEnded ss b) => IsEnded (Cap Nil End:|:ss) b
instance IsEnded Nil T
instance IsEnded (Cap e (Send x y):|:ss) F
instance IsEnded (Cap e (Recv x y):|:ss) F
instance IsEnded (Cap e (Throw x y):|:ss) F
instance IsEnded (Cap e (Catch x y):|:ss) F
instance IsEnded (Cap e (Select x y):|:ss) F
instance IsEnded (Cap e (Offer x y):|:ss) F
instance IsEnded (Cap e Bot:|:ss) F
instance IsEnded (Cap e (Rec r):|:ss) F
instance IsEnded (Cap e (Var v):|:ss) F

-- |generates a list of `ended` types
class Ended l ss | l -> ss
instance (TCast s (Cap Nil End), Ended n ss) => Ended (S n) (s:|:ss)
instance Ended Z Nil


-- |sesion type algebra
class Comp s t u | s u -> t, t u -> s, s t -> u
instance (Comp2 u u', TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Send t u)) (Cap e' (Recv t' u')) (Cap e'' Bot)
instance (Comp2 u u' , TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Recv t' u')) (Cap e' (Send t u)) (Cap e'' Bot)
instance (Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Throw v u)) (Cap e' (Catch v' u')) (Cap e'' Bot)
instance (Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Catch v u)) (Cap e' (Throw v' u')) (Cap e'' Bot)
instance (Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Select u v)) (Cap e' (Offer u' v')) (Cap e'' Bot)
instance (Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Offer u v)) (Cap e' (Select u' v')) (Cap e'' Bot)
instance (Comp2 r r', TCast e e', TCast e' Nil) => Comp (Cap e (Rec r)) (Cap e' (Rec r')) (Cap e'' Bot)
instance (TCast v v', TCast e e', TCast e' Nil) => Comp (Cap e (Var v)) (Cap e' (Var v')) (Cap e'' Bot)
instance Comp c (Cap Nil End) c
instance Comp (Cap Nil End) c c
instance Comp (Cap Nil End) (Cap Nil End) (Cap Nil End)

-- |session type algebra (2)
class Comp2 s t | s -> t, t -> s
instance Comp2 End End
instance (Comp2 u u', TCast t t') => Comp2 (Send t u) (Recv t' u')
instance (Comp2 u u' , TCast t t') => Comp2 (Recv t' u') (Send t u)
instance (Comp2 u u', TCast v v') => Comp2 (Throw v u) (Catch v' u')
instance (Comp2 u u', TCast v v') => Comp2 (Catch v u) (Throw v' u')
instance (Comp2 u u', Comp2 v v') => Comp2 (Select u v) (Offer u' v')
instance (Comp2 u u', Comp2 v v') => Comp2 (Offer u v) (Select u' v')
instance Comp2 r r' => Comp2 (Rec r) (Rec r')
instance TCast v v' => Comp2 (Var v) (Var v')


-- |parallel composition
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ss
instance Par Nil Nil Nil
instance (Comp s t' t, IsEnded ss b, Par2 b ss tt' tt) => Par (s:|:ss) (t':|:tt') (t:|:tt) 


-- |the specialized case for `ended' ss
class Par2 t ss tt' tt | t ss tt' -> tt, t ss tt-> tt', t tt tt' -> ss
instance (TCast tt' tt) => Par2 T ss tt' tt
instance Par ss tt' tt => Par2 F ss tt' tt

-- |
class EndedWithout n l s ss | n l s -> ss
instance (TCast ss (s:|:ss'), TCast l (S l'), Ended l' ss') => EndedWithout Z l s ss
instance (TCast ss (Cap Nil End:|:ss'), TCast l (S l'), EndedWithout n l' s ss') => EndedWithout (S n) l s ss

class AppendEnd n ss ss' | n ss -> ss', n ss' -> ss
instance TCast ss ss' => AppendEnd Z ss ss'
instance (AppendEnd n ss ss'', TCast ss' (Cap Nil End:|:ss'')) => AppendEnd (S n) ss ss'



typecheck :: (Ended l ss, Length ss l, IsEnded ss T) => Session t Nil ss a -> Session t Nil ss a
typecheck = id

typecheck' :: Session t Nil ss a -> Session t Nil ss a
typecheck' = id

check p = new >>>= \k -> forkIO (p k) >>>= \_ -> ireturn ()