Agda.TypeChecking.Reduce.Monad

Documentation

constructorForm :: HasBuiltins m => Term -> m Term

enterClosure :: LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b

getConstInfo :: HasConstInfo m => QName -> m Definition

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

askR :: ReduceM ReduceEnv

applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

Orphan instances

HasBuiltins ReduceM

Methods

getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun))

MonadAddContext ReduceM

Methods

addCtx :: Name -> Dom Type -> ReduceM a -> ReduceM a

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a

updateContext :: Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a

withFreshName :: Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a

MonadDebug ReduceM

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReduceM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a

getVerbosity :: ReduceM Verbosity

getProfileOptions :: ReduceM ProfileOptions

isDebugPrinting :: ReduceM Bool

nowDebugPrinting :: ReduceM a -> ReduceM a

PureTCM ReduceM

HasConstInfo ReduceM

Methods

getConstInfo :: QName -> ReduceM Definition

getConstInfo' :: QName -> ReduceM (Either SigError Definition)

getRewriteRulesFor :: QName -> ReduceM RewriteRules