Agda.TypeChecking.Monad.State · Agda-2.8.0.2

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

4 declarations

valueupdatePersistentState

:: PersistentTCState -> PersistentTCState
-> TCState
-> TCState

#

valuemodifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()

#

valuelensAccumStatisticsP :: Lens' PersistentTCState Statistics

#

Lens for stAccumStatistics.

valuelensAccumStatistics :: Lens' TCState Statistics

#

Scope

12 declarations

valuegetScope :: ReadTCState m => m ScopeInfo

#

Get the current scope.

valuesetScope :: ScopeInfo -> TCM ()

#

Set the current scope.

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

#

Modify the current scope without updating the inverse maps.

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

#

Modify the current scope.

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

#

Get a part of the current scope.

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

#

Run a computation in a modified scope.

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

#

Run a computation in a local scope.

valuewithScope_ :: ReadTCState m => ScopeInfo -> m a -> m a

#

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

valuelocalScope :: TCM a -> TCM a

#

Discard any changes to the scope by a computation.

valuenotInScopeError :: QName -> TCM a

#

Scope error.

valuenotInScopeWarning :: QName -> TCM ()

#

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

#

Debug print the scope.

Signature

0 declarations

Lens for stSignature and stImports

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

#

valuemodifyImportedSignature

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

#

valuegetSignature :: ReadTCState m => m Signature

#

valuemodifyGlobalDefinition

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

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

#

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

#

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

Modifiers for rewrite rules

valueaddRewriteRulesFor

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

#

valuesetMatchableSymbols :: QName -> [QName] -> Signature -> Signature

#

`modify` methods for the signature

valuemodifyRecEta

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

#

Modifiers for parts of the signature

valuelookupDefinition :: QName -> Signature -> Maybe Definition

#

valueupdateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature

#

valueupdateDefinition

#

valueupdateTheDef :: (Defn -> Defn) -> Definition -> Definition

#

valueupdateDefType :: (Type -> Type) -> Definition -> Definition

#

valueupdateDefArgOccurrences

#

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

#

valueupdateDefCompiledRep

:: CompiledRepresentation -> CompiledRepresentation
-> Definition
-> Definition

#

valueaddCompilerPragma

#

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

#

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

#

valueupdateCompiledClauses

:: Maybe CompiledClauses -> Maybe CompiledClauses
-> Defn
-> Defn

#

valueupdateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition

#

valueupdateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition

#

File identification

4 declarations

valueregisterFileIdWithBuiltin

#

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.

valueisBuiltinModule :: ReadTCState m => FileId -> m (Maybe IsBuiltinModule)

#

Does the given FileId belong to one of Agda's builtin modules?

valueisBuiltinModuleWithSafePostulates :: ReadTCState m => FileId -> m Bool

#

Does the given FileId belong to one of Agda's builtin modules that only uses safe postulates?

Implies isJust . isBuiltinModule.

valueisPrimitiveModule :: ReadTCState m => FileId -> m Bool

#

Does the given FileId belong to one of Agda's magical primitive modules?

Implies isBuiltinModuleWithSafePostulates.

Top level module

5 declarations

valuetopLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName

#

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

valuesetTopLevelModule :: TopLevelModuleName -> TCM ()

#

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

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

#

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

valuewithTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a

#

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

valuecurrentModuleNameHash :: ReadTCState m => m ModuleNameHash

#

Backends and foreign code

4 declarations

valuelookupBackend :: ReadTCState m => BackendName -> m (Maybe Backend)

#

Look for a backend of the given name.

valueactiveBackend :: TCM (Maybe Backend)

#

Get the currently active backend (if any).

valueactiveBackendMayEraseType :: QName -> TCM Bool

#

Ask the active backend whether a type may be erased. See issue #3732.

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

#

Interaction output callback

3 declarations

valuegetInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback

#

valueappInteractionOutputCallback :: Response -> TCM ()

#

valuesetInteractionOutputCallback :: InteractionOutputCallback -> TCM ()

#

Pattern synonyms

7 declarations

valuegetPatternSyns :: ReadTCState m => m PatternSynDefns

#

valuesetPatternSyns :: PatternSynDefns -> TCM ()

#

valuemodifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()

#

Lens for stPatternSyns.

valuegetPatternSynImports :: ReadTCState m => m PatternSynDefns

#

valuegetAllPatternSyns :: ReadTCState m => m PatternSynDefns

#

Get both local and imported pattern synonyms

valuelookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn

#

valuelookupSinglePatternSyn :: QName -> TCM PatternSynDefn

#

Instance definitions

6 declarations

valueupdateInstanceDefs

:: TempInstanceTable -> TempInstanceTable
-> TCState
-> TCState

#

Lens for stInstanceDefs.

valuemodifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()

#

valuegetAllInstanceDefs :: TCM TempInstanceTable

#

valuegetAnonInstanceDefs :: TCM (Set QName)

#

valueclearUnknownInstance :: QName -> TCM ()

#

Remove an instance from the set of unresolved instances.

valueaddUnknownInstance :: QName -> TCM ()

#

Add an instance whose type is still unresolved.

Orphan instances

1 instance

MonadIO m => MonadFileId (TCMT m)

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

Orphan instances

`modify` methods for the signature