| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Context
Contents
- modifyContextEntry :: (Dom (Name, Type) -> Dom (Name, Type)) -> ContextEntry -> ContextEntry
- modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context
- modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a
- mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry
- inTopContext :: MonadTCM tcm => tcm a -> tcm a
- escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
- withModuleParameters :: ModuleParamDict -> TCM a -> TCM a
- updateModuleParameters :: MonadTCM tcm => Substitution -> tcm a -> tcm a
- weakenModuleParameters :: MonadTCM tcm => Nat -> tcm a -> tcm a
- getModuleParameterSub :: MonadTCM tcm => ModuleName -> tcm Substitution
- addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a
- unshadowName :: MonadTCM tcm => Name -> tcm Name
- class AddContext b where
- addContext' :: (MonadTCM tcm, AddContext b) => b -> tcm a -> tcm a
- dummyDom :: Dom Type
- underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b
- addLetBinding :: MonadTCM tcm => ArgInfo -> Name -> Term -> Type -> tcm a -> tcm a
- getContext :: MonadReader TCEnv m => m [Dom (Name, Type)]
- getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat
- getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args
- getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term]
- getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope
- getContextId :: MonadReader TCEnv m => m [CtxId]
- getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name]
- lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type))
- 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)
Modifying the context
modifyContextEntry :: (Dom (Name, Type) -> Dom (Name, Type)) -> ContextEntry -> ContextEntry Source #
Modify the ctxEntry field of a ContextEntry.
modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context Source #
Modify all ContextEntrys.
modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a Source #
Modify a Context in a computation.
mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry Source #
inTopContext :: MonadTCM tcm => tcm a -> tcm a Source #
Change to top (=empty) context.
TODO: currently, this makes the ModuleParamDict ill-formed!
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a Source #
Delete the last n bindings from the context.
TODO: currently, this makes the ModuleParamDict ill-formed!
Manipulating module parameters --
withModuleParameters :: ModuleParamDict -> TCM a -> TCM a Source #
Locally set module parameters for a computation.
updateModuleParameters :: MonadTCM tcm => Substitution -> tcm a -> tcm a Source #
Apply a substitution to all module parameters.
weakenModuleParameters :: MonadTCM tcm => Nat -> tcm a -> tcm a Source #
Since the ModuleParamDict is relative to the current context,
this function should be called everytime the context is extended.
getModuleParameterSub :: MonadTCM tcm => ModuleName -> tcm Substitution Source #
Get substitution Γ ⊢ ρ : Γm where Γ is the current context
and Γm is the module parameter telescope of module m.
In case the current ModuleParamDict does not know 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 :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a Source #
addCtx x arg cont add a variable to the context.
Chooses an unused Name.
Warning: Does not update module parameter substitution!
unshadowName :: MonadTCM tcm => Name -> tcm Name Source #
Pick a concrete name that doesn't shadow anything in the context.
class AddContext b where Source #
Various specializations of addCtx.
Minimal complete definition
Instances
| AddContext String Source # | |
| AddContext Name Source # | |
| AddContext Telescope Source # | |
| AddContext a => AddContext [a] Source # | |
| AddContext (Dom (String, Type)) Source # | |
| AddContext (Dom (Name, Type)) Source # | |
| AddContext (Dom Type) Source # | |
| AddContext ([WithHiding Name], Dom Type) Source # | |
| AddContext ([Name], Dom Type) Source # | |
| AddContext (String, Dom Type) Source # | |
| AddContext (Name, Dom Type) Source # | |
addContext' :: (MonadTCM tcm, AddContext b) => b -> tcm a -> tcm a Source #
Since the module parameter substitution is relative to the current context, we need to weaken it when we extend the context. This function takes care of that.
underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b Source #
Go under an abstraction.
underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b Source #
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 Source #
Add a let bound variable.
Querying the context
getContext :: MonadReader TCEnv m => m [Dom (Name, Type)] Source #
Get the current context.
getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat Source #
Get the size of the current context.
getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args Source #
Generate [var (n - 1), ..., var 0] for all declarations in the context.
getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term] Source #
Generate [var (n - 1), ..., var 0] for all declarations in the context.
getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope Source #
Get the current context as a Telescope.
getContextId :: MonadReader TCEnv m => m [CtxId] Source #
Check if we are in a compatible context, i.e. an extension of the given context.
getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name] Source #
Get the names of all declarations in the context.
lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type)) Source #
get type of bound variable (i.e. deBruijn index)
typeOfBV' :: (Applicative m, MonadReader TCEnv m) => Nat -> m (Dom Type) Source #
typeOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Type Source #
nameOfBV :: (Applicative m, MonadReader TCEnv m) => Nat -> m Name Source #
getVarInfo :: MonadReader TCEnv 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.