{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.Modalities
( checkModality'
, checkModality
, checkModalityArgs
) where
import Control.Applicative ((<|>))
import Control.Monad
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.Utils.Function
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
checkRelevance' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
checkRelevance' :: forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkRelevance' QName
x Definition
def = do
case Definition -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def of
Relevance
Relevant -> Maybe TypeError -> m (Maybe TypeError)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
Relevance
drel -> do
let isProj :: Bool
isProj = Definition -> Defn
theDef Definition
def Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funProj
m Bool
-> m (Maybe TypeError)
-> m (Maybe TypeError)
-> m (Maybe TypeError)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
isProj m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
(Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections (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)) m (Maybe TypeError)
needIrrProj (m (Maybe TypeError) -> m (Maybe TypeError))
-> m (Maybe TypeError) -> m (Maybe TypeError)
forall a b. (a -> b) -> a -> b
$ do
rel <- Lens' TCEnv Relevance -> m Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance
reportSDoc "tc.irr" 50 $ vcat
[ "declaration relevance =" <+> text (show drel)
, "context relevance =" <+> text (show rel)
, prettyTCM x <+> "is" <+> applyUnless isProj ("not" <+>) "a projection"
]
return $ boolToMaybe (not $ drel `moreRelevant` rel) $ DefinitionIsIrrelevant x
where
needIrrProj :: m (Maybe TypeError)
needIrrProj = Maybe TypeError -> m (Maybe TypeError)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeError -> m (Maybe TypeError))
-> Maybe TypeError -> m (Maybe TypeError)
forall a b. (a -> b) -> a -> b
$ TypeError -> Maybe TypeError
forall a. a -> Maybe a
Just (TypeError -> Maybe TypeError) -> TypeError -> Maybe TypeError
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
ProjectionIsIrrelevant QName
x
checkQuantity' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
checkQuantity' :: forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkQuantity' QName
x Definition
def = do
case Definition -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Definition
def of
dq :: Quantity
dq@Quantityω{} -> do
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] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"declaration quantity =" 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 (Quantity -> VerboseKey
forall a. Show a => a -> VerboseKey
show Quantity
dq)
]
Maybe TypeError -> m (Maybe TypeError)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
forall a. Maybe a
Nothing
Quantity
dq -> do
q <- Lens' TCEnv Quantity -> m Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantity
reportSDoc "tc.irr" 50 $ vcat
[ "declaration quantity =" <+> text (show dq)
, "context quantity =" <+> text (show q)
]
return $ boolToMaybe (not $ dq `moreQuantity` q) $ DefinitionIsErased x
checkModality' :: (MonadConversion m) => QName -> Definition -> m (Maybe TypeError)
checkModality' :: forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkModality' QName
x Definition
def = do
relOk <- QName -> Definition -> m (Maybe TypeError)
forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkRelevance' QName
x Definition
def
qtyOk <- checkQuantity' x def
return $ relOk <|> qtyOk
checkModality :: (MonadConversion m) => QName -> Definition -> m ()
checkModality :: forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m ()
checkModality QName
x Definition
def = QName -> Definition -> m (Maybe TypeError)
forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkModality' QName
x Definition
def m (Maybe TypeError) -> (Maybe TypeError -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (TypeError -> m Any) -> Maybe TypeError -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeError -> m Any
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError
checkModalityArgs :: (MonadConversion m) => Definition -> Args -> m ()
checkModalityArgs :: forall (m :: * -> *).
MonadConversion m =>
Definition -> Args -> m ()
checkModalityArgs Definition
d Args
vs = do
let
vmap :: VarMap
vmap :: VarMap
vmap = Args -> VarMap
forall a c t.
(IsVarSet a c, Singleton VerboseLevel c, Free t) =>
t -> c
freeVars Args
vs
as <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
forM_ as $ \ (Arg ArgInfo
avail Term
t) -> do
let m :: Maybe Modality
m = do
v <- Term -> Maybe VerboseLevel
forall a. DeBruijn a => a -> Maybe VerboseLevel
deBruijnView Term
t
varModality <$> lookupVarMap v vmap
Maybe Modality -> (Modality -> m ()) -> m ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Modality
m ((Modality -> m ()) -> m ()) -> (Modality -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Modality
used -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
avail Cohesion -> Cohesion -> Bool
`moreCohesion` Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
used) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> m ()) -> m Doc -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ m Doc
"Telescope variable" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
, m Doc
"is indirectly being used in the" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> m Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Modality -> VerboseKey
forall a. Verbalize a => a -> VerboseKey
verbalize (Modality -> Modality
forall a. LensModality a => a -> Modality
getModality Modality
used)) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality"
, m Doc
"but only available as in the" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> m Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Modality -> VerboseKey
forall a. Verbalize a => a -> VerboseKey
verbalize (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
avail)) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality"
, m Doc
"when inserting into the top-level"
, QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> QName
defName Definition
d) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Definition -> Type
defType Definition
d)
]