{-# 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 y. Length ts1 -> Expr m (ts1 ++ ts2) y -> Expr m (ts1 ++ t ': ts2) y
    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)
    shift'  l     (EVal _)   = undefined
  
    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
  where
    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)
    beta' _  l     (EVal _)      = undefined

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)
evalExpr (EVar _)                 = error "EVar was given bottom"