1 files changed, 38 insertions, 0 deletions

diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs
new file mode 100644
index 0000000..3a23e0b
--- /dev/null
+++ b/events/src/Events/Spec/Eval.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables #-}
+
+module Events.Spec.Eval
+  ( evalExpr
+  ) where
+
+import Events.Spec.Types
+
+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' _ (ELit x)   = ELit x
+    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)
+  
+    shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2)
+    shiftElem LZ e = ES e
+    shiftElem (LS _) EZ = EZ
+    shiftElem (LS l) (ES e) = ES $ shiftElem l e
+    
+
+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' _  _     (ELit x)      = ELit x
+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)
+
+evalExpr :: Expr m '[] t -> Val m t
+evalExpr (ELit a)   = a
+evalExpr (ELam a)   = a
+evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f)