{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-}

module Events.Spec.Types
  ( Expr(..)
  , Val(..)
  , Spec
  , Cmnd(..)
  , 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 -> 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 Spec m = Expr (Eval m) '[] Cmnd

data Cmnd = COverride Object
          | COccurs Bool
          | CNop
          deriving (Show)

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 ++