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 :: MonadTCEnv tcm => CheckpointId -> tcm Substitution

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

checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)

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

getModuleParameterSub :: (MonadTCEnv 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!

addRecordNameContext :: (MonadDebug m, MonadTCM m) => Dom Type -> m b -> m b

class AddContext b where

Various specializations of addCtx.

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 ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([Arg Name], Type) -> 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 mark names as NotInScope. 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

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

Go under an abstraction. Do not extend context in case of NoAbs.

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

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

Go under an abstraction, treating NoAbs as Abs.

underAbstractionAbs' :: (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.

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

addLetBinding' :: MonadTCM tcm => Name -> Term -> Dom Type -> tcm a -> tcm a

Add a let bound variable

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

Add a let bound variable

Querying the context

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

Get the current context.

getContextSize :: (Applicative m, MonadTCEnv m) => m Nat

Get the size of the current context.

getContextArgs :: (Applicative m, MonadTCEnv m) => m Args

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

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

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

getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope

Get the current context as a Telescope.

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

Get the names of all declarations in the context.

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

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

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

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

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

getVarInfo :: MonadTCEnv 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.