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

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

canonicalName :: QName -> TCM QName Source

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

whatInduction :: QName -> TCM Induction Source

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

singleConstructorType :: QName -> TCM Bool Source

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 Source

Methods

getConstInfo :: QName -> m Definition Source

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

getRewriteRulesFor :: QName -> m RewriteRules Source

Lookup the rewrite rules with the given head symbol.

Instances

HasConstInfo Unify Source
HasConstInfo (TCMT IO) Source
(HasConstInfo m, Error err) => HasConstInfo (ExceptionT err m) Source

defaultGetRewriteRulesFor :: Monad m => m TCState -> QName -> m RewriteRules Source

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

getPolarity :: QName -> TCM [Polarity] Source

Look up the polarity of a definition.

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

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

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

Set the polarity of a definition.

getArgOccurrence :: QName -> Nat -> TCM Occurrence Source

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

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

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

getMutual :: QName -> TCM [QName] Source

Get the mutually recursive identifiers.

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

Set the mutually recursive identifiers.

mutuallyRecursive :: QName -> QName -> TCM Bool Source

Check whether two definitions are mutually recursive.

getSection :: ModuleName -> TCM (Maybe Section) Source

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 Source

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 Source

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

getDefFreeVars :: QName -> TCM Nat Source

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 Source

Compute the context variables to apply a definition to.

instantiateDef :: Definition -> TCM Definition Source

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

makeAbstract :: Definition -> Maybe Definition Source

Give the abstract view of a definition.

inAbstractMode :: TCM a -> TCM a Source

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

inConcreteMode :: TCM a -> TCM a Source

Not in abstract mode. All abstract definitions are opaque.

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

Ignore abstract mode. All abstract definitions are transparent.

inConcreteOrAbstractMode :: QName -> TCM a -> TCM a Source

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

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

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 Source

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 Source

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

relOfConst :: QName -> TCM Relevance Source

Get relevance of a constant.

colOfConst :: QName -> TCM [Color] Source

Get colors of a constant.

sortOfConst :: QName -> TCM Sort Source

The name must be a datatype.

defPars :: Definition -> Int Source

The number of parameters of a definition.

droppedPars :: Definition -> Int Source

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

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

Is it the name of a record projection?

isProjection_ :: Defn -> Maybe Projection Source

isProperProjection :: Defn -> Bool Source

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 Source

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

usesCopatterns :: QName -> TCM Bool Source

Check whether a definition uses copatterns.

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

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

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

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.