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 ()Source
Resets the type checking state. The persistent command line options are preserved.
withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)Source
Run a computation in a local scope.
withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm aSource
Same as withScope, but discard the scope from the computation.
localScope :: MonadTCM tcm => tcm a -> tcm aSource
Discard any changes to the scope by a computation.
setTopLevelModule :: MonadTCM tcm => QName -> tcm ()Source
Set the top-level module. This affects the global module id of freshly generated names.
withTopLevelModule :: MonadTCM tcm => QName -> tcm a -> tcm aSource
Use a different top-level module for a computation. Used when generating names for imported modules.
addHaskellImport :: MonadTCM tcm => String -> tcm ()Source
Tell the compiler to import the given Haskell module.
getHaskellImports :: MonadTCM tcm => tcm (Set String)Source
Get the Haskell imports.