diff options
Diffstat (limited to 'events/src/Events/Spec/Types.hs')
-rw-r--r-- | events/src/Events/Spec/Types.hs | 35 |
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 @@ | |||
1 | {-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-} | 1 | {-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-} |
2 | {-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-} | ||
3 | {-# LANGUAGE InstanceSigs #-} | ||
2 | 4 | ||
3 | module Events.Spec.Types | 5 | module Events.Spec.Types |
4 | ( Expr(..) | 6 | ( Expr(..) |
5 | , Val(..) | 7 | , Val(..) |
8 | , Bindable(..) | ||
6 | , Spec | 9 | , Spec |
7 | , Cmnd(..) | ||
8 | , Elem(..) | 10 | , Elem(..) |
9 | , Length(..) | 11 | , Length(..) |
10 | , type (++)(..) | 12 | , type (++)(..) |
@@ -26,12 +28,33 @@ type family Val m a where | |||
26 | Val m (a -> b) = Expr m '[a] b | 28 | Val m (a -> b) = Expr m '[a] b |
27 | Val m a = m a | 29 | Val m a = m a |
28 | 30 | ||
29 | type Spec m = Expr (Eval m) '[] Cmnd | 31 | type family Ctx m f where |
32 | Ctx m (m a -> b) = (a ': Ctx m b) | ||
33 | Ctx m a = '[] | ||
34 | |||
35 | type family Fin m f where | ||
36 | Fin m (m a -> b) = Fin m b | ||
37 | Fin m (m a) = a | ||
38 | Fin m a = a | ||
39 | |||
40 | class Bindable m a where | ||
41 | liftE :: a -> Expr m (Ctx m a) (Fin m a) | ||
42 | |||
43 | instance (Val m a ~ m a, Bindable m b) => Bindable m (m a -> b) where | ||
44 | liftE :: (m a -> b) -> Expr m (a ': Ctx m b) (Fin m b) | ||
45 | 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)) . ) | ||
46 | |||
47 | 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 | ||
48 | liftE :: (m a -> m b) -> Expr m '[a] b | ||
49 | liftE = EPri . (EVal .) | ||
50 | |||
51 | instance (Val m a ~ m a, Fin m (m a) ~ a, Ctx m (m a) ~ '[]) => Bindable m (m a) where | ||
52 | liftE :: m a -> Expr m '[] a | ||
53 | liftE = EVal | ||
54 | |||
55 | |||
56 | type Spec m = Expr (Eval m) '[] () | ||
30 | 57 | ||
31 | data Cmnd = COverride Object | ||
32 | | COccurs Bool | ||
33 | | CNop | ||
34 | deriving (Show) | ||
35 | 58 | ||
36 | data Elem :: a -> [a] -> * where | 59 | data Elem :: a -> [a] -> * where |
37 | EZ :: Elem x (x ': xs) | 60 | EZ :: Elem x (x ': xs) |