Agda.TypeChecking.Monad.Context

Modifying the context

unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a

Modify a Context in a computation. Warning: does not update the checkpoints. Use updateContext instead.

modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a

Modify the Dom' part of context entries.

inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a

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

unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a

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

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

Delete the last n bindings from the context.

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

escapeContext :: MonadAddContext m => Impossible -> Int -> m a -> m a

Delete the last n bindings from the context. Any occurrences of these variables are replaced with the given err.

Manipulating checkpoints --

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

Add a new checkpoint. Do not use directly!

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 (Maybe Substitution)

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

Returns Nothing in case the we don't have a checkpoint for m.

Adding to the context

class MonadTCEnv m => MonadAddContext m where

Minimal complete definition

Nothing

Methods

addCtx :: Name -> Dom Type -> m a -> m a

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

Warning: Does not update module parameter substitution!

default addCtx :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Name -> Dom Type -> m a -> m a

addLetBinding' :: Name -> Term -> Dom Type -> m a -> m a

Add a let bound variable to the context

default addLetBinding' :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Name -> Term -> Dom Type -> m a -> m a

updateContext :: Substitution -> (Context -> Context) -> m a -> m a

Update the context. Requires a substitution that transports things living in the old context to the new.

default updateContext :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Substitution -> (Context -> Context) -> m a -> m a

withFreshName :: Range -> ArgName -> (Name -> m a) -> m a

default withFreshName :: (MonadAddContext n, MonadTransControl t, t n ~ m) => Range -> ArgName -> (Name -> m a) -> m a

Instances

MonadAddContext TerM

Defined in Agda.Termination.Monad

Methods

addCtx :: Name -> Dom Type -> TerM a -> TerM a

addLetBinding' :: Name -> Term -> Dom Type -> TerM a -> TerM a

updateContext :: Substitution -> (Context -> Context) -> TerM a -> TerM a

withFreshName :: Range -> ArgName -> (Name -> TerM a) -> TerM a

MonadAddContext ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

addCtx :: Name -> Dom Type -> ReduceM a -> ReduceM a

addLetBinding' :: Name -> Term -> Dom Type -> ReduceM a -> ReduceM a

updateContext :: Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a

withFreshName :: Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a

MonadAddContext TCM

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a

MonadAddContext NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

addCtx :: Name -> Dom Type -> NLM a -> NLM a

addLetBinding' :: Name -> Term -> Dom Type -> NLM a -> NLM a

updateContext :: Substitution -> (Context -> Context) -> NLM a -> NLM a

withFreshName :: Range -> ArgName -> (Name -> NLM a) -> NLM a

MonadAddContext m => MonadAddContext (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addCtx :: Name -> Dom Type -> PureConversionT m a -> PureConversionT m a

addLetBinding' :: Name -> Term -> Dom Type -> PureConversionT m a -> PureConversionT m a

updateContext :: Substitution -> (Context -> Context) -> PureConversionT m a -> PureConversionT m a

withFreshName :: Range -> ArgName -> (Name -> PureConversionT m a) -> PureConversionT m a

MonadAddContext m => MonadAddContext (BlockT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> BlockT m a -> BlockT m a

addLetBinding' :: Name -> Term -> Dom Type -> BlockT m a -> BlockT m a

updateContext :: Substitution -> (Context -> Context) -> BlockT m a -> BlockT m a

withFreshName :: Range -> ArgName -> (Name -> BlockT m a) -> BlockT m a

MonadAddContext m => MonadAddContext (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a

addLetBinding' :: Name -> Term -> Dom Type -> NamesT m a -> NamesT m a

updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a

withFreshName :: Range -> ArgName -> (Name -> NamesT m a) -> NamesT m a

MonadAddContext m => MonadAddContext (ListT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ListT m a -> ListT m a

addLetBinding' :: Name -> Term -> Dom Type -> ListT m a -> ListT m a

updateContext :: Substitution -> (Context -> Context) -> ListT m a -> ListT m a

withFreshName :: Range -> ArgName -> (Name -> ListT m a) -> ListT m a

MonadAddContext m => MonadAddContext (MaybeT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> MaybeT m a -> MaybeT m a

addLetBinding' :: Name -> Term -> Dom Type -> MaybeT m a -> MaybeT m a

updateContext :: Substitution -> (Context -> Context) -> MaybeT m a -> MaybeT m a

withFreshName :: Range -> ArgName -> (Name -> MaybeT m a) -> MaybeT m a

MonadAddContext m => MonadAddContext (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ExceptT e m a -> ExceptT e m a

addLetBinding' :: Name -> Term -> Dom Type -> ExceptT e m a -> ExceptT e m a

updateContext :: Substitution -> (Context -> Context) -> ExceptT e m a -> ExceptT e m a

withFreshName :: Range -> ArgName -> (Name -> ExceptT e m a) -> ExceptT e m a

MonadAddContext m => MonadAddContext (IdentityT m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> IdentityT m a -> IdentityT m a

addLetBinding' :: Name -> Term -> Dom Type -> IdentityT m a -> IdentityT m a

updateContext :: Substitution -> (Context -> Context) -> IdentityT m a -> IdentityT m a

withFreshName :: Range -> ArgName -> (Name -> IdentityT m a) -> IdentityT m a

MonadAddContext m => MonadAddContext (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ReaderT r m a -> ReaderT r m a

addLetBinding' :: Name -> Term -> Dom Type -> ReaderT r m a -> ReaderT r m a

updateContext :: Substitution -> (Context -> Context) -> ReaderT r m a -> ReaderT r m a

withFreshName :: Range -> ArgName -> (Name -> ReaderT r m a) -> ReaderT r m a

MonadAddContext m => MonadAddContext (StateT r m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> StateT r m a -> StateT r m a

addLetBinding' :: Name -> Term -> Dom Type -> StateT r m a -> StateT r m a

updateContext :: Substitution -> (Context -> Context) -> StateT r m a -> StateT r m a

withFreshName :: Range -> ArgName -> (Name -> StateT r m a) -> StateT r m a

(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m)

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> WriterT w m a -> WriterT w m a

addLetBinding' :: Name -> Term -> Dom Type -> WriterT w m a -> WriterT w m a

updateContext :: Substitution -> (Context -> Context) -> WriterT w m a -> WriterT w m a

withFreshName :: Range -> ArgName -> (Name -> WriterT w m a) -> WriterT w m a

defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a

Default implementation of addCtx in terms of updateContext

withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a

withShadowingNameTCM :: Name -> TCM b -> TCM b

Run the given TCM action, and register the given variable as being shadowed by all the names with the same root that are added to the context during this TCM action.

addRecordNameContext :: (MonadAddContext m, MonadFresh NameId m) => Dom Type -> m b -> m b

class AddContext b where

Various specializations of addCtx.

Methods

addContext :: MonadAddContext m => b -> m a -> m a

contextSize :: b -> Nat

Instances

AddContext Name

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Name -> m a -> m a

contextSize :: Name -> Nat

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a

contextSize :: Telescope -> Nat

AddContext String

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => String -> m a -> m a

contextSize :: String -> Nat

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a

contextSize :: Dom Type -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a

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

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a

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

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a

contextSize :: KeepNames Telescope -> Nat

AddContext a => AddContext [a]

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => [a] -> m a0 -> m a0

contextSize :: [a] -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a

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

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a

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

AddContext (List1 Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a

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

AddContext (List1 (Arg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a

contextSize :: (List1 (Arg Name), Type) -> Nat

AddContext (List1 (NamedArg Name), Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a

contextSize :: (List1 (NamedArg Name), Type) -> Nat

AddContext (List1 (WithHiding Name), Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a

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

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a

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

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a

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

AddContext ([Arg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a

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

AddContext ([NamedArg Name], Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a

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

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a

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

newtype KeepNames a

Wrapper to tell addContext not to mark names as TypeError. 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 :: MonadAddContext m => KeepNames Telescope -> m a -> m a

contextSize :: KeepNames Telescope -> Nat

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a

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

underAbstraction :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b

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

underAbstraction' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b

underAbstractionAbs :: (Subst a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b

Go under an abstraction, treating NoAbs as Abs.

underAbstractionAbs' :: (Subst a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b

underAbstraction_ :: (Subst a, MonadAddContext m) => Abs a -> (a -> m b) -> m b

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

mapAbstraction :: (Subst a, Subst b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)

Map a monadic function on the thing under the abstraction, adding the abstracted variable to the context.

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

defaultAddLetBinding' :: (ReadTCState m, MonadTCEnv m) => Name -> Term -> Dom Type -> m a -> m a

Add a let bound variable

addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m 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 (Maybe (Dom (Name, Type)))

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

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

domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)

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

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

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

getVarInfo :: (MonadFail m, 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.