| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Modality
Description
Modality.
Agda has support for several modalities, namely:
In order to type check such modalities, we must store the current modality in the typing context. This module provides functions to update the context based on a given modality.
Synopsis
- hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a
- workOnTypes :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
- workOnTypes' :: MonadTCEnv m => Bool -> m a -> m a
- applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a
- applyRelevanceToContextOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a
- applyRelevanceToJudgementOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a
- applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a
- applyQuantityToJudgement :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
- applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a
- applyCohesionToContextOnly :: MonadTCEnv tcm => Cohesion -> tcm a -> tcm a
- splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool
- applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a
- applyModalityToContextOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a
- applyModalityToJudgementOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a
- applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a
- wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a
Operations on Dom.
hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a Source #
Prepare parts of a parameter telescope for abstraction in constructors and projections.
Operations on Context.
workOnTypes :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a Source #
Modify the context whenever going from the l.h.s. (term side) of the typing judgement to the r.h.s. (type side).
workOnTypes' :: MonadTCEnv m => Bool -> m a -> m a Source #
Internal workhorse, expects value of --experimental-irrelevance flag as argument.
applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a Source #
(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
Also allow the use of irrelevant definitions.
applyRelevanceToContextOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a Source #
(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
Precondition: Relevance /= Relevant
applyRelevanceToJudgementOnly :: MonadTCEnv tcm => Relevance -> tcm a -> tcm a Source #
Apply relevance rel the the relevance annotation of the (typing/equality)
judgement. This is part of the work done when going into a rel-context.
Precondition: Relevance /= Relevant
applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a Source #
Like applyRelevanceToContext, but only act on context if
--irrelevant-projections.
See issue #2170.
applyQuantityToJudgement :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a Source #
Apply the quantity to the quantity annotation of the (typing/equality) judgement.
Precondition: The quantity must not be Quantity1 something
applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a Source #
Apply inverse composition with the given cohesion to the typing context.
applyCohesionToContextOnly :: MonadTCEnv tcm => Cohesion -> tcm a -> tcm a Source #
splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool Source #
Can we split on arguments of the given cohesion?
applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a Source #
(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
Also allow the use of irrelevant definitions.
This function might also do something for other modalities.
applyModalityToContextOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a Source #
(Conditionally) wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
This function might also do something for other modalities, but not for quantities.
Precondition: Modality /= Relevant
applyModalityToJudgementOnly :: MonadTCEnv tcm => Modality -> tcm a -> tcm a Source #
Apply the relevance and quantity components of the modality to the modality annotation of the (typing/equality) judgement.
Precondition: The relevance component must not be Relevant.
applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a Source #
Like applyModalityToContext, but only act on context (for Relevance) if
--irrelevant-projections.
See issue #2170.
wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a Source #
Wake up irrelevant variables and make them relevant. This is used
when type checking terms in a hole, in which case you want to be able to
(for instance) infer the type of an irrelevant variable. In the course
of type checking an irrelevant function argument applyRelevanceToContext
is used instead, which also sets the context relevance to Irrelevant.
This is not the right thing to do when type checking interactively in a
hole since it also marks all metas created during type checking as
irrelevant (issue #2568).
Also set the current quantity to 0.