module FullSession.Ended where
import FullSession.Base
import FullSession.Types
class (SList ss n, IsEnded ss T) => Ended n ss | n -> ss where
ended :: n -> ss
instance Ended Z Nil where
ended _ = Nil
instance Ended n ss => Ended (S n) (ss :> End) where
ended ~(S n) = ended n :> End
class IsEnded ss b | ss -> b
instance IsEnded Nil T
instance (IsEnded ss b) => IsEnded (ss:>End) b
class IsEndedST s b | s -> b
instance IsEndedST End T
instance IsEndedST (Send x y) F
instance IsEndedST (Recv x y) F
instance IsEndedST (Throw x y) F
instance IsEndedST (Catch x y) F
instance IsEndedST (Select x y) F
instance IsEndedST (Offer x y) F
instance IsEndedST (SelectN x y) F
instance IsEndedST (OfferN x y) F
instance IsEndedST (Bot) F
instance IsEndedST (Close) F
instance IsEndedST (Rec n r) F
instance IsEndedST (Var v) F
class EndedWithout n s ss | n s -> ss
instance (SList ss l, EndedWithout' (SubT l (S n)) s l ss) => EndedWithout n s ss
class EndedWithout' n s l ss | n s l -> ss
instance (ss ~ (ss':>s), l ~ S l', Ended l' ss', IsEnded ss' T) => EndedWithout' Z s l ss
instance (ss ~ (ss':>End), l ~ S l', EndedWithout' n s l' ss') => EndedWithout' (S n) s l ss
class EndedWithout2 n m s t ss | n s m t -> ss
instance (SList ss l, EndedWithout2' (SubT l (S n)) (SubT l (S m)) s t l ss) => EndedWithout2 n m s t ss
class EndedWithout2' n m s t l ss | n m s t l -> ss
instance (ss ~ (ss':>s), l ~ S l', EndedWithout' m t l' ss') => EndedWithout2' Z (S m) s t l ss
instance (ss ~ (ss':>t), l ~ S l', EndedWithout' n s l' ss') => EndedWithout2' (S n) Z s t l ss
instance (ss ~ (ss':>End), l ~ S l', EndedWithout2' n m s t l' ss') => EndedWithout2' (S n) (S m) s t l ss
class AppendEnd ss ss' where
appendEnd :: ss -> ss'
deleteEnd :: ss' -> ss
instance (SList ss l, SList ss' l', Sub l' l, AppendEnd' (SubT l' l) ss ss') => AppendEnd ss ss' where
appendEnd ss = let d = sub (len_ ss') (len_ ss); ss' = appendEnd' d ss in ss'
deleteEnd ss' = let d = sub (len_ ss') (len_ ss); ss = deleteEnd' d ss' in ss
class AppendEnd' n ss ss' | n ss -> ss', n ss' -> ss where
appendEnd' :: n -> ss -> ss'
deleteEnd' :: n -> ss' -> ss
instance ss ~ ss' => AppendEnd' Z ss ss' where
appendEnd' _ ss = ss
deleteEnd' _ ss = ss
instance (AppendEnd' n ss ss'', ss' ~ (ss'':>End)) => AppendEnd' (S n) ss ss' where
appendEnd' (S n) ss = appendEnd' n ss :> End
deleteEnd' (S n) (ss:>_) = deleteEnd' n ss