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

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

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

-- | 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.
  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)
             ]