| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Monad.State
Contents
Description
Lenses for TCState and more.
- resetState :: TCM ()
- resetAllState :: TCM ()
- localTCState :: TCM a -> TCM a
- localTCStateSaving :: TCM a -> TCM (a, TCState)
- lensPersistentState :: Lens' PersistentTCState TCState
- updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
- modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
- lensAccumStatisticsP :: Lens' Statistics PersistentTCState
- lensAccumStatistics :: Lens' Statistics TCState
- getScope :: TCM ScopeInfo
- setScope :: ScopeInfo -> TCM ()
- modifyScope_ :: (ScopeInfo -> ScopeInfo) -> TCM ()
- modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
- withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)
- withScope_ :: ScopeInfo -> TCM a -> TCM a
- localScope :: TCM a -> TCM a
- notInScope :: QName -> TCM a
- printScope :: String -> Int -> String -> TCM ()
- modifySignature :: (Signature -> Signature) -> TCM ()
- modifyImportedSignature :: (Signature -> Signature) -> TCM ()
- getSignature :: TCM Signature
- getImportedSignature :: TCM Signature
- modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
- setSignature :: Signature -> TCM ()
- setImportedSignature :: Signature -> TCM ()
- withSignature :: Signature -> TCM a -> TCM a
- addRewriteRulesFor :: QName -> RewriteRules -> 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
- updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn
- setTopLevelModule :: QName -> TCM ()
- withTopLevelModule :: QName -> TCM a -> TCM a
- addHaskellImport :: String -> TCM ()
- getHaskellImports :: TCM (Set String)
- addHaskellImportUHC :: String -> TCM ()
- getHaskellImportsUHC :: TCM (Set String)
- addInlineHaskell :: String -> TCM ()
- getInteractionOutputCallback :: TCM InteractionOutputCallback
- appInteractionOutputCallback :: Response -> TCM ()
- setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
- getPatternSyns :: TCM PatternSynDefns
- setPatternSyns :: PatternSynDefns -> TCM ()
- modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
- getPatternSynImports :: TCM PatternSynDefns
- lookupPatternSyn :: QName -> TCM PatternSynDefn
- theBenchmark :: TCState -> Benchmark
- updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
- getBenchmark :: TCM Benchmark
- modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
- freshTCM :: TCM a -> TCM (Either TCErr a)
- addSignatureInstances :: Signature -> TCM ()
- updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
- modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
- getAllInstanceDefs :: TCM TempInstanceTable
- getAnonInstanceDefs :: TCM [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 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.
Lens for persistent states and its fields
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState Source #
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM () Source #
Scope
modifyScope_ :: (ScopeInfo -> ScopeInfo) -> TCM () Source #
Modify the current scope without updating the inverse maps.
withScope_ :: ScopeInfo -> TCM a -> TCM 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.
notInScope :: QName -> TCM a Source #
Scope error.
Signature
Lens for stSignature and stImports
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 #
setImportedSignature :: 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 -> 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 #
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.
Haskell imports
addHaskellImport :: String -> TCM () Source #
Tell the compiler to import the given Haskell module.
addHaskellImportUHC :: String -> TCM () Source #
Tell the compiler to import the given Haskell module.
addInlineHaskell :: String -> TCM () Source #
Interaction output callback
appInteractionOutputCallback :: Response -> TCM () Source #
Pattern synonyms
setPatternSyns :: PatternSynDefns -> TCM () Source #
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM () Source #
Lens for stPatternSyns.
Benchmark
freshTCM :: TCM a -> TCM (Either TCErr a) Source #
Run a fresh instance of the TCM (with initial state).
Benchmark info is preserved.
Instance definitions
addSignatureInstances :: 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 #
getAnonInstanceDefs :: TCM [QName] Source #
clearAnonInstanceDefs :: TCM () Source #
Remove all instances whose type is still unresolved.
addUnknownInstance :: QName -> TCM () Source #
Add an instance whose type is still unresolved.