Resets the non-persistent part of the type checking state.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.State
Lenses for TCState and more.
Contents
- Lens for persistent states and its fields
- Scope
- Signature
- Lens for stSignature and stImports
- Modifiers for rewrite rules
- modify methods for the signature
- Modifiers for parts of the signature
- File identification
- Top level module
- Backends and foreign code
- Interaction output callback
- Pattern synonyms
- Instance definitions
Synopsis
- value resetState
- value resetAllState
- value putTCPreservingSession
- value localTCState
- value localTCStateSaving
- value localTCStateSavingWarnings
- value freshTCM
- value updatePersistentState
- value modifyPersistentState
- value lensAccumStatisticsP
- value lensAccumStatistics
- value getScope
- value setScope
- value modifyScope_
- value modifyScope
- value useScope
- value locallyScope
- value withScope
- value withScope_
- value localScope
- value notInScopeError
- value notInScopeWarning
- value printScope
- value modifySignature
- value modifyImportedSignature
- value getSignature
- value modifyGlobalDefinition
- value setSignature
- value withSignature
- value addRewriteRulesFor
- value setMatchableSymbols
- value modifyRecEta
- value lookupDefinition
- value updateDefinitions
- value updateDefinition
- value updateTheDef
- value updateDefType
- value updateDefArgOccurrences
- value updateDefPolarity
- value updateDefCompiledRep
- value addCompilerPragma
- value updateFunClauses
- value updateCovering
- value updateCompiledClauses
- value updateDefCopatternLHS
- value updateDefBlocked
- value registerFileIdWithBuiltin
- value isBuiltinModule
- value isBuiltinModuleWithSafePostulates
- value isPrimitiveModule
- value topLevelModuleName
- value setTopLevelModule
- value currentTopLevelModule
- value withTopLevelModule
- value currentModuleNameHash
- value lookupBackend
- value activeBackend
- value activeBackendMayEraseType
- value addForeignCode
- value getInteractionOutputCallback
- value appInteractionOutputCallback
- value setInteractionOutputCallback
- value getPatternSyns
- value setPatternSyns
- value modifyPatternSyns
- value getPatternSynImports
- value getAllPatternSyns
- value lookupPatternSyn
- value lookupSinglePatternSyn
- value updateInstanceDefs
- value modifyInstanceDefs
- value getAllInstanceDefs
- value getAnonInstanceDefs
- value clearUnknownInstance
- value addUnknownInstance
- PackageAgda-2.8.0.2
- Exports75
- LanguageHaskell2010
- LicenceMIT
- SourceState.hs
Resets all of the type checking state.
Keep only the session state (backend information, Benchmark, file ids).
Overwrite the TCState, but not the SessionTCState part.
Restore TCState after performing subcomputation.
In contrast to localState, the SessionTCState from the subcomputation is saved.
Same as localTCState but also returns the state in which we were just before reverting it.
Same as localTCState but keep all warnings.
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
Lens for stAccumStatistics.
Scope
Get the current scope.
Set the current scope.
Modify the current scope without updating the inverse maps.
Modify the current scope.
Get a part of the current scope.
Run a computation in a modified scope.
Run a computation in a local scope.
Same as withScope, but discard the scope from the computation.
Discard any changes to the scope by a computation.
Scope error.
Debug print the scope.
Signature
Lens for stSignature and stImports
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.
Run some computation in a different signature, restore original signature.
Modifiers for rewrite rules
modify methods for the signature
Modifiers for parts of the signature
File identification
Translate an absolute path to a file id, and register a new file id if the path has not seen before. Also register whether the path belongs to one of Agda's builtin modules.
Does the given FileId belong to one of Agda's builtin modules?
Does the given FileId belong to one of Agda's builtin modules that only uses safe postulates?
Implies isJust . isBuiltinModule.
Does the given FileId belong to one of Agda's magical primitive modules?
Implies isBuiltinModuleWithSafePostulates.
Top level module
Tries to convert a raw top-level module name to a top-level module name.
Set the top-level module. This affects the global module id of freshly generated names.
The name of the current top-level module, if any.
Use a different top-level module for a computation. Used when generating names for imported modules.
Backends and foreign code
Look for a backend of the given name.
Get the currently active backend (if any).
Ask the active backend whether a type may be erased. See issue #3732.
Interaction output callback
Pattern synonyms
Lens for stPatternSyns.
Get both local and imported pattern synonyms
Instance definitions
Lens for stInstanceDefs.
Remove an instance from the set of unresolved instances.
Add an instance whose type is still unresolved.
Orphan instances
1 instanceMonadIO m => MonadFileId (TCMT m)