Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.State

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
- Orphan instances

Description

Lenses for `TCState` and more.

Synopsis

- resetState :: TCM ()
- resetAllState :: TCM ()
- putTCPreservingSession :: TCState -> TCM ()
- localTCState :: TCM a -> TCM a
- localTCStateSaving :: TCM a -> TCM (a, TCState)
- localTCStateSavingWarnings :: TCM a -> TCM a
- freshTCM :: TCM a -> TCM (Either TCErr a)
- updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
- modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
- lensAccumStatisticsP :: Lens' PersistentTCState Statistics
- lensAccumStatistics :: Lens' TCState Statistics
- getScope :: ReadTCState m => m ScopeInfo
- setScope :: ScopeInfo -> TCM ()
- modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
- modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
- useScope :: ReadTCState m => Lens' ScopeInfo a -> m a
- locallyScope :: ReadTCState m => Lens' ScopeInfo a -> (a -> a) -> m b -> m b
- withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
- withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
- localScope :: TCM a -> TCM a
- notInScopeError :: QName -> TCM a
- notInScopeWarning :: QName -> TCM ()
- printScope :: String -> Int -> String -> TCM ()
- modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()
- modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()
- getSignature :: ReadTCState m => m Signature
- modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()
- setSignature :: MonadTCState m => Signature -> m ()
- withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
- addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
- setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
- modifyRecEta :: MonadTCState m => QName -> (EtaEquality -> EtaEquality) -> m ()
- 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
- registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
- isBuiltinModule :: ReadTCState m => FileId -> m (Maybe IsBuiltinModule)
- isBuiltinModuleWithSafePostulates :: ReadTCState m => FileId -> m Bool
- isPrimitiveModule :: ReadTCState m => FileId -> m Bool
- topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName
- setTopLevelModule :: TopLevelModuleName -> TCM ()
- currentTopLevelModule :: (MonadTCEnv m, ReadTCState m) => m (Maybe TopLevelModuleName)
- withTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a
- currentModuleNameHash :: ReadTCState m => m ModuleNameHash
- lookupBackend :: ReadTCState m => BackendName -> m (Maybe Backend)
- activeBackend :: TCM (Maybe Backend)
- activeBackendMayEraseType :: QName -> TCM Bool
- addForeignCode :: BackendName -> String -> TCM ()
- getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
- appInteractionOutputCallback :: Response -> TCM ()
- setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
- getPatternSyns :: ReadTCState m => m PatternSynDefns
- setPatternSyns :: PatternSynDefns -> TCM ()
- modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
- getPatternSynImports :: ReadTCState m => m PatternSynDefns
- getAllPatternSyns :: ReadTCState m => m PatternSynDefns
- lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
- lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
- updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
- modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
- getAllInstanceDefs :: TCM TempInstanceTable
- getAnonInstanceDefs :: TCM (Set QName)
- clearUnknownInstance :: QName -> TCM ()
- addUnknownInstance :: QName -> TCM ()

# Documentation

resetState :: TCM () Source #

Resets the non-persistent part of the type checking state.

resetAllState :: TCM () Source #

Resets all of the type checking state.

Keep only the session state (backend information, `Benchmark`, file ids).

putTCPreservingSession :: TCState -> TCM () Source #

Overwrite the `TCState`, but not the `SessionTCState` part.

localTCState :: TCM a -> TCM a Source #

Restore `TCState` after performing subcomputation.

In contrast to `localState`, the `SessionTCState` from the subcomputation is saved.

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

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

localTCStateSavingWarnings :: TCM a -> TCM a Source #

Same as `localTCState` but keep all warnings.

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

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

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

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

lensAccumStatisticsP :: Lens' PersistentTCState Statistics Source #

Lens for `stAccumStatistics`.

lensAccumStatistics :: Lens' TCState Statistics Source #

# Scope

getScope :: ReadTCState m => m ScopeInfo Source #

Get the current scope.

setScope :: ScopeInfo -> TCM () Source #

Set the current scope.

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

Modify the current scope without updating the inverse maps.

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

Modify the current scope.

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

Get a part of the current scope.

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

Run a computation in a modified scope.

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

Run a computation in a local scope.

withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a Source #

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

localScope :: TCM a -> TCM a Source #

Discard any changes to the scope by a computation.

notInScopeError :: QName -> TCM a Source #

Scope error.

notInScopeWarning :: QName -> TCM () Source #

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

Debug print the scope.

# Signature

## Lens for `stSignature` and `stImports`

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

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

getSignature :: ReadTCState m => m Signature Source #

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

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 () Source #

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

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

## Modifiers for rewrite rules

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

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

## `modify` methods for the signature

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

## Modifiers for parts of the signature

lookupDefinition :: QName -> Signature -> Maybe Definition Source #

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

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

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

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

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

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

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

addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition Source #

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

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

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

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

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

# File identification

registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins) Source #

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.

isBuiltinModule :: ReadTCState m => FileId -> m (Maybe IsBuiltinModule) Source #

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

isBuiltinModuleWithSafePostulates :: ReadTCState m => FileId -> m Bool Source #

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

Implies `isJust . `isBuiltinModule``.

isPrimitiveModule :: ReadTCState m => FileId -> m Bool Source #

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

Implies `isBuiltinModuleWithSafePostulates`.

# Top level module

topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName Source #

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

setTopLevelModule :: TopLevelModuleName -> TCM () Source #

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

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

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

withTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a Source #

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

currentModuleNameHash :: ReadTCState m => m ModuleNameHash Source #

# Backends and foreign code

lookupBackend :: ReadTCState m => BackendName -> m (Maybe Backend) Source #

Look for a backend of the given name.

activeBackend :: TCM (Maybe Backend) Source #

Get the currently active backend (if any).

activeBackendMayEraseType :: QName -> TCM Bool Source #

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

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

# Interaction output callback

getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback Source #

appInteractionOutputCallback :: Response -> TCM () Source #

setInteractionOutputCallback :: InteractionOutputCallback -> TCM () Source #

# Pattern synonyms

getPatternSyns :: ReadTCState m => m PatternSynDefns Source #

setPatternSyns :: PatternSynDefns -> TCM () Source #

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

Lens for `stPatternSyns`.

getPatternSynImports :: ReadTCState m => m PatternSynDefns Source #

getAllPatternSyns :: ReadTCState m => m PatternSynDefns Source #

Get both local and imported pattern synonyms

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn Source #

lookupSinglePatternSyn :: QName -> TCM PatternSynDefn Source #

# Instance definitions

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

Lens for `stInstanceDefs`.

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

getAllInstanceDefs :: TCM TempInstanceTable Source #

getAnonInstanceDefs :: TCM (Set QName) Source #

clearUnknownInstance :: QName -> TCM () Source #

Remove an instance from the set of unresolved instances.

addUnknownInstance :: QName -> TCM () Source #

Add an instance whose type is still unresolved.

# Orphan instances

MonadIO m => MonadFileId (TCMT m) Source # |
Instance details Methods fileFromId :: FileId -> TCMT m File Source # idFromFile :: File -> TCMT m FileId Source #