summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--events/src/Events/Spec.hs1
-rw-r--r--events/src/Events/Spec/Eval.hs49
-rw-r--r--events/src/Events/Spec/Parse.hs2
-rw-r--r--events/src/Events/Spec/Types.hs11
4 files changed, 49 insertions, 14 deletions
diff --git a/events/src/Events/Spec.hs b/events/src/Events/Spec.hs
index cfa75be..c2a84ac 100644
--- a/events/src/Events/Spec.hs
+++ b/events/src/Events/Spec.hs
@@ -4,6 +4,7 @@ module Events.Spec
4 ( interpret 4 ( interpret
5 , Spec, Cmnd(..), Expr(..), Elem(..) 5 , Spec, Cmnd(..), Expr(..), Elem(..)
6 , module Events.Spec.Parse 6 , module Events.Spec.Parse
7 , module Events.Spec.Eval
7 ) where 8 ) where
8 9
9import Events.Spec.Types 10import Events.Spec.Types
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
3module Events.Spec.Eval 5module Events.Spec.Eval
4 ( evalExpr 6 ( evalExpr
7 , Bindable(..)
5 ) where 8 ) where
6 9
7import Events.Spec.Types 10import 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
25beta = flip beta' LZ 29beta = flip beta' LZ
26beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t 30beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t
27beta' _ _ (ELit x) = ELit x 31beta' e LZ (EPri f) = EApp (ELam (EPri f)) e
32beta' e (LS l) (EPri f) = EPri (beta' e l . f)
28beta' e LZ (EVar EZ ) = e 33beta' e LZ (EVar EZ ) = e
29beta' _ LZ (EVar (ES v)) = EVar v 34beta' _ LZ (EVar (ES v)) = EVar v
30beta' _ (LS _) (EVar EZ ) = EVar EZ 35beta' _ (LS _) (EVar EZ ) = EVar EZ
@@ -33,6 +38,32 @@ beta' e l (ELam b) = ELam $ beta' e (LS l) b
33beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) 38beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a)
34 39
35evalExpr :: Expr m '[] t -> Val m t 40evalExpr :: Expr m '[] t -> Val m t
36evalExpr (ELit a) = a 41evalExpr (EVal a) = a
37evalExpr (ELam a) = a 42evalExpr (ELam a) = a
38evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) 43evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a
44evalExpr (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
52type family Ctx f where
53 Ctx (a -> b) = (a ': Ctx b)
54 Ctx a = '[]
55
56type family Fin f where
57 Fin (a -> b) = Fin b
58 Fin a = a
59
60class Bindable m b where
61 bindE :: (Val m a -> m b) -> Expr m (a ': Ctx b) (Fin b)
62
63instance {-# 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
67instance (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 .)
diff --git a/events/src/Events/Spec/Parse.hs b/events/src/Events/Spec/Parse.hs
index 912a308..f3114f1 100644
--- a/events/src/Events/Spec/Parse.hs
+++ b/events/src/Events/Spec/Parse.hs
@@ -18,7 +18,7 @@ import Events.Spec.Types
18import Control.Monad.Catch (MonadThrow) 18import Control.Monad.Catch (MonadThrow)
19 19
20parse :: MonadThrow m => Consumer Text m (Spec m) 20parse :: MonadThrow m => Consumer Text m (Spec m)
21parse = sinkParser $ (tokenize >>= pSpec) <* endOfInput 21parse = sinkParser $ pSpec <* endOfInput
22 22
23pSpec :: Monad m => Parser (Spec m) 23pSpec :: Monad m => Parser (Spec m)
24pSpec = mzero 24pSpec = mzero
diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
index 5216f46..c7fd058 100644
--- a/events/src/Events/Spec/Types.hs
+++ b/events/src/Events/Spec/Types.hs
@@ -13,8 +13,11 @@ module Events.Spec.Types
13 13
14import Events.Types 14import Events.Types
15 15
16-- | A functional language reminiscent of typed lambda calculus with monadic
17-- side-effects and foreign primitives
16data Expr :: (* -> *) -> [*] -> * -> * where 18data Expr :: (* -> *) -> [*] -> * -> * where
17 ELit :: Val m a -> Expr m ctx a 19 EVal :: Val m a -> Expr m ctx a
20 EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
18 EVar :: Elem a ctx -> Expr m ctx a 21 EVar :: Elem a ctx -> Expr m ctx a
19 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res) 22 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)
20 EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a 23 EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a
@@ -38,8 +41,8 @@ data Length :: [a] -> * where
38 LZ :: Length '[] 41 LZ :: Length '[]
39 LS :: Length xs -> Length (x ': xs) 42 LS :: Length xs -> Length (x ': xs)
40 43
41type family (xs :: [a]) ++ (ys :: [a]) :: [a] 44type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
42type instance '[] ++ ys = ys 45 '[] ++ ys = ys
43type instance (x ': xs) ++ ys = x ': (xs ++ ys) 46 (x ': xs) ++ ys = x ': (xs ++ ys)
44infixr 5 ++ 47infixr 5 ++
45 48