Agda.TypeChecking.Monad.Env

Documentation

currentModule :: MonadTCEnv m => m ModuleName

Get the name of the current module, if any.

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

Set the name of the current module.

getCurrentPath :: MonadTCEnv m => m AbsolutePath

Get the path of the currently checked file

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

Get the number of variables bound by anonymous modules.

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

Add variables bound by an anonymous module.

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

Set the current environment to the given

getEnv :: TCM TCEnv

Get the current environment

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a

Set highlighting level

doExpandLast :: TCM a -> TCM a

Restore setting for ExpandLast to default.

dontExpandLast :: TCM a -> TCM a

reallyDontExpandLast :: TCM a -> TCM a

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

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

getSimplification :: MonadTCEnv m => m Simplification

Controlling reduction.

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

Lens for AllowedReductions.

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

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

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

Reduce Def f vs only if f is a projection.

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

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

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

Allow all reductions including non-terminating functions.

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

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

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

Update allowed reductions when working on types

Concerning envInsideDotPattern

insideDotPattern :: TCM a -> TCM a

isInsideDotPattern :: TCM Bool

callByName :: TCM a -> TCM a

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

dontFoldLetBindings :: MonadTCEnv m => m a -> m a

Don't fold let bindings when printing. This is a bit crude since it disables any folding of let bindings at all. In many cases it's better to use removeLetBinding before printing to drop the let bindings that should not be folded.