Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Monad.Signature

Synopsis

- modifySignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()
- modifyImportedSignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()
- getSignature :: MonadTCM tcm => tcm Signature
- getImportedSignature :: MonadTCM tcm => tcm Signature
- setSignature :: MonadTCM tcm => Signature -> tcm ()
- setImportedSignature :: MonadTCM tcm => Signature -> tcm ()
- withSignature :: MonadTCM tcm => Signature -> tcm a -> tcm a
- addConstant :: MonadTCM tcm => QName -> Definition -> tcm ()
- addHaskellCode :: MonadTCM tcm => QName -> HaskellType -> HaskellCode -> tcm ()
- addHaskellType :: MonadTCM tcm => QName -> HaskellType -> tcm ()
- addEpicCode :: MonadTCM tcm => QName -> EpicCode -> tcm ()
- unionSignatures :: [Signature] -> Signature
- addSection :: MonadTCM tcm => ModuleName -> Nat -> tcm ()
- lookupSection :: MonadTCM tcm => ModuleName -> tcm Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: MonadTCM tcm => ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> tcm ()
- addDisplayForm :: MonadTCM tcm => QName -> DisplayForm -> tcm ()
- canonicalName :: MonadTCM tcm => QName -> tcm QName
- whatInduction :: MonadTCM tcm => QName -> tcm Induction
- singleConstructorType :: QName -> TCM Bool
- getConstInfo :: MonadTCM tcm => QName -> tcm Definition
- getPolarity :: MonadTCM tcm => QName -> tcm [Polarity]
- getPolarity' :: MonadTCM tcm => Comparison -> QName -> tcm [Polarity]
- setPolarity :: MonadTCM tcm => QName -> [Polarity] -> tcm ()
- getArgOccurrence :: MonadTCM tcm => QName -> Nat -> tcm Occurrence
- setArgOccurrences :: MonadTCM tcm => QName -> [Occurrence] -> tcm ()
- getSecFreeVars :: MonadTCM tcm => ModuleName -> tcm Nat
- getModuleFreeVars :: MonadTCM tcm => ModuleName -> tcm Nat
- getDefFreeVars :: MonadTCM tcm => QName -> tcm Nat
- freeVarsToApply :: MonadTCM tcm => QName -> tcm Args
- instantiateDef :: MonadTCM tcm => Definition -> tcm Definition
- makeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: MonadTCM tcm => tcm a -> tcm a
- inConcreteMode :: MonadTCM tcm => tcm a -> tcm a
- ignoreAbstractMode :: MonadTCM tcm => tcm a -> tcm a
- treatAbstractly :: MonadTCM tcm => QName -> tcm Bool
- treatAbstractly' :: QName -> TCEnv -> Bool
- typeOfConst :: MonadTCM tcm => QName -> tcm Type
- relOfConst :: MonadTCM tcm => QName -> tcm Relevance
- sortOfConst :: MonadTCM tcm => QName -> tcm Sort
- isProjection :: MonadTCM tcm => QName -> tcm (Maybe Int)

# Documentation

modifySignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()

modifyImportedSignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()

getSignature :: MonadTCM tcm => tcm Signature

getImportedSignature :: MonadTCM tcm => tcm Signature

setSignature :: MonadTCM tcm => Signature -> tcm ()

setImportedSignature :: MonadTCM tcm => Signature -> tcm ()

withSignature :: MonadTCM tcm => Signature -> tcm a -> tcm a

addConstant :: MonadTCM tcm => QName -> Definition -> tcm ()

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

addHaskellCode :: MonadTCM tcm => QName -> HaskellType -> HaskellCode -> tcm ()

addHaskellType :: MonadTCM tcm => QName -> HaskellType -> tcm ()

addEpicCode :: MonadTCM tcm => QName -> EpicCode -> tcm ()

unionSignatures :: [Signature] -> Signature

addSection :: MonadTCM tcm => ModuleName -> Nat -> tcm ()

Add a section to the signature.

lookupSection :: MonadTCM tcm => ModuleName -> tcm Telescope

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

addDisplayForms :: QName -> TCM ()

applySection :: MonadTCM tcm => ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> tcm ()

addDisplayForm :: MonadTCM tcm => QName -> DisplayForm -> tcm ()

canonicalName :: MonadTCM tcm => QName -> tcm 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.

getConstInfo :: MonadTCM tcm => QName -> tcm Definition

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

getPolarity :: MonadTCM tcm => QName -> tcm [Polarity]

Look up the polarity of a definition.

getPolarity' :: MonadTCM tcm => Comparison -> QName -> tcm [Polarity]

setPolarity :: MonadTCM tcm => QName -> [Polarity] -> tcm ()

Set the polarity of a definition.

getArgOccurrence :: MonadTCM tcm => QName -> Nat -> tcm Occurrence

setArgOccurrences :: MonadTCM tcm => QName -> [Occurrence] -> tcm ()

getSecFreeVars :: MonadTCM tcm => 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 :: MonadTCM tcm => ModuleName -> tcm Nat

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

getDefFreeVars :: MonadTCM tcm => 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 :: MonadTCM tcm => QName -> tcm Args

Compute the context variables to apply a definition to.

instantiateDef :: MonadTCM tcm => 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 :: MonadTCM tcm => tcm a -> tcm a

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

inConcreteMode :: MonadTCM tcm => tcm a -> tcm a

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCM tcm => tcm a -> tcm a

Ignore abstract mode. All abstract definitions are transparent.

treatAbstractly :: MonadTCM tcm => QName -> tcm 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 :: MonadTCM tcm => QName -> tcm Type

get type of a constant

relOfConst :: MonadTCM tcm => QName -> tcm Relevance

get relevance of a constant

sortOfConst :: MonadTCM tcm => QName -> tcm Sort

The name must be a datatype.

isProjection :: MonadTCM tcm => QName -> tcm (Maybe Int)

Is it the name of a record projection?