Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 ()
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
sortOfConst :: MonadTCM tcm => QName -> tcm Sort
Documentation
modifySignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()Source
modifyImportedSignature :: MonadTCM tcm => (Signature -> Signature) -> tcm ()Source
getSignature :: MonadTCM tcm => tcm SignatureSource
getImportedSignature :: MonadTCM tcm => tcm SignatureSource
setSignature :: MonadTCM tcm => Signature -> tcm ()Source
setImportedSignature :: MonadTCM tcm => Signature -> tcm ()Source
withSignature :: MonadTCM tcm => Signature -> tcm a -> tcm aSource
addConstant :: MonadTCM tcm => QName -> Definition -> tcm ()Source
Add a constant to the signature. Lifts the definition to top level.
addHaskellCode :: MonadTCM tcm => QName -> HaskellType -> HaskellCode -> tcm ()Source
addHaskellType :: MonadTCM tcm => QName -> HaskellType -> tcm ()Source
unionSignatures :: [Signature] -> SignatureSource
addSection :: MonadTCM tcm => ModuleName -> Nat -> tcm ()Source
Add a section to the signature.
lookupSection :: MonadTCM tcm => ModuleName -> tcm TelescopeSource
Lookup a section. If it doesn't exist that just means that the module wasn't parameterised.
addDisplayForms :: QName -> TCM ()Source
applySection :: MonadTCM tcm => ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> tcm ()Source
addDisplayForm :: MonadTCM tcm => QName -> DisplayForm -> tcm ()Source
canonicalName :: MonadTCM tcm => QName -> tcm QNameSource
whatInduction :: MonadTCM tcm => QName -> tcm InductionSource
Can be called on either a (co)datatype, a record type or a (co)constructor.
singleConstructorType :: QName -> TCM BoolSource

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

Precondition: The name has to refer to a constructor.

getConstInfo :: MonadTCM tcm => QName -> tcm DefinitionSource
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]Source
Look up the polarity of a definition.
getPolarity' :: MonadTCM tcm => Comparison -> QName -> tcm [Polarity]Source
setPolarity :: MonadTCM tcm => QName -> [Polarity] -> tcm ()Source
Set the polarity of a definition.
getArgOccurrence :: MonadTCM tcm => QName -> Nat -> tcm OccurrenceSource
setArgOccurrences :: MonadTCM tcm => QName -> [Occurrence] -> tcm ()Source
getSecFreeVars :: MonadTCM tcm => ModuleName -> tcm NatSource
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 NatSource
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 NatSource
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 ArgsSource
Compute the context variables to apply a definition to.
instantiateDef :: MonadTCM tcm => Definition -> tcm DefinitionSource
Instantiate a closed definition with the correct part of the current context.
makeAbstract :: Definition -> Maybe DefinitionSource
Give the abstract view of a definition.
inAbstractMode :: MonadTCM tcm => tcm a -> tcm aSource
Enter abstract mode. Abstract definition in the current module are transparent.
inConcreteMode :: MonadTCM tcm => tcm a -> tcm aSource
Not in abstract mode. All abstract definitions are opaque.
ignoreAbstractMode :: MonadTCM tcm => tcm a -> tcm aSource
Ignore abstract mode. All abstract definitions are transparent.
treatAbstractly :: MonadTCM tcm => QName -> tcm BoolSource
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 -> BoolSource
typeOfConst :: MonadTCM tcm => QName -> tcm TypeSource
get type of a constant
sortOfConst :: MonadTCM tcm => QName -> tcm SortSource
The name must be a datatype.
Produced by Haddock version 2.6.0