{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
-- {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
-- {-# LANGUAGE UndecidableInstances #-}
-- {-# LANGUAGE EmptyDataDecls #-}
-- {-# LANGUAGE KindSignatures #-}
-- {-# LANGUAGE TypeOperators #-}

module Control.Concurrent.FullSession.Misc where

-- |TypeCast, from the HList library
class TCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TCast'  () a b => TCast a b where typeCast x = typeCast' () x
instance TCast'' t a b => TCast' t a b where typeCast' = typeCast''
instance TCast'' () a a where typeCast'' _ x  = x

-- |type-level peano number n+1
data S n
-- |type-level peano number 0
data Z

-- |subtraction
class Sub n n' n'' | n n' -> n''
instance Sub n n Z
instance Sub (S n) n (S Z)
instance Sub (S (S n)) n (S (S Z))
instance Sub (S (S (S n))) n (S (S (S Z)))
instance Sub (S (S (S (S n)))) n (S (S (S (S Z))))
instance Sub (S (S (S (S (S n))))) n (S (S (S (S (S Z)))))
instance Sub (S (S (S (S (S (S n)))))) n (S (S (S (S (S (S Z))))))
instance Sub (S (S (S (S (S (S (S n))))))) n (S (S (S (S (S (S (S Z)))))))
instance Sub (S (S (S (S (S (S (S (S n)))))))) n (S (S (S (S (S (S (S (S Z))))))))
instance Sub (S (S (S (S (S (S (S (S (S n))))))))) n (S (S (S (S (S (S (S (S (S Z)))))))))
instance Sub (S (S (S (S (S (S (S (S (S (S n)))))))))) n (S (S (S (S (S (S (S (S (S (S Z))))))))))
instance Sub (S (S (S (S (S (S (S (S (S (S (S n))))))))))) n (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))
instance Sub (S (S (S (S (S (S (S (S (S (S (S (S n)))))))))))) n (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))

-- |type-level boolean True
data T
-- |type-level boolean False
data F

-- |type-level list cons
data (:|:) hd tl
infixr 3 :|:
-- |type-level list nil
data Nil

-- |list length
class Length ls n | ls -> n
instance Length Nil Z
instance Length ts n => Length (t:|:ts) (S n)

-- |A type-level list update operation
-- @
-- update(n,s,t,ss) = tt
-- update(n+1, s, t, x:ss) = x:update(n, s, t, ss)
-- update(0,   s, t, x:ss) 
--     | x==s      = t:ss
--     | otherwise = undefined
-- ex. update(1, Cap Nil (Send Int End), Cap Nil End, c1:(Cap Nil Send Int End):c3:ss) = c1:(Cap Nil End):c3:ss
-- @
class Update n s t ss tt | n s t ss -> tt
instance (TCast a (s:|:ss), TCast b (t:|:ss)) => Update Z s t a b
instance (TCast a (x:|:ss), TCast b (x:|:tt), Update n s t ss tt) => Update (S n) s t a b