summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--events/src/Events/Spec/Eval.hs4
-rw-r--r--events/src/Events/Spec/Types.hs2
2 files changed, 3 insertions, 3 deletions
diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs
index a9c16de..ada273a 100644
--- a/events/src/Events/Spec/Eval.hs
+++ b/events/src/Events/Spec/Eval.hs
@@ -16,7 +16,7 @@ shift = shift' LZ
16 shift' l (EVar v) = EVar $ shiftElem l v 16 shift' l (EVar v) = EVar $ shiftElem l v
17 shift' l (ELam b) = ELam $ shift' (LS l) b 17 shift' l (ELam b) = ELam $ shift' (LS l) b
18 shift' l (EApp f x) = EApp (shift' l f) (shift' l x) 18 shift' l (EApp f x) = EApp (shift' l f) (shift' l x)
19 shift' l (EVal _) = undefined 19 shift' _ (EVal v) = EVal v
20 20
21 shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2) 21 shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2)
22 shiftElem LZ e = ES e 22 shiftElem LZ e = ES e
@@ -35,7 +35,7 @@ beta = flip beta' LZ
35 beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) 35 beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v)
36 beta' e l (ELam b) = ELam $ beta' e (LS l) b 36 beta' e l (ELam b) = ELam $ beta' e (LS l) b
37 beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) 37 beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a)
38 beta' _ l (EVal _) = undefined 38 beta' _ _ (EVal v) = EVal v
39 39
40evalExpr :: Expr m '[] t -> Val m t 40evalExpr :: Expr m '[] t -> Val m t
41evalExpr (EVal a) = a 41evalExpr (EVal a) = a
diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
index d9d1ef1..1f319c7 100644
--- a/events/src/Events/Spec/Types.hs
+++ b/events/src/Events/Spec/Types.hs
@@ -18,7 +18,7 @@ import Events.Types
18-- | A functional language reminiscent of typed lambda calculus with monadic 18-- | A functional language reminiscent of typed lambda calculus with monadic
19-- side-effects and foreign primitives 19-- side-effects and foreign primitives
20data Expr :: (* -> *) -> [*] -> * -> * where 20data Expr :: (* -> *) -> [*] -> * -> * where
21 EVal :: Val m a -> Expr m ctx a 21 EVal :: Val m a ~ m a => Val m a -> Expr m ctx a
22 EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b 22 EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
23 EVar :: Elem a ctx -> Expr m ctx a 23 EVar :: Elem a ctx -> Expr m ctx a
24 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res) 24 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)