{-# OPTIONS_GHC -Wunused-imports #-}

{- | 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".
-}

module Agda.TypeChecking.Monad.Modality where

import qualified Data.Map as Map

import Agda.Interaction.Options

import Agda.Syntax.Common

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Env

import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.Monad

-- | data 'Relevance'
--   see "Agda.Syntax.Common".

-- * Operations on 'Dom'.

-- | Prepare parts of a parameter telescope for abstraction in constructors
--   and projections.
hideAndRelParams :: (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams :: forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams = a -> a
forall a. LensHiding a => a -> a
hideOrKeepInstance (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Relevance -> Relevance) -> a -> a
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
nonStrictToIrr

-- * Operations on 'Context'.

-- | 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, HasOptions m, MonadDebug m)
            => m a -> m a
workOnTypes :: forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes m a
cont = do
  Bool
allowed <- PragmaOptions -> Bool
optExperimentalIrrelevance (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.irr" VerboseLevel
60 VerboseKey
"workOnTypes" (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
workOnTypes' Bool
allowed m a
cont

-- | Internal workhorse, expects value of --experimental-irrelevance flag
--   as argument.
workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a
workOnTypes' :: forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
workOnTypes' Bool
experimental
  = Bool -> (m a -> m a) -> m a -> m a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental ((forall e. Dom e -> Dom e) -> m a -> m a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo ((forall e. Dom e -> Dom e) -> m a -> m a)
-> (forall e. Dom e -> Dom e) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ (Relevance -> Relevance) -> Dom e -> Dom e
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict)
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> m a -> m a
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
zeroQuantity
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
typeLevelReductions
  (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envWorkingOnTypes = True })

-- | (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.
applyRelevanceToContext :: (MonadTCEnv tcm, LensRelevance r) => r -> tcm a -> tcm a
applyRelevanceToContext :: forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext r
thing =
  case r -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance r
thing of
    Relevance
Relevant -> tcm a -> tcm a
forall a. a -> a
id
    Relevance
rel      -> Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly   Relevance
rel
              (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly Relevance
rel

-- | (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@
applyRelevanceToContextOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly Relevance
rel = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
forall o i. Lens' o i -> LensMap o i
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
Lens' TCEnv [ContextEntry]
eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Relevance -> ContextEntry -> ContextEntry
forall a. LensRelevance a => Relevance -> a -> a
inverseApplyRelevance Relevance
rel)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv (Map Name (Open LetBinding))
-> LensMap TCEnv (Map Name (Open LetBinding))
forall o i. Lens' o i -> LensMap o i
over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings ((Open LetBinding -> Open LetBinding)
-> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
forall a b. (a -> b) -> Open a -> Open b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
-> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
-> (Dom Type -> Dom Type)
-> Open LetBinding
-> Open LetBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType ((Dom Type -> Dom Type)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall a b. (a -> b) -> a -> b
$ Relevance -> Dom Type -> Dom Type
forall a. LensRelevance a => Relevance -> a -> a
inverseApplyRelevance Relevance
rel)

-- | 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@
applyRelevanceToJudgementOnly :: (MonadTCEnv tcm) => Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Relevance -> TCEnv -> TCEnv) -> Relevance -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv Relevance -> LensMap TCEnv Relevance
forall o i. Lens' o i -> LensMap o i
over (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance LensMap TCEnv Relevance
-> (Relevance -> Relevance -> Relevance)
-> Relevance
-> TCEnv
-> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance

-- | Like 'applyRelevanceToContext', but only act on context if
--   @--irrelevant-projections@.
--   See issue #2170.
applyRelevanceToContextFunBody :: (MonadTCM tcm, LensRelevance r) => r -> tcm a -> tcm a
applyRelevanceToContextFunBody :: forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContextFunBody r
thing tcm a
cont =
  case r -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance r
thing of
    Relevance
Relevant -> tcm a
cont
    Relevance
rel -> tcm Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b (m :: * -> *) a.
(IsBool b, Monad m) =>
m b -> (m a -> m a) -> m a -> m a
applyWhenM (PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool) -> tcm PragmaOptions -> tcm Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      (Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly Relevance
rel) (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$    -- enable local irr. defs only when option
      Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly Relevance
rel tcm a
cont -- enable global irr. defs alway

-- | Apply the quantity to the quantity annotation of the
-- (typing/equality) judgement.
--
-- Precondition: The quantity must not be @'Quantity1' something@.
applyQuantityToJudgement ::
  (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
applyQuantityToJudgement :: forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement =
  (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (q -> TCEnv -> TCEnv) -> q -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv Quantity -> LensMap TCEnv Quantity
forall o i. Lens' o i -> LensMap o i
over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity LensMap TCEnv Quantity
-> (q -> Quantity -> Quantity) -> q -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity (Quantity -> Quantity -> Quantity)
-> (q -> Quantity) -> q -> Quantity -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. q -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity

-- | Apply inverse composition with the given cohesion to the typing context.
applyCohesionToContext :: (MonadTCEnv tcm, LensCohesion m) => m -> tcm a -> tcm a
applyCohesionToContext :: forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext m
thing =
  case m -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion m
thing of
    Cohesion
m | Cohesion
m Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
unitCohesion -> tcm a -> tcm a
forall a. a -> a
id
      | Bool
otherwise         -> Cohesion -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Cohesion -> tcm a -> tcm a
applyCohesionToContextOnly   Cohesion
m
                             -- Cohesion does not apply to the judgment.

applyCohesionToContextOnly :: (MonadTCEnv tcm) => Cohesion -> tcm a -> tcm a
applyCohesionToContextOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Cohesion -> tcm a -> tcm a
applyCohesionToContextOnly Cohesion
q = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
forall o i. Lens' o i -> LensMap o i
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
Lens' TCEnv [ContextEntry]
eContext     ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Cohesion -> ContextEntry -> ContextEntry
forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion Cohesion
q)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv (Map Name (Open LetBinding))
-> LensMap TCEnv (Map Name (Open LetBinding))
forall o i. Lens' o i -> LensMap o i
over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings ((Open LetBinding -> Open LetBinding)
-> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
forall a b. (a -> b) -> Open a -> Open b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
-> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
-> (Dom Type -> Dom Type)
-> Open LetBinding
-> Open LetBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType ((Dom Type -> Dom Type)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall a b. (a -> b) -> a -> b
$ Cohesion -> Dom Type -> Dom Type
forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion Cohesion
q)

-- | Can we split on arguments of the given cohesion?
splittableCohesion :: (HasOptions m, LensCohesion a) => a -> m Bool
splittableCohesion :: forall (m :: * -> *) a.
(HasOptions m, LensCohesion a) =>
a -> m Bool
splittableCohesion a
a = do
  let c :: Cohesion
c = a -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion a
a
  Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cohesion -> Bool
forall a. LensCohesion a => a -> Bool
usableCohesion Cohesion
c) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cohesion
c Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Cohesion
Flat) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do PragmaOptions -> Bool
optFlatSplit (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)

-- | (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.
applyModalityToContext :: (MonadTCEnv tcm, LensModality m) => m -> tcm a -> tcm a
applyModalityToContext :: forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext m
thing =
  case m -> Modality
forall a. LensModality a => a -> Modality
getModality m
thing of
    Modality
m | Modality
m Modality -> Modality -> Bool
forall a. Eq a => a -> a -> Bool
== Modality
unitModality -> tcm a -> tcm a
forall a. a -> a
id
      | Bool
otherwise         -> Modality -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Modality -> tcm a -> tcm a
applyModalityToContextOnly   Modality
m
                           (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Modality -> tcm a -> tcm a
applyModalityToJudgementOnly Modality
m

-- | (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@
applyModalityToContextOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
applyModalityToContextOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Modality -> tcm a -> tcm a
applyModalityToContextOnly Modality
m = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv [ContextEntry] -> LensMap TCEnv [ContextEntry]
forall o i. Lens' o i -> LensMap o i
over ([ContextEntry] -> f [ContextEntry]) -> TCEnv -> f TCEnv
Lens' TCEnv [ContextEntry]
eContext ((ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ((ContextEntry -> ContextEntry)
 -> [ContextEntry] -> [ContextEntry])
-> (ContextEntry -> ContextEntry)
-> [ContextEntry]
-> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Modality -> ContextEntry -> ContextEntry
forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCEnv (Map Name (Open LetBinding))
-> LensMap TCEnv (Map Name (Open LetBinding))
forall o i. Lens' o i -> LensMap o i
over (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings
      ((Open LetBinding -> Open LetBinding)
-> Map Name (Open LetBinding) -> Map Name (Open LetBinding)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding
forall a b. (a -> b) -> Open a -> Open b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LetBinding -> LetBinding) -> Open LetBinding -> Open LetBinding)
-> ((Dom Type -> Dom Type) -> LetBinding -> LetBinding)
-> (Dom Type -> Dom Type)
-> Open LetBinding
-> Open LetBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType ((Dom Type -> Dom Type)
 -> Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> (Dom Type -> Dom Type)
-> Map Name (Open LetBinding)
-> Map Name (Open LetBinding)
forall a b. (a -> b) -> a -> b
$ Modality -> Dom Type -> Dom Type
forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)

-- | 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'.
applyModalityToJudgementOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
applyModalityToJudgementOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Modality -> tcm a -> tcm a
applyModalityToJudgementOnly Modality
m =
  (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a. (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (TCEnv -> TCEnv) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv Relevance -> LensMap TCEnv Relevance
forall o i. Lens' o i -> LensMap o i
over (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance (Relevance -> Relevance -> Relevance
composeRelevance (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)) (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            Lens' TCEnv Quantity -> LensMap TCEnv Quantity
forall o i. Lens' o i -> LensMap o i
over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity  (Quantity -> Quantity -> Quantity
composeQuantity  (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
m))

-- | Like 'applyModalityToContext', but only act on context (for Relevance) if
--   @--irrelevant-projections@.
--   See issue #2170.
applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r) => r -> tcm a -> tcm a
applyModalityToContextFunBody :: forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody r
thing tcm a
cont = do
    tcm Bool -> tcm a -> tcm a -> tcm a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool) -> tcm PragmaOptions -> tcm Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      {-then-} (Modality -> tcm a -> tcm a
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
m tcm a
cont)                -- enable global irr. defs always
      {-else-} (Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContextFunBody (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)
               (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Cohesion -> tcm a -> tcm a
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
m)
               (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ Quantity -> tcm a -> tcm a
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
m) tcm a
cont) -- enable local irr. defs only when option
  where
    m :: Modality
m = r -> Modality
forall a. LensModality a => a -> Modality
getModality r
thing

-- | 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.
wakeIrrelevantVars :: (MonadTCEnv tcm) => tcm a -> tcm a
wakeIrrelevantVars :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
wakeIrrelevantVars
  = Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly Relevance
Irrelevant
  (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> tcm a -> tcm a
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
zeroQuantity