Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Monad.Context

Contents

- Modifying the context
- Adding to the context
- Querying the context

Synopsis

- modifyContextEntry :: (Dom (Name, Type) -> Dom (Name, Type)) -> ContextEntry -> ContextEntry
- modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context
- modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a
- mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry
- inContext :: MonadTCM tcm => [Dom (Name, Type)] -> tcm a -> tcm a
- inTopContext :: MonadTCM tcm => tcm a -> tcm a
- escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
- escapeContextToTopLevel :: MonadTCM tcm => tcm a -> tcm a
- addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a
- addContext :: MonadTCM tcm => [Dom (Name, Type)] -> tcm a -> tcm a
- addCtxs :: MonadTCM tcm => [Name] -> Dom Type -> tcm a -> tcm a
- addCtxString :: MonadTCM tcm => String -> Dom Type -> tcm a -> tcm a
- addCtxString_ :: MonadTCM tcm => String -> tcm a -> tcm a
- dummyDom :: Dom Type
- underAbstraction :: (Subst a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: (Subst a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b
- addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a
- addLetBinding :: MonadTCM tcm => Relevance -> Name -> Term -> Type -> tcm a -> tcm a
- getContext :: MonadTCM tcm => tcm [Dom (Name, Type)]
- getContextSize :: MonadTCM tcm => tcm Nat
- getContextArgs :: MonadTCM tcm => tcm Args
- getContextTerms :: MonadTCM tcm => tcm [Term]
- getContextTelescope :: MonadTCM tcm => tcm Telescope
- getContextId :: MonadTCM tcm => tcm [CtxId]
- typeOfBV' :: MonadTCM tcm => Nat -> tcm (Dom Type)
- typeOfBV :: MonadTCM tcm => Nat -> tcm Type
- nameOfBV :: MonadTCM tcm => Nat -> tcm Name
- (!!!) :: (Eq a, Num a, Show a, MonadTCM m) => [b] -> a -> m b
- getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Dom Type)

# 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 `ContextEntry`s.

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.

escapeContextToTopLevel :: MonadTCM tcm => tcm a -> tcm a

Deprecated.

# 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`.

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

N-ary variant of `addCtx`.

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.

dummyDom :: Dom Type

Context entries without a type have this dummy type.

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

Go under an abstraction.

underAbstraction_ :: (Subst 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 => Relevance -> Name -> Term -> Type -> tcm a -> tcm a

Add a let bound variable

# Querying the context

getContext :: MonadTCM tcm => tcm [Dom (Name, Type)]

Get the current context.

getContextSize :: MonadTCM tcm => tcm Nat

Get the size of the current context.

getContextArgs :: MonadTCM tcm => tcm Args

Generate [Var n - 1, .., Var 0] for all declarations in the context.

getContextTerms :: MonadTCM tcm => tcm [Term]

getContextTelescope :: MonadTCM tcm => tcm Telescope

Get the current context as a `Telescope` with the specified `Hiding`.

getContextId :: MonadTCM tcm => tcm [CtxId]

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

typeOfBV' :: MonadTCM tcm => Nat -> tcm (Dom Type)

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

typeOfBV :: MonadTCM tcm => Nat -> tcm Type

nameOfBV :: MonadTCM tcm => Nat -> tcm Name

(!!!) :: (Eq a, Num a, Show a, MonadTCM m) => [b] -> a -> m b

TODO: move(?)

getVarInfo :: MonadTCM tcm => Name -> tcm (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.