{-# 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.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 forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def of
Relevance
Relevant -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Relevance
drel -> do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ Defn -> Maybe Projection
isProjection_ forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
(Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)) m (Maybe TypeError)
needIrrProj forall a b. (a -> b) -> a -> b
$ do
Relevance
rel <- forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC Lens' TCEnv Relevance
eRelevance
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"declaration relevance =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show Relevance
drel)
, TCMT IO Doc
"context relevance =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show Relevance
rel)
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Bool -> a -> Maybe a
boolToMaybe (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Relevance
drel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsIrrelevant QName
x
where
needIrrProj :: m (Maybe TypeError)
needIrrProj = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
"Projection " , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x, m Doc
" is irrelevant."
, m Doc
" Turn on option --irrelevant-projections to use it (unsafe)."
]
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 forall a. LensQuantity a => a -> Quantity
getQuantity Definition
def of
dq :: Quantity
dq@Quantityω{} -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"declaration quantity =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show Quantity
dq)
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Quantity
dq -> do
Quantity
q <- forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC Lens' TCEnv Quantity
eQuantity
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"declaration quantity =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show Quantity
dq)
, TCMT IO Doc
"context quantity =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Show a => a -> VerboseKey
show Quantity
q)
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Bool -> a -> Maybe a
boolToMaybe (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Quantity
dq Quantity -> Quantity -> Bool
`moreQuantity` Quantity
q) forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsErased QName
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
Maybe TypeError
relOk <- forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkRelevance' QName
x Definition
def
Maybe TypeError
qtyOk <- forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkQuantity' QName
x Definition
def
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe TypeError
relOk forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe TypeError
qtyOk
checkModality :: (MonadConversion m) => QName -> Definition -> m ()
checkModality :: forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m ()
checkModality QName
x Definition
def = forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkModality' QName
x Definition
def forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ 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 = forall a c t.
(IsVarSet a c, Singleton VerboseLevel c, Free t) =>
t -> c
freeVars Args
vs
Args
as <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Args
as forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
avail Term
t) -> do
let m :: Maybe Modality
m = do
VerboseLevel
v <- forall a. DeBruijn a => a -> Maybe VerboseLevel
deBruijnView Term
t
forall a. VarOcc' a -> Modality
varModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. VerboseLevel -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap VerboseLevel
v VarMap
vmap
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Modality
m forall a b. (a -> b) -> a -> b
$ \ Modality
used -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
avail Cohesion -> Cohesion -> Bool
`moreCohesion` forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
used) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ m Doc
"Telescope variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
, m Doc
"is indirectly being used in the" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Verbalize a => a -> VerboseKey
verbalize (forall a. LensModality a => a -> Modality
getModality Modality
used)) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality"
, m Doc
"but only available as in the" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (forall a. Verbalize a => a -> VerboseKey
verbalize (forall a. LensModality a => a -> Modality
getModality ArgInfo
avail)) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"modality"
, m Doc
"when inserting into the top-level"
, forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Definition -> QName
defName Definition
d) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Definition -> Type
defType Definition
d)
]