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

-- | 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 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 functions can be used in any context.
    Relevance
drel -> do
      -- Andreas,, 2018-06-09, issue #2170
      -- irrelevant projections are only allowed if --irrelevant-projections
      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)) {-then-} m (Maybe TypeError)
needIrrProj {-else-} 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)."
        ]

-- | 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 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)
        -- , "context     quantity =" <+> text (show q)
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing -- Abundant definitions can be used in any context.
    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

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

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

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