{-# OPTIONS_GHC -Wunused-imports #-}
-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -dno-suppress-type-signatures -ddump-to-file -dno-typeable-binds #-}

{- | 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.Syntax.Internal

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Constraints (MonadConstraint, solveConstraint)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Env
import {-# SOURCE #-} Agda.TypeChecking.Rewriting (checkRewConstraint)

import Agda.Utils.Function
import Agda.Utils.Monad
import Agda.Utils.ExpandCase

-- | 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
shapeIrrelevantToIrrelevant

-- * Operations on 'Context'.


{-# INLINE workOnTypes #-}
-- | 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
  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
  verboseBracket "tc.irr" 60 "workOnTypes" $ workOnTypes' allowed cont

{-# INLINE workOnTypes' #-}
-- | 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
irrelevantToShapeIrrelevant)
  (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
. PolarityModality -> m a -> m a
forall (tcm :: * -> *) p a.
(MonadTCEnv tcm, LensModalPolarity p) =>
p -> tcm a -> tcm a
applyPolarityToContext (ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
UnusedPolarity)
  (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 (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
eWorkingOnTypes Bool
True)

applyPolarityToContext :: (MonadTCEnv tcm, LensModalPolarity p) => p -> tcm a -> tcm a
applyPolarityToContext :: forall (tcm :: * -> *) p a.
(MonadTCEnv tcm, LensModalPolarity p) =>
p -> tcm a -> tcm a
applyPolarityToContext p
p = (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
$ ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext     ((ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ PolarityModality -> ContextEntry -> ContextEntry
forall a. LensModalPolarity a => PolarityModality -> a -> a
inverseApplyPolarity PolarityModality
pol)
  (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv LetBindings LetBindings
-> (LetBindings -> LetBindings) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv LetBindings LetBindings
Lens' TCEnv LetBindings
eLetBindings ((Open LetBinding -> Open LetBinding) -> LetBindings -> LetBindings
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> LetBindings -> LetBindings)
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> LetBindings
-> LetBindings
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) -> LetBindings -> LetBindings)
-> (Dom Type -> Dom Type) -> LetBindings -> LetBindings
forall a b. (a -> b) -> a -> b
$ PolarityModality -> Dom Type -> Dom Type
forall a. LensModalPolarity a => PolarityModality -> a -> a
inverseApplyPolarity PolarityModality
pol)
  where
    pol :: PolarityModality
pol = p -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity p
p

-- | (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 =
  Bool -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant Relevance
rel)
   ((tcm a -> tcm a) -> tcm a -> tcm a)
-> (tcm a -> tcm a) -> tcm a -> tcm a
forall a b. (a -> b) -> a -> b
$ 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
  where rel :: Relevance
rel = r -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance r
thing

-- | (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
$ ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext     ((ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
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
. ASetter TCEnv TCEnv LetBindings LetBindings
-> (LetBindings -> LetBindings) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv LetBindings LetBindings
Lens' TCEnv LetBindings
eLetBindings ((Open LetBinding -> Open LetBinding) -> LetBindings -> LetBindings
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> LetBindings -> LetBindings)
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> LetBindings
-> LetBindings
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) -> LetBindings -> LetBindings)
-> (Dom Type -> Dom Type) -> LetBindings -> LetBindings
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
. ASetter TCEnv TCEnv Relevance Relevance
-> (Relevance -> Relevance) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Relevance Relevance
Lens' TCEnv Relevance
eRelevance ((Relevance -> Relevance) -> TCEnv -> TCEnv)
-> (Relevance -> Relevance -> Relevance)
-> Relevance
-> TCEnv
-> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance

{-# INLINE applyRelevanceToContextFunBody #-}
-- | Like 'applyRelevanceToContext', but only act on context if
--   @--irrelevant-projections@.
--   See issue #2170.
applyRelevanceToContextFunBody :: (MonadTCM tcm, ExpandCase (tcm a), LensRelevance r) => r -> tcm a -> tcm a
applyRelevanceToContextFunBody :: forall (tcm :: * -> *) a r.
(MonadTCM tcm, ExpandCase (tcm a), LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContextFunBody r
thing tcm a
cont = ((tcm a -> Result (tcm a)) -> Result (tcm a)) -> tcm a
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \tcm a -> Result (tcm a)
ret ->
  case r -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance r
thing of
    Relevant{} -> tcm a -> Result (tcm a)
ret tcm a
cont
    Relevance
rel -> tcm a -> Result (tcm a)
ret (tcm a -> Result (tcm a)) -> tcm a -> Result (tcm a)
forall a b. (a -> b) -> a -> b
$ 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
. ASetter TCEnv TCEnv Quantity Quantity
-> (Quantity -> Quantity) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Quantity Quantity
Lens' TCEnv Quantity
eQuantityZeroHardCompile ((Quantity -> Quantity) -> TCEnv -> TCEnv)
-> (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
$ ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext     ((ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
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
. ASetter TCEnv TCEnv LetBindings LetBindings
-> (LetBindings -> LetBindings) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv LetBindings LetBindings
Lens' TCEnv LetBindings
eLetBindings ((Open LetBinding -> Open LetBinding) -> LetBindings -> LetBindings
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> LetBindings -> LetBindings)
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> LetBindings
-> LetBindings
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) -> LetBindings -> LetBindings)
-> (Dom Type -> Dom Type) -> LetBindings -> LetBindings
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)

{-# NOINLINE applyDomToContext' #-}
applyDomToContext' :: RewDom' Term -> TCM ()
applyDomToContext' :: RewDom' Term -> TCM ()
applyDomToContext' RewDom' Term
r = LocalEquation -> TCM ()
checkRewConstraint (RewDom' Term -> LocalEquation
forall t. RewDom' t -> LocalEquation' t
rewDomEq RewDom' Term
r)

{-# INLINE applyDomToContext #-}
-- | Apply modalities and equational constraints (local rewrite rules) to the
--   context.
applyDomToContext :: Dom e -> TCM a -> TCM a
applyDomToContext :: forall e a. Dom e -> TCM a -> TCM a
applyDomToContext Dom e
d TCMT IO a
act = do
  ((TCM () -> Result (TCM ())) -> Result (TCM ())) -> TCM ()
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \TCM () -> Result (TCM ())
ret -> case Dom e -> Maybe (RewDom' Term)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom e
d of
    Maybe (RewDom' Term)
Nothing -> TCM () -> Result (TCM ())
ret (TCM () -> Result (TCM ())) -> TCM () -> Result (TCM ())
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just RewDom' Term
c  -> TCM () -> Result (TCM ())
ret (TCM () -> Result (TCM ())) -> TCM () -> Result (TCM ())
forall a b. (a -> b) -> a -> b
$ RewDom' Term -> TCM ()
applyDomToContext' RewDom' Term
c
  Dom e -> TCMT IO a -> TCMT IO a
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Dom e
d TCMT IO a
act

{-# INLINE addRewConstraint #-}
-- | Adds an equational constraint due to a local rewrite rule.
addRewConstraint :: MonadConstraint tcm
  => LocalEquation -> tcm ()
addRewConstraint :: forall (tcm :: * -> *).
MonadConstraint tcm =>
LocalEquation -> tcm ()
addRewConstraint = Constraint -> tcm ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint (Constraint -> tcm ())
-> (LocalEquation -> Constraint) -> LocalEquation -> tcm ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalEquation -> Constraint
RewConstraint

-- | (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.
{-# INLINE applyModalityToContext #-}
applyModalityToContext :: (MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) => m -> tcm a -> tcm a
applyModalityToContext :: forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext !m
thing !tcm a
act = ((tcm a -> Result (tcm a)) -> Result (tcm a)) -> tcm a
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \tcm a -> Result (tcm a)
ret ->
  case m -> Modality
forall a. LensModality a => a -> Modality
getModality m
thing of
    Modality
m | Modality -> Modality -> Bool
noinlineEqModality Modality
m Modality
unitModality -> tcm a -> Result (tcm a)
ret tcm a
act
      | Bool
otherwise                         -> tcm a -> Result (tcm a)
ret (tcm a -> Result (tcm a)) -> tcm a -> Result (tcm a)
forall a b. (a -> b) -> a -> b
$ (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 (Modality -> TCEnv -> TCEnv
applyModalityToContext' Modality
m) tcm a
act

{-# NOINLINE applyModalityToContext' #-}
applyModalityToContext' :: Modality -> TCEnv -> TCEnv
applyModalityToContext' :: Modality -> TCEnv -> TCEnv
applyModalityToContext' Modality
m TCEnv
e =
  TCEnv
e TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext     ((ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Modality -> ContextEntry -> ContextEntry
forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)
    TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv LetBindings LetBindings
-> (LetBindings -> LetBindings) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv LetBindings LetBindings
Lens' TCEnv LetBindings
eLetBindings ((Open LetBinding -> Open LetBinding) -> LetBindings -> LetBindings
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> LetBindings -> LetBindings)
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> LetBindings
-> LetBindings
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) -> LetBindings -> LetBindings)
-> (Dom Type -> Dom Type) -> LetBindings -> LetBindings
forall a b. (a -> b) -> a -> b
$ Modality -> Dom Type -> Dom Type
forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)
    TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Relevance Relevance
-> (Relevance -> Relevance) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Relevance Relevance
Lens' TCEnv Relevance
eRelevance                (Relevance -> Relevance -> Relevance
composeRelevance (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m))
    TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Quantity Quantity
-> (Quantity -> Quantity) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Quantity Quantity
Lens' TCEnv Quantity
eQuantityZeroHardCompile  (Quantity -> Quantity -> Quantity
composeQuantity  (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity 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@
{-# INLINE applyModalityToContextOnly #-}
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 (Modality -> TCEnv -> TCEnv
applyModalityToContextOnly' Modality
m)

{-# NOINLINE applyModalityToContextOnly' #-}
applyModalityToContextOnly' :: Modality -> TCEnv -> TCEnv
applyModalityToContextOnly' :: Modality -> TCEnv -> TCEnv
applyModalityToContextOnly' Modality
m TCEnv
e =
  TCEnv
e TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Context Context
-> (Context -> Context) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Context Context
Lens' TCEnv Context
eContext     ((ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> Context' a -> Context' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ContextEntry -> ContextEntry) -> Context -> Context)
-> (ContextEntry -> ContextEntry) -> Context -> Context
forall a b. (a -> b) -> a -> b
$ Modality -> ContextEntry -> ContextEntry
forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m)
    TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv LetBindings LetBindings
-> (LetBindings -> LetBindings) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv LetBindings LetBindings
Lens' TCEnv LetBindings
eLetBindings ((Open LetBinding -> Open LetBinding) -> LetBindings -> LetBindings
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open LetBinding -> Open LetBinding)
 -> LetBindings -> LetBindings)
-> ((Dom Type -> Dom Type) -> Open LetBinding -> Open LetBinding)
-> (Dom Type -> Dom Type)
-> LetBindings
-> LetBindings
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) -> LetBindings -> LetBindings)
-> (Dom Type -> Dom Type) -> LetBindings -> LetBindings
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'.
{-# INLINE applyModalityToJudgementOnly #-}
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 (Modality -> TCEnv -> TCEnv
applyModalityToJudgementOnly' Modality
m)

{-# NOINLINE applyModalityToJudgementOnly' #-}
applyModalityToJudgementOnly' :: Modality -> TCEnv -> TCEnv
applyModalityToJudgementOnly' :: Modality -> TCEnv -> TCEnv
applyModalityToJudgementOnly' Modality
m TCEnv
e =
  TCEnv
e TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Relevance Relevance
-> (Relevance -> Relevance) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Relevance Relevance
Lens' TCEnv Relevance
eRelevance                (Relevance -> Relevance -> Relevance
composeRelevance (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m))
    TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& ASetter TCEnv TCEnv Quantity Quantity
-> (Quantity -> Quantity) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCEnv TCEnv Quantity Quantity
Lens' TCEnv Quantity
eQuantityZeroHardCompile  (Quantity -> Quantity -> Quantity
composeQuantity  (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
m))

{-# INLINE applyModalityToContextFunBody #-}
-- | Like 'applyModalityToContext', but only act on context (for Relevance) if
--   @--irrelevant-projections@.
--   See issue #2170.
applyModalityToContextFunBody :: (MonadTCM tcm, LensModality r, ExpandCase (tcm a)) => r -> tcm a -> tcm a
applyModalityToContextFunBody :: forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r, ExpandCase (tcm a)) =>
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 :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), 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 :: * -> *) a r.
(MonadTCM tcm, ExpandCase (tcm a), 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
$ PolarityModality -> tcm a -> tcm a
forall (tcm :: * -> *) p a.
(MonadTCEnv tcm, LensModalPolarity p) =>
p -> tcm a -> tcm a
applyPolarityToContext (Modality -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity 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