Agda.TypeChecking.Monad.Signature

Documentation

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

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

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

Set termination info of a defined function symbol.

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

Modify the clauses of a function.

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

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 `{--}`

Temporary **

type HaskellCode = String

type HaskellType = String

type JSCode = String

type CoreCode = String

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

dataFormat :: String -> [String] -> String

addHaskellCode :: QName -> HaskellCode -> TCM ()

addHaskellExport :: QName -> String -> TCM ()

addHaskellType :: QName -> HaskellType -> TCM ()

addHaskellData :: QName -> HaskellType -> [HaskellCode] -> TCM ()

addJSCode :: QName -> JSCode -> TCM ()

addCoreCode :: QName -> CoreCode -> TCM ()

addCoreType :: QName -> CoreCode -> [CoreCode] -> TCM ()

End of temporary functions **

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

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

markStatic :: QName -> TCM ()

markInline :: QName -> TCM ()

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

setDefaultModuleParameters :: ModuleName -> TCM ()

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 ()

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 :: QName -> TCM Bool

getDisplayForms :: QName -> TCM [LocalDisplayForm]

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 :: QName -> TCM QName

sameDef :: QName -> QName -> TCM (Maybe QName)

whatInduction :: MonadTCM tcm => QName -> tcm Induction

Can be called on either a (co)datatype, a record type or a (co)constructor.

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.

sigError :: (String -> a) -> a -> SigError -> a

Standard eliminator for SigError.

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

Minimal complete definition

getRewriteRulesFor

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:

getRewriteRulesFor :: QName -> m RewriteRules

Lookup the rewrite rules with the given head symbol.

Instances

HasConstInfo TerM

Methods

getConstInfo :: QName -> TerM Definition

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

getRewriteRulesFor :: QName -> TerM RewriteRules

HasConstInfo m => HasConstInfo (MaybeT m)

Methods

getConstInfo :: QName -> MaybeT m Definition

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

getRewriteRulesFor :: QName -> MaybeT m RewriteRules

HasConstInfo (TCMT IO)

Methods

getConstInfo :: QName -> TCMT IO Definition

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

getRewriteRulesFor :: QName -> TCMT IO RewriteRules

HasConstInfo m => HasConstInfo (ExceptT err m)

Methods

getConstInfo :: QName -> ExceptT err m Definition

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

getRewriteRulesFor :: QName -> ExceptT err m RewriteRules

defaultGetRewriteRulesFor :: Monad m => m TCState -> 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) => TCState -> TCEnv -> QName -> m (Either SigError Definition)

getConInfo :: MonadTCM tcm => ConHead -> tcm Definition

getPolarity :: QName -> TCM [Polarity]

Look up the polarity of a definition.

getPolarity' :: Comparison -> QName -> TCM [Polarity]

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

setPolarity :: QName -> [Polarity] -> TCM ()

Set the polarity of a definition.

getArgOccurrence :: QName -> Nat -> TCM Occurrence

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

setArgOccurrences :: QName -> [Occurrence] -> TCM ()

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

modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()

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

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

getCompiled :: QName -> TCM (Maybe Compiled)

getErasedConArgs :: QName -> TCM [Bool]

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

getTreeless :: QName -> TCM (Maybe TTerm)

getCompiledArgUse :: QName -> TCM [Bool]

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.

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.

getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv 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, MonadReader TCEnv m, MonadDebug m) => QName -> m Args

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

moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadReader TCEnv 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.) y 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 :: Definition -> TCM Definition

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

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

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

makeAbstract :: Definition -> Maybe Definition

Give the abstract view of a definition.

inAbstractMode :: MonadReader TCEnv m => m a -> m a

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

inConcreteMode :: MonadReader TCEnv m => m a -> m a

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a

Ignore abstract mode. All abstract definitions are transparent.

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

Enter concrete or abstract mode depending on whether the given identifier is concrete or abstract.

treatAbstractly :: MonadReader TCEnv m => QName -> m Bool

Check whether a name might have to be treated abstractly (either if we're inAbstractMode or it's not a local name). Returns true for things not declared abstract as well, but for those makeAbstract will have no effect.

treatAbstractly' :: QName -> TCEnv -> Bool

Andreas, 2015-07-01: If the current module is a weak suffix of the identifier module, we can see through its abstract definition if we are abstract. (Then treatAbstractly' returns False).

If I am not mistaken, then we cannot see definitions in the where block of an abstract function from the perspective of the function, because then the current module is a strict prefix of the module of the local identifier. This problem is fixed by removing trailing anonymous module name parts (underscores) from both names.

typeOfConst :: QName -> TCM Type

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

relOfConst :: QName -> TCM Relevance

Get relevance 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

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 :: Defn -> Int

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

usesCopatterns :: QName -> TCM Bool

Check whether a definition uses copatterns.

applyDef :: ProjOrigin -> QName -> Arg Term -> TCM Term

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