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
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)