| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Monad.Signature
- addConstant :: QName -> Definition -> TCM ()
- setTerminates :: QName -> Bool -> TCM ()
- modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
- addClauses :: QName -> [Clause] -> TCM ()
- ensureNoCompiledHaskell :: QName -> TCM ()
- addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
- addHaskellExport :: QName -> HaskellType -> String -> TCM ()
- addHaskellType :: QName -> HaskellType -> TCM ()
- addEpicCode :: QName -> EpicCode -> TCM ()
- addJSCode :: QName -> String -> TCM ()
- addCoreCode :: QName -> CoreExpr -> TCM ()
- addCoreConstr :: QName -> CoreConstr -> TCM ()
- addCoreType :: QName -> CoreType -> TCM ()
- markNoSmashing :: QName -> TCM ()
- markStatic :: QName -> TCM ()
- markInline :: QName -> TCM ()
- unionSignatures :: [Signature] -> Signature
- addSection :: ModuleName -> TCM ()
- lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: ModuleName -> Telescope -> ModuleName -> Args -> Ren QName -> Ren ModuleName -> TCM ()
- applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> Ren QName -> Ren ModuleName -> TCM ()
- addDisplayForm :: QName -> DisplayForm -> TCM ()
- getDisplayForms :: QName -> TCM [Open DisplayForm]
- chaseDisplayForms :: QName -> TCM (Set QName)
- hasLoopingDisplayForm :: QName -> TCM Bool
- canonicalName :: QName -> TCM QName
- sameDef :: QName -> QName -> TCM (Maybe QName)
- whatInduction :: QName -> TCM Induction
- singleConstructorType :: QName -> TCM Bool
- class (Functor m, Applicative m, Monad m) => HasConstInfo m where
- getConstInfo :: QName -> m Definition
- getRewriteRulesFor :: QName -> m RewriteRules
- defaultGetRewriteRulesFor :: Monad m => m TCState -> QName -> m RewriteRules
- getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
- getPolarity :: QName -> TCM [Polarity]
- getPolarity' :: Comparison -> QName -> TCM [Polarity]
- setPolarity :: QName -> [Polarity] -> TCM ()
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: QName -> [Occurrence] -> TCM ()
- modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
- setTreeless :: QName -> TTerm -> TCM ()
- setCompiledArgUse :: QName -> [Bool] -> TCM ()
- getCompiled :: QName -> TCM (Maybe Compiled)
- getTreeless :: QName -> TCM (Maybe TTerm)
- getCompiledArgUse :: QName -> TCM [Bool]
- getMutual :: QName -> TCM [QName]
- setMutual :: QName -> [QName] -> TCM ()
- mutuallyRecursive :: QName -> QName -> TCM Bool
- getSection :: ModuleName -> TCM (Maybe Section)
- getCurrentModuleFreeVars :: TCM Nat
- getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => QName -> m Nat
- freeVarsToApply :: QName -> TCM Args
- inFreshModuleIfFreeParams :: TCM a -> TCM a
- instantiateDef :: Definition -> TCM Definition
- makeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: TCM a -> TCM a
- inConcreteMode :: TCM a -> TCM a
- ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
- inConcreteOrAbstractMode :: QName -> TCM a -> TCM a
- treatAbstractly :: MonadReader TCEnv m => QName -> m Bool
- treatAbstractly' :: QName -> TCEnv -> Bool
- typeOfConst :: QName -> TCM Type
- relOfConst :: QName -> TCM Relevance
- sortOfConst :: QName -> TCM Sort
- defPars :: Definition -> Int
- droppedPars :: Definition -> Int
- isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
- isProjection_ :: Defn -> Maybe Projection
- isStaticFun :: Defn -> Bool
- isInlineFun :: Defn -> Bool
- isProperProjection :: Defn -> Bool
- projectionArgs :: Defn -> Int
- usesCopatterns :: QName -> TCM Bool
- applyDef :: QName -> Arg Term -> TCM Term
Documentation
addConstant :: QName -> Definition -> TCM () Source
Add a constant to the signature. Lifts the definition to top level.
setTerminates :: QName -> Bool -> TCM () Source
Set termination info of a defined function symbol.
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () Source
Modify the clauses of a function.
addClauses :: QName -> [Clause] -> TCM () Source
Lifts clauses to the top-level and adds them to definition.
ensureNoCompiledHaskell :: QName -> TCM () Source
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM () Source
addHaskellExport :: QName -> HaskellType -> String -> TCM () Source
addHaskellType :: QName -> HaskellType -> TCM () Source
addEpicCode :: QName -> EpicCode -> TCM () Source
addCoreCode :: QName -> CoreExpr -> TCM () Source
addCoreConstr :: QName -> CoreConstr -> TCM () Source
addCoreType :: QName -> CoreType -> TCM () Source
markNoSmashing :: QName -> TCM () Source
markStatic :: QName -> TCM () Source
markInline :: QName -> TCM () Source
unionSignatures :: [Signature] -> Signature Source
addSection :: ModuleName -> TCM () Source
Add a section to the signature.
The current context will be stored as the cumulative module parameters for this section.
lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope Source
Lookup a section. If it doesn't exist that just means that the module wasn't parameterised.
addDisplayForms :: QName -> TCM () Source
Arguments
| :: 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).
applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> Ren QName -> Ren ModuleName -> TCM () Source
addDisplayForm :: QName -> DisplayForm -> TCM () Source
Add a display form to a definition (could be in this or imported signature).
getDisplayForms :: QName -> TCM [Open DisplayForm] Source
chaseDisplayForms :: QName -> TCM (Set QName) Source
Find all names used (recursively) by display forms of a given name.
hasLoopingDisplayForm :: QName -> TCM Bool Source
Check if a display form is looping.
canonicalName :: QName -> TCM 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 (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
setTreeless :: QName -> TTerm -> TCM () Source
setCompiledArgUse :: QName -> [Bool] -> TCM () Source
getCompiledArgUse :: QName -> TCM [Bool] Source
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.
getCurrentModuleFreeVars :: TCM Nat Source
Get the number of parameters to the current module.
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => QName -> m Nat Source
Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).
freeVarsToApply :: QName -> TCM Args Source
Compute the context variables to apply a definition to.
We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)
Example:
module M₁ Γ where
module M₁ Δ where
f = ...
module M₃ Θ where
... M₁.M₂.f [insert Γ raised by Θ]
inFreshModuleIfFreeParams :: TCM a -> TCM a Source
Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.
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.
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
isStaticFun :: Defn -> Bool Source
Is it a function marked STATIC?
isInlineFun :: Defn -> Bool Source
Is it a function marked INLINE?
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.