{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Modalities
  ( checkModality'
  , checkModality
  , checkModalityArgs
  ) where

import Control.Applicative ((<|>))

import Agda.Interaction.Options

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute

import Agda.Utils.Function
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' :: QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' :: QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' QName
x Definition
def = do
  case Definition -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def of
    Relevant{} -> Maybe TypeError -> TCM (Maybe TypeError)
forall a. a -> TCMT IO 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 -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funProj
      TCMT IO Bool
-> TCM (Maybe TypeError)
-> TCM (Maybe TypeError)
-> TCM (Maybe TypeError)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
isProj TCMT IO Bool -> TCMT IO Bool -> TCMT IO 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) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)) {-then-} TCM (Maybe TypeError)
needIrrProj {-else-} (TCM (Maybe TypeError) -> TCM (Maybe TypeError))
-> TCM (Maybe TypeError) -> TCM (Maybe TypeError)
forall a b. (a -> b) -> a -> b
$ do
        rel <- Lens' TCEnv Relevance -> TCMT IO 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 :: TCM (Maybe TypeError)
needIrrProj = Maybe TypeError -> TCM (Maybe TypeError)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeError -> TCM (Maybe TypeError))
-> Maybe TypeError -> TCM (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' :: QName -> Definition -> TCM (Maybe TypeError)
checkQuantity' :: QName -> Definition -> TCM (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 -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.irr" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
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 -> TCM (Maybe TypeError)
forall a. a -> TCMT IO 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 -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantityZeroHardCompile
      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' :: QName -> Definition -> TCM (Maybe TypeError)
checkModality' :: QName -> Definition -> TCM (Maybe TypeError)
checkModality' QName
x Definition
def = do
  relOk <- QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' QName
x Definition
def
  qtyOk <- checkQuantity' x def
  return $ relOk <|> qtyOk

-- | The second argument is the definition of the first.
checkModality :: QName -> Definition -> TCM ()
checkModality :: QName -> Definition -> TCMT IO ()
checkModality QName
x Definition
def = QName -> Definition -> TCM (Maybe TypeError)
checkModality' QName
x Definition
def TCM (Maybe TypeError)
-> (Maybe TypeError -> TCMT IO ()) -> TCMT IO ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (TypeError -> TCMT IO (ZonkAny 0)) -> Maybe TypeError -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeError -> TCMT IO (ZonkAny 0)
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 :: Definition -> Args -> TCM ()
checkModalityArgs :: Definition -> [Arg Term] -> TCMT IO ()
checkModalityArgs Definition
d [Arg Term]
vs = do
  let
    vmap :: VarMap
    vmap :: VarMap
vmap = [Arg Term] -> VarMap
forall t. Free t => t -> VarMap
freeVarMap [Arg Term]
vs

  -- we iterate over all vars in the context and their ArgInfo,
  -- checking for each that "vs" uses them as allowed.
  as <- TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
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 -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Modality
m ((Modality -> TCMT IO ()) -> TCMT IO ())
-> (Modality -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ Modality
used -> do
      let availPosMod :: Modality
availPosMod = Modality -> Modality
positionalModalityComponent (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
avail)
          usedPosMod :: Modality
usedPosMod = Modality -> Modality
positionalModalityComponent (Modality -> Modality
forall a. LensModality a => a -> Modality
getModality Modality
used)
      Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Modality
availPosMod Modality -> Modality -> Bool
`moreUsableModality` Modality
usedPosMod) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
         TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Term -> Modality -> Modality -> Definition -> TypeError
InvalidModalTelescopeUse Term
t Modality
usedPosMod Modality
availPosMod Definition
d