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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Env

Contents

- Controlling reduction.
- Concerning `envInsideDotPattern`

Synopsis

- currentModule :: MonadTCEnv m => m ModuleName
- withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a
- getCurrentPath :: MonadTCEnv m => m AbsolutePath
- getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat
- withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
- withEnv :: MonadTCEnv m => TCEnv -> m a -> m a
- getEnv :: TCM TCEnv
- withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
- doExpandLast :: TCM a -> TCM a
- dontExpandLast :: TCM a -> TCM a
- reallyDontExpandLast :: TCM a -> TCM a
- performedSimplification :: MonadTCEnv m => m a -> m a
- performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a
- getSimplification :: MonadTCEnv m => m Simplification
- updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
- modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a
- putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a
- onlyReduceProjections :: MonadTCEnv m => m a -> m a
- allowAllReductions :: MonadTCEnv m => m a -> m a
- allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a
- onlyReduceTypes :: MonadTCEnv m => m a -> m a
- typeLevelReductions :: MonadTCEnv m => m a -> m a
- insideDotPattern :: TCM a -> TCM a
- isInsideDotPattern :: TCM Bool
- callByName :: TCM a -> TCM a

# Documentation

currentModule :: MonadTCEnv m => m ModuleName Source #

Get the name of the current module, if any.

withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a Source #

Set the name of the current module.

getCurrentPath :: MonadTCEnv m => m AbsolutePath Source #

Get the path of the currently checked file

getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat Source #

Get the number of variables bound by anonymous modules.

withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a Source #

Add variables bound by an anonymous module.

withEnv :: MonadTCEnv m => TCEnv -> m a -> m a Source #

Set the current environment to the given

getEnv :: TCM TCEnv Source #

Get the current environment

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a Source #

Set highlighting level

doExpandLast :: TCM a -> TCM a Source #

Restore setting for `ExpandLast` to default.

dontExpandLast :: TCM a -> TCM a Source #

reallyDontExpandLast :: TCM a -> TCM a Source #

performedSimplification :: MonadTCEnv m => m a -> m a Source #

If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.

performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a Source #

getSimplification :: MonadTCEnv m => m Simplification Source #

# Controlling reduction.

updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv Source #

Lens for `AllowedReductions`.

modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a Source #

putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a Source #

onlyReduceProjections :: MonadTCEnv m => m a -> m a Source #

Reduce `Def f vs` only if `f` is a projection.

allowAllReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions except for non-terminating functions (default).

allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions including non-terminating functions.

onlyReduceTypes :: MonadTCEnv m => m a -> m a Source #

Allow all reductions when reducing types. Otherwise only allow inlined functions to be unfolded.

typeLevelReductions :: MonadTCEnv m => m a -> m a Source #

Update allowed reductions when working on types

# Concerning `envInsideDotPattern`

insideDotPattern :: TCM a -> TCM a Source #

isInsideDotPattern :: TCM Bool Source #

callByName :: TCM a -> TCM a Source #

Don't use call-by-need evaluation for the given computation.