{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Irrelevance where
import Control.Monad.Except
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Concrete.Pretty
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute.Class
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
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 Int
i Elims
vs -> do
Relevance
irel <- forall a. LensRelevance a => a -> Relevance
getRelevance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
let ok :: Bool
ok = Relevance
irel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has relevance " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Relevance
irel forall a. [a] -> [a] -> [a]
++ [Char]
", which is " forall a. [a] -> [a] -> [a]
++
(if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more relevant than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Relevance
rel)
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
f
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
frel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Lam ArgInfo
_ Abs Term
v -> 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 -> 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 -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaV MetaId
m Elims
vs -> do
Relevance
mrel <- forall a. LensRelevance a => a -> Relevance
getRelevance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m
forall (m :: * -> *) a. Monad m => a -> m a
return (Relevance
mrel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 -> 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{} -> 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) = 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
Univ Univ
_ Level
l -> 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 Univ
_ Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Sort
SizeUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Sort
LockUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Sort
LevelUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Sort
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> 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 -> 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 -> 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 -> 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 -> forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
DummyS{} -> 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) = 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) = 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 = forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
a forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
a forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel b
b forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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) = 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
relOfConst QName
p
forall (m :: * -> *) a. Monad m => a -> m a
return 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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel Relevance
rel a
v
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' = forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info
in 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} = 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 = forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs a
abs forall a b. (a -> b) -> a -> b
$ \a
u -> 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 Int
i Elims
vs -> do
Modality
imod <- forall a. LensModality a => a -> Modality
getModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m (Dom Type)
domOfBV Int
i
let ok :: Bool
ok = Modality
imod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
imod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
(if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
f
let ok :: Bool
ok = forall a. LensCohesion a => Cohesion -> a -> a
setCohesion Cohesion
Flat Modality
fmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Definition" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
f []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
fmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
(if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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
o Elims
vs -> do
Modality
cmod <- forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst (ConHead -> QName
conName ConHead
c)
let ok :: Bool
ok = Modality
cmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"The constructor" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
o []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has the modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
cmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is " forall a. [a] -> [a] -> [a]
++
(if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++
[Char]
"more usable than the modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod forall a. [a] -> [a] -> [a]
++ [Char]
".")
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Lam ArgInfo
info Abs Term
v -> 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 -> 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 (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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 (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
a) Modality
mod (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)
where
domMod :: Modality
domMod = forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
composeQuantity forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
a) forall a b. (a -> b) -> a -> b
$
forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
mapCohesion (Cohesion -> Cohesion -> Cohesion
composeCohesion forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
a) Modality
mod
Sort Sort
s -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaV MetaId
m Elims
vs -> do
Modality
mmod <- forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m
let ok :: Bool
ok = Modality
mmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mod
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Metavariable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"has modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mmod forall a. [a] -> [a] -> [a]
++ [Char]
", which is a " forall a. [a] -> [a] -> [a]
++
(if Bool
ok then [Char]
"" else [Char]
"NOT ") forall a. [a] -> [a] -> [a]
++ [Char]
"more usable modality than " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Modality
mod)
(forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do
Term
u <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
u
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall a. IsMeta a => a -> Maybe MetaId
isMeta Term
u) (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) forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MetaId -> Blocker
UnblockOnMeta MetaId
m)
DontCare Term
v -> 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{} -> 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 = forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ HasCallStack => Dom Type
__DUMMY_DOM__) Abs a
abs forall a b. (a -> b) -> a -> b
$ \ a
u -> 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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (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 = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (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) = forall a (m :: * -> *).
(UsableRelevance a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m) =>
Relevance -> a -> m Bool
usableRel (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 = forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (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) = 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 forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` 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) = 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Modality
modalityOfConst QName
p
forall (m :: * -> *) a. Monad m => a -> m a
return 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) = 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
v
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' = forall a. LensModality a => a -> Modality
getModality ArgInfo
info
in 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} = 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
=> Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' :: MonadConstraint (TCMT IO) =>
Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' Maybe Sort
ms WhyCheckModality
why Modality
mod Term
t =
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
why Maybe Sort
ms Modality
mod Term
t) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Maybe Sort
ms) forall a b. (a -> b) -> a -> b
$ do
Either Blocker Bool
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ 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 -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
formatWhy
Left Blocker
blocker -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
where
formatWhy :: TCMT IO Doc
formatWhy = do
Bool
compatible <- PragmaOptions -> Bool
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
Bool
cubical <- forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let
context :: [Char]
context
| Bool
cubical = [Char]
"in Cubical Agda,"
| Bool
compatible = [Char]
"to maintain compatibility with Cubical Agda,"
| Bool
otherwise = [Char]
"when --without-K is enabled,"
explanation :: [Char] -> [TCMT IO Doc]
explanation [Char]
what
| Bool
cubical Bool -> Bool -> Bool
|| Bool
compatible =
[ TCMT IO Doc
""
, forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( TCMT IO Doc
"Note:"forall a. a -> [a] -> [a]
:forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
context
forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
what forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"must be usable at the modality"
forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in which the function was defined, since it will be"
forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"used for computing transports"
)
, TCMT IO Doc
""
]
| Bool
otherwise = []
case WhyCheckModality
why of
WhyCheckModality
IndexedClause ->
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
( forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"This clause has target type"
forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t]
forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is not usable at the required modality"
forall a. [a] -> [a] -> [a]
++ [forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."]
)
forall a. a -> [a] -> [a]
: [Char] -> [TCMT IO Doc]
explanation [Char]
"the target type")
IndexedClauseArg Name
forced Name
the_arg ->
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
( forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The argument" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
the_arg] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has type")
forall a. a -> [a] -> [a]
: forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t)
forall a. a -> [a] -> [a]
: forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is not usable at the required modality"
forall a. [a] -> [a] -> [a]
++ [forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."] )
forall a. a -> [a] -> [a]
: [Char] -> [TCMT IO Doc]
explanation [Char]
"this argument's type")
WhyCheckModality
GeneratedClause ->
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is not usable at the required modality"
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod)
WhyCheckModality
_ -> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is not usable at the required modality"
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Modality -> Doc
attributesForModality Modality
mod)
usableAtModality :: MonadConstraint TCM => WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality :: MonadConstraint (TCMT IO) =>
WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality = MonadConstraint (TCMT IO) =>
Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' forall a. Maybe a
Nothing
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
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc [Char]
"tc.prop" Int
80 (TCMT IO Doc
"Is " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of sort" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"in Prop?") forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LensRelevance a => a -> Bool
isIrrelevant a
x) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` 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 = forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
Univ Univ
u Level
_ -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
Inf Univ
u Integer
_ -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
SizeUniv{} -> Bool
False
LockUniv{} -> Bool
False
LevelUniv{} -> Bool
False
IntervalUniv{} -> 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 = forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (forall a. LensSort a => a -> Sort
getSort a
a) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
Univ Univ
u Level
_ -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
Inf Univ
u Integer
_ -> Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant
SizeUniv{} -> Bool
False
LockUniv{} -> Bool
True
LevelUniv{} -> Bool
False
IntervalUniv{} -> Bool
True
PiSort{} -> Bool
False
FunSort{} -> Bool
False
UnivSort{} -> Bool
False
MetaS{} -> Bool
False
DefS{} -> Bool
False
DummyS{} -> Bool
False