diff options
Diffstat (limited to 'events/src/Events/Spec/Eval.hs')
| -rw-r--r-- | events/src/Events/Spec/Eval.hs | 24 |
1 files changed, 14 insertions, 10 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 | |||
| 10 | shift = shift' LZ | 10 | shift = 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 | ||
| 26 | beta = flip beta' LZ | 27 | beta = flip beta' LZ |
| 27 | beta' :: 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 |
| 28 | beta' 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 |
| 29 | beta' e (LS l) (EPri f) = EPri (beta' e l . f) | 30 | beta' e LZ (EPri f) = EApp (ELam (EPri f)) e |
| 30 | beta' e LZ (EVar EZ ) = e | 31 | beta' e (LS l) (EPri f) = EPri (beta' e l . f) |
| 31 | beta' _ LZ (EVar (ES v)) = EVar v | 32 | beta' e LZ (EVar EZ ) = e |
| 32 | beta' _ (LS _) (EVar EZ ) = EVar EZ | 33 | beta' _ LZ (EVar (ES v)) = EVar v |
| 33 | beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) | 34 | beta' _ (LS _) (EVar EZ ) = EVar EZ |
| 34 | beta' e l (ELam b) = ELam $ beta' e (LS l) b | 35 | beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v) |
| 35 | beta' 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 | ||
| 37 | evalExpr :: Expr m '[] t -> Val m t | 40 | evalExpr :: Expr m '[] t -> Val m t |
| 38 | evalExpr (EVal a) = a | 41 | evalExpr (EVal a) = a |
| 39 | evalExpr (ELam a) = a | 42 | evalExpr (ELam a) = a |
| 40 | evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a | 43 | evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a |
| 41 | evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) | 44 | evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) |
| 45 | evalExpr (EVar _) = error "EVar was given bottom" | ||