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

Safe Haskell | None

Agda.TypeChecking.Monad.Signature

Contents

- modifiers for parts of the signature

Synopsis

- 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
- updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
- updateTheDef :: (Defn -> Defn) -> Definition -> Definition
- updateDefType :: (Type -> Type) -> Definition -> Definition
- updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition
- updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition
- updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> Definition -> Definition
- addConstant :: QName -> Definition -> TCM ()
- setTerminates :: QName -> Bool -> 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 ()
- getArgOccurrences :: QName -> TCM [Occurrence]
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: QName -> [Occurrence] -> TCM ()
- getMutual :: QName -> TCM [QName]
- setMutual :: QName -> [QName] -> TCM ()
- mutuallyRecursive :: QName -> QName -> TCM Bool
- 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

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

# modifiers for parts of the signature

updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature

updateTheDef :: (Defn -> Defn) -> Definition -> Definition

updateDefType :: (Type -> Type) -> Definition -> Definition

updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition

updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition

updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> Definition -> Definition

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.

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

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 :: ModuleName -> Telescope -> ModuleName -> Args -> Map QName QName -> Map ModuleName ModuleName -> TCM ()

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

canonicalName :: QName -> TCM 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.

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

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

Ignore abstract mode. All abstract definitions are transparent.

treatAbstractly :: 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 :: QName -> TCM Type

get type of a constant

relOfConst :: QName -> TCM Relevance

get relevance of a constant

sortOfConst :: QName -> TCM Sort

The name must be a datatype.

isProjection :: QName -> TCM (Maybe (QName, Int))

Is it the name of a record projection?