module Agda.TypeChecking.Substitute.Pattern where
import Data.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Substitute
#include "undefined.h"
import Agda.Utils.Impossible
instance DeBruijn DeBruijnPattern where
debruijnNamedVar n i = VarP (i,n)
debruijnView (VarP (i,_)) = Just i
debruijnView _ = Nothing
fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution = fmap patternToTerm
applyPatSubst :: (Subst Term a) => PatternSubstitution -> a -> a
applyPatSubst = applySubst . fromPatternSubstitution
instance Subst DeBruijnPattern DeBruijnPattern where
applySubst IdS p = p
applySubst rho p = case p of
VarP (i,n) -> useName n $ lookupS rho i
DotP u -> DotP $ applyPatSubst rho u
ConP c ci ps -> ConP c ci $ applySubst rho ps
LitP x -> p
ProjP f -> p
where
useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
useName n (VarP (i,"_")) = VarP (i,n)
useName _ x = x