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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Modality

Contents

- Operations on `Dom`.
- Operations on `Context`.

Description

Modality.

Agda has support for several modalities, namely:

- `Cohesion`
- `Quantity`
- `Relevance`

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.

See Agda.TypeChecking.Irrelevance.

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
- applyPolarityToContext :: (MonadTCEnv tcm, LensModalPolarity p) => p -> tcm a -> tcm 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.

applyPolarityToContext :: (MonadTCEnv tcm, LensModalPolarity p) => p -> tcm a -> tcm a Source #

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.