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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.State

Contents

Description

Lenses for TCState and more.

Synopsis

Documentation

resetState :: TCM () #

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

resetAllState :: TCM () #

Resets all of the type checking state.

Keep only Benchmark and backend information.

localTCState :: TCM a -> TCM a #

Restore TCState after performing subcomputation.

In contrast to localState, the Benchmark info from the subcomputation is saved.

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

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

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

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 #

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

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

lensAccumStatisticsP :: Lens' Statistics PersistentTCState #

Lens for stAccumStatistics.

lensAccumStatistics :: Lens' Statistics TCState #

Scope

getScope :: TCM ScopeInfo #

Get the current scope.

setScope :: ScopeInfo -> TCM () #

Set the current scope.

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

Modify the current scope without updating the inverse maps.

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

Modify the current scope.

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

Run a computation in a local scope.

withScope_ :: ScopeInfo -> TCM a -> TCM a #

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

localScope :: TCM a -> TCM a #

Discard any changes to the scope by a computation.

notInScope :: QName -> TCM a #

Scope error.

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

Debug print the scope.

Signature

Lens for stSignature and stImports

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

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

getSignature :: TCM Signature #

modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () #

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

withSignature :: Signature -> TCM a -> TCM a #

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

Modifiers for rewrite rules

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

Modifiers for parts of the 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 #

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

updateFunCopatternLHS :: (Bool -> Bool) -> Defn -> Defn #

Top level module

setTopLevelModule :: QName -> TCM () #

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

withTopLevelModule :: QName -> TCM a -> TCM a #

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

Foreign code

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

Temporary: Haskell imports

addDeprecatedForeignCode :: String -> BackendName -> String -> TCM () #

addHaskellImport :: String -> TCM () #

Tell the compiler to import the given Haskell module.

addHaskellImportUHC :: String -> TCM () #

Tell the compiler to import the given Haskell module.

addInlineHaskell :: String -> TCM () #

Interaction output callback

getInteractionOutputCallback :: TCM InteractionOutputCallback #

appInteractionOutputCallback :: Response -> TCM () #

setInteractionOutputCallback :: InteractionOutputCallback -> TCM () #

Pattern synonyms

getPatternSyns :: TCM PatternSynDefns #

setPatternSyns :: PatternSynDefns -> TCM () #

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

Lens for stPatternSyns.

getPatternSynImports :: TCM PatternSynDefns #

getAllPatternSyns :: TCM PatternSynDefns #

Get both local and imported pattern synonyms

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn #

lookupSinglePatternSyn :: QName -> TCM PatternSynDefn #

Benchmark

theBenchmark :: TCState -> Benchmark #

Lens getter for Benchmark from TCState.

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

Lens map for Benchmark.

getBenchmark :: TCM Benchmark #

Lens getter for Benchmark from TCM.

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

Lens modify for Benchmark.

Instance definitions

addImportedInstances :: Signature -> TCM () #

Look through the signature and reconstruct the instance table.

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

Lens for stInstanceDefs.

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

getAllInstanceDefs :: TCM TempInstanceTable #

getAnonInstanceDefs :: TCM (Set QName) #

clearAnonInstanceDefs :: TCM () #

Remove all instances whose type is still unresolved.

addUnknownInstance :: QName -> TCM () #

Add an instance whose type is still unresolved.

addNamedInstance #

Arguments

:: QName

Name of the instance.

-> QName

Name of the class.

-> TCM () 

Add instance to some `class'.