module Agda.Syntax.Concrete.Definitions.Monad where

import Control.Monad        ( unless )
import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
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 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 -> 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
           , 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 = 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
. NiceEnv -> 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 -> ExceptT DeclarationException (State NiceEnv) a
unNice Nice a
m) 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 = 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 :: 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) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' NameId NiceEnv
lensNameId
  Lens' NameId NiceEnv
lensNameId forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (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' LoneSigs NiceEnv
loneSigs :: Lens' LoneSigs NiceEnv
loneSigs LoneSigs -> f LoneSigs
f NiceEnv
e = LoneSigs -> f LoneSigs
f (NiceEnv -> LoneSigs
_loneSigs NiceEnv
e) 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' <- 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' LoneSigs NiceEnv
loneSigs forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (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 Catchall -> Catchall
not forall a b. (a -> b) -> a -> b
$ forall a. IsNoName a => a -> Catchall
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' LoneSigs NiceEnv
loneSigs forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (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' 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 = forall (t :: * -> *) a. Foldable t => t a -> Catchall
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= forall k a. Map k a
Map.empty

checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs :: LoneSigs -> Nice ()
checkLoneSigs LoneSigs
xs = do
  Nice ()
forgetLoneSigs
  forall (f :: * -> *). Applicative f => Catchall -> f () -> f ()
unless (forall k a. Map k a -> Catchall
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

-- | 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 -> Catchall) -> [a] -> [a]
filter (DataRecOrFun -> Catchall
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' TerminationCheck NiceEnv
terminationCheckPragma :: Lens' TerminationCheck NiceEnv
terminationCheckPragma TerminationCheck -> f TerminationCheck
f NiceEnv
e = TerminationCheck -> f TerminationCheck
f (NiceEnv -> TerminationCheck
_termChk NiceEnv
e) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
  Lens' TerminationCheck NiceEnv
terminationCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= TerminationCheck
tc
  a
result <- Nice a
f
  Lens' TerminationCheck NiceEnv
terminationCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= TerminationCheck
tc_old
  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) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
coverageCheckPragma
  Lens' CoverageCheck NiceEnv
coverageCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= CoverageCheck
tc
  a
result <- Nice a
f
  Lens' CoverageCheck NiceEnv
coverageCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= CoverageCheck
tc_old
  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) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
  Lens' PositivityCheck NiceEnv
positivityCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= PositivityCheck
pc
  a
result <- Nice a
f
  Lens' PositivityCheck NiceEnv
positivityCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= PositivityCheck
pc_old
  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) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
  Lens' UniverseCheck NiceEnv
universeCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= UniverseCheck
uc
  a
result <- Nice a
f
  Lens' UniverseCheck NiceEnv
universeCheckPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> 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' Catchall NiceEnv
catchallPragma :: Lens' Catchall NiceEnv
catchallPragma Catchall -> f Catchall
f NiceEnv
e = Catchall -> f Catchall
f (NiceEnv -> Catchall
_catchall NiceEnv
e) 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Catchall NiceEnv
catchallPragma
  Lens' Catchall NiceEnv
catchallPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
False
  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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Catchall NiceEnv
catchallPragma
  Lens' Catchall NiceEnv
catchallPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
ca
  a
result <- Nice a
f
  Lens' Catchall NiceEnv
catchallPragma forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Catchall
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
$ \ NiceEnv
st -> NiceEnv
st { niceWarn :: NiceWarnings
niceWarn = DeclarationWarning
w 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 = 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'