{-# 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 = forall a. LensHiding a => a -> a
hideOrKeepInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.irr" VerboseLevel
60 VerboseKey
"workOnTypes" forall a b. (a -> b) -> a -> b
$ 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
  = forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
experimental (forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
zeroQuantity
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
typeLevelReductions
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envWorkingOnTypes :: Bool
envWorkingOnTypes = Bool
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 forall a. LensRelevance a => a -> Relevance
getRelevance r
thing of
    Relevance
Relevant -> forall a. a -> a
id
    Relevance
rel      -> forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly   Relevance
rel
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Context
eContext     (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => Relevance -> a -> a
inverseApplyRelevance Relevance
rel)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv LetBindings
eLetBindings (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Relevance
eRelevance 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 forall a. LensRelevance a => a -> Relevance
getRelevance r
thing of
    Relevance
Relevant -> tcm a
cont
    Relevance
rel -> forall b (m :: * -> *) a.
(IsBool b, Monad m) =>
m b -> (m a -> m a) -> m a -> m a
applyWhenM (PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      (forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly Relevance
rel) forall a b. (a -> b) -> a -> b
$    -- enable local irr. defs only when option
      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 =
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Quantity
eQuantity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. LensCohesion a => a -> Cohesion
getCohesion m
thing of
    Cohesion
m | Cohesion
m forall a. Eq a => a -> a -> Bool
== Cohesion
unitCohesion -> forall a. a -> a
id
      | Bool
otherwise         -> 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Context
eContext     (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion Cohesion
q)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv LetBindings
eLetBindings (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType forall a b. (a -> b) -> a -> b
$ 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 = forall a. LensCohesion a => a -> Cohesion
getCohesion a
a
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. LensCohesion a => a -> Bool
usableCohesion Cohesion
c) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cohesion
c forall a. Eq a => a -> a -> Bool
/= Cohesion
Flat) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do PragmaOptions -> Bool
optFlatSplit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)


{-# SPECIALIZE applyModalityToContext :: Modality -> TCM a -> TCM a #-}
-- | (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 forall a. LensModality a => a -> Modality
getModality m
thing of
    Modality
m | Modality
m forall a. Eq a => a -> a -> Bool
== Modality
unitModality -> forall a. a -> a
id
      | Bool
otherwise         -> forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Modality -> tcm a -> tcm a
applyModalityToContextOnly   Modality
m
                           forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC
  forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Context
eContext (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv LetBindings
eLetBindings
      (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> LetBinding -> LetBinding
onLetBindingType forall a b. (a -> b) -> a -> b
$ 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 =
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Relevance
eRelevance (Relevance -> Relevance -> Relevance
composeRelevance (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall o i. Lens' o i -> LensMap o i
over Lens' TCEnv Quantity
eQuantity  (Quantity -> Quantity -> Quantity
composeQuantity  (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
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
      {-then-} (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-} (forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContextFunBody (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)
               forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext (forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
m)
               forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement (forall a. LensQuantity a => a -> Quantity
getQuantity Modality
m) tcm a
cont) -- enable local irr. defs only when option
  where
    m :: Modality
m = 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
  = forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToContextOnly Relevance
Irrelevant
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
zeroQuantity