From 5597e2f90b1e093a3b4dd110a84d40173e9abc77 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 5 Aug 2016 10:54:42 +0200 Subject: rename lifting --- events/src/Events/Spec/Eval.hs | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs index ddb32e4..9cfb7c1 100644 --- a/events/src/Events/Spec/Eval.hs +++ b/events/src/Events/Spec/Eval.hs @@ -43,12 +43,6 @@ evalExpr (ELam a) = a evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) --- liftE :: (Val m a -> Val m b) -> Expr m (a ': ctx) b --- liftE = EPri . (EVal .) - --- bindE :: (m a -> b) -> Expr m (a ': Ctx b) (Fin b) --- bindE f = liftE $ bindE . f - type family Ctx m f where Ctx m (m a -> b) = (a ': Ctx m b) Ctx m a = '[] @@ -59,12 +53,12 @@ type family Fin m f where Fin m a = a class Bindable m b where - bindE :: (Val m a -> b) -> Expr m (a ': Ctx m b) (Fin m b) + liftE :: (Val m a -> b) -> Expr m (a ': Ctx m b) (Fin m b) instance ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (m b -> c) where - bindE :: (Val m a -> m b -> c) -> Expr m (a ': b ': Ctx m c) (Fin m c) - bindE f = (EPri :: (Val m a -> Expr m (b ': Ctx m c) (Fin m c)) -> Expr m (a ': b ': Ctx m c) (Fin m c)) . ((bindE :: (Val m b -> c) -> Expr m (b ': Ctx m c) (Fin m c)) . ) $ f + liftE :: (Val m a -> m b -> c) -> Expr m (a ': b ': Ctx m c) (Fin m c) + liftE f = (EPri :: (Val m a -> Expr m (b ': Ctx m c) (Fin m c)) -> Expr m (a ': b ': Ctx m c) (Fin m c)) . ((liftE :: (Val m b -> c) -> Expr m (b ': Ctx m c) (Fin m c)) . ) $ f instance {-# OVERLAPPABLE #-} (Val m b ~ m b, Ctx m (m b) ~ '[], Fin m (m b) ~ b) => Bindable m (m b) where - bindE :: (Val m a -> Val m b) -> Expr m '[a] b - bindE = EPri . (EVal .) + liftE :: (Val m a -> Val m b) -> Expr m '[a] b + liftE = EPri . (EVal .) -- cgit v1.2.3