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