From 95b623a3ebaa115b6ef889032854b355a010a037 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 5 Aug 2016 15:51:20 +0200 Subject: cleanup --- events/src/Events/Spec.hs | 2 +- events/src/Events/Spec/Eval.hs | 24 ++++++++++++++---------- events/src/Events/Spec/Types.hs | 4 ++-- events/src/Events/Types/NDT.hs | 10 ++-------- 4 files changed, 19 insertions(+), 21 deletions(-) (limited to 'events/src/Events') diff --git a/events/src/Events/Spec.hs b/events/src/Events/Spec.hs index 734a2dd..8b82873 100644 --- a/events/src/Events/Spec.hs +++ b/events/src/Events/Spec.hs @@ -1,5 +1,5 @@ module Events.Spec - ( Spec, Expr(..), Val(..), Bindable(..), Elem(..) + ( Spec, Expr(..), Val, Bindable(..), Elem(..) , module Events.Spec.Parse , module Events.Spec.Eval ) where diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs index fdc18c8..a9c16de 100644 --- a/events/src/Events/Spec/Eval.hs +++ b/events/src/Events/Spec/Eval.hs @@ -10,12 +10,13 @@ shift :: forall m ts2 t x. Expr m ts2 x -> Expr m (t ': ts2) x shift = shift' LZ where -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x - shift' :: forall ts1 x. Length ts1 -> Expr m (ts1 ++ ts2) x -> Expr m (ts1 ++ t ': ts2) x + shift' :: forall ts1 y. Length ts1 -> Expr m (ts1 ++ ts2) y -> Expr m (ts1 ++ t ': ts2) y shift' LZ (EPri f) = EPri $ const (EPri f) shift' (LS l) (EPri f) = EPri $ shift' l . f shift' l (EVar v) = EVar $ shiftElem l v shift' l (ELam b) = ELam $ shift' (LS l) b shift' l (EApp f x) = EApp (shift' l f) (shift' l x) + shift' l (EVal _) = undefined shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2) shiftElem LZ e = ES e @@ -24,18 +25,21 @@ shift = shift' LZ beta = flip beta' LZ -beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t -beta' e LZ (EPri f) = EApp (ELam (EPri f)) e -beta' e (LS l) (EPri f) = EPri (beta' e l . f) -beta' e LZ (EVar EZ ) = e -beta' _ LZ (EVar (ES v)) = EVar v -beta' _ (LS _) (EVar EZ ) = EVar EZ -beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) -beta' e l (ELam b) = ELam $ beta' e (LS l) b -beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) + where + beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t + beta' e LZ (EPri f) = EApp (ELam (EPri f)) e + beta' e (LS l) (EPri f) = EPri (beta' e l . f) + beta' e LZ (EVar EZ ) = e + beta' _ LZ (EVar (ES v)) = EVar v + beta' _ (LS _) (EVar EZ ) = EVar EZ + beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) + beta' e l (ELam b) = ELam $ beta' e (LS l) b + beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) + beta' _ l (EVal _) = undefined evalExpr :: Expr m '[] t -> Val m t evalExpr (EVal a) = a evalExpr (ELam a) = a evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) +evalExpr (EVar _) = error "EVar was given bottom" diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs index af99f55..d9d1ef1 100644 --- a/events/src/Events/Spec/Types.hs +++ b/events/src/Events/Spec/Types.hs @@ -4,12 +4,12 @@ module Events.Spec.Types ( Expr(..) - , Val(..) + , Val , Bindable(..) , Spec , Elem(..) , Length(..) - , type (++)(..) + , type (++) , module Events.Types ) where diff --git a/events/src/Events/Types/NDT.hs b/events/src/Events/Types/NDT.hs index a417029..c37d47c 100644 --- a/events/src/Events/Types/NDT.hs +++ b/events/src/Events/Types/NDT.hs @@ -12,22 +12,16 @@ module Events.Types.NDT import Data.Monoid import Data.Foldable (foldr) -import Data.Maybe -import Data.Either import Data.Bool (bool) import Control.Applicative (Alternative) import qualified Control.Applicative as Alt (Alternative(..)) import Control.Monad -import Control.Monad.Identity import Control.Monad.Trans import Control.Monad.Reader (MonadReader(..)) -import Control.Monad.Trans.Maybe import Control.Monad.Catch (MonadThrow(..)) -import Debug.Trace - data NDT m a where NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a @@ -37,7 +31,7 @@ instance Functor m => Functor (NDT m) where fmap f (NDTCons x) = NDTCons $ fmap f' x where f' Nothing = Nothing - f' (Just (x, xs)) = Just (f x, fmap f xs) + f' (Just (x', xs)) = Just (f x', fmap f xs) instance Applicative m => Applicative (NDT m) where pure x = NDTCons . pure $ Just (x, empty) @@ -49,7 +43,7 @@ instance Applicative m => Monad (NDT m) where instance Monad m => Monoid (NDT m a) where mempty = empty - mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x, xs) -> return $ Just (x, xs <> y')) =<< x + mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x', xs) -> return $ Just (x', xs <> y')) =<< x mappend (NDTBind x f) (NDTBind y g) = NDTBind (fmap Left x <> fmap Right y) (either f g) mappend x@(NDTBind _ _) y = x <> NDTBind y return mappend x y@(NDTBind _ _) = NDTBind x return <> y -- cgit v1.2.3