Agda.TypeChecking.Monad.Context

Modifying the context

modifyContextEntry :: (Dom (Name, Type) -> Dom (Name, Type)) -> ContextEntry -> ContextEntry

Modify the ctxEntry field of a ContextEntry.

modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context

Modify all ContextEntrys.

modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a

Modify a Context in a computation.

mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry

inContext :: MonadTCM tcm => [Dom (Name, Type)] -> tcm a -> tcm a

Change the context.

inTopContext :: MonadTCM tcm => tcm a -> tcm a

Change to top (=empty) context.

escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a

Delete the last n bindings from the context.

Adding to the context

addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

class AddContext b where

Various specializations of addCtx.

Minimal complete definition

addContext

Methods

addContext :: MonadTCM tcm => b -> tcm a -> tcm a

Instances

AddContext String

Methods

addContext :: MonadTCM tcm => String -> tcm a -> tcm a

AddContext Name

Methods

addContext :: MonadTCM tcm => Name -> tcm a -> tcm a

AddContext Telescope

Methods

addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a

AddContext a => AddContext [a]

Methods

addContext :: MonadTCM tcm => [a] -> tcm a -> tcm a

AddContext (Dom (String, Type))

Methods

addContext :: MonadTCM tcm => Dom (String, Type) -> tcm a -> tcm a

AddContext (Dom (Name, Type))

Methods

addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a

AddContext (Dom Type)

Methods

addContext :: MonadTCM tcm => Dom Type -> tcm a -> tcm a

AddContext ([WithHiding Name], Dom Type)

Methods

addContext :: MonadTCM tcm => ([WithHiding Name], Dom Type) -> tcm a -> tcm a

AddContext ([Name], Dom Type)

Methods

addContext :: MonadTCM tcm => ([Name], Dom Type) -> tcm a -> tcm a

AddContext (String, Dom Type)

Methods

addContext :: MonadTCM tcm => (String, Dom Type) -> tcm a -> tcm a

AddContext (Name, Dom Type)

Methods

addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a

addCtxs :: MonadTCM tcm => [Name] -> Dom Type -> tcm a -> tcm a

add a bunch of variables with the same type to the context

addCtxString :: MonadTCM tcm => String -> Dom Type -> tcm a -> tcm a

Turns the string into a name and adds it to the context.

addCtxString_ :: MonadTCM tcm => String -> tcm a -> tcm a

Turns the string into a name and adds it to the context, with dummy type.

addCtxStrings_ :: MonadTCM tcm => [String] -> tcm a -> tcm a

dummyDom :: Dom Type

Context entries without a type have this dummy type.

underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b

Go under an abstraction.

underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b

Go under an abstract without worrying about the type to add to the context.

addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a

Add a telescope to the context.

addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a

Add a let bound variable

Querying the context

getContext :: MonadReader TCEnv m => m [Dom (Name, Type)]

Get the current context.

getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat

Get the size of the current context.

getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term]

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope

Get the current context as a Telescope.

getContextId :: MonadReader TCEnv m => m [CtxId]

Check if we are in a compatible context, i.e. an extension of the given context.

getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name]

Get the names of all declarations in the context.

lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type))

get type of bound variable (i.e. deBruijn index)

typeOfBV' :: (Applicative m, MonadReader TCEnv m) => Nat -> m (Dom Type)

typeOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Type

nameOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Name

getVarInfo :: MonadReader TCEnv m => Name -> m (Term, Dom Type)

Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.