Agda.TypeChecking.Monad.Context

Modifying the context

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

Modify a Context in a computation.

safeInTopContext :: MonadTCM tcm => tcm a -> tcm a

Change to top (=empty) context. Resets the checkpoints.

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

Change to top (=empty) context, but don't update the checkpoints. Totally not safe!

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

Delete the last n bindings from the context.

Doesn't update checkpoints!! Use `updateContext rho (drop n)` instead, for an appropriate substitution rho.

Manipulating checkpoints --

checkpoint :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> tcm a -> tcm a

Add a new checkpoint. Do not use directly!

updateContext :: (MonadDebug tcm, MonadTCM tcm) => Substitution -> (Context -> Context) -> tcm a -> tcm a

Update the context. Requires a substitution from the old context to the new.

checkpointSubstitution :: MonadReader TCEnv tcm => CheckpointId -> tcm Substitution

Get the substitution from the context at a given checkpoint to the current context.

getModuleParameterSub :: (MonadReader TCEnv m, ReadTCState m) => ModuleName -> m Substitution

Get substitution Γ ⊢ ρ : Γm where Γ is the current context and Γm is the module parameter telescope of module m.

In case the we don't have a checkpoint for m we return the identity substitution. This is ok for instance if we are outside module m (in which case we have to supply all module parameters to any symbol defined within m we want to refer).

Adding to the context

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

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

Warning: Does not update module parameter substitution!

unshadowedName :: [Name] -> Name -> Name

Pick a concrete name that doesn't shadow anything in the given list.

unshadowName :: MonadTCM tcm => Name -> tcm Name

Pick a concrete name that doesn't shadow anything in the context.

class AddContext b where

Various specializations of addCtx.

Minimal complete definition

addContext, contextSize

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => b -> tcm a -> tcm a

contextSize :: b -> Nat

Instances

AddContext String

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: String -> Nat

AddContext Name

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Name -> Nat

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a

contextSize :: Telescope -> Nat

AddContext a => AddContext [a]

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => [a] -> tcm a0 -> tcm a0

contextSize :: [a] -> Nat

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom (String, Type) -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom (Name, Type) -> Nat

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([WithHiding Name], Dom Type) -> Nat

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([Name], Dom Type) -> Nat

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (String, Dom Type) -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (Name, Dom Type) -> Nat

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (KeepNames String, Dom Type) -> Nat

newtype KeepNames a

Wrapper to tell 'addContext not to unshadowNames. Used when adding a user-provided, but already type checked, telescope to the context.

Constructors

KeepNames a

Instances

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: (KeepNames String, Dom Type) -> Nat

dummyDom :: Dom Type

Context entries without a type have this dummy type.

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

Go under an abstraction.

underAbstraction' :: (Subst t a, MonadTCM tcm, MonadDebug tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b

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

Go under an abstract without worrying about the type to add 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.

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.