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 = debruijnNamedVar underscore

  -- | Produce a variable with name suggestion.
  debruijnNamedVar :: String -> Int -> a
  debruijnNamedVar _ = 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 = 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