module Agda.Syntax.Concrete.Definitions.Monad where

import Control.Monad.Except
import Control.Monad.State

import Data.Bifunctor (second)
import Data.Map (Map)
import qualified Data.Map as Map

import Agda.Syntax.Position
import Agda.Syntax.Common hiding (TerminationCheck())
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Definitions.Types
import Agda.Syntax.Concrete.Definitions.Errors

import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.Lens

import Agda.Utils.Impossible

-- | Nicifier monad.
--   Preserve the state when throwing an exception.

newtype Nice a = Nice { forall a. Nice a -> ExceptT DeclarationException (State NiceEnv) a
unNice :: ExceptT DeclarationException (State NiceEnv) a }
  deriving ( (forall a b. (a -> b) -> Nice a -> Nice b)
-> (forall a b. a -> Nice b -> Nice a) -> Functor Nice
forall a b. a -> Nice b -> Nice a
forall a b. (a -> b) -> Nice a -> Nice b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Nice b -> Nice a
$c<$ :: forall a b. a -> Nice b -> Nice a
fmap :: forall a b. (a -> b) -> Nice a -> Nice b
$cfmap :: forall a b. (a -> b) -> Nice a -> Nice b
Functor, Functor Nice
Functor Nice
-> (forall a. a -> Nice a)
-> (forall a b. Nice (a -> b) -> Nice a -> Nice b)
-> (forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c)
-> (forall a b. Nice a -> Nice b -> Nice b)
-> (forall a b. Nice a -> Nice b -> Nice a)
-> Applicative Nice
forall a. a -> Nice a
forall a b. Nice a -> Nice b -> Nice a
forall a b. Nice a -> Nice b -> Nice b
forall a b. Nice (a -> b) -> Nice a -> Nice b
forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Nice a -> Nice b -> Nice a
$c<* :: forall a b. Nice a -> Nice b -> Nice a
*> :: forall a b. Nice a -> Nice b -> Nice b
$c*> :: forall a b. Nice a -> Nice b -> Nice b
liftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
$cliftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
$c<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
pure :: forall a. a -> Nice a
$cpure :: forall a. a -> Nice a
Applicative, Applicative Nice
Applicative Nice
-> (forall a b. Nice a -> (a -> Nice b) -> Nice b)
-> (forall a b. Nice a -> Nice b -> Nice b)
-> (forall a. a -> Nice a)
-> Monad Nice
forall a. a -> Nice a
forall a b. Nice a -> Nice b -> Nice b
forall a b. Nice a -> (a -> Nice b) -> Nice b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Nice a
$creturn :: forall a. a -> Nice a
>> :: forall a b. Nice a -> Nice b -> Nice b
$c>> :: forall a b. Nice a -> Nice b -> Nice b
>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
$c>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
Monad
           , MonadState NiceEnv, MonadError DeclarationException
           )

-- | Run a Nicifier computation, return result and warnings
--   (in chronological order).
runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
runNice :: forall a. Nice a -> (Either DeclarationException a, NiceWarnings)
runNice Nice a
m = (NiceEnv -> NiceWarnings)
-> (Either DeclarationException a, NiceEnv)
-> (Either DeclarationException a, NiceWarnings)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (NiceWarnings -> NiceWarnings
forall a. [a] -> [a]
reverse (NiceWarnings -> NiceWarnings)
-> (NiceEnv -> NiceWarnings) -> NiceEnv -> NiceWarnings
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NiceEnv -> NiceWarnings
niceWarn) ((Either DeclarationException a, NiceEnv)
 -> (Either DeclarationException a, NiceWarnings))
-> (Either DeclarationException a, NiceEnv)
-> (Either DeclarationException a, NiceWarnings)
forall a b. (a -> b) -> a -> b
$
  ExceptT DeclarationException (State NiceEnv) a
-> StateT NiceEnv Identity (Either DeclarationException a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Nice a -> ExceptT DeclarationException (State NiceEnv) a
forall a. Nice a -> ExceptT DeclarationException (State NiceEnv) a
unNice Nice a
m) StateT NiceEnv Identity (Either DeclarationException a)
-> NiceEnv -> (Either DeclarationException a, NiceEnv)
forall s a. State s a -> s -> (a, s)
`runState` NiceEnv
initNiceEnv

-- | Nicifier state.

data NiceEnv = NiceEnv
  { NiceEnv -> LoneSigs
_loneSigs :: LoneSigs
    -- ^ Lone type signatures that wait for their definition.
  , NiceEnv -> TerminationCheck
_termChk  :: TerminationCheck
    -- ^ Termination checking pragma waiting for a definition.
  , NiceEnv -> PositivityCheck
_posChk   :: PositivityCheck
    -- ^ Positivity checking pragma waiting for a definition.
  , NiceEnv -> UniverseCheck
_uniChk   :: UniverseCheck
    -- ^ Universe checking pragma waiting for a data/rec signature or definition.
  , NiceEnv -> Catchall
_catchall :: Catchall
    -- ^ Catchall pragma waiting for a function clause.
  , NiceEnv -> CoverageCheck
_covChk  :: CoverageCheck
    -- ^ Coverage pragma waiting for a definition.
  , NiceEnv -> NiceWarnings
niceWarn :: NiceWarnings
    -- ^ Stack of warnings. Head is last warning.
  , NiceEnv -> NameId
_nameId  :: NameId
    -- ^ We distinguish different 'NoName's (anonymous definitions) by a unique 'NameId'.
  }

data LoneSig = LoneSig
  { LoneSig -> Range
loneSigRange :: Range
  , LoneSig -> Name
loneSigName  :: Name
      -- ^ If 'isNoName', this name can have a different 'NameId'
      --   than the key of 'LoneSigs' pointing to it.
  , LoneSig -> DataRecOrFun
loneSigKind  :: DataRecOrFun
  }

type LoneSigs     = Map Name LoneSig
     -- ^ We retain the 'Name' also in the codomain since
     --   'Name' as a key is up to @Eq Name@ which ignores the range.
     --   However, without range names are not unique in case the
     --   user gives a second definition of the same name.
     --   This causes then problems in 'replaceSigs' which might
     --   replace the wrong signature.
     --
     --   Another reason is that we want to distinguish different
     --   occurrences of 'NoName' in a mutual block (issue #4157).
     --   The 'NoName' in the codomain will have a unique 'NameId'.

type NiceWarnings = [DeclarationWarning]
     -- ^ Stack of warnings. Head is last warning.

-- | Initial nicifier state.

initNiceEnv :: NiceEnv
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
  { _loneSigs :: LoneSigs
_loneSigs = LoneSigs
forall k a. Map k a
Map.empty
  , _termChk :: TerminationCheck
_termChk  = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
  , _posChk :: PositivityCheck
_posChk   = PositivityCheck
YesPositivityCheck
  , _uniChk :: UniverseCheck
_uniChk   = UniverseCheck
YesUniverseCheck
  , _catchall :: Catchall
_catchall = Catchall
False
  , _covChk :: CoverageCheck
_covChk   = CoverageCheck
YesCoverageCheck
  , niceWarn :: NiceWarnings
niceWarn  = []
  , _nameId :: NameId
_nameId   = Word64 -> ModuleNameHash -> NameId
NameId Word64
1 ModuleNameHash
noModuleNameHash
  }

lensNameId :: Lens' NameId NiceEnv
lensNameId :: Lens' NameId NiceEnv
lensNameId NameId -> f NameId
f NiceEnv
e = NameId -> f NameId
f (NiceEnv -> NameId
_nameId NiceEnv
e) f NameId -> (NameId -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ NameId
i -> NiceEnv
e { _nameId :: NameId
_nameId = NameId
i }

nextNameId :: Nice NameId
nextNameId :: Nice NameId
nextNameId = do
  NameId
i <- Lens' NameId NiceEnv -> Nice NameId
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' NameId NiceEnv
lensNameId
  Lens' NameId NiceEnv
lensNameId Lens' NameId NiceEnv -> (NameId -> NameId) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= NameId -> NameId
forall a. Enum a => a -> a
succ
  NameId -> Nice NameId
forall (m :: * -> *) a. Monad m => a -> m a
return NameId
i

-- * Handling the lone signatures, stored to infer mutual blocks.

-- | Lens for field '_loneSigs'.

loneSigs :: Lens' LoneSigs NiceEnv
loneSigs :: Lens' LoneSigs NiceEnv
loneSigs LoneSigs -> f LoneSigs
f NiceEnv
e = LoneSigs -> f LoneSigs
f (NiceEnv -> LoneSigs
_loneSigs NiceEnv
e) f LoneSigs -> (LoneSigs -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ LoneSigs
s -> NiceEnv
e { _loneSigs :: LoneSigs
_loneSigs = LoneSigs
s }

-- | Adding a lone signature to the state.
--   Return the name (which is made unique if 'isNoName').

addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k = do
  -- Andreas, 2020-05-19, issue #4157, make '_' unique.
  Name
x' <- if Catchall -> Catchall
not (Catchall -> Catchall) -> Catchall -> Catchall
forall a b. (a -> b) -> a -> b
$ Name -> Catchall
forall a. IsNoName a => a -> Catchall
isNoName Name
x then Name -> Nice Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x else do
    NameId
i <- Nice NameId
nextNameId
    Name -> Nice Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x{ nameId :: NameId
nameId = NameId
i }
  Lens' LoneSigs NiceEnv
loneSigs Lens' LoneSigs NiceEnv -> (LoneSigs -> Nice LoneSigs) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> m i) -> m ()
%== \ LoneSigs
s -> do
    let (Maybe LoneSig
mr, LoneSigs
s') = (Name -> LoneSig -> LoneSig -> LoneSig)
-> Name -> LoneSig -> LoneSigs -> (Maybe LoneSig, LoneSigs)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\ Name
_k LoneSig
new LoneSig
_old -> LoneSig
new) Name
x (Range -> Name -> DataRecOrFun -> LoneSig
LoneSig Range
r Name
x' DataRecOrFun
k) LoneSigs
s
    case Maybe LoneSig
mr of
      Maybe LoneSig
Nothing -> LoneSigs -> Nice LoneSigs
forall (m :: * -> *) a. Monad m => a -> m a
return LoneSigs
s'
      Just{}  -> DeclarationException' -> Nice LoneSigs
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice LoneSigs)
-> DeclarationException' -> Nice LoneSigs
forall a b. (a -> b) -> a -> b
$
        if Catchall -> Catchall
not (Catchall -> Catchall) -> Catchall -> Catchall
forall a b. (a -> b) -> a -> b
$ Name -> Catchall
forall a. IsNoName a => a -> Catchall
isNoName Name
x then Name -> DeclarationException'
DuplicateDefinition Name
x else Range -> DeclarationException'
DuplicateAnonDeclaration Range
r
  Name -> Nice Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x'

-- | Remove a lone signature from the state.

removeLoneSig :: Name -> Nice ()
removeLoneSig :: Name -> Nice ()
removeLoneSig Name
x = Lens' LoneSigs NiceEnv
loneSigs Lens' LoneSigs NiceEnv -> (LoneSigs -> LoneSigs) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= Name -> LoneSigs -> LoneSigs
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x

-- | Search for forward type signature.

getSig :: Name -> Nice (Maybe DataRecOrFun)
getSig :: Name -> Nice (Maybe DataRecOrFun)
getSig Name
x = (LoneSig -> DataRecOrFun) -> Maybe LoneSig -> Maybe DataRecOrFun
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LoneSig -> DataRecOrFun
loneSigKind (Maybe LoneSig -> Maybe DataRecOrFun)
-> (LoneSigs -> Maybe LoneSig) -> LoneSigs -> Maybe DataRecOrFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> LoneSigs -> Maybe LoneSig
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (LoneSigs -> Maybe DataRecOrFun)
-> Nice LoneSigs -> Nice (Maybe DataRecOrFun)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' LoneSigs NiceEnv -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs

-- | Check that no lone signatures are left in the state.

noLoneSigs :: Nice Bool
noLoneSigs :: Nice Catchall
noLoneSigs = LoneSigs -> Catchall
forall (t :: * -> *) a. Foldable t => t a -> Catchall
null (LoneSigs -> Catchall) -> Nice LoneSigs -> Nice Catchall
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' LoneSigs NiceEnv -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs

-- | Ensure that all forward declarations have been given a definition.

forgetLoneSigs :: Nice ()
forgetLoneSigs :: Nice ()
forgetLoneSigs = Lens' LoneSigs NiceEnv
loneSigs Lens' LoneSigs NiceEnv -> LoneSigs -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= LoneSigs
forall k a. Map k a
Map.empty

checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs LoneSigs
xs = do
  Nice ()
forgetLoneSigs
  Catchall -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Catchall -> f () -> f ()
unless (LoneSigs -> Catchall
forall k a. Map k a -> Catchall
Map.null LoneSigs
xs) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> DeclarationWarning'
MissingDefinitions ([(Name, Range)] -> DeclarationWarning')
-> [(Name, Range)] -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$
    (LoneSig -> (Name, Range)) -> [LoneSig] -> [(Name, Range)]
forall a b. (a -> b) -> [a] -> [b]
map (\LoneSig
s -> (LoneSig -> Name
loneSigName LoneSig
s , LoneSig -> Range
loneSigRange LoneSig
s)) ([LoneSig] -> [(Name, Range)]) -> [LoneSig] -> [(Name, Range)]
forall a b. (a -> b) -> a -> b
$ LoneSigs -> [LoneSig]
forall k a. Map k a -> [a]
Map.elems LoneSigs
xs

-- | Get names of lone function signatures, plus their unique names.

loneFuns :: LoneSigs -> [(Name,Name)]
loneFuns :: LoneSigs -> [(Name, Name)]
loneFuns = ((Name, LoneSig) -> (Name, Name))
-> [(Name, LoneSig)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((LoneSig -> Name) -> (Name, LoneSig) -> (Name, Name)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second LoneSig -> Name
loneSigName) ([(Name, LoneSig)] -> [(Name, Name)])
-> (LoneSigs -> [(Name, LoneSig)]) -> LoneSigs -> [(Name, Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, LoneSig) -> Catchall)
-> [(Name, LoneSig)] -> [(Name, LoneSig)]
forall a. (a -> Catchall) -> [a] -> [a]
filter (DataRecOrFun -> Catchall
isFunName (DataRecOrFun -> Catchall)
-> ((Name, LoneSig) -> DataRecOrFun) -> (Name, LoneSig) -> Catchall
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSig -> DataRecOrFun
loneSigKind (LoneSig -> DataRecOrFun)
-> ((Name, LoneSig) -> LoneSig) -> (Name, LoneSig) -> DataRecOrFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, LoneSig) -> LoneSig
forall a b. (a, b) -> b
snd) ([(Name, LoneSig)] -> [(Name, LoneSig)])
-> (LoneSigs -> [(Name, LoneSig)]) -> LoneSigs -> [(Name, LoneSig)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSigs -> [(Name, LoneSig)]
forall k a. Map k a -> [(k, a)]
Map.toList

-- | Create a 'LoneSigs' map from an association list.

loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames = (LoneSig -> LoneSig -> LoneSig) -> [(Name, LoneSig)] -> LoneSigs
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith LoneSig -> LoneSig -> LoneSig
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(Name, LoneSig)] -> LoneSigs)
-> ([(Range, Name, DataRecOrFun)] -> [(Name, LoneSig)])
-> [(Range, Name, DataRecOrFun)]
-> LoneSigs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Range, Name, DataRecOrFun) -> (Name, LoneSig))
-> [(Range, Name, DataRecOrFun)] -> [(Name, LoneSig)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Range
r,Name
x,DataRecOrFun
k) -> (Name
x, Range -> Name -> DataRecOrFun -> LoneSig
LoneSig Range
r Name
x DataRecOrFun
k))

-- | Lens for field '_termChk'.

terminationCheckPragma :: Lens' TerminationCheck NiceEnv
terminationCheckPragma :: Lens' TerminationCheck NiceEnv
terminationCheckPragma TerminationCheck -> f TerminationCheck
f NiceEnv
e = TerminationCheck -> f TerminationCheck
f (NiceEnv -> TerminationCheck
_termChk NiceEnv
e) f TerminationCheck -> (TerminationCheck -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ TerminationCheck
s -> NiceEnv
e { _termChk :: TerminationCheck
_termChk = TerminationCheck
s }

withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma :: forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma TerminationCheck
tc Nice a
f = do
  TerminationCheck
tc_old <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
  Lens' TerminationCheck NiceEnv
terminationCheckPragma Lens' TerminationCheck NiceEnv -> TerminationCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= TerminationCheck
tc
  a
result <- Nice a
f
  Lens' TerminationCheck NiceEnv
terminationCheckPragma Lens' TerminationCheck NiceEnv -> TerminationCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= TerminationCheck
tc_old
  a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

coverageCheckPragma :: Lens' CoverageCheck NiceEnv
coverageCheckPragma :: Lens' CoverageCheck NiceEnv
coverageCheckPragma CoverageCheck -> f CoverageCheck
f NiceEnv
e = CoverageCheck -> f CoverageCheck
f (NiceEnv -> CoverageCheck
_covChk NiceEnv
e) f CoverageCheck -> (CoverageCheck -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ CoverageCheck
s -> NiceEnv
e { _covChk :: CoverageCheck
_covChk = CoverageCheck
s }

withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma :: forall a. CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma CoverageCheck
tc Nice a
f = do
  CoverageCheck
tc_old <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
coverageCheckPragma
  Lens' CoverageCheck NiceEnv
coverageCheckPragma Lens' CoverageCheck NiceEnv -> CoverageCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= CoverageCheck
tc
  a
result <- Nice a
f
  Lens' CoverageCheck NiceEnv
coverageCheckPragma Lens' CoverageCheck NiceEnv -> CoverageCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= CoverageCheck
tc_old
  a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Lens for field '_posChk'.

positivityCheckPragma :: Lens' PositivityCheck NiceEnv
positivityCheckPragma :: Lens' PositivityCheck NiceEnv
positivityCheckPragma PositivityCheck -> f PositivityCheck
f NiceEnv
e = PositivityCheck -> f PositivityCheck
f (NiceEnv -> PositivityCheck
_posChk NiceEnv
e) f PositivityCheck -> (PositivityCheck -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ PositivityCheck
s -> NiceEnv
e { _posChk :: PositivityCheck
_posChk = PositivityCheck
s }

withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma :: forall a. PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma PositivityCheck
pc Nice a
f = do
  PositivityCheck
pc_old <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
  Lens' PositivityCheck NiceEnv
positivityCheckPragma Lens' PositivityCheck NiceEnv -> PositivityCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= PositivityCheck
pc
  a
result <- Nice a
f
  Lens' PositivityCheck NiceEnv
positivityCheckPragma Lens' PositivityCheck NiceEnv -> PositivityCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= PositivityCheck
pc_old
  a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Lens for field '_uniChk'.

universeCheckPragma :: Lens' UniverseCheck NiceEnv
universeCheckPragma :: Lens' UniverseCheck NiceEnv
universeCheckPragma UniverseCheck -> f UniverseCheck
f NiceEnv
e = UniverseCheck -> f UniverseCheck
f (NiceEnv -> UniverseCheck
_uniChk NiceEnv
e) f UniverseCheck -> (UniverseCheck -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ UniverseCheck
s -> NiceEnv
e { _uniChk :: UniverseCheck
_uniChk = UniverseCheck
s }

withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma :: forall a. UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma UniverseCheck
uc Nice a
f = do
  UniverseCheck
uc_old <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
  Lens' UniverseCheck NiceEnv
universeCheckPragma Lens' UniverseCheck NiceEnv -> UniverseCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= UniverseCheck
uc
  a
result <- Nice a
f
  Lens' UniverseCheck NiceEnv
universeCheckPragma Lens' UniverseCheck NiceEnv -> UniverseCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= UniverseCheck
uc_old
  a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Get universe check pragma from a data/rec signature.
--   Defaults to 'YesUniverseCheck'.

getUniverseCheckFromSig :: Name -> Nice UniverseCheck
getUniverseCheckFromSig :: Name -> Nice UniverseCheck
getUniverseCheckFromSig Name
x = UniverseCheck
-> (DataRecOrFun -> UniverseCheck)
-> Maybe DataRecOrFun
-> UniverseCheck
forall b a. b -> (a -> b) -> Maybe a -> b
maybe UniverseCheck
YesUniverseCheck DataRecOrFun -> UniverseCheck
universeCheck (Maybe DataRecOrFun -> UniverseCheck)
-> Nice (Maybe DataRecOrFun) -> Nice UniverseCheck
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Nice (Maybe DataRecOrFun)
getSig Name
x

-- | Lens for field '_catchall'.

catchallPragma :: Lens' Catchall NiceEnv
catchallPragma :: Lens' Catchall NiceEnv
catchallPragma Catchall -> f Catchall
f NiceEnv
e = Catchall -> f Catchall
f (NiceEnv -> Catchall
_catchall NiceEnv
e) f Catchall -> (Catchall -> NiceEnv) -> f NiceEnv
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Catchall
s -> NiceEnv
e { _catchall :: Catchall
_catchall = Catchall
s }

-- | Get current catchall pragma, and reset it for the next clause.

popCatchallPragma :: Nice Catchall
popCatchallPragma :: Nice Catchall
popCatchallPragma = do
  Catchall
ca <- Lens' Catchall NiceEnv -> Nice Catchall
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Catchall NiceEnv
catchallPragma
  Lens' Catchall NiceEnv
catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
False
  Catchall -> Nice Catchall
forall (m :: * -> *) a. Monad m => a -> m a
return Catchall
ca

withCatchallPragma :: Catchall -> Nice a -> Nice a
withCatchallPragma :: forall a. Catchall -> Nice a -> Nice a
withCatchallPragma Catchall
ca Nice a
f = do
  Catchall
ca_old <- Lens' Catchall NiceEnv -> Nice Catchall
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Catchall NiceEnv
catchallPragma
  Lens' Catchall NiceEnv
catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
ca
  a
result <- Nice a
f
  Lens' Catchall NiceEnv
catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
ca_old
  a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Add a new warning.
niceWarning :: DeclarationWarning -> Nice ()
niceWarning :: DeclarationWarning -> Nice ()
niceWarning DeclarationWarning
w = (NiceEnv -> NiceEnv) -> Nice ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((NiceEnv -> NiceEnv) -> Nice ())
-> (NiceEnv -> NiceEnv) -> Nice ()
forall a b. (a -> b) -> a -> b
$ \ NiceEnv
st -> NiceEnv
st { niceWarn :: NiceWarnings
niceWarn = DeclarationWarning
w DeclarationWarning -> NiceWarnings -> NiceWarnings
forall a. a -> [a] -> [a]
: NiceEnv -> NiceWarnings
niceWarn NiceEnv
st }

declarationException :: HasCallStack => DeclarationException' -> Nice a
declarationException :: forall a. HasCallStack => DeclarationException' -> Nice a
declarationException DeclarationException'
e = (CallStack -> Nice a) -> Nice a
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Nice a) -> Nice a)
-> (CallStack -> Nice a) -> Nice a
forall a b. (a -> b) -> a -> b
$ DeclarationException -> Nice a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (DeclarationException -> Nice a)
-> (CallStack -> DeclarationException) -> CallStack -> Nice a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallStack -> DeclarationException' -> DeclarationException)
-> DeclarationException' -> CallStack -> DeclarationException
forall a b c. (a -> b -> c) -> b -> a -> c
flip CallStack -> DeclarationException' -> DeclarationException
DeclarationException DeclarationException'
e

declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
declarationWarning' DeclarationWarning'
w CallStack
loc = DeclarationWarning -> Nice ()
niceWarning (DeclarationWarning -> Nice ()) -> DeclarationWarning -> Nice ()
forall a b. (a -> b) -> a -> b
$ CallStack -> DeclarationWarning' -> DeclarationWarning
DeclarationWarning CallStack
loc DeclarationWarning'
w

declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning = (CallStack -> Nice ()) -> Nice ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
-> (DeclarationWarning' -> CallStack -> Nice ())
-> DeclarationWarning'
-> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning' -> CallStack -> Nice ()
declarationWarning'