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 = forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar forall a. Underscore a => a
underscore

  -- | Produce a variable with name suggestion.
  debruijnNamedVar :: String -> Int -> a
  debruijnNamedVar String
_ = 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 [] -> forall a. a -> Maybe a
Just Int
i
      Level Level
l -> forall a. DeBruijn a => a -> Maybe Int
deBruijnView Level
l
      Term
_ -> forall a. Maybe a
Nothing

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

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

instance DeBruijn DBPatVar where
  debruijnNamedVar :: String -> Int -> DBPatVar
debruijnNamedVar = String -> Int -> DBPatVar
DBPatVar
  deBruijnView :: DBPatVar -> Maybe Int
deBruijnView = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBPatVar -> Int
dbPatVarIndex


instance DeBruijn a => DeBruijn (Named_ a) where
  debruijnNamedVar :: String -> Int -> Named_ a
debruijnNamedVar String
nm Int
i = forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar String
nm Int
i
  deBruijnView :: Named_ a -> Maybe Int
deBruijnView = forall a. DeBruijn a => a -> Maybe Int
deBruijnView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing