Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.TypeChecking.Monad.State
Contents
Description
Lenses for TCState
and more.
- resetState :: TCM ()
- resetAllState :: TCM ()
- localTCState :: TCM a -> TCM a
- updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
- modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
- getScope :: TCM ScopeInfo
- setScope :: ScopeInfo -> TCM ()
- modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
- withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)
- withScope_ :: ScopeInfo -> TCM a -> TCM a
- localScope :: TCM a -> TCM a
- notInScope :: QName -> TCM a
- printScope :: String -> Int -> String -> TCM ()
- setTopLevelModule :: QName -> TCM ()
- withTopLevelModule :: QName -> TCM a -> TCM a
- addHaskellImport :: String -> TCM ()
- getHaskellImports :: TCM (Set String)
- getInteractionOutputCallback :: TCM InteractionOutputCallback
- appInteractionOutputCallback :: Response -> TCM ()
- setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
- getPatternSyns :: TCM PatternSynDefns
- setPatternSyns :: PatternSynDefns -> TCM ()
- modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
- getPatternSynImports :: TCM PatternSynDefns
- lookupPatternSyn :: QName -> TCM PatternSynDefn
- theBenchmark :: TCState -> Benchmark
- updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
- getBenchmark :: TCM Benchmark
- modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
- freshTCM :: TCM a -> TCM (Either TCErr a)
Documentation
resetState :: TCM ()
Resets the non-persistent part of the type checking state.
resetAllState :: TCM ()
Resets all of the type checking state.
Keep only Benchmark
information.
localTCState :: TCM a -> TCM a
Restore TCState
after performing subcomputation.
In contrast to localState
, the Benchmark
info from the subcomputation is saved.
Lens for persistent state
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
Scope
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
Modify the current 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.
notInScope :: QName -> TCM a
Scope error.
printScope :: String -> Int -> String -> TCM ()
Debug print the scope.
Top level module
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.
Haskell imports
addHaskellImport :: String -> TCM ()
Tell the compiler to import the given Haskell module.
getHaskellImports :: TCM (Set String)
Get the Haskell imports.
Interaction output callback
appInteractionOutputCallback :: Response -> TCM ()
Pattern synonyms
setPatternSyns :: PatternSynDefns -> TCM ()
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
Lens for stPatternSyns
.
Benchmark
theBenchmark :: TCState -> Benchmark
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
Lens modify for Benchmark
.