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

Safe Haskell | None

Agda.TypeChecking.Monad.State

Synopsis

- resetState :: TCM ()
- resetAllState :: TCM ()
- setScope :: ScopeInfo -> TCM ()
- getScope :: TCM ScopeInfo
- getPatternSyns :: TCM PatternSynDefns
- setPatternSyns :: PatternSynDefns -> TCM ()
- modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
- getPatternSynImports :: TCM PatternSynDefns
- lookupPatternSyn :: QName -> TCM PatternSynDefn
- setExtLambdaTele :: Map QName (Int, Int) -> TCM ()
- getExtLambdaTele :: TCM (Map QName (Int, Int))
- addExtLambdaTele :: QName -> (Int, Int) -> TCM ()
- modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
- withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)
- withScope_ :: ScopeInfo -> TCM a -> TCM a
- localScope :: TCM a -> TCM a
- setTopLevelModule :: QName -> TCM ()
- withTopLevelModule :: QName -> TCM a -> TCM a
- addHaskellImport :: String -> TCM ()
- getHaskellImports :: TCM (Set String)

# Documentation

resetState :: TCM ()

Resets the non-persistent part of the type checking state.

resetAllState :: TCM ()

Resets all of the type checking state.

setScope :: ScopeInfo -> TCM ()

Set the current scope.

getScope :: TCM ScopeInfo

Get the current scope.

getPatternSyns :: TCM PatternSynDefns

setPatternSyns :: PatternSynDefns -> TCM ()

modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()

getPatternSynImports :: TCM PatternSynDefns

lookupPatternSyn :: QName -> TCM PatternSynDefn

setExtLambdaTele :: Map QName (Int, Int) -> TCM ()

Sets stExtLambdaTele .

getExtLambdaTele :: TCM (Map QName (Int, Int))

Get stExtLambdaTele.

addExtLambdaTele :: QName -> (Int, Int) -> TCM ()

modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()

Modify the current scope.

withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)

Run a computation in a local scope.

withScope_ :: ScopeInfo -> TCM a -> TCM a

Same as `withScope`, but discard the scope from the computation.

localScope :: TCM a -> TCM a

Discard any changes to the scope by a computation.

setTopLevelModule :: QName -> TCM ()

Set the top-level module. This affects the global module id of freshly generated names.

withTopLevelModule :: QName -> TCM a -> TCM a

Use a different top-level module for a computation. Used when generating names for imported modules.

addHaskellImport :: String -> TCM ()

Tell the compiler to import the given Haskell module.

getHaskellImports :: TCM (Set String)

Get the Haskell imports.