summaryrefslogtreecommitdiff
path: root/events/src/Events/Spec
diff options
context:
space:
mode:
Diffstat (limited to 'events/src/Events/Spec')
-rw-r--r--events/src/Events/Spec/Eval.hs24
-rw-r--r--events/src/Events/Spec/Types.hs4
2 files changed, 16 insertions, 12 deletions
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