content: {-# LANGUAGE GADTs #-}
  
  module TypeChecking.Context where
  
  import Control.Monad
  
  import Syntax.Term
  
  data Ctx s f b a where
      Nil  :: Ctx s f b b
      Snoc :: Ctx s f b a -> s -> f a -> Ctx s f b (Scoped a)
  
  (+++) :: Ctx s f a b -> Ctx s f b c -> Ctx s f a c
  ctx +++ Nil = ctx
  ctx +++ Snoc ctx' s t = Snoc (ctx +++ ctx') s t
  
  lengthCtx :: Ctx s f b a -> Int
  lengthCtx Nil = 0
  lengthCtx (Snoc ctx _ _) = lengthCtx ctx + 1
  
  lookupCtx :: (Monad g, Functor f, Eq s) => s -> Ctx s f b a -> Maybe (g a, f a)
  lookupCtx _ Nil = Nothing
  lookupCtx b (Snoc ctx s t) = if s == b
      then Just (return Bound, fmap Free t)
      else fmap (\(te, ty) -> (liftM Free te, fmap Free ty)) (lookupCtx b ctx)
  
  ctxToVars :: Ctx s f b a -> [a]
  ctxToVars = reverse . go
    where
      go :: Ctx s f b a -> [a]
      go Nil = []
      go (Snoc ctx s _) = Bound : map Free (go ctx)
  
  close :: Functor f => Ctx c g b a -> f (Either c a) -> f (Either c b)
  close Nil            t = t
  close (Snoc ctx s _) t = close ctx $ fmap (\v -> case v of
      Left c          -> Left c
      Right Bound     -> Left s
      Right (Free a)  -> Right a) t
  
  liftBase :: Ctx s f b a -> b -> a
  liftBase Nil = id
  liftBase (Snoc ctx _ _) = Free . liftBase ctx
  
  toBase :: Ctx s f b a -> a -> Maybe b
  toBase Nil b = Just b
  toBase Snoc{} Bound = Nothing
  toBase (Snoc ctx _ _) (Free a) = toBase ctx a
  
  ctxVars :: Ctx s f b a -> [s]
  ctxVars = reverse . go
    where
      go :: Ctx s f b a -> [s]
      go Nil = []
      go (Snoc ctx v _) = v : go ctx
  
  abstractTerm :: Ctx s f b a -> Term p a -> Term p b
  abstractTerm Nil term = term
  abstractTerm (Snoc ctx v _) term = abstractTerm ctx (Lambda term)
  