Agda.TypeChecking.Monad.State

Lenses for TCState and more.

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

getScope :: TCM ScopeInfo

Get the current scope.

setScope :: ScopeInfo -> TCM ()

Set the current scope.

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.

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

getInteractionOutputCallback :: TCM InteractionOutputCallback

appInteractionOutputCallback :: Response -> TCM ()

setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()

Pattern synonyms

getPatternSyns :: TCM PatternSynDefns

setPatternSyns :: PatternSynDefns -> TCM ()

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

Lens for stPatternSyns.

getPatternSynImports :: TCM PatternSynDefns

lookupPatternSyn :: QName -> TCM PatternSynDefn

Benchmark

theBenchmark :: TCState -> Benchmark

Lens getter for Benchmark from TCState.

updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState

Lens map for Benchmark.

getBenchmark :: TCM Benchmark

Lens getter for Benchmark from TCM.

modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()

Lens modify for Benchmark.

freshTCM :: TCM a -> TCM (Either TCErr a)

Run a fresh instance of the TCM (with initial state). Benchmark info is preserved.