{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Irrelevance where
import Control.Arrow (second)
import Control.Monad.Except
import qualified Data.Map as Map
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute.Class
import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
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
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 (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
workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a
workOnTypes' :: forall (m :: * -> *) a. MonadTCEnv m => Bool -> m a -> m a
workOnTypes' 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 ((Relevance -> Relevance) -> Dom e -> Dom e
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)
(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
applyQuantityToContext 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 (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envWorkingOnTypes :: Bool
envWorkingOnTypes = Bool
True })
where
f :: Relevance -> Relevance
f | Bool
experimental = Relevance -> Relevance
irrToNonStrict
| Bool
otherwise = Relevance -> Relevance
forall a. a -> a
id
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
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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
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' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Relevance -> Dom Type -> Dom Type
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 = (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' Relevance TCEnv -> LensMap Relevance TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Relevance TCEnv
eRelevance LensMap Relevance TCEnv
-> (Relevance -> Relevance -> Relevance)
-> Relevance
-> TCEnv
-> TCEnv
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 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 (m :: * -> *) a.
Monad m =>
m Bool -> (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
$
Relevance -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Relevance -> tcm a -> tcm a
applyRelevanceToJudgementOnly Relevance
rel tcm a
cont
applyQuantityToContext :: (MonadTCEnv tcm, LensQuantity q) => q -> tcm a -> tcm a
applyQuantityToContext :: forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext q
thing =
case q -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity q
thing of
Quantity1{} -> tcm a -> tcm a
forall a. a -> a
id
Quantity
q -> Quantity -> tcm a -> tcm a
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Quantity -> tcm a -> tcm a
applyQuantityToJudgementOnly Quantity
q
applyQuantityToJudgementOnly :: (MonadTCEnv tcm) => Quantity -> tcm a -> tcm a
applyQuantityToJudgementOnly :: forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
Quantity -> tcm a -> tcm a
applyQuantityToJudgementOnly = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Quantity -> TCEnv -> TCEnv) -> Quantity -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Quantity TCEnv -> LensMap Quantity TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Quantity TCEnv
eQuantity LensMap Quantity TCEnv
-> (Quantity -> Quantity -> Quantity) -> Quantity -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity
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
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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
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' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Cohesion -> Dom Type -> Dom Type
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 = a -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion a
a
Bool -> m Bool
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 (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)
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
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 (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' [ContextEntry] TCEnv -> LensMap [ContextEntry] TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [ContextEntry] TCEnv
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' (Map Name (Open (Term, Dom Type))) TCEnv
-> LensMap (Map Name (Open (Term, Dom Type))) TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' (Map Name (Open (Term, Dom Type))) TCEnv
eLetBindings
((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Open (Term, Dom Type) -> Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> ((Dom Type -> Dom Type)
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Dom Type) -> (Term, Dom Type))
-> Open (Term, Dom Type) -> Open (Term, Dom Type))
-> ((Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type))
-> (Dom Type -> Dom Type)
-> Open (Term, Dom Type)
-> Open (Term, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom Type -> Dom Type) -> (Term, Dom Type) -> (Term, Dom Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type)))
-> (Dom Type -> Dom Type)
-> Map Name (Open (Term, Dom Type))
-> Map Name (Open (Term, Dom Type))
forall a b. (a -> b) -> a -> b
$ Modality -> Dom Type -> Dom Type
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 = (TCEnv -> TCEnv) -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> tcm a -> tcm a)
-> (Modality -> TCEnv -> TCEnv) -> Modality -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Modality TCEnv -> LensMap Modality TCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' Modality TCEnv
eModality LensMap Modality TCEnv
-> (Modality -> Modality -> Modality) -> Modality -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> Modality -> Modality
composeModality
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)
(Modality -> tcm a -> tcm a
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
m tcm a
cont)
(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
applyQuantityToContext (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
m) tcm a
cont)
where
m :: Modality
m = r -> Modality
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
= 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 :: * -> *) a.
MonadTCEnv tcm =>
Quantity -> tcm a -> tcm a
applyQuantityToJudgementOnly Quantity
zeroQuantity
class UsableRelevance a where
usableRel
:: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m)
=> Relevance -> a -> m Bool
instance UsableRelevance Term where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Term -> m Bool
usableRel Relevance
rel = \case
Var VerboseLevel
i Elims
vs -> do
Relevance
irel <- Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Dom Type -> Relevance) -> m (Dom Type) -> m Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m (Dom Type)
domOfBV VerboseLevel
i
let ok :: Bool
ok = Relevance
irel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"has relevance " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Relevance -> VerboseKey
forall a. Show a => a -> VerboseKey
show Relevance
irel VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
", which is " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
(if Bool
ok then VerboseKey
"" else VerboseKey
"NOT ") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"more relevant than " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Relevance -> VerboseKey
forall a. Show a => a -> VerboseKey
show Relevance
rel)
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
vs
Def QName
f Elims
vs -> do
Relevance
frel <- QName -> m Relevance
forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
f
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
frel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
vs
Con ConHead
c ConInfo
_ Elims
vs -> Relevance -> Elims -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
vs
Lit Literal
l -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Lam ArgInfo
_ Abs Term
v -> Relevance -> Abs Term -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Abs Term
v
Pi Dom Type
a Abs Type
b -> Relevance -> (Dom Type, Abs Type) -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Dom Type
a,Abs Type
b)
Sort Sort
s -> Relevance -> Sort -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Sort
s
Level Level
l -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaV MetaId
m Elims
vs -> do
Relevance
mrel <- MetaVariable -> Relevance
getMetaRelevance (MetaVariable -> Relevance) -> m MetaVariable -> m Relevance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
mrel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> Elims -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
vs
DontCare Term
v -> Relevance -> Term -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Term
v
Dummy{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
instance UsableRelevance a => UsableRelevance (Type' a) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Type' a -> m Bool
usableRel Relevance
rel (El Sort
_ a
t) = Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
t
instance UsableRelevance Sort where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Sort -> m Bool
usableRel Relevance
rel = \case
Type Level
l -> Relevance -> Level -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Level
l
Prop Level
l -> Relevance -> Level -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Level
l
Inf IsFibrant
f Integer
n -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
SSet Level
l -> Relevance -> Level -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Level
l
Sort
SizeUniv -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Sort
LockUniv -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Relevance -> (Dom' Term Term, Sort, Abs Sort) -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Dom' Term Term
a,Sort
s1,Abs Sort
s2)
FunSort Sort
s1 Sort
s2 -> Relevance -> (Sort, Sort) -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Sort
s1,Sort
s2)
UnivSort Sort
s -> Relevance -> Sort -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Sort
s
MetaS MetaId
x Elims
es -> Relevance -> Elims -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Elims
es
DefS QName
d Elims
es -> Relevance -> Term -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel (Term -> m Bool) -> Term -> m Bool
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
DummyS{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
instance UsableRelevance Level where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Level -> m Bool
usableRel Relevance
rel (Max Integer
_ [PlusLevel' Term]
ls) = Relevance -> [PlusLevel' Term] -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel [PlusLevel' Term]
ls
instance UsableRelevance PlusLevel where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> PlusLevel' Term -> m Bool
usableRel Relevance
rel (Plus Integer
_ Term
l) = Relevance -> Term -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Term
l
instance UsableRelevance a => UsableRelevance [a] where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> [a] -> m Bool
usableRel Relevance
rel = [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Bool) -> [a] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel)
instance (UsableRelevance a, UsableRelevance b) => UsableRelevance (a,b) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> (a, b) -> m Bool
usableRel Relevance
rel (a
a,b
b) = Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
a m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> b -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel b
b
instance (UsableRelevance a, UsableRelevance b, UsableRelevance c) => UsableRelevance (a,b,c) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> (a, b, c) -> m Bool
usableRel Relevance
rel (a
a,b
b,c
c) = Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
a m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> b -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel b
b m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Relevance -> c -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel c
c
instance UsableRelevance a => UsableRelevance (Elim' a) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Elim' a -> m Bool
usableRel Relevance
rel (Apply Arg a
a) = Relevance -> Arg a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel Arg a
a
usableRel Relevance
rel (Proj ProjOrigin
_ QName
p) = do
Relevance
prel <- QName -> m Relevance
forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
p
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Relevance
prel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel
usableRel Relevance
rel (IApply a
x a
y a
v) = [a] -> (a -> m Bool) -> m Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM [a
x,a
y,a
v] ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel
instance UsableRelevance a => UsableRelevance (Arg a) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Arg a -> m Bool
usableRel Relevance
rel (Arg ArgInfo
info a
u) =
let rel' :: Relevance
rel' = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info
in Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (Relevance
rel Relevance -> Relevance -> Relevance
`composeRelevance` Relevance
rel') a
u
instance UsableRelevance a => UsableRelevance (Dom a) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Dom a -> m Bool
usableRel Relevance
rel Dom{unDom :: forall t e. Dom' t e -> e
unDom = a
u} = Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
u
instance (Subst a, UsableRelevance a) => UsableRelevance (Abs a) where
usableRel :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m) =>
Relevance -> Abs a -> m Bool
usableRel Relevance
rel Abs a
abs = Abs a -> (a -> m Bool) -> m Bool
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
abs ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \a
u -> Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
u
class UsableModality a where
usableMod
:: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m)
=> Modality -> a -> m Bool
instance UsableModality Term where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Term -> m Bool
usableMod Modality
mod Term
u = do
case Term
u of
Var VerboseLevel
i Elims
vs -> do
Modality
imod <- Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality (Dom Type -> Modality) -> m (Dom Type) -> m Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> m (Dom Type)
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m (Dom Type)
domOfBV VerboseLevel
i
let ok :: Bool
ok = Modality
imod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"has modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
imod VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
", which is a " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
(if Bool
ok then VerboseKey
"" else VerboseKey
"NOT ") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
mod)
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
Def QName
f Elims
vs -> do
Modality
fmod <- QName -> m Modality
forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
f
let ok :: Bool
ok = Modality
fmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Definition" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
f []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"has modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
fmod VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
", which is a " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
(if Bool
ok then VerboseKey
"" else VerboseKey
"NOT ") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
mod)
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
Con ConHead
c ConInfo
_ Elims
vs -> Modality -> Elims -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs
Lit Literal
l -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Lam ArgInfo
info Abs Term
v -> ArgInfo -> Modality -> Abs Term -> m Bool
forall a (m :: * -> *).
(Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
ArgInfo -> Modality -> Abs a -> m Bool
usableModAbs ArgInfo
info Modality
mod Abs Term
v
Pi Dom Type
a Abs Type
b -> Modality -> Term -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
domMod (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` ArgInfo -> Modality -> Abs Term -> m Bool
forall a (m :: * -> *).
(Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
ArgInfo -> Modality -> Abs a -> m Bool
usableModAbs (Dom Type -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
a) Modality
mod (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Abs Type -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
where
domMod :: Modality
domMod = (Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
composeQuantity (Quantity -> Quantity -> Quantity)
-> Quantity -> Quantity -> Quantity
forall a b. (a -> b) -> a -> b
$ Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
a) (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$
(Cohesion -> Cohesion) -> Modality -> Modality
forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
mapCohesion (Cohesion -> Cohesion -> Cohesion
composeCohesion (Cohesion -> Cohesion -> Cohesion)
-> Cohesion -> Cohesion -> Cohesion
forall a b. (a -> b) -> a -> b
$ Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
a) Modality
mod
Sort Sort
s -> Modality -> Sort -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Sort
s
Level Level
l -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaV MetaId
m Elims
vs -> do
Modality
mmod <- MetaVariable -> Modality
getMetaModality (MetaVariable -> Modality) -> m MetaVariable -> m Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
let ok :: Bool
ok = Modality
mmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Metavariable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"has modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
mmod VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
", which is a " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
(if Bool
ok then VerboseKey
"" else VerboseKey
"NOT ") VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"more usable modality than " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Modality -> VerboseKey
forall a. Show a => a -> VerboseKey
show Modality
mod)
(Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> Elims -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Elims
vs) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do
Term
u <- Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
u
Maybe MetaId -> m Bool -> (MetaId -> m Bool) -> m Bool
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta Term
u) (Modality -> Term -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
u) ((MetaId -> m Bool) -> m Bool) -> (MetaId -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> Blocker -> m Bool
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MetaId -> Blocker
UnblockOnMeta MetaId
m)
DontCare Term
v -> Modality -> Term -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
v
Dummy{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
usableModAbs :: (Subst a, MonadAddContext m, UsableModality a,
ReadTCState m, HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
ArgInfo -> Modality -> Abs a -> m Bool
usableModAbs :: forall a (m :: * -> *).
(Subst a, MonadAddContext m, UsableModality a, ReadTCState m,
HasConstInfo m, MonadReduce m, MonadError Blocker m) =>
ArgInfo -> Modality -> Abs a -> m Bool
usableModAbs ArgInfo
info Modality
mod Abs a
abs = Dom Type -> Abs a -> (a -> m Bool) -> m Bool
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction (ArgInfo -> Dom Type -> Dom Type
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__) Abs a
abs ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ \ a
u -> Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod a
u
instance UsableRelevance a => UsableModality (Type' a) where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Type' a -> m Bool
usableMod Modality
mod (El Sort
_ a
t) = Relevance -> a -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) a
t
instance UsableModality Sort where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Sort -> m Bool
usableMod Modality
mod Sort
s = Relevance -> Sort -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) Sort
s
instance UsableModality Level where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Level -> m Bool
usableMod Modality
mod (Max Integer
_ [PlusLevel' Term]
ls) = Relevance -> [PlusLevel' Term] -> m Bool
forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) [PlusLevel' Term]
ls
instance UsableModality a => UsableModality [a] where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> [a] -> m Bool
usableMod Modality
mod = [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Bool) -> [a] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod)
instance (UsableModality a, UsableModality b) => UsableModality (a,b) where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> (a, b) -> m Bool
usableMod Modality
mod (a
a,b
b) = Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod a
a m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Modality -> b -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod b
b
instance UsableModality a => UsableModality (Elim' a) where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Elim' a -> m Bool
usableMod Modality
mod (Apply Arg a
a) = Modality -> Arg a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Arg a
a
usableMod Modality
mod (Proj ProjOrigin
_ QName
p) = do
Modality
pmod <- QName -> m Modality
forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
p
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Modality
pmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
usableMod Modality
mod (IApply a
x a
y a
v) = [a] -> (a -> m Bool) -> m Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM [a
x,a
y,a
v] ((a -> m Bool) -> m Bool) -> (a -> m Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod
instance UsableModality a => UsableModality (Arg a) where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Arg a -> m Bool
usableMod Modality
mod (Arg ArgInfo
info a
u) =
let mod' :: Modality
mod' = ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info
in Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod (Modality
mod Modality -> Modality -> Modality
`composeModality` Modality
mod') a
u
instance UsableModality a => UsableModality (Dom a) where
usableMod :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Dom a -> m Bool
usableMod Modality
mod Dom{unDom :: forall t e. Dom' t e -> e
unDom = a
u} = Modality -> a -> m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod a
u
usableAtModality :: MonadConstraint TCM => Modality -> Term -> TCM ()
usableAtModality :: MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
usableAtModality Modality
mod Term
t = Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Modality -> Term -> Constraint
UsableAtModality Modality
mod Term
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Either Blocker Bool
res <- ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool))
-> ExceptT Blocker (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Modality -> Term -> ExceptT Blocker (TCMT IO) Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
t
case Either Blocker Bool
res of
Right Bool
b -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is not usable at the required modality" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Modality -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod)
Left Blocker
blocker -> Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
isPropM
:: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m)
=> a -> m Bool
isPropM :: forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM a
a = do
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m Bool -> m Bool
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m a -> m a
traceSDoc VerboseKey
"tc.prop" VerboseLevel
80 (TCMT IO Doc
"Is " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"in Prop?") (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
Sort -> m Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a) m Sort -> (Sort -> Bool) -> m Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
Prop{} -> Bool
True
Sort
_ -> Bool
False
isIrrelevantOrPropM
:: (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m, MonadBlock m)
=> a -> m Bool
isIrrelevantOrPropM :: forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM a
x = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant a
x) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` a -> m Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM a
x
isFibrant
:: (LensSort a, PureTCM m, MonadBlock m)
=> a -> m Bool
isFibrant :: forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant a
a = Sort -> m Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a) m Sort -> (Sort -> Bool) -> m Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
Type{} -> Bool
True
Prop{} -> Bool
True
Inf IsFibrant
f Integer
_ -> IsFibrant
f IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
SSet{} -> Bool
False
SizeUniv{} -> Bool
False
LockUniv{} -> Bool
False
PiSort{} -> Bool
False
FunSort{} -> Bool
False
UnivSort{} -> Bool
False
MetaS{} -> Bool
False
DefS{} -> Bool
False
DummyS{} -> Bool
False
isCoFibrantSort :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool
isCoFibrantSort :: forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isCoFibrantSort a
a = Sort -> m Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (a -> Sort
forall a. LensSort a => a -> Sort
getSort a
a) m Sort -> (Sort -> Bool) -> m Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
Type{} -> Bool
True
Prop{} -> Bool
True
Inf IsFibrant
f Integer
_ -> IsFibrant
f IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
SSet{} -> Bool
False
SizeUniv{} -> Bool
False
LockUniv{} -> Bool
True
PiSort{} -> Bool
False
FunSort{} -> Bool
False
UnivSort{} -> Bool
False
MetaS{} -> Bool
False
DefS{} -> Bool
False
DummyS{} -> Bool
False