    module Agda.TypeChecking.Substitute.DeBruijn where

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    -- | Things we can substitute for a variable.
    --   Needs to be able to represent variables, e.g. for substituting under binders.
    class DeBruijn a where

      -- | Produce a variable without name suggestion.
      deBruijnVar  :: Int -> a
      deBruijnVar = String -> Int -> a
    forall a. DeBruijn a => String -> Int -> a
    debruijnNamedVar String
    forall a. Underscore a => a
    underscore

      -- | Produce a variable with name suggestion.
      debruijnNamedVar :: String -> Int -> a
      debruijnNamedVar String
    _ = Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar

      -- | Are we dealing with a variable?
      --   If yes, what is its index?
      deBruijnView :: a -> Maybe Int

    -- | We can substitute @Term@s for variables.
    instance DeBruijn Term where
      deBruijnVar :: Int -> Term
    deBruijnVar = Int -> Term
    var
      deBruijnView :: Term -> Maybe Int
    deBruijnView Term
    u =
        case Term
    u of
          Var Int
    i [] -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i
          Level Level
    l -> Level -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView Level
    l
          Term
    _ -> Maybe Int
    forall a. Maybe a
    Nothing

    instance DeBruijn PlusLevel where
      deBruijnVar :: Int -> PlusLevel
    deBruijnVar = Integer -> Term -> PlusLevel
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    0 (Term -> PlusLevel) -> (Int -> Term) -> Int -> PlusLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    forall a. DeBruijn a => Int -> a
    deBruijnVar
      deBruijnView :: PlusLevel -> Maybe Int
    deBruijnView PlusLevel
    l =
        case PlusLevel
    l of
          Plus Integer
    0 Term
    a -> Term -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView Term
    a
          PlusLevel
    _ -> Maybe Int
    forall a. Maybe a
    Nothing

    instance DeBruijn Level where
      deBruijnVar :: Int -> Level
    deBruijnVar Int
    i = Integer -> [PlusLevel] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [Int -> PlusLevel
    forall a. DeBruijn a => Int -> a
    deBruijnVar Int
    i]
      deBruijnView :: Level -> Maybe Int
    deBruijnView Level
    l =
        case Level
    l of
          Max Integer
    0 [PlusLevel
    p] -> PlusLevel -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView PlusLevel
    p
          Level
    _ -> 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