{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Syntax.Concrete.Definitions.Monad where

import Prelude hiding ( null )

import Control.Monad        ( unless )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
import Control.Monad.Reader ( MonadReader, ReaderT, runReaderT )
import Control.Monad.State  ( MonadState(..), modify, State, runState )

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 qualified Agda.Utils.List1 as List1
import Agda.Utils.Null (Null(..))

import Agda.Utils.Impossible

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

newtype Nice a = Nice { forall a.
Nice a
-> ReaderT
     NiceEnv (ExceptT DeclarationException (State NiceState)) a
unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a }
  deriving ( 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
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
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
           , MonadReader NiceEnv, MonadState NiceState, MonadError DeclarationException
           )

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

instance Null a => Null (Nice a) where
  empty :: Nice a
empty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Null a => a
empty
  null :: Nice a -> Bool
null Nice a
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Nicifier parameters.

data NiceEnv = NiceEnv
  { NiceEnv -> Bool
safeButNotBuiltin :: Bool
       -- ^ We are in a module declared @--safe@ which is not a builtin module.
  }

-- | Nicifier state.

data NiceState = NiceState
  { NiceState -> LoneSigs
_loneSigs :: LoneSigs
    -- ^ Lone type signatures that wait for their definition.
  , NiceState -> TerminationCheck
_termChk  :: TerminationCheck
    -- ^ Termination checking pragma waiting for a definition.
  , NiceState -> PositivityCheck
_posChk   :: PositivityCheck
    -- ^ Positivity checking pragma waiting for a definition.
  , NiceState -> UniverseCheck
_uniChk   :: UniverseCheck
    -- ^ Universe checking pragma waiting for a data/rec signature or definition.
  , NiceState -> Bool
_catchall :: Catchall
    -- ^ Catchall pragma waiting for a function clause.
  , NiceState -> CoverageCheck
_covChk  :: CoverageCheck
    -- ^ Coverage pragma waiting for a definition.
  , NiceState -> NiceWarnings
niceWarn :: NiceWarnings
    -- ^ Stack of warnings. Head is last warning.
  , NiceState -> 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
  }
  deriving Int -> LoneSig -> ShowS
[LoneSig] -> ShowS
LoneSig -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LoneSig] -> ShowS
$cshowList :: [LoneSig] -> ShowS
show :: LoneSig -> String
$cshow :: LoneSig -> String
showsPrec :: Int -> LoneSig -> ShowS
$cshowsPrec :: Int -> LoneSig -> ShowS
Show

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.

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

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

nextNameId :: Nice NameId
nextNameId :: Nice NameId
nextNameId = do
  NameId
i <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState NameId
lensNameId
  Lens' NiceState NameId
lensNameId forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (i -> i) -> m ()
%= forall a. Enum a => a -> a
succ
  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' NiceState LoneSigs
loneSigs :: Lens' NiceState LoneSigs
loneSigs LoneSigs -> f LoneSigs
f NiceState
e = LoneSigs -> f LoneSigs
f (NiceState -> LoneSigs
_loneSigs NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ LoneSigs
s -> NiceState
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' <- case Name
x of
    Name{}     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
x
    NoName Range
r NameId
_ -> Range -> NameId -> Name
NoName Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nice NameId
nextNameId
  Lens' NiceState LoneSigs
loneSigs forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (i -> m i) -> m ()
%== \ LoneSigs
s -> do
    let (Maybe LoneSig
mr, LoneSigs
s') = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return LoneSigs
s'
      Just{}  -> forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$
        if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. IsNoName a => a -> Bool
isNoName Name
x then Name -> DeclarationException'
DuplicateDefinition Name
x else Range -> DeclarationException'
DuplicateAnonDeclaration Range
r
  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' NiceState LoneSigs
loneSigs forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (i -> i) -> m ()
%= 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LoneSig -> DataRecOrFun
loneSigKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState LoneSigs
loneSigs

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

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

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

-- | Ensure that all forward declarations have been given a definition.
checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs LoneSigs
xs = do
  Nice ()
forgetLoneSigs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k a. Map k a -> Bool
Map.null LoneSigs
xs) forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> DeclarationWarning'
MissingDefinitions forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map (\LoneSig
s -> (LoneSig -> Name
loneSigName LoneSig
s , LoneSig -> Range
loneSigRange LoneSig
s)) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems LoneSigs
xs

-- | Ensure that all forward declarations have been given a definition,
-- raising an error indicating *why* they would have had to have been
-- defined.
breakImplicitMutualBlock :: Range -> String -> Nice ()
breakImplicitMutualBlock :: Range -> String -> Nice ()
breakImplicitMutualBlock Range
r String
why = do
  LoneSigs
m <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState LoneSigs
loneSigs
  forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull (forall k a. Map k a -> [a]
Map.elems LoneSigs
m) forall a b. (a -> b) -> a -> b
$ \ List1 LoneSig
xs ->
    forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Range -> String -> List1 Name -> DeclarationException'
DisallowedInterleavedMutual Range
r String
why forall a b. (a -> b) -> a -> b
$
      -- Andreas, 2023-09-07: We discard the 'loneSigRange's because the 'Name' already has a range.
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LoneSig -> Name
loneSigName List1 LoneSig
xs

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

loneFuns :: LoneSigs -> [(Name,Name)]
loneFuns :: LoneSigs -> [(Name, Name)]
loneFuns = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second LoneSig -> Name
loneSigName) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (DataRecOrFun -> Bool
isFunName forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSig -> DataRecOrFun
loneSigKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' NiceState TerminationCheck
terminationCheckPragma :: Lens' NiceState TerminationCheck
terminationCheckPragma TerminationCheck -> f TerminationCheck
f NiceState
e = TerminationCheck -> f TerminationCheck
f (NiceState -> TerminationCheck
_termChk NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ TerminationCheck
s -> NiceState
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 <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState TerminationCheck
terminationCheckPragma
  Lens' NiceState TerminationCheck
terminationCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= TerminationCheck
tc
  a
result <- Nice a
f
  Lens' NiceState TerminationCheck
terminationCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= TerminationCheck
tc_old
  forall (m :: * -> *) a. Monad m => a -> m a
return a
result

coverageCheckPragma :: Lens' NiceState CoverageCheck
coverageCheckPragma :: Lens' NiceState CoverageCheck
coverageCheckPragma CoverageCheck -> f CoverageCheck
f NiceState
e = CoverageCheck -> f CoverageCheck
f (NiceState -> CoverageCheck
_covChk NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ CoverageCheck
s -> NiceState
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 <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState CoverageCheck
coverageCheckPragma
  Lens' NiceState CoverageCheck
coverageCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= CoverageCheck
tc
  a
result <- Nice a
f
  Lens' NiceState CoverageCheck
coverageCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= CoverageCheck
tc_old
  forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Lens for field '_posChk'.

positivityCheckPragma :: Lens' NiceState PositivityCheck
positivityCheckPragma :: Lens' NiceState PositivityCheck
positivityCheckPragma PositivityCheck -> f PositivityCheck
f NiceState
e = PositivityCheck -> f PositivityCheck
f (NiceState -> PositivityCheck
_posChk NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ PositivityCheck
s -> NiceState
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 <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState PositivityCheck
positivityCheckPragma
  Lens' NiceState PositivityCheck
positivityCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= PositivityCheck
pc
  a
result <- Nice a
f
  Lens' NiceState PositivityCheck
positivityCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= PositivityCheck
pc_old
  forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Lens for field '_uniChk'.

universeCheckPragma :: Lens' NiceState UniverseCheck
universeCheckPragma :: Lens' NiceState UniverseCheck
universeCheckPragma UniverseCheck -> f UniverseCheck
f NiceState
e = UniverseCheck -> f UniverseCheck
f (NiceState -> UniverseCheck
_uniChk NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ UniverseCheck
s -> NiceState
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 <- forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use Lens' NiceState UniverseCheck
universeCheckPragma
  Lens' NiceState UniverseCheck
universeCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= UniverseCheck
uc
  a
result <- Nice a
f
  Lens' NiceState UniverseCheck
universeCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= UniverseCheck
uc_old
  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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe UniverseCheck
YesUniverseCheck DataRecOrFun -> UniverseCheck
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' NiceState Catchall
catchallPragma :: Lens' NiceState Bool
catchallPragma Bool -> f Bool
f NiceState
e = Bool -> f Bool
f (NiceState -> Bool
_catchall NiceState
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Bool
s -> NiceState
e { _catchall :: Bool
_catchall = Bool
s }

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

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

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

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

declarationException :: HasCallStack => DeclarationException' -> Nice a
declarationException :: forall a. HasCallStack => DeclarationException' -> Nice a
declarationException DeclarationException'
e = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ CallStack -> DeclarationWarning' -> DeclarationWarning
DeclarationWarning CallStack
loc DeclarationWarning'
w

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