Agda.TypeChecking.Monad.Signature

Documentation

setHardCompileTimeModeIfErased

Arguments

:: Erased

-> TCM a

Continuation.

-> TCM a

If the first argument is Erased something, then hard compile-time mode is enabled when the continuation is run.

setHardCompileTimeModeIfErased'

Arguments

:: LensQuantity q

=> q

The quantity.

-> TCM a

Continuation.

-> TCM a

If the quantity is "erased", then hard compile-time mode is enabled when the continuation is run.

Precondition: The quantity must not be Quantity1 something.

setRunTimeModeUnlessInHardCompileTimeMode

Arguments

:: TCM a

Continuation.

-> TCM a

Use run-time mode in the continuation unless the current mode is the hard compile-time mode.

setModeUnlessInHardCompileTimeMode

Arguments

:: Erased

-> TCM a

Continuation.

-> TCM a

Use hard compile-time mode in the continuation if the first argument is Erased something. Use run-time mode if the first argument is NotErased something and the current mode is not hard compile-time mode.

warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()

Warn if the user explicitly wrote @ω or @plenty but the current mode is the hard compile-time mode.

addConstant :: QName -> Definition -> TCM ()

Add a constant to the signature. Lifts the definition to top level.

addConstant' :: QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()

A combination of addConstant and defaultDefn. The Language does not need to be supplied.

setTerminates :: MonadTCState m => QName -> Bool -> m ()

Set termination info of a defined function symbol.

setCompiledClauses :: QName -> CompiledClauses -> TCM ()

Set CompiledClauses of a defined function symbol.

setSplitTree :: QName -> SplitTree -> TCM ()

Set SplitTree of a defined function symbol.

modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()

Modify the clauses of a function.

addClauses :: (MonadConstraint m, MonadTCState m) => QName -> [Clause] -> m ()

Lifts clauses to the top-level and adds them to definition. Also adjusts the funCopatternLHS field if necessary.

mkPragma :: String -> TCM CompilerPragma

addPragma :: BackendName -> QName -> String -> TCM ()

Add a compiler pragma `{-# COMPILE backend name text #-}`

getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)

setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()

markStatic :: QName -> TCM ()

markInline :: Bool -> QName -> TCM ()

markInjective :: QName -> TCM ()

markFirstOrder :: QName -> TCM ()

unionSignatures :: [Signature] -> Signature

addSection :: ModuleName -> TCM ()

Add a section to the signature.

The current context will be stored as the cumulative module parameters for this section.

setModuleCheckpoint :: ModuleName -> TCM ()

Sets the checkpoint for the given module to the current checkpoint.

getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)

Get a section.

Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.

lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope

Lookup a section telescope.

If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.

addDisplayForms :: QName -> TCM ()

Add display forms for a name f copied by a module application. Essentially if f can reduce to

λ xs → A.B.C.f vs

by unfolding module application copies (defCopy), then we add a display form

A.B.C.f vs ==> f xs

applySection

Arguments

:: ModuleName

Name of new module defined by the module macro.

-> Telescope

Parameters of new module.

-> ModuleName

Name of old module applied to arguments.

-> Args

Arguments of module application.

-> ScopeCopyInfo

Imported names and modules

-> TCM ()

Module application (followed by module parameter abstraction).

applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()

addDisplayForm :: QName -> DisplayForm -> TCM ()

Add a display form to a definition (could be in this or imported signature).

isLocal :: ReadTCState m => QName -> m Bool

getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]

hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool

chaseDisplayForms :: QName -> TCM (Set QName)

Find all names used (recursively) by display forms of a given name.

hasLoopingDisplayForm :: QName -> TCM Bool

Check if a display form is looping.

canonicalName :: HasConstInfo m => QName -> m QName

sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)

singleConstructorType :: QName -> TCM Bool

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

data SigError

Signature lookup errors.

Constructors

SigUnknown String

The name is not in the signature; default error message.

SigAbstract

The name is not available, since it is abstract.

SigCubicalNotErasure

The name is not available because it was defined in Cubical Agda, but the current language is Erased Cubical Agda, and --erasure is not active.

notSoPrettySigCubicalNotErasure :: QName -> String

Generates an error message corresponding to SigCubicalNotErasure for a given QName.

prettySigCubicalNotErasure :: MonadPretty m => QName -> m Doc

Generates an error message corresponding to SigCubicalNotErasure for a given QName.

sigError :: (HasCallStack, MonadDebug m) => m a -> SigError -> m a

An eliminator for SigError. All constructors except for SigAbstract are assumed to be impossible.

class (Functor m, Applicative m, MonadFail m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo m where

Minimal complete definition

Nothing

Methods

getConstInfo :: QName -> m Definition

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

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

Version that reports exceptions:

default getConstInfo' :: (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m (Either SigError Definition)

getRewriteRulesFor :: QName -> m RewriteRules

Lookup the rewrite rules with the given head symbol.

default getRewriteRulesFor :: (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m RewriteRules

Instances

HasConstInfo AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getConstInfo :: QName -> AbsToCon Definition

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

getRewriteRulesFor :: QName -> AbsToCon RewriteRules

HasConstInfo TerM

Defined in Agda.Termination.Monad

Methods

getConstInfo :: QName -> TerM Definition

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

getRewriteRulesFor :: QName -> TerM RewriteRules

HasConstInfo ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getConstInfo :: QName -> ReduceM Definition

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

getRewriteRulesFor :: QName -> ReduceM RewriteRules

HasConstInfo NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getConstInfo :: QName -> NLM Definition

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

getRewriteRulesFor :: QName -> NLM RewriteRules

HasConstInfo m => HasConstInfo (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getConstInfo :: QName -> PureConversionT m Definition

getConstInfo' :: QName -> PureConversionT m (Either SigError Definition)

getRewriteRulesFor :: QName -> PureConversionT m RewriteRules

HasConstInfo m => HasConstInfo (BlockT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> BlockT m Definition

getConstInfo' :: QName -> BlockT m (Either SigError Definition)

getRewriteRulesFor :: QName -> BlockT m RewriteRules

HasConstInfo (TCMT IO)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> TCMT IO Definition

getConstInfo' :: QName -> TCMT IO (Either SigError Definition)

getRewriteRulesFor :: QName -> TCMT IO RewriteRules

HasConstInfo m => HasConstInfo (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getConstInfo :: QName -> NamesT m Definition

getConstInfo' :: QName -> NamesT m (Either SigError Definition)

getRewriteRulesFor :: QName -> NamesT m RewriteRules

HasConstInfo m => HasConstInfo (ListT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ListT m Definition

getConstInfo' :: QName -> ListT m (Either SigError Definition)

getRewriteRulesFor :: QName -> ListT m RewriteRules

HasConstInfo m => HasConstInfo (ChangeT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ChangeT m Definition

getConstInfo' :: QName -> ChangeT m (Either SigError Definition)

getRewriteRulesFor :: QName -> ChangeT m RewriteRules

HasConstInfo m => HasConstInfo (MaybeT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> MaybeT m Definition

getConstInfo' :: QName -> MaybeT m (Either SigError Definition)

getRewriteRulesFor :: QName -> MaybeT m RewriteRules

HasConstInfo m => HasConstInfo (ExceptT err m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ExceptT err m Definition

getConstInfo' :: QName -> ExceptT err m (Either SigError Definition)

getRewriteRulesFor :: QName -> ExceptT err m RewriteRules

HasConstInfo m => HasConstInfo (IdentityT m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> IdentityT m Definition

getConstInfo' :: QName -> IdentityT m (Either SigError Definition)

getRewriteRulesFor :: QName -> IdentityT m RewriteRules

HasConstInfo m => HasConstInfo (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ReaderT r m Definition

getConstInfo' :: QName -> ReaderT r m (Either SigError Definition)

getRewriteRulesFor :: QName -> ReaderT r m RewriteRules

HasConstInfo m => HasConstInfo (StateT s m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> StateT s m Definition

getConstInfo' :: QName -> StateT s m (Either SigError Definition)

getRewriteRulesFor :: QName -> StateT s m RewriteRules

(Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m)

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> WriterT w m Definition

getConstInfo' :: QName -> WriterT w m (Either SigError Definition)

getRewriteRulesFor :: QName -> WriterT w m RewriteRules

getOriginalConstInfo :: (ReadTCState m, HasConstInfo m) => QName -> m Definition

The computation getConstInfo sometimes tweaks the returned Definition, depending on the current Language and the Language of the Definition. This variant of getConstInfo does not perform any tweaks.

defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules

getOriginalProjection :: HasConstInfo m => QName -> m QName

Get the original name of the projection (the current one could be from a module application).

defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadTCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition)

getConInfo :: HasConstInfo m => ConHead -> m Definition

getPolarity :: HasConstInfo m => QName -> m [Polarity]

Look up the polarity of a definition.

getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]

Look up polarity of a definition and compose with polarity represented by Comparison.

setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m ()

Set the polarity of a definition.

getForcedArgs :: HasConstInfo m => QName -> m [IsForced]

Look up the forced arguments of a definition.

getArgOccurrence :: QName -> Nat -> TCM Occurrence

Get argument occurrence info for argument i of definition d (never fails).

setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m ()

Sets the defArgOccurrences for the given identifier (which should already exist in the signature).

modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m ()

setTreeless :: QName -> TTerm -> TCM ()

setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()

getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled)

getErasedConArgs :: HasConstInfo m => QName -> m [Bool]

Returns a list of length conArity. If no erasure analysis has been performed yet, this will be a list of Falses.

setErasedConArgs :: QName -> [Bool] -> TCM ()

getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm)

getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage])

addDataCons :: QName -> [QName] -> TCM ()

add data constructors to a datatype

getMutual :: QName -> TCM (Maybe [QName])

Get the mutually recursive identifiers of a symbol from the signature.

getMutual_ :: Defn -> Maybe [QName]

Get the mutually recursive identifiers from a Definition.

setMutual :: QName -> [QName] -> TCM ()

Set the mutually recursive identifiers.

TODO: This produces data of quadratic size (which has to be processed upon serialization). Presumably qs is usually short, but in some cases (for instance for generated code) it may be long. It would be better to assign a unique identifier to each SCC, and store the names separately.

mutuallyRecursive :: QName -> QName -> TCM Bool

Check whether two definitions are mutually recursive.

definitelyNonRecursive_ :: Defn -> Bool

A functiondatarecord definition is nonRecursive if it is not even mutually recursive with itself.

getCurrentModuleFreeVars :: TCM Nat

Get the number of parameters to the current module.

getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)

getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat

Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).

freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> m Args

getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) => ModuleName -> m Nat

moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args

Compute the context variables to apply a definition to.

We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)

Example: module M₁ Γ where module M₁ Δ where f = ... module M₃ Θ where ... M₁.M₂.f [insert Γ raised by Θ]

inFreshModuleIfFreeParams :: TCM a -> TCM a

Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.

instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition

Instantiate a closed definition with the correct part of the current context.

instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule

instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules

alwaysMakeAbstract :: Definition -> Maybe Definition

Return the abstract view of a definition, regardless of whether the definition would be treated abstractly.

inAbstractMode :: MonadTCEnv m => m a -> m a

Enter abstract mode. Abstract definition in the current module are transparent.

inConcreteMode :: MonadTCEnv m => m a -> m a

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCEnv m => m a -> m a

Ignore abstract mode. All abstract definitions are transparent.

underOpaqueId :: MonadTCEnv m => OpaqueId -> m a -> m a

Go under the given opaque block. The unfolding set will turn opaque definitions transparent.

notUnderOpaque :: MonadTCEnv m => m a -> m a

Outside of any opaque blocks.

inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a

Enter the reducibility environment associated with a definition: The environment will have the same concreteness as the name, and we will be in the opaque block enclosing the name, if any.

typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type

Get type of a constant, instantiated to the current context.

relOfConst :: HasConstInfo m => QName -> m Relevance

Get relevance of a constant.

modalityOfConst :: HasConstInfo m => QName -> m Modality

Get modality of a constant.

droppedPars :: Definition -> Int

The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.

isProjection :: HasConstInfo m => QName -> m (Maybe Projection)

Is it the name of a record projection?

isProjection_ :: Defn -> Maybe Projection

isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)

Is it the name of a non-irrelevant record projection?

isRelevantProjection_ :: Definition -> Maybe Projection

isStaticFun :: Defn -> Bool

Is it a function marked STATIC?

isInlineFun :: Defn -> Bool

Is it a function marked INLINE?

isProperProjection :: Defn -> Bool

Returns True if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

projectionArgs :: Definition -> Int

Number of dropped initial arguments of a projection(-like) function.

usesCopatterns :: (HasConstInfo m, HasBuiltins m) => QName -> m Bool

Check whether a definition uses copatterns.

applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term

Apply a function f to its first argument, producing the proper postfix projection if f is a projection which is not irrelevant.