module Agda.TypeChecking.Substitute.DeBruijn where
import Agda.Syntax.Common
import Agda.Syntax.Internal
class DeBruijn a where
deBruijnVar :: Int -> a
deBruijnVar = debruijnNamedVar underscore
debruijnNamedVar :: String -> Int -> a
debruijnNamedVar _ = deBruijnVar
deBruijnView :: a -> Maybe Int
instance DeBruijn Term where
deBruijnVar = var
deBruijnView u =
case u of
Var i [] -> Just i
Level l -> deBruijnView l
_ -> Nothing
instance DeBruijn LevelAtom where
deBruijnVar = NeutralLevel ReallyNotBlocked . deBruijnVar
deBruijnView l =
case l of
NeutralLevel _ u -> deBruijnView u
UnreducedLevel u -> deBruijnView u
MetaLevel{} -> Nothing
BlockedLevel{} -> Nothing
instance DeBruijn PlusLevel where
deBruijnVar = Plus 0 . deBruijnVar
deBruijnView l =
case l of
Plus 0 a -> deBruijnView a
_ -> Nothing
instance DeBruijn Level where
deBruijnVar i = Max [deBruijnVar i]
deBruijnView l =
case l of
Max [p] -> deBruijnView p
_ -> Nothing