Safe Haskell | None |
---|---|
Language | Haskell2010 |
- 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 Source #
Modify the ctxEntry
field of a ContextEntry
.
modifyContextEntries :: (Dom (Name, Type) -> Dom (Name, Type)) -> Context -> Context Source #
Modify all ContextEntry
s.
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, MonadDebug tcm) => Substitution -> tcm a -> tcm a Source #
Apply a substitution to all module parameters.
weakenModuleParameters :: (MonadTCM tcm, MonadDebug 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 :: (Functor m, ReadTCState m) => ModuleName -> m 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
.
addContext :: MonadTCM tcm => b -> tcm a -> tcm a Source #
contextSize :: b -> Nat Source #
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 (KeepNames Telescope) Source # | |
AddContext ([WithHiding Name], Dom Type) Source # | |
AddContext ([Name], Dom Type) Source # | |
AddContext (String, Dom Type) Source # | |
AddContext (Name, Dom Type) Source # | |
AddContext (KeepNames String, Dom Type) Source # | |
addContext' :: (MonadTCM tcm, MonadDebug 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.
Wrapper to tell addContext
not to unshadowName
s. Used when adding a
user-provided, but already type checked, telescope to the context.
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, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> tcm b) -> tcm b Source #
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.