1 files changed, 29 insertions, 6 deletions

diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
index c7fd058..af99f55 100644
--- a/events/src/Events/Spec/Types.hs
+++ b/events/src/Events/Spec/Types.hs
@@ -1,10 +1,12 @@
 {-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-}
+{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
 
 module Events.Spec.Types
   ( Expr(..)
   , Val(..)
+  , Bindable(..)
   , Spec
-  , Cmnd(..)
   , Elem(..)
   , Length(..)
   , type (++)(..)
@@ -26,12 +28,33 @@ 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
+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 Cmnd = COverride Object
-          | COccurs Bool
-          | CNop
-          deriving (Show)
 
 data Elem :: a -> [a] -> * where
   EZ :: Elem x (x ': xs)