| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.State
Description
Lenses for TCState and more.
Synopsis
- resetState :: TCM ()
- resetAllState :: TCM ()
- localTCState :: TCM a -> TCM a
- localTCStateSaving :: TCM a -> TCM (a, TCState)
- localTCStateSavingWarnings :: TCM a -> TCM a
- data SpeculateResult
- speculateTCState :: TCM (a, SpeculateResult) -> TCM a
- speculateTCState_ :: TCM SpeculateResult -> TCM ()
- freshTCM :: TCM a -> TCM (Either TCErr a)
- lensPersistentState :: Lens' PersistentTCState TCState
- updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
- modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
- lensAccumStatisticsP :: Lens' Statistics PersistentTCState
- lensAccumStatistics :: Lens' Statistics TCState
- getScope :: ReadTCState m => m ScopeInfo
- setScope :: ScopeInfo -> TCM ()
- modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
- modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
- useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
- locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (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 :: (Signature -> Signature) -> TCM ()
- modifyImportedSignature :: (Signature -> Signature) -> TCM ()
- getSignature :: ReadTCState m => m Signature
- modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
- setSignature :: Signature -> TCM ()
- withSignature :: Signature -> TCM a -> TCM a
- addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
- setMatchableSymbols :: QName -> [QName] -> Signature -> 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
- setTopLevelModule :: QName -> TCM ()
- withTopLevelModule :: QName -> TCM a -> TCM a
- addForeignCode :: BackendName -> String -> TCM ()
- getInteractionOutputCallback :: TCM 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
- theBenchmark :: TCState -> Benchmark
- updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
- getBenchmark :: TCM Benchmark
- modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
- addImportedInstances :: Signature -> TCM ()
- updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
- modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
- getAllInstanceDefs :: TCM TempInstanceTable
- getAnonInstanceDefs :: TCM (Set QName)
- clearAnonInstanceDefs :: TCM ()
- addUnknownInstance :: QName -> TCM ()
- addNamedInstance :: QName -> 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 Benchmark and backend information.
localTCState :: TCM a -> TCM a Source #
Restore TCState after performing subcomputation.
In contrast to localState, the Benchmark
info 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.
data SpeculateResult Source #
Constructors
| SpeculateAbort | |
| SpeculateCommit |
speculateTCState :: TCM (a, SpeculateResult) -> TCM a Source #
Allow rolling back the state changes of a TCM computation.
speculateTCState_ :: TCM SpeculateResult -> TCM () Source #
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 #
Scope
getScope :: ReadTCState m => m ScopeInfo Source #
Get 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.
locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (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 #
Signature
Lens for stSignature and stImports
getSignature :: ReadTCState m => m Signature Source #
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () 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 :: Signature -> TCM () Source #
withSignature :: Signature -> TCM a -> TCM a Source #
Run some computation in a different signature, restore original signature.
Modifiers for rewrite rules
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature 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 #
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn Source #
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition Source #
updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition Source #
Top level module
setTopLevelModule :: QName -> TCM () Source #
Set the top-level module. This affects the global module id of freshly generated names.
withTopLevelModule :: QName -> TCM a -> TCM a Source #
Use a different top-level module for a computation. Used when generating names for imported modules.
Foreign code
addForeignCode :: BackendName -> String -> TCM () Source #
Interaction output callback
appInteractionOutputCallback :: Response -> 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
Benchmark
Instance definitions
addImportedInstances :: Signature -> TCM () Source #
Look through the signature and reconstruct the instance table.
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState Source #
Lens for stInstanceDefs.
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM () Source #
clearAnonInstanceDefs :: TCM () Source #
Remove all instances whose type is still unresolved.
addUnknownInstance :: QName -> TCM () Source #
Add an instance whose type is still unresolved.