{-# LANGUAGE GADTs, DataKinds, TypeFamilies, TypeOperators, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}

module Events.Spec.Eval
  ( evalExpr
  , Bindable(..) 
  ) 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)

type family Ctx m f where
  Ctx m (m a -> b) = (a ': Ctx m b)
  Ctx m a = '[]

type family Fin m f where
  Fin m (m a -> b) = Fin m b
  Fin m (m a) = a
  Fin m a = a

class Bindable m b where
  liftE :: (Val m a -> b) -> Expr m (a ': Ctx m b) (Fin m b)

instance ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (m b -> c) where
  liftE :: (Val m a -> m b -> c) -> Expr m (a ': b ': Ctx m c) (Fin m c)
  liftE f = (EPri :: (Val m a -> Expr m (b ': Ctx m c) (Fin m c)) -> Expr m (a ': b ': Ctx m c) (Fin m c)) . ((liftE :: (Val m b -> c) -> Expr m (b ': Ctx m c) (Fin m c)) . ) $ f

instance {-# OVERLAPPABLE #-} (Val m b ~ m b, Ctx m (m b) ~ '[], Fin m (m b) ~ b) => Bindable m (m b) where
  liftE :: (Val m a -> Val m b) -> Expr m '[a] b
  liftE = EPri . (EVal .)