blob: fdc18c808ef30dd271eb3782249e2cf6a0652c02 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
{-# LANGUAGE GADTs, DataKinds, TypeFamilies, 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' 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)
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' 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)
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)
|
