Agda.TypeChecking.Monad.State
- resetState :: MonadTCM tcm => tcm ()
- setScope :: MonadTCM tcm => ScopeInfo -> tcm ()
- getScope :: MonadTCM tcm => tcm ScopeInfo
- modifyScope :: MonadTCM tcm => (ScopeInfo -> ScopeInfo) -> tcm ()
- withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)
- withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm a
- localScope :: MonadTCM tcm => tcm a -> tcm a
- setTopLevelModule :: MonadTCM tcm => QName -> tcm ()
- withTopLevelModule :: MonadTCM tcm => QName -> tcm a -> tcm a
- addHaskellImport :: MonadTCM tcm => String -> tcm ()
- getHaskellImports :: MonadTCM tcm => tcm (Set String)
Documentation
resetState :: MonadTCM tcm => tcm ()
Resets the type checking state. The persistent command line options are preserved.
modifyScope :: MonadTCM tcm => (ScopeInfo -> ScopeInfo) -> tcm ()
Modify the current scope.
withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)
Run a computation in a local scope.
withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm a
Same as withScope
, but discard the scope from the computation.
localScope :: MonadTCM tcm => tcm a -> tcm a
Discard any changes to the scope by a computation.
setTopLevelModule :: MonadTCM tcm => QName -> tcm ()
Set the top-level module. This affects the global module id of freshly generated names.
withTopLevelModule :: MonadTCM tcm => QName -> tcm a -> tcm a
Use a different top-level module for a computation. Used when generating names for imported modules.
addHaskellImport :: MonadTCM tcm => String -> tcm ()
Tell the compiler to import the given Haskell module.
getHaskellImports :: MonadTCM tcm => tcm (Set String)
Get the Haskell imports.