{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-}
{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}

module Events.Spec.Types
  ( Expr(..)
  , Val
  , Bindable(..)
  , Spec
  , Elem(..)
  , Length(..)
  , type (++)
  , module Events.Types
  ) where

import Events.Types

-- | A functional language reminiscent of typed lambda calculus with monadic
-- side-effects and foreign primitives
data Expr :: (* -> *) -> [*] -> * -> * where
  EVal :: Val m a ~ m a => Val m a -> Expr m ctx a
  EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
  EVar :: Elem a ctx -> Expr m ctx a
  ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)
  EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a

type family Val m a where
  Val m (a -> b) = Expr m '[a] b
  Val m a        = m a

type family Ctx m f where
  Ctx m (m a -> b) = (a ': Ctx m b)
  Ctx m a = '[]

type family Fin m f where
  Fin m (m a -> b) = Fin m b
  Fin m (m a) = a
  Fin m a = a

class Bindable m a where
  liftE :: a -> Expr m (Ctx m a) (Fin m a)

instance (Val m a ~ m a, Bindable m b) => Bindable m (m a -> b) where
  liftE :: (m a -> b) -> Expr m (a ': Ctx m b) (Fin m b)
  liftE = (EPri :: (Val m a -> Expr m (Ctx m b) (Fin m b)) -> Expr m (a ': Ctx m b) (Fin m b)) . ((liftE :: b -> Expr m (Ctx m b) (Fin m b)) . )

instance {-# OVERLAPPABLE #-} (Val m a ~ m a, Val m b ~ m b, Ctx m (m b) ~ '[], Fin m (m b) ~ b) => Bindable m (m a -> m b) where
  liftE :: (m a -> m b) -> Expr m '[a] b
  liftE = EPri . (EVal .)

instance (Val m a ~ m a, Fin m (m a) ~ a, Ctx m (m a) ~ '[]) => Bindable m (m a) where
  liftE :: m a -> Expr m '[] a
  liftE = EVal


type Spec m = Expr (Eval m) '[] ()


data Elem :: a -> [a] -> * where
  EZ :: Elem x (x ': xs)
  ES :: Elem x xs -> Elem x (y ': xs)

data Length :: [a] -> * where
  LZ :: Length '[]
  LS :: Length xs -> Length (x ': xs)

type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
  '[]       ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)
infixr 5 ++