{-# 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 -> 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
$cfmap :: forall a b. (a -> b) -> Nice a -> Nice b
fmap :: forall a b. (a -> b) -> Nice a -> Nice b
$c<$ :: forall a b. a -> Nice b -> Nice a
<$ :: forall a b. a -> Nice b -> Nice a
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
$cpure :: forall a. a -> Nice a
pure :: forall a. a -> Nice a
$c<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
$cliftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
liftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
$c*> :: forall a b. Nice a -> Nice b -> Nice b
*> :: forall a b. Nice a -> Nice b -> Nice b
$c<* :: forall a b. Nice a -> Nice b -> Nice a
<* :: forall a b. Nice a -> Nice b -> 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
$c>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
$c>> :: forall a b. Nice a -> Nice b -> Nice b
>> :: forall a b. Nice a -> Nice b -> Nice b
$creturn :: forall a. a -> Nice a
return :: forall a. a -> Nice a
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 = (NiceState -> NiceWarnings)
-> (Either DeclarationException a, NiceState)
-> (Either DeclarationException a, NiceWarnings)
forall b c a. (b -> c) -> (a, b) -> (a, c)
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)
-> (NiceState -> NiceWarnings) -> NiceState -> NiceWarnings
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NiceState -> NiceWarnings
niceWarn) ((Either DeclarationException a, NiceState)
 -> (Either DeclarationException a, NiceWarnings))
-> (Either DeclarationException a, NiceState)
-> (Either DeclarationException a, NiceWarnings)
forall a b. (a -> b) -> a -> b
$
  ExceptT DeclarationException (State NiceState) a
-> StateT NiceState Identity (Either DeclarationException a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Nice a
-> ReaderT
     NiceEnv (ExceptT DeclarationException (State NiceState)) a
forall a.
Nice a
-> ReaderT
     NiceEnv (ExceptT DeclarationException (State NiceState)) a
unNice Nice a
m ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a
-> NiceEnv -> ExceptT DeclarationException (State NiceState) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` NiceEnv
env) StateT NiceState Identity (Either DeclarationException a)
-> NiceState -> (Either DeclarationException a, NiceState)
forall s a. State s a -> s -> (a, s)
`runState` NiceState
initNiceState

instance Null a => Null (Nice a) where
  empty :: Nice a
empty = a -> Nice a
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
forall a. Null a => a
empty
  null :: Nice a -> Bool
null Nice a
_ = Bool
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
(Int -> LoneSig -> ShowS)
-> (LoneSig -> String) -> ([LoneSig] -> ShowS) -> Show LoneSig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LoneSig -> ShowS
showsPrec :: Int -> LoneSig -> ShowS
$cshow :: LoneSig -> String
show :: LoneSig -> String
$cshowList :: [LoneSig] -> ShowS
showList :: [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 = 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 :: 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) f NameId -> (NameId -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ NameId
i -> NiceState
e { _nameId = i }

nextNameId :: Nice NameId
nextNameId :: Nice NameId
nextNameId = do
  NameId
i <- Lens' NiceState NameId -> Nice NameId
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (NameId -> f NameId) -> NiceState -> f NiceState
Lens' NiceState NameId
lensNameId
  (NameId -> f NameId) -> NiceState -> f NiceState
Lens' NiceState NameId
lensNameId Lens' NiceState NameId -> (NameId -> NameId) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (i -> i) -> m ()
%= NameId -> NameId
forall a. Enum a => a -> a
succ
  NameId -> Nice NameId
forall a. a -> Nice a
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) f LoneSigs -> (LoneSigs -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ LoneSigs
s -> NiceState
e { _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{}     -> Name -> Nice Name
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
x
    NoName Range
r NameId
_ -> Range -> NameId -> Name
NoName Range
r (NameId -> Name) -> Nice NameId -> Nice Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nice NameId
nextNameId
  (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs Lens' NiceState LoneSigs -> (LoneSigs -> Nice LoneSigs) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (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 a. a -> Nice a
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 Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x then Name -> DeclarationException'
DuplicateDefinition Name
x else Range -> DeclarationException'
DuplicateAnonDeclaration Range
r
  Name -> Nice Name
forall a. a -> Nice a
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 = (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs Lens' NiceState LoneSigs -> (LoneSigs -> LoneSigs) -> Nice ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' o i -> (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 a b. (a -> b) -> Maybe a -> Maybe b
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' NiceState LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs

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

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

forgetLoneSigs :: Nice ()
forgetLoneSigs :: Nice ()
forgetLoneSigs = (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs Lens' NiceState LoneSigs -> LoneSigs -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= LoneSigs
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
  Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LoneSigs -> Bool
forall k a. Map k a -> Bool
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

-- | 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 <- Lens' NiceState LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs
  [LoneSig] -> (List1 LoneSig -> Nice ()) -> Nice ()
forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull (LoneSigs -> [LoneSig]
forall k a. Map k a -> [a]
Map.elems LoneSigs
m) ((List1 LoneSig -> Nice ()) -> Nice ())
-> (List1 LoneSig -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ \ List1 LoneSig
xs ->
    DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> String -> List1 Name -> DeclarationException'
DisallowedInterleavedMutual Range
r String
why (List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$
      -- Andreas, 2023-09-07: We discard the 'loneSigRange's because the 'Name' already has a range.
      (LoneSig -> Name) -> List1 LoneSig -> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
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 = ((Name, LoneSig) -> (Name, Name))
-> [(Name, LoneSig)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((LoneSig -> Name) -> (Name, LoneSig) -> (Name, Name)
forall b c a. (b -> c) -> (a, b) -> (a, c)
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) -> Bool) -> [(Name, LoneSig)] -> [(Name, LoneSig)]
forall a. (a -> Bool) -> [a] -> [a]
filter (DataRecOrFun -> Bool
isFunName (DataRecOrFun -> Bool)
-> ((Name, LoneSig) -> DataRecOrFun) -> (Name, LoneSig) -> Bool
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' NiceState TerminationCheck
terminationCheckPragma :: Lens' NiceState TerminationCheck
terminationCheckPragma TerminationCheck -> f TerminationCheck
f NiceState
e = TerminationCheck -> f TerminationCheck
f (NiceState -> TerminationCheck
_termChk NiceState
e) f TerminationCheck
-> (TerminationCheck -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ TerminationCheck
s -> NiceState
e { _termChk = 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' NiceState TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma
  (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma Lens' NiceState TerminationCheck -> TerminationCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= TerminationCheck
tc
  a
result <- Nice a
f
  (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma Lens' NiceState TerminationCheck -> TerminationCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= TerminationCheck
tc_old
  a -> Nice a
forall a. a -> Nice a
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) f CoverageCheck -> (CoverageCheck -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ CoverageCheck
s -> NiceState
e { _covChk = 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' NiceState CoverageCheck -> Nice CoverageCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (CoverageCheck -> f CoverageCheck) -> NiceState -> f NiceState
Lens' NiceState CoverageCheck
coverageCheckPragma
  (CoverageCheck -> f CoverageCheck) -> NiceState -> f NiceState
Lens' NiceState CoverageCheck
coverageCheckPragma Lens' NiceState CoverageCheck -> CoverageCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= CoverageCheck
tc
  a
result <- Nice a
f
  (CoverageCheck -> f CoverageCheck) -> NiceState -> f NiceState
Lens' NiceState CoverageCheck
coverageCheckPragma Lens' NiceState CoverageCheck -> CoverageCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= CoverageCheck
tc_old
  a -> Nice a
forall a. a -> Nice a
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) f PositivityCheck -> (PositivityCheck -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PositivityCheck
s -> NiceState
e { _posChk = 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' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
  (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma Lens' NiceState PositivityCheck -> PositivityCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= PositivityCheck
pc
  a
result <- Nice a
f
  (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma Lens' NiceState PositivityCheck -> PositivityCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= PositivityCheck
pc_old
  a -> Nice a
forall a. a -> Nice a
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) f UniverseCheck -> (UniverseCheck -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ UniverseCheck
s -> NiceState
e { _uniChk = 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' NiceState UniverseCheck -> Nice UniverseCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (UniverseCheck -> f UniverseCheck) -> NiceState -> f NiceState
Lens' NiceState UniverseCheck
universeCheckPragma
  (UniverseCheck -> f UniverseCheck) -> NiceState -> f NiceState
Lens' NiceState UniverseCheck
universeCheckPragma Lens' NiceState UniverseCheck -> UniverseCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= UniverseCheck
uc
  a
result <- Nice a
f
  (UniverseCheck -> f UniverseCheck) -> NiceState -> f NiceState
Lens' NiceState UniverseCheck
universeCheckPragma Lens' NiceState UniverseCheck -> UniverseCheck -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= UniverseCheck
uc_old
  a -> Nice a
forall a. 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' NiceState Catchall
catchallPragma :: Lens' NiceState Bool
catchallPragma Bool -> f Bool
f NiceState
e = Bool -> f Bool
f (NiceState -> Bool
_catchall NiceState
e) f Bool -> (Bool -> NiceState) -> f NiceState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Bool
s -> NiceState
e { _catchall = s }

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

popCatchallPragma :: Nice Catchall
popCatchallPragma :: Nice Bool
popCatchallPragma = do
  Bool
ca <- Lens' NiceState Bool -> Nice Bool
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Bool -> f Bool) -> NiceState -> f NiceState
Lens' NiceState Bool
catchallPragma
  (Bool -> f Bool) -> NiceState -> f NiceState
Lens' NiceState Bool
catchallPragma Lens' NiceState Bool -> Bool -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Bool
False
  Bool -> Nice Bool
forall a. a -> Nice a
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 <- Lens' NiceState Bool -> Nice Bool
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Bool -> f Bool) -> NiceState -> f NiceState
Lens' NiceState Bool
catchallPragma
  (Bool -> f Bool) -> NiceState -> f NiceState
Lens' NiceState Bool
catchallPragma Lens' NiceState Bool -> Bool -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Bool
ca
  a
result <- Nice a
f
  (Bool -> f Bool) -> NiceState -> f NiceState
Lens' NiceState Bool
catchallPragma Lens' NiceState Bool -> Bool -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Bool
ca_old
  a -> Nice a
forall a. 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 = (NiceState -> NiceState) -> Nice ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((NiceState -> NiceState) -> Nice ())
-> (NiceState -> NiceState) -> Nice ()
forall a b. (a -> b) -> a -> b
$ \ NiceState
st -> NiceState
st { niceWarn = w : niceWarn 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 a. 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'