Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Monad.State

Synopsis

- 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.

setScope :: MonadTCM tcm => ScopeInfo -> tcm ()

Set the current scope.

getScope :: MonadTCM tcm => tcm ScopeInfo

Get the current scope.

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.