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.

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

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

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

addEpicCode :: QName -> EpicCode -> TCM ()

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

markStatic :: QName -> TCM ()

unionSignatures :: [Signature] -> Signature

addSection :: ModuleName -> Nat -> TCM ()

Add a section to the signature.

lookupSection :: ModuleName -> TCM Telescope

Lookup a section. If it doesn't exist that just means that the module wasn't parameterised.

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.

-> Ren QName

Imported names (given as renaming).

-> Ren ModuleName

Imported modules (given as renaming).

-> TCM ()

Module application (followed by module parameter abstraction).

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

canonicalName :: QName -> TCM QName

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

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

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

Methods

getConstInfo :: QName -> m Definition

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

Instances

HasConstInfo ReduceM

HasConstInfo Unify

HasConstInfo (TCMT IO)

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.

getArgOccurrences :: QName -> TCM [Occurrence]

Return a finite list of argument occurrences.

getArgOccurrence :: QName -> Nat -> TCM Occurrence

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

getMutual :: QName -> TCM [QName]

Get the mutually recursive identifiers.

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

Set the mutually recursive identifiers.

mutuallyRecursive :: QName -> QName -> TCM Bool

Check whether two definitions are mutually recursive.

getSection :: ModuleName -> TCM (Maybe 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.

getSecFreeVars :: ModuleName -> TCM Nat

Look up the number of free variables of a section. This is equal to the number of parameters if we're currently inside the section and 0 otherwise.

getModuleFreeVars :: ModuleName -> TCM Nat

Compute the number of free variables of a module. This is the sum of the free variables of its sections.

getDefFreeVars :: QName -> TCM Nat

Compute the number of free variables of a defined name. This is the sum of the free variables of the sections it's contained in.

freeVarsToApply :: QName -> TCM Args

Compute the context variables to apply a definition to.

instantiateDef :: Definition -> TCM Definition

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

makeAbstract :: Definition -> Maybe Definition

Give the abstract view of a definition.

inAbstractMode :: TCM a -> TCM a

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

inConcreteMode :: TCM a -> TCM 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.

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

typeOfConst :: QName -> TCM Type

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

relOfConst :: QName -> TCM Relevance

Get relevance of a constant.

colOfConst :: QName -> TCM [Color]

Get colors of a constant.

sortOfConst :: QName -> TCM Sort

The name must be a datatype.

isProjection :: QName -> TCM (Maybe Projection)

Is it the name of a record projection?

isProjection_ :: Defn -> Maybe Projection

isProperProjection :: Defn -> Bool

projectionArgs :: Defn -> Int

Number of dropped initial arguments.

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

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

getDefType :: QName -> Type -> TCM (Maybe Type)

getDefType f t computes the type of (possibly projection-(like)) function t whose first argument has type t. The parameters for f are extracted from t. Nothing if f is projection(like) but t is not a datarecordaxiom type.

Precondition: t is reduced.

See also: getConType