{-# OPTIONS_GHC -Wunused-imports #-}

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 -> 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
           , 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 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)
-> (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
  }
  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.

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' NiceEnv NameId
lensNameId :: Lens' NiceEnv NameId
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 = i }

nextNameId :: Nice NameId
nextNameId :: Nice NameId
nextNameId = do
  NameId
i <- Lens' NiceEnv NameId -> Nice NameId
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (NameId -> f NameId) -> NiceEnv -> f NiceEnv
Lens' NiceEnv NameId
lensNameId
  (NameId -> f NameId) -> NiceEnv -> f NiceEnv
Lens' NiceEnv NameId
lensNameId Lens' NiceEnv 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' NiceEnv LoneSigs
loneSigs :: Lens' NiceEnv LoneSigs
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 = 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs Lens' NiceEnv 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 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 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs Lens' NiceEnv 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' NiceEnv LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs

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

noLoneSigs :: Nice Bool
noLoneSigs :: Nice Catchall
noLoneSigs = LoneSigs -> Catchall
forall a. Map Name a -> 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' NiceEnv LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs

forgetLoneSigs :: Nice ()
forgetLoneSigs :: Nice ()
forgetLoneSigs = (LoneSigs -> f LoneSigs) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs Lens' NiceEnv 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
  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

-- | 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
xs <- Lens' NiceEnv LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceEnv -> f NiceEnv
Lens' NiceEnv LoneSigs
loneSigs
  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
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> String -> [(Name, Range)] -> DeclarationException'
DisallowedInterleavedMutual Range
r String
why ([(Name, Range)] -> DeclarationException')
-> [(Name, Range)] -> DeclarationException'
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 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) -> 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' NiceEnv TerminationCheck
terminationCheckPragma :: Lens' NiceEnv TerminationCheck
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 = 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' NiceEnv TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv TerminationCheck
terminationCheckPragma
  (TerminationCheck -> f TerminationCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv TerminationCheck
terminationCheckPragma Lens' NiceEnv 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv TerminationCheck
terminationCheckPragma Lens' NiceEnv 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' NiceEnv CoverageCheck
coverageCheckPragma :: Lens' NiceEnv CoverageCheck
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 = 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' NiceEnv CoverageCheck -> Nice CoverageCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (CoverageCheck -> f CoverageCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv CoverageCheck
coverageCheckPragma
  (CoverageCheck -> f CoverageCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv CoverageCheck
coverageCheckPragma Lens' NiceEnv 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv CoverageCheck
coverageCheckPragma Lens' NiceEnv 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' NiceEnv PositivityCheck
positivityCheckPragma :: Lens' NiceEnv PositivityCheck
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 = 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' NiceEnv PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv PositivityCheck
positivityCheckPragma
  (PositivityCheck -> f PositivityCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv PositivityCheck
positivityCheckPragma Lens' NiceEnv 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv PositivityCheck
positivityCheckPragma Lens' NiceEnv 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' NiceEnv UniverseCheck
universeCheckPragma :: Lens' NiceEnv UniverseCheck
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 = 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' NiceEnv UniverseCheck -> Nice UniverseCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (UniverseCheck -> f UniverseCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv UniverseCheck
universeCheckPragma
  (UniverseCheck -> f UniverseCheck) -> NiceEnv -> f NiceEnv
Lens' NiceEnv UniverseCheck
universeCheckPragma Lens' NiceEnv 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) -> NiceEnv -> f NiceEnv
Lens' NiceEnv UniverseCheck
universeCheckPragma Lens' NiceEnv 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' NiceEnv Catchall
catchallPragma :: Lens' NiceEnv Catchall
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 = s }

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

popCatchallPragma :: Nice Catchall
popCatchallPragma :: Nice Catchall
popCatchallPragma = do
  Catchall
ca <- Lens' NiceEnv Catchall -> Nice Catchall
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Catchall -> f Catchall) -> NiceEnv -> f NiceEnv
Lens' NiceEnv Catchall
catchallPragma
  (Catchall -> f Catchall) -> NiceEnv -> f NiceEnv
Lens' NiceEnv Catchall
catchallPragma Lens' NiceEnv Catchall -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Catchall
False
  Catchall -> Nice Catchall
forall a. a -> Nice a
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' NiceEnv Catchall -> Nice Catchall
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Catchall -> f Catchall) -> NiceEnv -> f NiceEnv
Lens' NiceEnv Catchall
catchallPragma
  (Catchall -> f Catchall) -> NiceEnv -> f NiceEnv
Lens' NiceEnv Catchall
catchallPragma Lens' NiceEnv Catchall -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Catchall
ca
  a
result <- Nice a
f
  (Catchall -> f Catchall) -> NiceEnv -> f NiceEnv
Lens' NiceEnv Catchall
catchallPragma Lens' NiceEnv Catchall -> Catchall -> Nice ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= Catchall
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 = (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 = 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'