- modifySignature :: (Signature -> Signature) -> TCM ()
- modifyImportedSignature :: (Signature -> Signature) -> TCM ()
- getSignature :: TCM Signature
- getImportedSignature :: TCM Signature
- setSignature :: Signature -> TCM ()
- setImportedSignature :: Signature -> TCM ()
- withSignature :: Signature -> TCM a -> TCM a
- addConstant :: QName -> Definition -> TCM ()
- makeProjection :: QName -> TCM ()
- addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
- addHaskellType :: QName -> HaskellType -> TCM ()
- addEpicCode :: QName -> EpicCode -> TCM ()
- addJSCode :: QName -> String -> TCM ()
- markStatic :: QName -> TCM ()
- unionSignatures :: [Signature] -> Signature
- addSection :: ModuleName -> Nat -> TCM ()
- lookupSection :: ModuleName -> TCM Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> TCM ()
- addDisplayForm :: QName -> DisplayForm -> TCM ()
- canonicalName :: QName -> TCM QName
- whatInduction :: QName -> TCM Induction
- singleConstructorType :: QName -> TCM Bool
- getConstInfo :: MonadTCM tcm => QName -> tcm Definition
- getPolarity :: QName -> TCM [Polarity]
- getPolarity' :: Comparison -> QName -> TCM [Polarity]
- setPolarity :: QName -> [Polarity] -> TCM ()
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: QName -> [Occurrence] -> TCM ()
- getSecFreeVars :: ModuleName -> TCM Nat
- getModuleFreeVars :: ModuleName -> TCM Nat
- getDefFreeVars :: QName -> TCM Nat
- freeVarsToApply :: QName -> TCM Args
- instantiateDef :: Definition -> TCM Definition
- makeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: TCM a -> TCM a
- inConcreteMode :: TCM a -> TCM a
- ignoreAbstractMode :: TCM a -> TCM a
- treatAbstractly :: QName -> TCM Bool
- treatAbstractly' :: QName -> TCEnv -> Bool
- typeOfConst :: QName -> TCM Type
- relOfConst :: QName -> TCM Relevance
- sortOfConst :: QName -> TCM Sort
- isProjection :: QName -> TCM (Maybe (QName, Int))
Documentation
setSignature :: Signature -> TCM ()Source
withSignature :: Signature -> TCM a -> TCM aSource
addConstant :: QName -> Definition -> TCM ()Source
Add a constant to the signature. Lifts the definition to top level.
makeProjection :: QName -> TCM ()Source
Turn a definition into a projection if it looks like a projection.
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()Source
addHaskellType :: QName -> HaskellType -> TCM ()Source
markStatic :: QName -> TCM ()Source
unionSignatures :: [Signature] -> SignatureSource
addSection :: ModuleName -> Nat -> TCM ()Source
Add a section to the signature.
lookupSection :: 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 :: ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> TCM ()Source
addDisplayForm :: QName -> DisplayForm -> TCM ()Source
canonicalName :: QName -> TCM QNameSource
whatInduction :: 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 :: QName -> TCM [Polarity]Source
Look up the polarity of a definition.
getPolarity' :: Comparison -> QName -> TCM [Polarity]Source
getArgOccurrence :: QName -> Nat -> TCM OccurrenceSource
setArgOccurrences :: QName -> [Occurrence] -> TCM ()Source
getSecFreeVars :: 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 :: ModuleName -> TCM NatSource
Compute the number of free variables of a module. This is the sum of the free variables of its sections.
getDefFreeVars :: 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 :: QName -> TCM ArgsSource
Compute the context variables to apply a definition to.
instantiateDef :: 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 :: TCM a -> TCM aSource
Enter abstract mode. Abstract definition in the current module are transparent.
inConcreteMode :: TCM a -> TCM aSource
Not in abstract mode. All abstract definitions are opaque.
ignoreAbstractMode :: TCM a -> TCM aSource
Ignore abstract mode. All abstract definitions are transparent.
treatAbstractly :: 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 :: QName -> TCM TypeSource
get type of a constant
relOfConst :: QName -> TCM RelevanceSource
get relevance of a constant
sortOfConst :: QName -> TCM SortSource
The name must be a datatype.