    {-# LANGUAGE CPP #-}

    -- | Functions for abstracting terms over other terms.
    module Agda.TypeChecking.Abstract where

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Substitute
    import Data.Function

    #include "../undefined.h"
    import Agda.Utils.Impossible

    piAbstractTerm :: Term -> Type -> Type -> Type
    piAbstractTerm v a b = fun a (abstractTerm v b)
      where
        fun a b = El s $ Pi (Arg NotHidden a) $ Abs "w" b
          where s = (sLub `on` getSort) a b

    class AbstractTerm a where
      -- | @subst u . abstractTerm u == id@
      abstractTerm :: Term -> a -> a

    instance AbstractTerm Term where
      abstractTerm u v = case v of
        v | u == v  -> Var 0 []
        Var i vs    -> Var (i + 1) $ absT vs
        Lam h b     -> Lam h $ absT b
        Def c vs    -> Def c $ absT vs
        Con c vs    -> Con c $ absT vs
        Pi a b      -> uncurry Pi $ absT (a, b)
        Fun a b      -> uncurry Fun $ absT (a, b)
        Lit l       -> Lit l
        Sort s      -> Sort s
        MetaV m vs  -> MetaV m $ absT vs
        where
          absT x = abstractTerm u x

    instance AbstractTerm Type where
      abstractTerm u (El s v) = El s $ abstractTerm u v

    instance AbstractTerm a => AbstractTerm (Arg a) where
      abstractTerm = fmap . abstractTerm

    instance AbstractTerm a => AbstractTerm [a] where
      abstractTerm = fmap . abstractTerm

    instance (Subst a, AbstractTerm a) => AbstractTerm (Abs a) where
      abstractTerm u (Abs x v) = Abs x $ swap $ abstractTerm (raise 1 u) v
        where
          swap = substs $ [Var 1 [], Var 0 []] ++ [Var i [] | i <- [2..]]

    instance (AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b) where
      abstractTerm u (x, y) = (abstractTerm u x, abstractTerm u y)