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


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