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 and backend information.

localTCState :: TCM a -> TCM a

Restore TCState after performing subcomputation.

In contrast to localState, the Benchmark info from the subcomputation is saved.

localTCStateSaving :: TCM a -> TCM (a, TCState)

Same as localTCState but also returns the state in which we were just before reverting it.

localTCStateSavingWarnings :: TCM a -> TCM a

Same as localTCState but keep all warnings.

data SpeculateResult

Constructors

SpeculateAbort

SpeculateCommit

speculateTCState :: TCM (a, SpeculateResult) -> TCM a

Allow rolling back the state changes of a TCM computation.

speculateTCState_ :: TCM SpeculateResult -> TCM ()

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

A fresh TCM instance.

The computation is run in a fresh state, with the exception that the persistent state is preserved. If the computation changes the state, then these changes are ignored, except for changes to the persistent state. (Changes to the persistent state are also ignored if errors other than type errors or IO exceptions are encountered.)

Lens for persistent states and its fields

lensPersistentState :: Lens' TCState PersistentTCState

updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState

modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()

lensAccumStatisticsP :: Lens' PersistentTCState Statistics

Lens for stAccumStatistics.

lensAccumStatistics :: Lens' TCState Statistics

Scope

getScope :: ReadTCState m => m ScopeInfo

Get the current scope.

setScope :: ScopeInfo -> TCM ()

Set the current scope.

modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()

Modify the current scope without updating the inverse maps.

modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()

Modify the current scope.

useScope :: ReadTCState m => Lens' ScopeInfo a -> m a

Get a part of the current scope.

locallyScope :: ReadTCState m => Lens' ScopeInfo a -> (a -> a) -> m b -> m b

Run a computation in a modified scope.

withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)

Run a computation in a local scope.

withScope_ :: ReadTCState m => ScopeInfo -> m a -> m 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.

notInScopeError :: QName -> TCM a

Scope error.

notInScopeWarning :: QName -> TCM ()

printScope :: String -> Int -> String -> TCM ()

Debug print the scope.

Signature

Lens for stSignature and stImports

modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()

modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()

getSignature :: ReadTCState m => m Signature

modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()

Update a possibly imported definition. Warning: changes made to imported definitions (during type checking) will not persist outside the current module. This function is currently used to update the compiled representation of a function during compilation.

setSignature :: MonadTCState m => Signature -> m ()

withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a

Run some computation in a different signature, restore original signature.

Modifiers for rewrite rules

addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature

setMatchableSymbols :: QName -> [QName] -> Signature -> Signature

modify methods for the signature

modifyRecEta :: MonadTCState m => QName -> (EtaEquality -> EtaEquality) -> m ()

Modifiers for parts of the signature

lookupDefinition :: QName -> Signature -> Maybe Definition

updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature

updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature

updateTheDef :: (Defn -> Defn) -> Definition -> Definition

updateDefType :: (Type -> Type) -> Definition -> Definition

updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition

updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition

updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> Definition -> Definition

addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition

updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn

updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn

updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn

updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition

updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition

Top level module

topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName

Tries to convert a raw top-level module name to a top-level module name.

setTopLevelModule :: TopLevelModuleName -> TCM ()

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

currentTopLevelModule :: (MonadTCEnv m, ReadTCState m) => m (Maybe TopLevelModuleName)

The name of the current top-level module, if any.

withTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a

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

currentModuleNameHash :: ReadTCState m => m ModuleNameHash

Foreign code

addForeignCode :: BackendName -> String -> TCM ()

Interaction output callback

getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback

appInteractionOutputCallback :: Response -> TCM ()

setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()

Pattern synonyms

getPatternSyns :: ReadTCState m => m PatternSynDefns

setPatternSyns :: PatternSynDefns -> TCM ()

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

Lens for stPatternSyns.

getPatternSynImports :: ReadTCState m => m PatternSynDefns

getAllPatternSyns :: ReadTCState m => m PatternSynDefns

Get both local and imported pattern synonyms

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn

lookupSinglePatternSyn :: 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 TCMT.

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

Lens modify for Benchmark.

Instance definitions

updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState

Lens for stInstanceDefs.

modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()

getAllInstanceDefs :: TCM TempInstanceTable

getAnonInstanceDefs :: TCM (Set QName)

clearUnknownInstance :: QName -> TCM ()

Remove an instance from the set of unresolved instances.

addUnknownInstance :: QName -> TCM ()

Add an instance whose type is still unresolved.