Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Context

Synopsis

Modifying the context

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

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 Source #

Modify the Dom' part of context entries.

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

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

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

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

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

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 Source #

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 Source #

Add a new checkpoint. Do not use directly!

checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution Source #

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

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

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

getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution) Source #

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 Source #

Minimal complete definition

Nothing

Methods

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

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 Source #

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

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 Source #

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

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 Source #

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

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

Instances

Instances details
MonadAddContext TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadAddContext m => MonadAddContext (BlockT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

MonadAddContext m => MonadAddContext (StateT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

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

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

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

Default implementation of addCtx in terms of updateContext

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

withShadowingNameTCM :: Name -> TCM b -> TCM b Source #

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.

class AddContext b where Source #

Various specializations of addCtx.

Methods

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

contextSize :: b -> Nat Source #

Instances

Instances details
AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Name -> Nat Source #

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat Source #

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext a => AddContext [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: [a] -> Nat Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (Arg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (List1 (NamedArg Name), Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (List1 (WithHiding Name), Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

newtype KeepNames a Source #

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 

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

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 Source #

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

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 Source #

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

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) Source #

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

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

Add a let bound variable

addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m a Source #

Add a let bound variable

Querying the context

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

Get the current context.

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

Get the size of the current context.

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

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

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

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

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

Get the current context as a Telescope.

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

Get the names of all declarations in the context.

lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type))) Source #

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

getVarInfo :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type) Source #

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.