diff options
Diffstat (limited to 'events/src/Events/Spec/Eval.hs')
-rw-r--r-- | events/src/Events/Spec/Eval.hs | 49 |
1 files changed, 40 insertions, 9 deletions
diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs index 3a23e0b..24cfeb6 100644 --- a/events/src/Events/Spec/Eval.hs +++ b/events/src/Events/Spec/Eval.hs | |||
@@ -1,7 +1,10 @@ | |||
1 | {-# LANGUAGE GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables #-} | 1 | {-# LANGUAGE GADTs, DataKinds, TypeFamilies, TypeOperators, RankNTypes, ScopedTypeVariables #-} |
2 | {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} | ||
3 | {-# LANGUAGE InstanceSigs #-} | ||
2 | 4 | ||
3 | module Events.Spec.Eval | 5 | module Events.Spec.Eval |
4 | ( evalExpr | 6 | ( evalExpr |
7 | , Bindable(..) | ||
5 | ) where | 8 | ) where |
6 | 9 | ||
7 | import Events.Spec.Types | 10 | import Events.Spec.Types |
@@ -11,10 +14,11 @@ shift = shift' LZ | |||
11 | where | 14 | where |
12 | -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x | 15 | -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x |
13 | shift' :: forall ts1 x. Length ts1 -> Expr m (ts1 ++ ts2) x -> Expr m (ts1 ++ t ': ts2) x | 16 | shift' :: forall ts1 x. Length ts1 -> Expr m (ts1 ++ ts2) x -> Expr m (ts1 ++ t ': ts2) x |
14 | shift' _ (ELit x) = ELit x | 17 | shift' LZ (EPri f) = EPri $ const (EPri f) |
15 | shift' l (EVar v) = EVar $ shiftElem l v | 18 | shift' (LS l) (EPri f) = EPri $ shift' l . f |
16 | shift' l (ELam b) = ELam $ shift' (LS l) b | 19 | shift' l (EVar v) = EVar $ shiftElem l v |
17 | shift' l (EApp f x) = EApp (shift' l f) (shift' l x) | 20 | shift' l (ELam b) = ELam $ shift' (LS l) b |
21 | shift' l (EApp f x) = EApp (shift' l f) (shift' l x) | ||
18 | 22 | ||
19 | shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2) | 23 | shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2) |
20 | shiftElem LZ e = ES e | 24 | shiftElem LZ e = ES e |
@@ -24,7 +28,8 @@ shift = shift' LZ | |||
24 | 28 | ||
25 | beta = flip beta' LZ | 29 | beta = flip beta' LZ |
26 | beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t | 30 | beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t |
27 | beta' _ _ (ELit x) = ELit x | 31 | beta' e LZ (EPri f) = EApp (ELam (EPri f)) e |
32 | beta' e (LS l) (EPri f) = EPri (beta' e l . f) | ||
28 | beta' e LZ (EVar EZ ) = e | 33 | beta' e LZ (EVar EZ ) = e |
29 | beta' _ LZ (EVar (ES v)) = EVar v | 34 | beta' _ LZ (EVar (ES v)) = EVar v |
30 | beta' _ (LS _) (EVar EZ ) = EVar EZ | 35 | beta' _ (LS _) (EVar EZ ) = EVar EZ |
@@ -33,6 +38,32 @@ beta' e l (ELam b) = ELam $ beta' e (LS l) b | |||
33 | beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) | 38 | beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) |
34 | 39 | ||
35 | evalExpr :: Expr m '[] t -> Val m t | 40 | evalExpr :: Expr m '[] t -> Val m t |
36 | evalExpr (ELit a) = a | 41 | evalExpr (EVal a) = a |
37 | evalExpr (ELam a) = a | 42 | evalExpr (ELam a) = a |
38 | evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) | 43 | evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a |
44 | evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) | ||
45 | |||
46 | -- liftE :: (Val m a -> Val m b) -> Expr m (a ': ctx) b | ||
47 | -- liftE = EPri . (EVal .) | ||
48 | |||
49 | -- bindE :: (m a -> b) -> Expr m (a ': Ctx b) (Fin b) | ||
50 | -- bindE f = liftE $ bindE . f | ||
51 | |||
52 | type family Ctx f where | ||
53 | Ctx (a -> b) = (a ': Ctx b) | ||
54 | Ctx a = '[] | ||
55 | |||
56 | type family Fin f where | ||
57 | Fin (a -> b) = Fin b | ||
58 | Fin a = a | ||
59 | |||
60 | class Bindable m b where | ||
61 | bindE :: (Val m a -> m b) -> Expr m (a ': Ctx b) (Fin b) | ||
62 | |||
63 | instance {-# OVERLAPS #-} ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (b -> c) where | ||
64 | bindE :: (Val m a -> m (b -> c)) -> Expr m (a ': b ': Ctx c) (Fin c) | ||
65 | bindE f = (EPri :: (Val m a -> Expr m (b ': Ctx c) (Fin c)) -> Expr m (a ': b ': Ctx c) (Fin c)) . ((bindE :: (Val m b -> m c) -> Expr m (b ': Ctx c) (Fin c)) . ) $ ((<*>) . f) | ||
66 | |||
67 | instance (Val m b ~ m b, Ctx b ~ '[], Fin b ~ b) => Bindable m b where | ||
68 | bindE :: (Val m a -> Val m b) -> Expr m '[a] b | ||
69 | bindE = EPri . (EVal .) | ||