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

Safe HaskellNone
LanguageHaskell98

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 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.

Lens for persistent states and its fields

Scope

getScope :: TCM ScopeInfo

Get the current scope.

setScope :: ScopeInfo -> TCM ()

Set the current scope.

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

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

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

Modifiers for parts of the signature

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.

Haskell imports

addHaskellImport :: String -> TCM ()

Tell the compiler to import the given Haskell module.

getHaskellImports :: TCM (Set String)

Get the Haskell imports.

Interaction output callback

Pattern synonyms

Benchmark

theBenchmark :: TCState -> Benchmark

Lens getter for Benchmark from TCState.

getBenchmark :: TCM Benchmark

Lens getter for Benchmark from TCM.

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

Lens modify for Benchmark.

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

Run a fresh instance of the TCM (with initial state). Benchmark info is preserved.

Instance definitions

addSignatureInstances :: Signature -> TCM ()

Look through the signature and reconstruct the instance table.

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'.