Agda-2.6.0.1: 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
  - Modifiers for parts of the signature
- Top level module
- Foreign code
- Interaction output callback
- Pattern synonyms
- Benchmark
- Instance definitions

Description

Lenses for `TCState` and more.

Synopsis

- resetState :: TCM ()
- resetAllState :: TCM ()
- localTCState :: TCM a -> TCM a
- localTCStateSaving :: TCM a -> TCM (a, TCState)
- data SpeculateResult
  - = SpeculateAbort
  - | SpeculateCommit
- 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 :: 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
- modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
- setSignature :: Signature -> TCM ()
- withSignature :: Signature -> TCM a -> TCM a
- addRewriteRulesFor :: QName -> RewriteRules -> [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 :: ([Closure Clause] -> [Closure Clause]) -> Defn -> Defn
- updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
- updateFunCopatternLHS :: (Bool -> Bool) -> Defn -> Defn
- setTopLevelModule :: QName -> TCM ()
- withTopLevelModule :: QName -> TCM a -> TCM a
- addForeignCode :: BackendName -> String -> TCM ()
- getInteractionOutputCallback :: TCM InteractionOutputCallback
- appInteractionOutputCallback :: Response -> TCM ()
- setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
- getPatternSyns :: TCM PatternSynDefns
- setPatternSyns :: PatternSynDefns -> TCM ()
- modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
- getPatternSynImports :: TCM PatternSynDefns
- getAllPatternSyns :: TCM 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.

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

lensPersistentState :: Lens' PersistentTCState TCState Source #

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

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

lensAccumStatisticsP :: Lens' Statistics PersistentTCState Source #

Lens for `stAccumStatistics`.

lensAccumStatistics :: Lens' Statistics TCState Source #

# Scope

getScope :: TCM ScopeInfo Source #

Get the current scope.

setScope :: ScopeInfo -> TCM () Source #

Set the current scope.

modifyScope_ :: (ScopeInfo -> ScopeInfo) -> TCM () Source #

Modify the current scope without updating the inverse maps.

modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM () Source #

Modify the current scope.

withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo) Source #

Run a computation in a local scope.

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.

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

Debug print the scope.

# Signature

## Lens for `stSignature` and `stImports`

modifySignature :: (Signature -> Signature) -> TCM () Source #

modifyImportedSignature :: (Signature -> Signature) -> TCM () Source #

getSignature :: TCM 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 #

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

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

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

updateFunCopatternLHS :: (Bool -> Bool) -> Defn -> Defn 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

getInteractionOutputCallback :: TCM InteractionOutputCallback Source #

appInteractionOutputCallback :: Response -> TCM () Source #

setInteractionOutputCallback :: InteractionOutputCallback -> TCM () Source #

# Pattern synonyms

getPatternSyns :: TCM PatternSynDefns Source #

setPatternSyns :: PatternSynDefns -> TCM () Source #

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

Lens for `stPatternSyns`.

getPatternSynImports :: TCM PatternSynDefns Source #

getAllPatternSyns :: TCM PatternSynDefns Source #

Get both local and imported pattern synonyms

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn Source #

lookupSinglePatternSyn :: QName -> TCM PatternSynDefn Source #

# Benchmark

theBenchmark :: TCState -> Benchmark Source #

Lens getter for `Benchmark` from `TCState`.

updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState Source #

Lens map for `Benchmark`.

getBenchmark :: TCM Benchmark Source #

Lens getter for `Benchmark` from `TCMT`.

modifyBenchmark :: (Benchmark -> Benchmark) -> TCM () Source #

Lens modify for `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 #

getAllInstanceDefs :: TCM TempInstanceTable Source #

getAnonInstanceDefs :: TCM (Set 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.

addNamedInstance Source #

Arguments

:: QName | Name of the instance.
-> QName | Name of the class.
-> TCM () |

Add instance to some ``class'`.