summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--events/events.cabal3
-rw-r--r--events/src/Events/Spec.hs2
-rw-r--r--events/src/Events/Spec/Eval.hs24
-rw-r--r--events/src/Events/Spec/Types.hs4
-rw-r--r--events/src/Events/Types/NDT.hs10
5 files changed, 21 insertions, 22 deletions
diff --git a/events/events.cabal b/events/events.cabal
index 4ab12fd..390f062 100644
--- a/events/events.cabal
+++ b/events/events.cabal
@@ -45,4 +45,5 @@ executable events
45 , attoparsec >=0.13.0.2 && <1 45 , attoparsec >=0.13.0.2 && <1
46 , exceptions >=0.8.3 && <1 46 , exceptions >=0.8.3 && <1
47 hs-source-dirs: src 47 hs-source-dirs: src
48 default-language: Haskell2010 \ No newline at end of file 48 default-language: Haskell2010
49 ghc-options: -Wall \ No newline at end of file
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 @@
1module Events.Spec 1module Events.Spec
2 ( Spec, Expr(..), Val(..), Bindable(..), Elem(..) 2 ( Spec, Expr(..), Val, Bindable(..), Elem(..)
3 , module Events.Spec.Parse 3 , module Events.Spec.Parse
4 , module Events.Spec.Eval 4 , module Events.Spec.Eval
5 ) where 5 ) 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
10shift = shift' LZ 10shift = shift' LZ
11 where 11 where
12 -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x 12 -- 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 13 shift' :: forall ts1 y. Length ts1 -> Expr m (ts1 ++ ts2) y -> Expr m (ts1 ++ t ': ts2) y
14 shift' LZ (EPri f) = EPri $ const (EPri f) 14 shift' LZ (EPri f) = EPri $ const (EPri f)
15 shift' (LS l) (EPri f) = EPri $ shift' l . f 15 shift' (LS l) (EPri f) = EPri $ shift' l . f
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 20
20 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)
21 shiftElem LZ e = ES e 22 shiftElem LZ e = ES e
@@ -24,18 +25,21 @@ shift = shift' LZ
24 25
25 26
26beta = flip beta' LZ 27beta = flip beta' LZ
27beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t 28 where
28beta' e LZ (EPri f) = EApp (ELam (EPri f)) e 29 beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t
29beta' e (LS l) (EPri f) = EPri (beta' e l . f) 30 beta' e LZ (EPri f) = EApp (ELam (EPri f)) e
30beta' e LZ (EVar EZ ) = e 31 beta' e (LS l) (EPri f) = EPri (beta' e l . f)
31beta' _ LZ (EVar (ES v)) = EVar v 32 beta' e LZ (EVar EZ ) = e
32beta' _ (LS _) (EVar EZ ) = EVar EZ 33 beta' _ LZ (EVar (ES v)) = EVar v
33beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) 34 beta' _ (LS _) (EVar EZ ) = EVar EZ
34beta' e l (ELam b) = ELam $ beta' e (LS l) b 35 beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v)
35beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) 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)
38 beta' _ l (EVal _) = undefined
36 39
37evalExpr :: Expr m '[] t -> Val m t 40evalExpr :: Expr m '[] t -> Val m t
38evalExpr (EVal a) = a 41evalExpr (EVal a) = a
39evalExpr (ELam a) = a 42evalExpr (ELam a) = a
40evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a 43evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a
41evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) 44evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f)
45evalExpr (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 @@
4 4
5module Events.Spec.Types 5module Events.Spec.Types
6 ( Expr(..) 6 ( Expr(..)
7 , Val(..) 7 , Val
8 , Bindable(..) 8 , Bindable(..)
9 , Spec 9 , Spec
10 , Elem(..) 10 , Elem(..)
11 , Length(..) 11 , Length(..)
12 , type (++)(..) 12 , type (++)
13 , module Events.Types 13 , module Events.Types
14 ) where 14 ) where
15 15
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
12 12
13import Data.Monoid 13import Data.Monoid
14import Data.Foldable (foldr) 14import Data.Foldable (foldr)
15import Data.Maybe
16import Data.Either
17import Data.Bool (bool) 15import Data.Bool (bool)
18 16
19import Control.Applicative (Alternative) 17import Control.Applicative (Alternative)
20import qualified Control.Applicative as Alt (Alternative(..)) 18import qualified Control.Applicative as Alt (Alternative(..))
21import Control.Monad 19import Control.Monad
22import Control.Monad.Identity
23 20
24import Control.Monad.Trans 21import Control.Monad.Trans
25import Control.Monad.Reader (MonadReader(..)) 22import Control.Monad.Reader (MonadReader(..))
26import Control.Monad.Trans.Maybe
27import Control.Monad.Catch (MonadThrow(..)) 23import Control.Monad.Catch (MonadThrow(..))
28 24
29import Debug.Trace
30
31data NDT m a where 25data NDT m a where
32 NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b 26 NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b
33 NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a 27 NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a
@@ -37,7 +31,7 @@ instance Functor m => Functor (NDT m) where
37 fmap f (NDTCons x) = NDTCons $ fmap f' x 31 fmap f (NDTCons x) = NDTCons $ fmap f' x
38 where 32 where
39 f' Nothing = Nothing 33 f' Nothing = Nothing
40 f' (Just (x, xs)) = Just (f x, fmap f xs) 34 f' (Just (x', xs)) = Just (f x', fmap f xs)
41 35
42instance Applicative m => Applicative (NDT m) where 36instance Applicative m => Applicative (NDT m) where
43 pure x = NDTCons . pure $ Just (x, empty) 37 pure x = NDTCons . pure $ Just (x, empty)
@@ -49,7 +43,7 @@ instance Applicative m => Monad (NDT m) where
49 43
50instance Monad m => Monoid (NDT m a) where 44instance Monad m => Monoid (NDT m a) where
51 mempty = empty 45 mempty = empty
52 mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x, xs) -> return $ Just (x, xs <> y')) =<< x 46 mappend (NDTCons x) y'@(NDTCons y) = NDTCons $ maybe y (\(x', xs) -> return $ Just (x', xs <> y')) =<< x
53 mappend (NDTBind x f) (NDTBind y g) = NDTBind (fmap Left x <> fmap Right y) (either f g) 47 mappend (NDTBind x f) (NDTBind y g) = NDTBind (fmap Left x <> fmap Right y) (either f g)
54 mappend x@(NDTBind _ _) y = x <> NDTBind y return 48 mappend x@(NDTBind _ _) y = x <> NDTBind y return
55 mappend x y@(NDTBind _ _) = NDTBind x return <> y 49 mappend x y@(NDTBind _ _) = NDTBind x return <> y