{-# 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

-- | The second argument is the definition of the first.
--   Returns 'Nothing' if ok, otherwise the error message.
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 functions can be used in any context.
    Relevance
drel -> do
      -- Andreas,, 2018-06-09, issue #2170
      -- irrelevant projections are only allowed if --irrelevant-projections
      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)) {-then-} m (Maybe TypeError)
needIrrProj {-else-} (m (Maybe TypeError) -> m (Maybe TypeError))
-> m (Maybe TypeError) -> m (Maybe TypeError)
forall a b. (a -> b) -> a -> b
$ do
        Relevance
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
        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 relevance =" 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 (Relevance -> VerboseKey
forall a. Show a => a -> VerboseKey
show Relevance
drel)
          , TCMT IO Doc
"context     relevance =" 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 (Relevance -> VerboseKey
forall a. Show a => a -> VerboseKey
show Relevance
rel)
          , QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
isProj (TCMT IO Doc
"not" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) TCMT IO Doc
"a projection"
          ]
        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
$ Bool -> TypeError -> Maybe TypeError
forall a. Bool -> a -> Maybe a
boolToMaybe (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Relevance
drel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) (TypeError -> Maybe TypeError) -> TypeError -> Maybe TypeError
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsIrrelevant QName
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

-- | The second argument is the definition of the first.
--   Returns 'Nothing' if ok, otherwise the error message.
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)
        -- , "context     quantity =" <+> text (show q)
        ]
      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 -- Abundant definitions can be used in any context.
    Quantity
dq -> do
      Quantity
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
      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)
        , TCMT IO Doc
"context     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
q)
        ]
      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
$ Bool -> TypeError -> Maybe TypeError
forall a. Bool -> a -> Maybe a
boolToMaybe (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Quantity
dq Quantity -> Quantity -> Bool
`moreQuantity` Quantity
q) (TypeError -> Maybe TypeError) -> TypeError -> Maybe TypeError
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsErased QName
x

-- | The second argument is the definition of the first.
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 <- QName -> Definition -> m (Maybe TypeError)
forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkRelevance' QName
x Definition
def
  Maybe TypeError
qtyOk <- QName -> Definition -> m (Maybe TypeError)
forall (m :: * -> *).
MonadConversion m =>
QName -> Definition -> m (Maybe TypeError)
checkQuantity' QName
x Definition
def
  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
$ Maybe TypeError
relOk Maybe TypeError -> Maybe TypeError -> Maybe TypeError
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe TypeError
qtyOk

-- | The second argument is the definition of the first.
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

-- | Checks that the given implicitely inserted arguments, are used in a modally
--   correct way.
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

  -- we iterate over all vars in the context and their ArgInfo,
  -- checking for each that "vs" uses them as allowed.
  Args
as <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Args -> (Arg Term -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Args
as ((Arg Term -> m ()) -> m ()) -> (Arg Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
avail Term
t) -> do
    let m :: Maybe Modality
m = do
          VerboseLevel
v <- Term -> Maybe VerboseLevel
forall a. DeBruijn a => a -> Maybe VerboseLevel
deBruijnView Term
t
          VarOcc' MetaSet -> Modality
forall a. VarOcc' a -> Modality
varModality (VarOcc' MetaSet -> Modality)
-> Maybe (VarOcc' MetaSet) -> Maybe Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> VarMap -> Maybe (VarOcc' MetaSet)
forall a. VerboseLevel -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap VerboseLevel
v VarMap
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)
             ]