| 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, MonadDebug tcm) => Substitution -> tcm a -> tcm a
- weakenModuleParameters :: (MonadTCM tcm, MonadDebug tcm) => Nat -> tcm a -> tcm a
- getModuleParameterSub :: (Functor m, ReadTCState m) => ModuleName -> m Substitution
- addCtx :: MonadTCM tcm => Name -> Dom Type -> tcm a -> tcm a
- unshadowName :: MonadTCM tcm => Name -> tcm Name
- class AddContext b where
- addContext' :: (MonadTCM tcm, MonadDebug tcm, AddContext b) => b -> tcm a -> tcm a
- newtype KeepNames a = KeepNames 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, AddContext (name, Dom Type)) => (String -> name) -> 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 #
Modify the ctxEntry field of a ContextEntry.
modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context #
Modify all ContextEntrys.
modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm a #
Modify a Context in a computation.
mkContextEntry :: MonadTCM tcm => Dom (Name, Type) -> tcm ContextEntry #
inTopContext :: MonadTCM tcm => tcm a -> tcm a #
Change to top (=empty) context.
TODO: currently, this makes the ModuleParamDict ill-formed!
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a #
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 #
Locally set module parameters for a computation.
updateModuleParameters :: (MonadTCM tcm, MonadDebug tcm) => Substitution -> tcm a -> tcm a #
Apply a substitution to all module parameters.
weakenModuleParameters :: (MonadTCM tcm, MonadDebug tcm) => Nat -> tcm a -> tcm a #
Since the ModuleParamDict is relative to the current context,
this function should be called everytime the context is extended.
getModuleParameterSub :: (Functor 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 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 #
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 #
Pick a concrete name that doesn't shadow anything in the context.
class AddContext b where #
Various specializations of addCtx.
Minimal complete definition
Instances
| AddContext String # | |
| AddContext Name # | |
| AddContext Telescope # | |
| AddContext a => AddContext [a] # | |
| AddContext (Dom (String, Type)) # | |
| AddContext (Dom (Name, Type)) # | |
| AddContext (Dom Type) # | |
| AddContext (KeepNames Telescope) # | |
| AddContext ([WithHiding Name], Dom Type) # | |
| AddContext ([Name], Dom Type) # | |
| AddContext (String, Dom Type) # | |
| AddContext (Name, Dom Type) # | |
| AddContext (KeepNames String, Dom Type) # | |
addContext' :: (MonadTCM tcm, MonadDebug tcm, AddContext b) => b -> tcm a -> tcm a #
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.
Wrapper to tell addContext not to unshadowNames. Used when adding a
user-provided, but already type checked, telescope to the context.
Constructors
| KeepNames a |
Instances
underAbstraction :: (Subst t a, MonadTCM tcm) => Dom Type -> Abs a -> (a -> tcm b) -> tcm b #
Go under an abstraction.
underAbstraction' :: (Subst t a, MonadTCM tcm, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b #
underAbstraction_ :: (Subst t a, MonadTCM tcm) => Abs a -> (a -> tcm b) -> tcm b #
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 #
Add a let bound variable.
Querying the context
getContext :: MonadReader TCEnv m => m [Dom (Name, Type)] #
Get the current context.
getContextSize :: (Applicative m, MonadReader TCEnv m) => m Nat #
Get the size of the current context.
getContextArgs :: (Applicative m, MonadReader TCEnv m) => m Args #
Generate [var (n - 1), ..., var 0] for all declarations in the context.
getContextTerms :: (Applicative m, MonadReader TCEnv m) => m [Term] #
Generate [var (n - 1), ..., var 0] for all declarations in the context.
getContextTelescope :: (Applicative m, MonadReader TCEnv m) => m Telescope #
Get the current context as a Telescope.
getContextId :: MonadReader TCEnv m => m [CtxId] #
Check if we are in a compatible context, i.e. an extension of the given context.
getContextNames :: (Applicative m, MonadReader TCEnv m) => m [Name] #
Get the names of all declarations in the context.
lookupBV :: MonadReader TCEnv m => Nat -> m (Dom (Name, Type)) #
get type of bound variable (i.e. deBruijn index)
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) #
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.