{-# OPTIONS_GHC -Wunused-imports #-}
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
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
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
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 })
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
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)
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
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
$
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly Relevance
rel tcm a
cont
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
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
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)
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 #-}
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
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)
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))
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)
(forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
m tcm a
cont)
(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)
where
m :: Modality
m = forall a. LensModality a => a -> Modality
getModality r
thing
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