Modify a Context in a computation. Warning: does not update
the checkpoints. Use updateContext instead.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Context
Contents
Synopsis
- value unsafeModifyContext
- value modifyContextInfo
- value inTopContext
- value unsafeInTopContext
- value unsafeEscapeContext
- value escapeContext
- value checkpoint
- value checkpointSubstitution
- value checkpointSubstitution'
- value getModuleParameterSub
- class MonadAddContext
- value defaultAddCtx
- value withFreshName_
- value withShadowingNameTCM
- value addRecordNameContext
- class AddContext
- newtype KeepNames
- value underAbstraction
- value underAbstraction'
- value underAbstractionAbs
- value underAbstractionAbs'
- value underAbstraction_
- value mapAbstraction
- value mapAbstraction_
- value getLetBindings
- value defaultAddLetBinding'
- value addLetBinding
- value removeLetBinding
- value removeLetBindingsFrom
- value getContext
- value getContextSize
- value getContextVars
- value getContextVars'
- value contextVars
- value contextVars'
- value getContextArgs
- value contextArgs
- value getContextTerms
- value contextTerms
- value getContextTelescope
- value contextToTel
- value getContextNames
- value getContextNames'
- value contextNames
- value contextNames'
- value lookupBV_
- value lookupBV'
- value lookupBV
- value ctxEntryName
- value ctxEntryDom
- value ctxEntryType
- value domOfBV
- value typeOfBV
- value nameOfBV'
- value nameOfBV
- value getVarInfo
- PackageAgda-2.8.0.2
- Exports56
- LanguageHaskell2010
- LicenceMIT
- SourceContext.hs
Modifying the context
Modify the Dom part of context entries.
Change to top (=empty) context. Resets the checkpoints.
Change to top (=empty) context, but don't update the checkpoints. Totally not safe!
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.
Delete the last n bindings from the context. Any occurrences of
these variables are replaced with the given err.
Manipulating checkpoints --
Add a new checkpoint. Do not use directly!
Get the substitution from the context at a given checkpoint to the current context.
Get the substitution from the context at a given checkpoint to the current context.
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
Methods
addCtx :: Name -> Dom Type -> m a -> m aaddCtx x arg contadd a variable to the context.Chooses an unused Name.
Warning: Does not update module parameter substitution!
addLetBinding' :: Origin -> Name -> Term -> Dom Type -> m a -> m aAdd a let bound variable to the context
updateContext :: Substitution -> (Context -> Context) -> m a -> m aUpdate the context. Requires a substitution that transports things living in the old context to the new.
withFreshName :: Range -> ArgName -> (Name -> m a) -> m a
Instances16MonadAddContext, …
MonadAddContext TerMDefined in Agda-2.8.0.2 · Agda.Termination.MonadMonadAddContext ReduceMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce.Monad · orphanMonadAddContext TCMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext NLMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatchMonadAddContext m => MonadAddContext (AbsToConT m)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcreteMonadAddContext m => MonadAddContext (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadAddContext m => MonadAddContext (BlockT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.NamesMonadAddContext m => MonadAddContext (ListT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (MaybeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (IdentityT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextMonadAddContext m => MonadAddContext (StateT r m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
Default implementation of addCtx in terms of updateContext
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.
Various specializations of addCtx.
Methods
addContext :: MonadAddContext m => b -> m a -> m acontextSize :: b -> Nat
Instances21AddContext, …
AddContext NameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext TelescopeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext StringDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (Dom (Name, Type))Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (Dom (String, Type))Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (KeepNames Telescope)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext a => AddContext [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (Name, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (KeepNames String, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (List1 Name, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (List1 (Arg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (List1 (WithHiding Name), Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (String, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (Text, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext ([Name], Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext ([Arg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext ([WithHiding Name], Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
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
Instances2AddContext
AddContext (KeepNames Telescope)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextAddContext (KeepNames String, Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
Go under an abstraction. Do not extend context in case of NoAbs.
Go under an abstract without worrying about the type to add to the context.
Map a monadic function on the thing under the abstraction, adding the abstracted variable to the context.
Add a let bound variable
Add a let bound variable
Remove a let bound variable.
Remove a let bound variable and all let bindings introduced after it. For instance before printing its body to avoid folding the binding itself, or using bindings defined later. Relies on the invariant that names introduced later are sorted after earlier names.
Querying the context
Get the current context.
Get the size of the current context.
Generate [var (n - 1), ..., var 0] for all bound variables in the context.
Generate [var (n - 1), ..., var 0] for all declarations in the context.
Get the current context as a Telescope.
Get the names of all declarations in the context.
get type of bound variable (i.e. deBruijn index)
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.