-- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's.
--
--   * Attach fixity and syntax declarations to the definition they refer to.
--
--   * Distribute the following attributes to the individual definitions:
--       @abstract@,
--       @instance@,
--       @postulate@,
--       @primitive@,
--       @private@,
--       termination pragmas.
--
--   * Gather the function clauses belonging to one function definition.
--
--   * Expand ellipsis @...@ in function clauses following @with@.
--
--   * Infer mutual blocks.
--     A block starts when a lone signature is encountered, and ends when
--     all lone signatures have seen their definition.
--
--   * Handle interleaved mutual blocks.
--     In an `interleaved mutual' block we:
--     * leave the data and fun sigs in place
--     * classify signatures in `constructor' block based on their return type
--       and group them all as a data def at the position in the block where the
--       first constructor for the data sig in question occured
--     * classify fun clauses based on the declared function used and group them
--       all as a fundef at the position in the block where the first such fun
--       clause appeared
--
--   * Report basic well-formedness error,
--     when one of the above transformation fails.
--     When possible, errors should be deferred to the scope checking phase
--     (ConcreteToAbstract), where we are in the TCM and can produce more
--     informative error messages.

{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

module Agda.Syntax.Concrete.Definitions
    ( NiceDeclaration(..)
    , NiceConstructor, NiceTypeSignature
    , Clause(..)
    , DeclarationException(..)
    , DeclarationWarning(..), DeclarationWarning'(..), unsafeDeclarationWarning
    , Nice, NiceEnv(..), runNice
    , niceDeclarations
    , notSoNiceDeclarations
    , niceHasAbstract
    , Measure
    , declarationWarningName
    ) where


import Prelude hiding (null)

import Control.Monad.Except  ( )
import Control.Monad.Reader  ( asks )
import Control.Monad.State   ( MonadState(..), gets, runStateT )

import Data.Either           ( isRight )
import Data.Function         ( on )
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.List as List
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav

import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Common hiding (TerminationCheck())
import Agda.Syntax.Position
import Agda.Syntax.Notation
import Agda.Syntax.Concrete.Fixity
import Agda.Syntax.Concrete.Definitions.Errors
import Agda.Syntax.Concrete.Definitions.Monad
import Agda.Syntax.Concrete.Definitions.Types

import Agda.Utils.AffineHole
import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List (spanJust)
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Three
import Agda.Utils.Tuple
import Agda.Utils.Update

import Agda.Utils.Impossible

{--------------------------------------------------------------------------
    The niceifier
 --------------------------------------------------------------------------}

-- | Check that declarations in a mutual block are consistently
--   equipped with MEASURE pragmas, or whether there is a
--   NO_TERMINATION_CHECK pragma.
combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks Range
r = [TerminationCheck] -> Nice TerminationCheck
loop
  where
  loop :: [TerminationCheck] -> Nice TerminationCheck
  loop :: [TerminationCheck] -> Nice TerminationCheck
loop []         = TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
TerminationCheck
  loop (TerminationCheck
tc : [TerminationCheck]
tcs) = do
    tc' <- [TerminationCheck] -> Nice TerminationCheck
loop [TerminationCheck]
tcs
    case (tc, tc') of
      (TerminationCheck
TerminationCheck      , TerminationCheck
tc'                   ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc'
      (TerminationCheck
tc                    , TerminationCheck
TerminationCheck      ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
      (TerminationCheck
NonTerminating        , TerminationCheck
NonTerminating        ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
NonTerminating
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
NoTerminationCheck
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
Terminating           ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
      (TerminationCheck
Terminating           , TerminationCheck
NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
      (TerminationCheck
Terminating           , TerminationCheck
Terminating           ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
forall m. TerminationCheck m
Terminating
      (TerminationMeasure{}  , TerminationMeasure{}  ) -> TerminationCheck -> Nice TerminationCheck
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
      (TerminationMeasure Range
r Name
_, TerminationCheck
NoTerminationCheck    ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationMeasure Range
r Name
_, TerminationCheck
Terminating           ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NoTerminationCheck    , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
Terminating           , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationMeasure Range
r Name
_, TerminationCheck
NonTerminating        ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationMeasure Range
r Name
_) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
NonTerminating        ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
Terminating           , TerminationCheck
NonTerminating        ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationCheck
NoTerminationCheck    ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationCheck
Terminating           ) -> Range -> Nice TerminationCheck
forall {a}. Range -> Nice a
failure Range
r
  failure :: Range -> Nice a
failure Range
r = DeclarationException' -> Nice a
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice a)
-> DeclarationException' -> Nice a
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationException'
InvalidMeasureMutual Range
r

combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
combineCoverageChecks = [CoverageCheck] -> CoverageCheck
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold

combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks = [PositivityCheck] -> PositivityCheck
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold

data DeclKind
    = LoneSigDecl Range DataRecOrFun Name
    | LoneDefs DataRecOrFun [Name]
    | OtherDecl
  deriving (DeclKind -> DeclKind -> Bool
(DeclKind -> DeclKind -> Bool)
-> (DeclKind -> DeclKind -> Bool) -> Eq DeclKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeclKind -> DeclKind -> Bool
== :: DeclKind -> DeclKind -> Bool
$c/= :: DeclKind -> DeclKind -> Bool
/= :: DeclKind -> DeclKind -> Bool
Eq, Int -> DeclKind -> ShowS
[DeclKind] -> ShowS
DeclKind -> String
(Int -> DeclKind -> ShowS)
-> (DeclKind -> String) -> ([DeclKind] -> ShowS) -> Show DeclKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclKind -> ShowS
showsPrec :: Int -> DeclKind -> ShowS
$cshow :: DeclKind -> String
show :: DeclKind -> String
$cshowList :: [DeclKind] -> ShowS
showList :: [DeclKind] -> ShowS
Show)

declKind :: NiceDeclaration -> DeclKind
declKind :: NiceDeclaration -> DeclKind
declKind (FunSig Range
r Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
ai TerminationCheck
tc CoverageCheck
cc Name
x Expr
_)     = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (ArgInfo -> TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName ArgInfo
ai TerminationCheck
tc CoverageCheck
cc) Name
x
declKind (NiceRecSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_)    = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (NiceDataSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_)   = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (FunDef Range
_r List1 Declaration
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
cc Name
x (Clause
cl :| [Clause]
_)) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (ArgInfo -> TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName (Clause -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Clause
cl) TerminationCheck
tc CoverageCheck
cc) [Name
x]
declKind (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_par [NiceDeclaration]
_)  = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceUnquoteData Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [Name]
_ Expr
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
_ [LamBinding]
_par [Declaration]
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Name]
xs Expr
_)   = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (ArgInfo -> TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName ArgInfo
forall a. Null a => a
empty TerminationCheck
tc CoverageCheck
cc) [Name]
xs
declKind Axiom{}                             = DeclKind
OtherDecl
declKind NiceField{}                         = DeclKind
OtherDecl
declKind PrimitiveFunction{}                 = DeclKind
OtherDecl
declKind NiceMutual{}                        = DeclKind
OtherDecl
declKind NiceModule{}                        = DeclKind
OtherDecl
declKind NiceModuleMacro{}                   = DeclKind
OtherDecl
declKind NiceOpen{}                          = DeclKind
OtherDecl
declKind NiceImport{}                        = DeclKind
OtherDecl
declKind NicePragma{}                        = DeclKind
OtherDecl
declKind NiceFunClause{}                     = DeclKind
OtherDecl
declKind NicePatternSyn{}                    = DeclKind
OtherDecl
declKind NiceGeneralize{}                    = DeclKind
OtherDecl
declKind NiceUnquoteDecl{}                   = DeclKind
OtherDecl
declKind NiceLoneConstructor{}               = DeclKind
OtherDecl
declKind NiceOpaque{}                        = DeclKind
OtherDecl

-- | Replace @(Data/Rec/Fun)Sigs@ with @Axiom@s for postulated names.
--   The first argument is a list of axioms only.
replaceSigs
  :: LoneSigs               -- ^ Lone signatures to be turned into Axioms.
  -> [NiceDeclaration]      -- ^ Declarations containing them.
  -> [NiceDeclaration]      -- ^ In the output, everything should be defined.
replaceSigs :: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps = if LoneSigs -> Bool
forall k a. Map k a -> Bool
Map.null LoneSigs
ps then [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> a
id else \case
  []     -> [NiceDeclaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
  (NiceDeclaration
d:[NiceDeclaration]
ds) ->
    case NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable NiceDeclaration
d of
      -- If declaration d of x is mentioned in the map of lone signatures then replace
      -- it with an axiom.
      Just (Name
x, NiceDeclaration
axiom)
        | (Just (LoneSig Range
_ Name
x' DataRecOrFun
_), LoneSigs
ps') <- (Name -> LoneSig -> Maybe LoneSig)
-> Name -> LoneSigs -> (Maybe LoneSig, LoneSigs)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\ Name
_ LoneSig
_ -> Maybe LoneSig
forall a. Maybe a
Nothing) Name
x LoneSigs
ps
        , Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x'
            -- Use the range as UID to ensure we do not replace the wrong signature.
            -- This could happen if the user wrote a duplicate definition.
        -> NiceDeclaration
axiom NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps' [NiceDeclaration]
ds
      Maybe (Name, NiceDeclaration)
_ -> NiceDeclaration
d     NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps  [NiceDeclaration]
ds

  where

    -- A @replaceable@ declaration is a signature. It has a name and we can make an
    -- @Axiom@ out of it.
    replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
    replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable = \case
      FunSig Range
r Access
acc IsAbstract
abst IsInstance
inst IsMacro
_ ArgInfo
argi TerminationCheck
_ CoverageCheck
_ Name
x' Expr
e -> do
        -- #4881: Don't use the unique NameId for NoName lookups.
        let x :: Name
x = if Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x' then Range -> Name
noName (Name -> Range
nameRange Name
x') else Name
x'
        let ai :: ArgInfo
ai = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
argi
        (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
inst ArgInfo
ai Name
x' Expr
e)
      NiceRecSig  Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t -> Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> [LamBinding]
-> Expr
-> Maybe (Name, NiceDeclaration)
forall {m :: * -> *}.
Monad m =>
Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> [LamBinding]
-> Expr
-> m (Name, NiceDeclaration)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x [LamBinding]
pars Expr
t
      NiceDataSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t -> Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> [LamBinding]
-> Expr
-> Maybe (Name, NiceDeclaration)
forall {m :: * -> *}.
Monad m =>
Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> [LamBinding]
-> Expr
-> m (Name, NiceDeclaration)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x [LamBinding]
pars Expr
t
      NiceDeclaration
_ -> Maybe (Name, NiceDeclaration)
forall a. Maybe a
Nothing
      where
        retAx :: Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> [LamBinding]
-> Expr
-> m (Name, NiceDeclaration)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x [LamBinding]
pars Expr
t = do
          let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t
          let ai :: ArgInfo
ai = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (Erased -> Quantity
asQuantity Erased
erased) ArgInfo
defaultArgInfo)
          (Name, NiceDeclaration) -> m (Name, NiceDeclaration)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef ArgInfo
ai Name
x Expr
e)

-- | Main. Fixities (or more precisely syntax declarations) are needed when
--   grouping function clauses.
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations Fixities
fixs [Declaration]
ds = do

  -- Run the nicifier in an initial environment. But keep the warnings.
  st <- Nice NiceState
forall s (m :: * -> *). MonadState s m => m s
get
  put $ initNiceState { niceWarn = niceWarn st }
  nds <- nice ds

  -- Check that every signature got its definition.
  ps <- use loneSigs
  checkLoneSigs ps
  -- We postulate the missing ones and insert them in place of the corresponding @FunSig@
  let ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
nds

  -- Note that loneSigs is ensured to be empty.
  -- (Important, since inferMutualBlocks also uses loneSigs state).
  res <- inferMutualBlocks ds

  -- Restore the old state, but keep the warnings.
  warns <- gets niceWarn
  put $ st { niceWarn = warns }
  return res

  where

    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    inferMutualBlocks (NiceDeclaration
d : [NiceDeclaration]
ds) =
      case NiceDeclaration -> DeclKind
declKind NiceDeclaration
d of
        DeclKind
OtherDecl    -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds
        LoneDefs{}   -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds  -- Andreas, 2017-10-09, issue #2576: report error in ConcreteToAbstract
        LoneSigDecl Range
r DataRecOrFun
k Name
x  -> do
          _ <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k
          InferredMutual checks nds0 ds1 <- untilAllDefined (mutualChecks k) ds
          -- If we still have lone signatures without any accompanying definition,
          -- we postulate the definition and substitute the axiom for the lone signature
          ps <- use loneSigs
          checkLoneSigs ps
          let ds0 = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
nds0) -- NB: don't forget the LoneSig the block started with!
          -- We then keep processing the rest of the block
          tc <- combineTerminationChecks (getRange d) (mutualTermination checks)
          let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks              (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
          let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks            (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
          (NiceMutual empty tc cc pc ds0 :) <$> inferMutualBlocks ds1
      where
        untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
        untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds = do
          done <- Nice Bool
noLoneSigs
          if done then return (InferredMutual checks [] ds) else
            case ds of
              []     -> InferredMutual -> Nice InferredMutual
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
checks [] [NiceDeclaration]
ds)
              NiceDeclaration
d : [NiceDeclaration]
ds -> case NiceDeclaration -> DeclKind
declKind NiceDeclaration
d of
                LoneSigDecl Range
r DataRecOrFun
k Name
x -> do
                  Nice Name -> Nice ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Nice Name -> Nice ()) -> Nice Name -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k
                  NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock  NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                LoneDefs DataRecOrFun
k [Name]
xs -> do
                  (Name -> Nice ()) -> [Name] -> Nice ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> Nice ()
removeLoneSig [Name]
xs
                  NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock  NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                DeclKind
OtherDecl -> NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds

    nice :: [Declaration] -> Nice [NiceDeclaration]
    nice :: [Declaration] -> Nice [NiceDeclaration]
nice [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    nice [Declaration]
ds = do
      (xs , ys) <- [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      (xs ++) <$> nice ys

    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 []     = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], []) -- Andreas, 2017-09-16, issue #2759: no longer __IMPOSSIBLE__
    nice1 (Declaration
d:[Declaration]
ds) = do
      let justWarning :: HasCallStack => DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
          justWarning :: HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning DeclarationWarning'
w = do
            -- NOTE: This is the location of the invoker of justWarning, not here.
            (CallStack -> Nice ()) -> Nice ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
-> (CallStack -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationWarning' -> CallStack -> Nice ()
declarationWarning' DeclarationWarning'
w
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

      case Declaration
d of

        TypeSig ArgInfo
info TacticAttribute
tac Name
x Expr
t -> do
          TacticAttribute -> Nice ()
dropTactic TacticAttribute
tac
          termCheck <- 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
          covCheck  <- use coverageCheckPragma
          -- Andreas, 2020-09-28, issue #4950: take only range of identifier,
          -- since parser expands type signatures with several identifiers
          -- (like @x y z : A@) into several type signatures (with imprecise ranges).
          let r = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
          -- register x as lone type signature, to recognize clauses later
          x' <- addLoneSig r x $ FunName info termCheck covCheck
          return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x' t] , ds)

        -- Should not show up: all FieldSig are part of a Field block
        FieldSig{} -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__

        Generalize KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyGeneralize KwRange
r
        Generalize KwRange
_ [Declaration]
sigs -> do
          gs <- [Declaration]
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
sigs ((Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration])
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ \case
            sig :: Declaration
sig@(TypeSig ArgInfo
info TacticAttribute
tac Name
x Expr
t) -> do
              -- Andreas, 2022-03-25, issue #5850:
              -- Warn about @variable {x} : A@ which is equivalent to @variable x : A@.
              Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) (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
$ Range -> DeclarationWarning'
HiddenGeneralize (Range -> DeclarationWarning') -> Range -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
              NiceDeclaration -> Nice NiceDeclaration
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
sig) Access
PublicAccess ArgInfo
info TacticAttribute
tac Name
x Expr
t
            Declaration
_ -> Nice NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__
          return (gs, ds)

        FunClause ArgInfo
ai LHS
lhs RHS
_ WhereClause
_ Catchall
_ -> do
          termCheck <- 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
          covCheck  <- use coverageCheckPragma
          catchall  <- popCatchallPragma
          xs <- loneFuns <$> use loneSigs
          -- for each type signature 'x' waiting for clauses, we try
          -- if we have some clauses for 'x'
          case [ (x, (x', fits, rest))
               | (x, x') <- xs
               , let (fits0, rest) =
                      -- Anonymous declarations only have 1 clause each!
                      if isNoName x then ([d], ds)
                      else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
               , fits <- maybeToList $ List1.nonEmpty fits0
               ] of

            -- case: clauses match none of the sigs
            [] -> case LHS
lhs of
              -- Subcase: The lhs is single identifier (potentially anonymous).
              -- Treat it as a function clause without a type signature.
              LHS Pattern
p [] [] | Just Name
x <- Pattern -> Maybe Name
isSingleIdentifierP Pattern
p -> do
                d  <- ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Maybe Expr
-> List1 Declaration
-> Nice [NiceDeclaration]
mkFunDef (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
ai) TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
forall a. Maybe a
Nothing (List1 Declaration -> Nice [NiceDeclaration])
-> List1 Declaration -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton Declaration
d -- fun def without type signature can have modality
                return (d , ds)
              -- Subcase: The lhs is a proper pattern.
              -- This could be a let-pattern binding. Pass it on.
              -- A missing type signature error might be raise in ConcreteToAbstract
              LHS
_ -> do
                ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Catchall
-> Declaration
-> NiceDeclaration
NiceFunClause (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef TerminationCheck
termCheck CoverageCheck
covCheck Catchall
catchall Declaration
d] , [Declaration]
ds)

            -- case: clauses match exactly one of the sigs
            [(Name
x, (Arg ArgInfo
info Name
x', List1 Declaration
fits, [Declaration]
rest))] -> do
               -- The x'@NoName{} is the unique version of x@NoName{}.
               Name -> Nice ()
removeLoneSig Name
x
               ds <- List1 Declaration -> Nice (List1 Declaration)
expandEllipsis1 List1 Declaration
fits
               cs <- mkClauses1 info x' ds empty
               return ([FunDef (getRange fits) fits ConcreteDef NotInstanceDef termCheck covCheck x' cs] , rest)

            -- case: clauses match more than one sigs (ambiguity)
            (Name, (Arg Name, List1 Declaration, [Declaration]))
xf:[(Name, (Arg Name, List1 Declaration, [Declaration]))]
xfs -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs (List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Name -> List1 Name
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ ((Name, (Arg Name, List1 Declaration, [Declaration])) -> Name)
-> NonEmpty (Name, (Arg Name, List1 Declaration, [Declaration]))
-> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, (Arg Name, List1 Declaration, [Declaration])) -> Name
forall a b. (a, b) -> a
fst (NonEmpty (Name, (Arg Name, List1 Declaration, [Declaration]))
 -> List1 Name)
-> NonEmpty (Name, (Arg Name, List1 Declaration, [Declaration]))
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, (Arg Name, List1 Declaration, [Declaration]))
xf (Name, (Arg Name, List1 Declaration, [Declaration]))
-> [(Name, (Arg Name, List1 Declaration, [Declaration]))]
-> NonEmpty (Name, (Arg Name, List1 Declaration, [Declaration]))
forall a. a -> [a] -> NonEmpty a
:| [(Name, (Arg Name, List1 Declaration, [Declaration]))]
xfs
                 -- "ambiguous function clause; cannot assign it uniquely to one type signature"

        Field KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyField KwRange
r
        Field KwRange
_ [Declaration]
fs -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          [Declaration]
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
fs \case
            d :: Declaration
d@(FieldSig IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt) -> NiceDeclaration -> Nice NiceDeclaration
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt
            Declaration
d -> DeclarationException' -> Nice NiceDeclaration
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice NiceDeclaration)
-> DeclarationException' -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
FieldBlock (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d

        DataSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
          pc <- 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
          uc <- use universeCheckPragma
          _ <- addLoneSig r x $ DataName pc uc
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig erased) (niceAxioms DataBlock) r
                      x (Just (tel, t)) Nothing

        Data Range
r Erased
erased Name
x [LamBinding]
tel Expr
t [Declaration]
cs -> do
          pc <- 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
          -- Andreas, 2018-10-27, issue #3327
          -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
          -- Universe check is performed if both the current value of
          -- 'universeCheckPragma' AND the one from the signature say so.
          uc <- use universeCheckPragma
          uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
          mt <- defaultTypeSig (DataName pc uc) x (Just t)
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig erased) (niceAxioms DataBlock) r
                      x ((tel,) <$> mt) (Just (tel, cs))

        DataDef Range
r Name
x [LamBinding]
tel [Declaration]
cs -> do
          pc <- 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
          -- Andreas, 2018-10-27, issue #3327
          -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
          -- Universe check is performed if both the current value of
          -- 'universeCheckPragma' AND the one from the signature say so.
          uc <- use universeCheckPragma
          uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
          mt <- defaultTypeSig (DataName pc uc) x Nothing
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig defaultErased)
                      (niceAxioms DataBlock) r x ((tel,) <$> mt)
                      (Just (tel, cs))

        RecordSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
          pc <- 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
          uc <- use universeCheckPragma
          _ <- addLoneSig r x $ RecName pc uc
          return ( [NiceRecSig r erased PublicAccess ConcreteDef pc uc x
                      tel t]
                 , ds
                 )

        Record Range
r Erased
erased Name
x [RecordDirective]
dir [LamBinding]
tel Expr
t [Declaration]
cs -> do
          pc <- 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
          -- Andreas, 2018-10-27, issue #3327
          -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
          -- Universe check is performed if both the current value of
          -- 'universeCheckPragma' AND the one from the signature say so.
          uc <- use universeCheckPragma
          uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
          mt <- defaultTypeSig (RecName pc uc) x (Just t)
          (,ds) <$> dataOrRec pc uc
                      (\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs ->
                        Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs)
                      (flip NiceRecSig erased) return r x
                      ((tel,) <$> mt) (Just (tel, cs))

        RecordDef Range
r Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs   -> do
          pc <- 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
          -- Andreas, 2018-10-27, issue #3327
          -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
          -- Universe check is performed if both the current value of
          -- 'universeCheckPragma' AND the one from the signature say so.
          uc <- use universeCheckPragma
          uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
          mt <- defaultTypeSig (RecName pc uc) x Nothing
          (,ds) <$> dataOrRec pc uc
                      (\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs ->
                        Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
tel [Declaration]
cs)
                      (flip NiceRecSig defaultErased) return r x
                      ((tel,) <$> mt) (Just (tel, cs))

        Mutual KwRange
r [Declaration]
ds' -> do
          -- The lone signatures encountered so far are not in scope
          -- for the mutual definition
          KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`mutual` blocks"
          case [Declaration]
ds' of
            [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual KwRange
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))

        InterleavedMutual KwRange
r [Declaration]
ds' -> do
          -- The lone signatures encountered so far are not in scope
          -- for the mutual definition
          KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`interleaved mutual` blocks"
          case [Declaration]
ds' of
            [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual KwRange
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))

        Abstract KwRange
r []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyAbstract KwRange
r
        Abstract KwRange
r [Declaration]
ds' ->
          (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
abstractBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')

        Private KwRange
r Origin
UserWritten []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPrivate KwRange
r
        Private KwRange
r Origin
o [Declaration]
ds' ->
          (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')

        InstanceB KwRange
r []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyInstance KwRange
r
        InstanceB KwRange
r [Declaration]
ds' ->
          (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')

        Macro KwRange
r []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMacro KwRange
r
        Macro KwRange
r [Declaration]
ds' ->
          (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
macroBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds')

        LoneConstructor KwRange
r [Declaration]
ds' -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
constructorBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
ConstructorBlock [Declaration]
ds'

        Postulate KwRange
r [Declaration]
ds' -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
postulateBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PostulateBlock [Declaration]
ds'

        Primitive KwRange
r [Declaration]
ds' -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
primitiveBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PrimitiveBlock [Declaration]
ds'

        Module Range
r Erased
erased QName
x Telescope
tel [Declaration]
ds' -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$
          ([Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
PublicAccess IsAbstract
ConcreteDef Erased
erased QName
x Telescope
tel [Declaration]
ds'], [Declaration]
ds)

        ModuleMacro Range
r Erased
erased Name
x ModuleApplication
modapp OpenShortHand
op ImportDirective
is -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$
          ([Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
PublicAccess Erased
erased Name
x ModuleApplication
modapp OpenShortHand
op ImportDirective
is], [Declaration]
ds)

        -- Fixity and syntax declarations and polarity pragmas have
        -- already been processed.
        Infix Fixity
_ List1 Name
_  -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
        Syntax Name
_ Notation
_ -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)

        PatternSyn Range
r Name
n [WithHiding Name]
as Pattern
p -> do
          ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceDeclaration
NicePatternSyn Range
r Access
PublicAccess Name
n [WithHiding Name]
as Pattern
p] , [Declaration]
ds)
        Open Range
r QName
x ImportDirective
is         -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> QName -> ImportDirective -> NiceDeclaration
NiceOpen Range
r QName
x ImportDirective
is] , [Declaration]
ds)
        Import Range
r QName
x Maybe AsName
as OpenShortHand
op ImportDirective
is -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceImport Range
r QName
x Maybe AsName
as OpenShortHand
op ImportDirective
is] , [Declaration]
ds)

        UnquoteDecl Range
r [Name]
xs Expr
e -> do
          tc <- 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
          cc <- use coverageCheckPragma
          return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds)

        UnquoteDef Range
r [Name]
xs Expr
e -> do
          sigs <- ((Name, Arg Name) -> Name) -> [(Name, Arg Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Arg Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Arg Name)] -> [Name])
-> (LoneSigs -> [(Name, Arg Name)]) -> LoneSigs -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSigs -> [(Name, Arg Name)]
loneFuns (LoneSigs -> [Name]) -> Nice LoneSigs -> Nice [Name]
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
          List1.ifNotNull (filter (`notElem` sigs) xs)
            {-then-} (declarationException . UnquoteDefRequiresSignature)
            {-else-} $ do
              mapM_ removeLoneSig xs
              return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds)

        UnquoteData Range
r Name
xs [Name]
cs Expr
e -> do
          pc <- 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
          uc <- use universeCheckPragma
          return ([NiceUnquoteData r PublicAccess ConcreteDef pc uc xs cs e], ds)

        Pragma Pragma
p -> do
          -- Warn about unsafe pragmas unless we are in a builtin module.
          Nice Bool -> Nice () -> Nice ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((NiceEnv -> Bool) -> Nice Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks NiceEnv -> Bool
safeButNotBuiltin) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$
            Maybe DeclarationWarning'
-> (DeclarationWarning' -> Nice ()) -> Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Pragma -> Maybe DeclarationWarning'
forall m. CMaybe DeclarationWarning' m => Pragma -> m
unsafePragma Pragma
p) ((DeclarationWarning' -> Nice ()) -> Nice ())
-> (DeclarationWarning' -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ \ DeclarationWarning'
w ->
              HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning DeclarationWarning'
w
          Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma Pragma
p [Declaration]
ds

        Opaque KwRange
r [Declaration]
ds' -> do
          KwRange -> String -> Nice ()
breakImplicitMutualBlock KwRange
r String
"`opaque` blocks"

          -- Split the enclosed declarations into an initial run of
          -- 'unfolding' statements and the rest of the body.
          let
            ([[QName]]
unfoldings, [Declaration]
body) = ((Declaration -> Maybe [QName])
 -> [Declaration] -> ([[QName]], [Declaration]))
-> [Declaration]
-> (Declaration -> Maybe [QName])
-> ([[QName]], [Declaration])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Declaration -> Maybe [QName])
-> [Declaration] -> ([[QName]], [Declaration])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
spanMaybe [Declaration]
ds' ((Declaration -> Maybe [QName]) -> ([[QName]], [Declaration]))
-> (Declaration -> Maybe [QName]) -> ([[QName]], [Declaration])
forall a b. (a -> b) -> a -> b
$ \case
              Unfolding KwRange
_ [QName]
ns -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
ns
              Declaration
_ -> Maybe [QName]
forall a. Maybe a
Nothing

          -- The body of an 'opaque' definition can have mutual
          -- recursion by interleaving type signatures and definitions,
          -- just like the body of a module.
          decls0 <- [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
body
          ps <- use loneSigs
          checkLoneSigs ps
          let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
decls0
          body <- inferMutualBlocks decls
          pure ([NiceOpaque r (concat unfoldings) body], ds)

        Unfolding KwRange
r [QName]
_ -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationException'
UnfoldingOutsideOpaque KwRange
r

    -- Some pragmas attach to the following declarations,
    -- handle this situation here.

    nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma Pragma
p [Declaration]
ds = case Pragma
p of

     TerminationCheckPragma Range
r TerminationCheck
NoTerminationCheck -> do
      -- This PRAGMA has been deprecated in favour of (NON_)TERMINATING
      -- We warn the user about it and then assume the function is NON_TERMINATING.
      HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
PragmaNoTerminationCheck Range
r
      Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma (Range -> TerminationCheck -> Pragma
TerminationCheckPragma Range
r TerminationCheck
forall m. TerminationCheck m
NonTerminating) [Declaration]
ds

     TerminationCheckPragma Range
r (TerminationMeasure Range
_ Name
x) ->
      if [Declaration] -> Bool
canHaveTerminationMeasure [Declaration]
ds then
        TerminationCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma (Range -> Name -> TerminationCheck
forall m. Range -> m -> TerminationCheck m
TerminationMeasure Range
r Name
x) (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidTerminationCheckPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     TerminationCheckPragma Range
r TerminationCheck
tc ->
      if [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds then
        TerminationCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma TerminationCheck
tc (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidTerminationCheckPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     NoCoverageCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveCoverageCheckPragma [Declaration]
ds then
        CoverageCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma CoverageCheck
NoCoverageCheck (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCoverageCheckPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     CatchallPragma Range
r ->
      if [Declaration] -> Bool
canHaveCatchallPragma [Declaration]
ds then
        Catchall
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. Catchall -> Nice a -> Nice a
withCatchallPragma (Range -> Catchall
YesCatchall Range
r) (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     NoPositivityCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds then
        PositivityCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma PositivityCheck
NoPositivityCheck (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidNoPositivityCheckPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     NoUniverseCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveNoUniverseCheckPragma [Declaration]
ds then
        UniverseCheck
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma UniverseCheck
NoUniverseCheck (Nice ([NiceDeclaration], [Declaration])
 -> Nice ([NiceDeclaration], [Declaration]))
-> Nice ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidNoUniverseCheckPragma Range
r
        [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

     -- Polarity pragmas have been handled with fixity declarations, can be deleted.
     PolarityPragma{} -> ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)

     -- The other pragmas are less context-sensitive, so nothing to do:
     BuiltinPragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     CompilePragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     DisplayPragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     EtaPragma{}                   -> Nice ([NiceDeclaration], [Declaration])
keep
     ForeignPragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     ImpossiblePragma{}            -> Nice ([NiceDeclaration], [Declaration])
keep
     InjectiveForInferencePragma{} -> Nice ([NiceDeclaration], [Declaration])
keep
     InjectivePragma{}             -> Nice ([NiceDeclaration], [Declaration])
keep
     InlinePragma{}                -> Nice ([NiceDeclaration], [Declaration])
keep
     NotProjectionLikePragma{}     -> Nice ([NiceDeclaration], [Declaration])
keep
     OptionsPragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     OverlapPragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     RewritePragma{}               -> Nice ([NiceDeclaration], [Declaration])
keep
     StaticPragma{}                -> Nice ([NiceDeclaration], [Declaration])
keep
     WarningOnImport{}             -> Nice ([NiceDeclaration], [Declaration])
keep
     WarningOnUsage{}              -> Nice ([NiceDeclaration], [Declaration])
keep

     where keep :: Nice ([NiceDeclaration], [Declaration])
keep = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)

    canHaveTerminationMeasure :: [Declaration] -> Bool
    canHaveTerminationMeasure :: [Declaration] -> Bool
canHaveTerminationMeasure [] = Bool
False
    canHaveTerminationMeasure (Declaration
d:[Declaration]
ds) = case Declaration
d of
      TypeSig{} -> Bool
True
      (Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveTerminationMeasure [Declaration]
ds
      Declaration
_         -> Bool
False

    canHaveTerminationCheckPragma :: [Declaration] -> Bool
    canHaveTerminationCheckPragma :: [Declaration] -> Bool
canHaveTerminationCheckPragma []     = Bool
False
    canHaveTerminationCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
      Mutual KwRange
_ [Declaration]
ds   -> (Declaration -> Bool) -> [Declaration] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveTerminationCheckPragma ([Declaration] -> Bool)
-> (Declaration -> [Declaration]) -> Declaration -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton) [Declaration]
ds
      TypeSig{}     -> Bool
True
      FunClause{}   -> Bool
True
      UnquoteDecl{} -> Bool
True
      (Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds
      Declaration
_             -> Bool
False

    canHaveCoverageCheckPragma :: [Declaration] -> Bool
    canHaveCoverageCheckPragma :: [Declaration] -> Bool
canHaveCoverageCheckPragma = [Declaration] -> Bool
canHaveTerminationCheckPragma

    canHaveCatchallPragma :: [Declaration] -> Bool
    canHaveCatchallPragma :: [Declaration] -> Bool
canHaveCatchallPragma []     = Bool
False
    canHaveCatchallPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
      FunClause{} -> Bool
True
      (Pragma Pragma
p) | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveCatchallPragma [Declaration]
ds
      Declaration
_           -> Bool
False

    canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
    canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
canHaveNoPositivityCheckPragma []     = Bool
False
    canHaveNoPositivityCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
      Mutual KwRange
_ [Declaration]
ds                   -> (Declaration -> Bool) -> [Declaration] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveNoPositivityCheckPragma ([Declaration] -> Bool)
-> (Declaration -> [Declaration]) -> Declaration -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton) [Declaration]
ds
      Data{}                        -> Bool
True
      DataSig{}                     -> Bool
True
      DataDef{}                     -> Bool
True
      Record{}                      -> Bool
True
      RecordSig{}                   -> Bool
True
      RecordDef{}                   -> Bool
True
      Pragma Pragma
p | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds
      Declaration
_                             -> Bool
False

    canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
    canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
canHaveNoUniverseCheckPragma []     = Bool
False
    canHaveNoUniverseCheckPragma (Declaration
d:[Declaration]
ds) = case Declaration
d of
      Data{}                        -> Bool
True
      DataSig{}                     -> Bool
True
      DataDef{}                     -> Bool
True
      Record{}                      -> Bool
True
      RecordSig{}                   -> Bool
True
      RecordDef{}                   -> Bool
True
      Pragma Pragma
p | Pragma -> Bool
isAttachedPragma Pragma
p -> [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds
      Declaration
_                             -> Bool
False

    -- Pragma that attaches to the following declaration.
    isAttachedPragma :: Pragma -> Bool
    isAttachedPragma :: Pragma -> Bool
isAttachedPragma = \case
      TerminationCheckPragma{}  -> Bool
True
      CatchallPragma{}          -> Bool
True
      NoPositivityCheckPragma{} -> Bool
True
      NoUniverseCheckPragma{}   -> Bool
True
      Pragma
_                         -> Bool
False

    -- We could add a default type signature here, but at the moment we can't
    -- infer the type of a record or datatype, so better to just fail here.
    defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
    defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
defaultTypeSig DataRecOrFun
_ Name
_ t :: Maybe Expr
t@Just{} = Maybe Expr -> Nice (Maybe Expr)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
t
    defaultTypeSig DataRecOrFun
k Name
x Maybe Expr
Nothing  = do
      Nice (Maybe DataRecOrFun)
-> Nice (Maybe Expr)
-> (DataRecOrFun -> Nice (Maybe Expr))
-> Nice (Maybe Expr)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Name -> Nice (Maybe DataRecOrFun)
getSig Name
x) (Maybe Expr -> Nice (Maybe Expr)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing) ((DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr))
-> (DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ \ DataRecOrFun
k' -> do
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (DataRecOrFun -> DataRecOrFun -> Bool
sameKind DataRecOrFun
k DataRecOrFun
k') (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
$ Name -> DataRecOrFun -> DataRecOrFun -> DeclarationException'
WrongDefinition Name
x DataRecOrFun
k' DataRecOrFun
k
        Maybe Expr
forall a. Maybe a
Nothing Maybe Expr -> Nice () -> Nice (Maybe Expr)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Name -> Nice ()
removeLoneSig Name
x

    dataOrRec
      :: forall a decl
      .  PositivityCheck
      -> UniverseCheck
      -> (Range -> Origin -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> [decl] -> NiceDeclaration)
         -- Construct definition.
      -> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration)
         -- Construct signature.
      -> ([a] -> Nice [decl])        -- Constructor checking.
      -> Range
      -> Name                        -- Data/record type name.
      -> Maybe ([LamBinding], Expr)  -- Parameters and type.  If not @Nothing@ a signature is created.
      -> Maybe ([LamBinding], [a])   -- Parameters and constructors.  If not @Nothing@, a definition body is created.
      -> Nice [NiceDeclaration]
    dataOrRec :: forall a decl.
PositivityCheck
-> UniverseCheck
-> (Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [decl]
    -> NiceDeclaration)
-> (Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration)
-> ([a] -> Nice [decl])
-> Range
-> Name
-> Maybe ([LamBinding], Expr)
-> Maybe ([LamBinding], [a])
-> Nice [NiceDeclaration]
dataOrRec PositivityCheck
pc UniverseCheck
uc Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig [a] -> Nice [decl]
niceD Range
r Name
x Maybe ([LamBinding], Expr)
mt Maybe ([LamBinding], [a])
mcs = do
      mds <- Maybe ([LamBinding], [a])
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe ([LamBinding], [a])
mcs ((([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
 -> Nice (Maybe ([LamBinding], [decl])))
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall a b. (a -> b) -> a -> b
$ \ ([LamBinding]
tel, [a]
cs) -> ([LamBinding]
tel,) ([decl] -> ([LamBinding], [decl]))
-> Nice [decl] -> Nice ([LamBinding], [decl])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Nice [decl]
niceD [a]
cs
      -- We set origin to UserWritten if the user split the data/rec herself,
      -- and to Inserted if the she wrote a single declaration that we're
      -- splitting up here. We distinguish these because the scoping rules for
      -- generalizable variables differ in these cases.
      let o | Maybe ([LamBinding], Expr) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], Expr)
mt Bool -> Bool -> Bool
&& Maybe ([LamBinding], [a]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], [a])
mcs = Origin
Inserted
            | Bool
otherwise               = Origin
UserWritten
      return $ catMaybes $
        [ mt  <&> \ ([LamBinding]
tel, Expr
t)  -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig (Name -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Expr
t) Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel Expr
t
        , mds <&> \ ([LamBinding]
tel, [decl]
ds) -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
r Origin
o IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x (Maybe ([LamBinding], Expr)
-> [LamBinding]
-> (([LamBinding], Expr) -> [LamBinding])
-> [LamBinding]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ([LamBinding], Expr)
mt [LamBinding]
tel ((([LamBinding], Expr) -> [LamBinding]) -> [LamBinding])
-> (([LamBinding], Expr) -> [LamBinding]) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. a -> b -> a
const ([LamBinding] -> ([LamBinding], Expr) -> [LamBinding])
-> [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
tel) [decl]
ds
          -- If a type is given (mt /= Nothing), we have to delete the types in @tel@
          -- for the data definition, lest we duplicate them. And also drop modalities (#1886).
        ]
    -- Translate axioms
    niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
    niceAxioms :: KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds = [[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[NiceDeclaration]] -> [NiceDeclaration])
-> Nice [[NiceDeclaration]] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> Nice [NiceDeclaration])
-> [Declaration] -> Nice [[NiceDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Declaration -> Nice [NiceDeclaration]
niceAxiom [Declaration]
ds
      where
        niceAxiom :: TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
        niceAxiom :: Declaration -> Nice [NiceDeclaration]
niceAxiom = \case
          d :: Declaration
d@(TypeSig ArgInfo
rel TacticAttribute
tac Name
x Expr
t) -> do
            TacticAttribute -> Nice ()
dropTactic TacticAttribute
tac
            [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef ArgInfo
rel Name
x Expr
t ]
          -- @instance@ and @private@ blocks mix well with other blocks.
          InstanceB KwRange
r [Declaration]
ds -> KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds
          Private KwRange
r Origin
o [Declaration]
ds | Bool
privateAllowed -> KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds
          -- @data _ where@, @postulate@ and @primitive@ blocks exclude each other.
          Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
          Pragma p :: Pragma
p@(OverlapPragma Range
r [QName]
_ OverlapMode
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
          Declaration
d -> DeclarationException' -> Nice [NiceDeclaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [NiceDeclaration])
-> DeclarationException' -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
b (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d
        -- @private@ is not allowed for constructors.
        privateAllowed :: Bool
        privateAllowed :: Bool
privateAllowed = case KindOfBlock
b of
          KindOfBlock
PrimitiveBlock   -> Bool
True
          KindOfBlock
PostulateBlock   -> Bool
True
          KindOfBlock
DataBlock        -> Bool
False
          KindOfBlock
ConstructorBlock -> Bool
False
          -- We do not handle @field@ blocks here.
          KindOfBlock
FieldBlock -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

    constructorBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    constructorBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
constructorBlock KwRange
r [] = [] [NiceDeclaration] -> Nice () -> Nice [NiceDeclaration]
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (KwRange -> DeclarationWarning'
EmptyConstructor KwRange
r)
    constructorBlock KwRange
r [NiceDeclaration]
ds = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceDeclaration] -> Nice [NiceDeclaration])
-> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> NiceDeclaration -> [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r [NiceDeclaration]
ds

    postulateBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    postulateBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
postulateBlock KwRange
r [] = [] [NiceDeclaration] -> Nice () -> Nice [NiceDeclaration]
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (KwRange -> DeclarationWarning'
EmptyPostulate KwRange
r)
    postulateBlock KwRange
_ [NiceDeclaration]
ds = [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds

    primitiveBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    primitiveBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
primitiveBlock KwRange
r [] = [] [NiceDeclaration] -> Nice () -> Nice [NiceDeclaration]
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (KwRange -> DeclarationWarning'
EmptyPrimitive KwRange
r)
    primitiveBlock KwRange
_ [NiceDeclaration]
ds = (NiceDeclaration -> Nice NiceDeclaration)
-> [NiceDeclaration] -> Nice [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM NiceDeclaration -> Nice NiceDeclaration
toPrim [NiceDeclaration]
ds

    toPrim :: NiceDeclaration -> Nice NiceDeclaration
    toPrim :: NiceDeclaration -> Nice NiceDeclaration
toPrim (Axiom Range
r Access
p IsAbstract
a IsInstance
inst ArgInfo
rel Name
x Expr
t) = do
      case IsInstance
inst of
        InstanceDef KwRange
r  -> HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
UselessInstance KwRange
r
        IsInstance
NotInstanceDef -> () -> Nice ()
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      NiceDeclaration -> Nice NiceDeclaration
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x (ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
rel Expr
t)
    toPrim NiceDeclaration
_ = Nice NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Create a function definition.
    mkFunDef ::
         ArgInfo
      -> TerminationCheck
      -> CoverageCheck
      -> Name
      -> Maybe Expr
      -> List1 Declaration
      -> Nice [NiceDeclaration]
    mkFunDef :: ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Maybe Expr
-> List1 Declaration
-> Nice [NiceDeclaration]
mkFunDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
mt List1 Declaration
ds0 = do
      ds <- List1 Declaration -> Nice (List1 Declaration)
expandEllipsis1 List1 Declaration
ds0
      cs <- mkClauses1 info x ds empty
      return [ FunSig (fuseRange x t) PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x t
             , FunDef (getRange ds0) ds0 ConcreteDef NotInstanceDef termCheck covCheck x cs ]
        where
          t :: Expr
t = Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (Range -> Expr
underscore (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x)) Maybe Expr
mt

    underscore :: Range -> Expr
underscore Range
r = Range -> Maybe String -> Expr
Underscore Range
r Maybe String
forall a. Maybe a
Nothing

    -- Search for the first clause that does not have an ellipsis (usually the very first one)
    -- and then use its lhs pattern to replace ellipses in the subsequent clauses (if any).
    expandEllipsis :: [Declaration] -> Nice [Declaration]
    expandEllipsis :: [Declaration] -> Nice [Declaration]
expandEllipsis [] = [Declaration] -> Nice [Declaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    expandEllipsis (Declaration
d : [Declaration]
ds) = List1 Declaration -> [Item (List1 Declaration)]
List1 Declaration -> [Declaration]
forall l. IsList l => l -> [Item l]
List1.toList (List1 Declaration -> [Declaration])
-> Nice (List1 Declaration) -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Declaration -> Nice (List1 Declaration)
expandEllipsis1 (Declaration
d Declaration -> [Declaration] -> List1 Declaration
forall a. a -> [a] -> NonEmpty a
:| [Declaration]
ds)

    expandEllipsis1 :: List1 Declaration -> Nice (List1 Declaration)
    expandEllipsis1 :: List1 Declaration -> Nice (List1 Declaration)
expandEllipsis1 (d :: Declaration
d@(FunClause ArgInfo
_ (LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Catchall
_) :| [Declaration]
ds)
      | Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p = (Declaration
d Declaration -> [Declaration] -> List1 Declaration
forall a. a -> [a] -> NonEmpty a
:|) ([Declaration] -> List1 Declaration)
-> Nice [Declaration] -> Nice (List1 Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds
      | Bool
otherwise     = (Declaration
d Declaration -> [Declaration] -> List1 Declaration
forall a. a -> [a] -> NonEmpty a
:|) ([Declaration] -> List1 Declaration)
-> Nice [Declaration] -> Nice (List1 Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p) [Declaration]
ds
      where
        expand :: Pattern -> [Declaration] -> Nice [Declaration]
        expand :: Pattern -> [Declaration] -> Nice [Declaration]
expand Pattern
_ [] = [Declaration] -> Nice [Declaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        expand Pattern
p (Declaration
d : [Declaration]
ds) = do
          case Declaration
d of
            Pragma (CatchallPragma Range
_) -> do
                  (Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand Pattern
p [Declaration]
ds
            FunClause ArgInfo
ai (LHS Pattern
p0 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Catchall
ca -> do
              case Pattern -> AffineHole Pattern Pattern
forall p. CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' Pattern
p0 of
                AffineHole Pattern Pattern
ManyHoles -> DeclarationException' -> Nice [Declaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [Declaration])
-> DeclarationException' -> Nice [Declaration]
forall a b. (a -> b) -> a -> b
$ Pattern -> DeclarationException'
MultipleEllipses Pattern
p0
                OneHole KillRangeT Pattern
cxt ~(EllipsisP Range
r Maybe Pattern
Nothing) -> do
                  -- Replace the ellipsis by @p@.
                  let p1 :: Pattern
p1 = KillRangeT Pattern
cxt KillRangeT Pattern -> KillRangeT Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Pattern -> Pattern
EllipsisP Range
r (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Range -> KillRangeT Pattern
forall a. SetRange a => Range -> a -> a
setRange Range
r Pattern
p
                  let d' :: Declaration
d' = ArgInfo -> LHS -> RHS -> WhereClause -> Catchall -> Declaration
FunClause ArgInfo
ai (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
LHS Pattern
p1 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Catchall
ca
                  -- If we have with-expressions (es /= []) then the following
                  -- ellipses also get the additional patterns in p0.
                  (Declaration
d' Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if [WithExpr] -> Bool
forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p1) [Declaration]
ds
                ZeroHoles Pattern
_ -> do
                  -- We can have ellipses after a fun clause without.
                  -- They refer to the last clause that introduced new with-expressions.
                  -- Same here: If we have new with-expressions, the next ellipses will
                  -- refer to us.
                  -- Andreas, Jesper, 2017-05-13, issue #2578
                  -- Need to update the range also on the next with-patterns.
                  (Declaration
d Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration])
-> Nice [Declaration] -> Nice [Declaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if [WithExpr] -> Bool
forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else KillRangeT Pattern
forall a. KillRange a => KillRangeT a
killRange Pattern
p0) [Declaration]
ds
            Declaration
_ -> Nice [Declaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
    expandEllipsis1 List1 Declaration
_ = Nice (List1 Declaration)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Turn function clauses into nice function clauses.
    mkClauses1 ::
         ArgInfo
           -- Clauses need to conform to this 'Modality'.
      -> Name -> List1 Declaration -> Catchall -> Nice (List1 Clause)
    mkClauses1 :: ArgInfo
-> Name -> List1 Declaration -> Catchall -> Nice (NonEmpty Clause)
mkClauses1 ArgInfo
info Name
x List1 Declaration
ds Catchall
ca = NonEmpty Clause -> [Clause] -> NonEmpty Clause
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe NonEmpty Clause
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Clause] -> NonEmpty Clause)
-> Nice [Clause] -> Nice (NonEmpty Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgInfo -> Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses ArgInfo
info Name
x (List1 Declaration -> [Item (List1 Declaration)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Declaration
ds) Catchall
ca

    mkClauses ::
         ArgInfo
           -- Clauses need to conform to this 'Modality'.
      -> Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses :: ArgInfo -> Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses ArgInfo
_ Name
_ [] Catchall
_ = [Clause] -> Nice [Clause]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    -- A CATCHALL pragma after the last clause is useless.
    mkClauses ArgInfo
_ Name
_ [Pragma (CatchallPragma Range
r)] Catchall
_ = [] [Clause] -> Nice () -> Nice [Clause]
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
      HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r

    mkClauses ArgInfo
info Name
x (Pragma (CatchallPragma Range
r) : [Declaration]
cs) Catchall
catchall = do
      -- Warn about consecutive CATCHALL pragmas
      Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Catchall -> Bool
forall a. Null a => a -> Bool
null Catchall
catchall) (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
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
      ArgInfo -> Name -> [Declaration] -> Catchall -> Nice [Clause]
mkClauses ArgInfo
info Name
x [Declaration]
cs (Range -> Catchall
YesCatchall Range
r)

    mkClauses ArgInfo
info Name
x (FunClause ArgInfo
ai LHS
lhs RHS
rhs WhereClause
wh Catchall
ca : [Declaration]
cs) Catchall
catchall
      | [WithExpr] -> Bool
forall a. Null a => a -> Bool
null (LHS -> [WithExpr]
lhsWithExpr LHS
lhs) Bool -> Bool -> Bool
|| LHS -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis LHS
lhs = do
      ai <- ArgInfo -> ArgInfo -> Nice ArgInfo
checkModality ArgInfo
info ArgInfo
ai
      (Clause x (ca <> catchall) ai lhs rhs wh [] :) <$> mkClauses info x cs empty

    mkClauses ArgInfo
info Name
x (FunClause ArgInfo
ai LHS
lhs RHS
rhs WhereClause
wh Catchall
ca : [Declaration]
cs) Catchall
catchall = do
      ai <- ArgInfo -> ArgInfo -> Nice ArgInfo
checkModality ArgInfo
info ArgInfo
ai
      when (null withClauses) $ declarationException $ MissingWithClauses x lhs
      wcs <- mkClauses info x withClauses empty
      (Clause x (ca <> catchall) ai lhs rhs wh wcs :) <$> mkClauses info x cs' empty
      where
        ([Declaration]
withClauses, [Declaration]
cs') = [Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs

        -- A clause is a subclause if the number of with-patterns is
        -- greater or equal to the current number of with-patterns plus the
        -- number of with arguments.
        numWith :: Int
numWith = Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [WithExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((WithExpr -> Bool) -> [WithExpr] -> [WithExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter WithExpr -> Bool
forall a. LensHiding a => a -> Bool
visible [WithExpr]
es)
          where LHS Pattern
p [RewriteEqn]
_ [WithExpr]
es = LHS
lhs

        subClauses :: [Declaration] -> ([Declaration],[Declaration])
        subClauses :: [Declaration] -> ([Declaration], [Declaration])
subClauses (c :: Declaration
c@(FunClause ArgInfo
_ (LHS Pattern
p0 [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Catchall
_) : [Declaration]
cs)
         | Pattern -> Bool
forall a. IsEllipsis a => a -> Bool
isEllipsis Pattern
p0 Bool -> Bool -> Bool
||
           Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
numWith = ([Declaration] -> [Declaration])
-> ([Declaration], [Declaration]) -> ([Declaration], [Declaration])
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs)
         | Bool
otherwise                           = ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs)
        subClauses (c :: Declaration
c@(Pragma (CatchallPragma Range
_r)) : [Declaration]
cs) = case [Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs of
          ([], [Declaration]
cs') -> ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs')
          ([Declaration]
cs, [Declaration]
cs') -> (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs, [Declaration]
cs')
        subClauses [] = ([],[])
        subClauses [Declaration]
_  = ([Declaration], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__
    mkClauses ArgInfo
_ Name
_ [Declaration]
_ Catchall
_ = Nice [Clause]
forall a. HasCallStack => a
__IMPOSSIBLE__

    checkModality ::
         ArgInfo       -- Authoritative 'Modality' from type signature.
      -> ArgInfo       -- 'Modality' from clause, has to conform.
      -> Nice ArgInfo  -- Deviant 'Modality' conformed to authoritative source.
    checkModality :: ArgInfo -> ArgInfo -> Nice ArgInfo
checkModality ArgInfo
info ArgInfo
ai
      | (ArgInfo -> Bool
forall a. Null a => a -> Bool
null ArgInfo
ai Bool -> Bool -> Bool
|| ArgInfo -> ArgInfo -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality ArgInfo
info ArgInfo
ai) = ArgInfo -> Nice ArgInfo
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
ai
      | Bool
otherwise = ArgInfo
info ArgInfo -> Nice () -> Nice ArgInfo
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (ArgInfo -> ArgInfo -> DeclarationWarning'
DivergentModalityInClause ArgInfo
info ArgInfo
ai)

    couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Name
x Pattern
p =
      let
      pns :: [QName]
pns        = Pattern -> [QName]
forall p. CPatternLike p => p -> [QName]
patternQNames Pattern
p
      xStrings :: [String]
xStrings   = Name -> [String]
nameStringParts Name
x
      patStrings :: [String]
patStrings = (Name -> [String]) -> [Name] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [String]
nameStringParts ([Name] -> [String]) -> [Name] -> [String]
forall a b. (a -> b) -> a -> b
$ (QName -> Maybe Name) -> [QName] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe QName -> Maybe Name
isUnqualified [QName]
pns
      in
--          trace ("x = " ++ prettyShow x) $
--          trace ("pns = " ++ show pns) $
--          trace ("xStrings = " ++ show xStrings) $
--          trace ("patStrings = " ++ show patStrings) $
--          trace ("mFixity = " ++ show mFixity) $
      case ([QName] -> Maybe QName
forall a. [a] -> Maybe a
listToMaybe [QName]
pns, Maybe Fixity'
mFixity) of
        -- first identifier in the patterns is the fun.symbol?
        (Just QName
y, Maybe Fixity'
_) | Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== QName -> Maybe Name
isUnqualified QName
y -> Bool
True -- trace ("couldBe since y = " ++ prettyShow y) $ True
        -- are the parts of x contained in p
        (Maybe QName, Maybe Fixity')
_ | [String]
xStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSubsequenceOf` [String]
patStrings -> Bool
True
        -- looking for a mixfix fun.symb
        (Maybe QName
_, Just Fixity'
fix) ->  -- also matches in case of a postfix
           let notStrings :: [String]
notStrings = Notation -> [String]
stringParts (Fixity' -> Notation
theNotation Fixity'
fix)
           in  -- trace ("notStrings = " ++ show notStrings) $
               -- trace ("patStrings = " ++ show patStrings) $
               Bool -> Bool
not ([String] -> Bool
forall a. Null a => a -> Bool
null [String]
notStrings) Bool -> Bool -> Bool
&& ([String]
notStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSubsequenceOf` [String]
patStrings)
        -- not a notation, not first id: give up
        (Maybe QName, Maybe Fixity')
_ -> Bool
False -- trace ("couldBe not (case default)") $ False


    -- for finding nice clauses for a type sig in mutual blocks
    couldBeNiceFunClauseOf :: Maybe Fixity' -> Name -> NiceDeclaration
                           -> Maybe (MutualChecks, Declaration)
    couldBeNiceFunClauseOf :: Maybe Fixity'
-> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf Maybe Fixity'
mf Name
n (NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Catchall
_ Declaration
d)
      = ([TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] [], Declaration
d) (MutualChecks, Declaration)
-> Maybe () -> Maybe (MutualChecks, Declaration)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mf Name
n Declaration
d)
    couldBeNiceFunClauseOf Maybe Fixity'
_ Name
_ NiceDeclaration
_ = Maybe (MutualChecks, Declaration)
forall a. Maybe a
Nothing

    -- for finding clauses for a type sig in mutual blocks
    couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
    couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
_ Name
_ (Pragma (CatchallPragma{})) = Bool
True
    couldBeFunClauseOf Maybe Fixity'
mFixity Name
x (FunClause ArgInfo
_ (LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Catchall
_) =
       Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p Bool -> Bool -> Bool
|| Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Name
x Pattern
p
    couldBeFunClauseOf Maybe Fixity'
_ Name
_ Declaration
_ = Bool
False -- trace ("couldBe not (fun default)") $ False

    -- Turn a new style `interleaved mutual' block into a new style mutual block
    -- by grouping the declarations in blocks.
    mkInterleavedMutual
      :: KwRange               -- Range of the @interleaved mutual@ keywords.
      -> [NiceDeclaration]     -- Declarations inside the block.
      -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
    mkInterleavedMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual KwRange
kwr [NiceDeclaration]
ds' = do
      (other, ISt m checks _) <- StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> InterleavedState
-> Nice ([(Int, NiceDeclaration)], InterleavedState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
groupByBlocks KwRange
kwr [NiceDeclaration]
ds') (InterleavedState
 -> Nice ([(Int, NiceDeclaration)], InterleavedState))
-> InterleavedState
-> Nice ([(Int, NiceDeclaration)], InterleavedState)
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> MutualChecks -> Int -> InterleavedState
ISt InterleavedMutual
forall a. Null a => a
empty MutualChecks
forall a. Monoid a => a
mempty Int
0
      let idecls = [(Int, NiceDeclaration)]
other [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++ ((Name, InterleavedDecl) -> [(Int, NiceDeclaration)])
-> [(Name, InterleavedDecl)] -> [(Int, NiceDeclaration)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Name -> InterleavedDecl -> [(Int, NiceDeclaration)])
-> (Name, InterleavedDecl) -> [(Int, NiceDeclaration)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl) (InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m)
      let decls0 = ((Int, NiceDeclaration) -> NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map (Int, NiceDeclaration) -> NiceDeclaration
forall a b. (a, b) -> b
snd ([(Int, NiceDeclaration)] -> [NiceDeclaration])
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ ((Int, NiceDeclaration) -> (Int, NiceDeclaration) -> Ordering)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, NiceDeclaration) -> Int)
-> (Int, NiceDeclaration)
-> (Int, NiceDeclaration)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, NiceDeclaration) -> Int
forall a b. (a, b) -> a
fst) [(Int, NiceDeclaration)]
idecls
      ps <- use loneSigs
      checkLoneSigs ps
      let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
decls0
      -- process the checks
      let r = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
ds'
      tc <- combineTerminationChecks r (mutualTermination checks)
      let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks   (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
      let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
      pure $ NiceMutual kwr tc cc pc decls

      where

        ------------------------------------------------------------------------------
        -- Adding Signatures
        addType :: Name -> (DeclNum -> InterleavedDecl) -> MutualChecks -> INice ()
        addType :: Name -> (Int -> InterleavedDecl) -> MutualChecks -> INice ()
addType Name
n Int -> InterleavedDecl
c MutualChecks
mc = do
          ISt m checks i <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get
          when (isJust $ Map.lookup n m) $ lift $ declarationException $ DuplicateDefinition n
          put $ ISt (Map.insert n (c i) m) (mc <> checks) (i + 1)

        addFunType :: NiceDeclaration -> INice ()
addFunType d :: NiceDeclaration
d@(FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
cc Name
n Expr
_) = do
           let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
           Name -> (Int -> InterleavedDecl) -> MutualChecks -> INice ()
addType Name
n (\ Int
i -> Int
-> NiceDeclaration
-> Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
-> InterleavedDecl
InterleavedFun Int
i NiceDeclaration
d Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
forall a. Maybe a
Nothing) MutualChecks
checks
        addFunType NiceDeclaration
_ = INice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        addDataType :: NiceDeclaration -> INice ()
addDataType d :: NiceDeclaration
d@(NiceDataSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_uc Name
n [LamBinding]
_ Expr
_) = do
          let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [] [] [PositivityCheck
pc]
          Name -> (Int -> InterleavedDecl) -> MutualChecks -> INice ()
addType Name
n (\ Int
i -> Int
-> NiceDeclaration
-> Maybe (Int, List1 [NiceDeclaration])
-> InterleavedDecl
InterleavedData Int
i NiceDeclaration
d Maybe (Int, List1 [NiceDeclaration])
forall a. Maybe a
Nothing) MutualChecks
checks
        addDataType NiceDeclaration
_ = INice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        ------------------------------------------------------------------------------
        -- Adding constructors & clauses

        addDataConstructors ::
             Maybe Name         -- Data type the constructors belong to
          -> [NiceConstructor]  -- Constructors to add
          -> INice ()
        -- if we know the type's name, we can go ahead
        addDataConstructors :: Maybe Name -> [NiceDeclaration] -> INice ()
addDataConstructors (Just Name
n) [NiceDeclaration]
ds = do
          ISt m checks i <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get
          case Map.lookup n m of
            Just (InterleavedData Int
i0 NiceDeclaration
sig Maybe (Int, List1 [NiceDeclaration])
cs) -> do
              Nice () -> INice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT InterleavedState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> INice ()) -> Nice () -> INice ()
forall a b. (a -> b) -> a -> b
$ Name -> Nice ()
removeLoneSig Name
n
              -- add the constructors to the existing ones (if any)
              let ((Int, List1 [NiceDeclaration])
cs', Int
i') = case Maybe (Int, List1 [NiceDeclaration])
cs of
                    Maybe (Int, List1 [NiceDeclaration])
Nothing        -> ((Int
i , [NiceDeclaration]
ds [NiceDeclaration] -> [[NiceDeclaration]] -> List1 [NiceDeclaration]
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    Just (Int
i1, List1 [NiceDeclaration]
ds1) -> ((Int
i1, [NiceDeclaration]
ds [NiceDeclaration]
-> List1 [NiceDeclaration] -> List1 [NiceDeclaration]
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 [NiceDeclaration]
ds1), Int
i)
              InterleavedState -> INice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedState -> INice ()) -> InterleavedState -> INice ()
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> MutualChecks -> Int -> InterleavedState
ISt (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 [NiceDeclaration])
-> InterleavedDecl
InterleavedData Int
i0 NiceDeclaration
sig ((Int, List1 [NiceDeclaration])
-> Maybe (Int, List1 [NiceDeclaration])
forall a. a -> Maybe a
Just (Int, List1 [NiceDeclaration])
cs')) InterleavedMutual
m) MutualChecks
checks Int
i'
            Maybe InterleavedDecl
_ -> Nice () -> INice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT InterleavedState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> INice ()) -> Nice () -> INice ()
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 -> DeclarationWarning'
MissingDataDeclaration Name
n

        addDataConstructors Maybe Name
Nothing [] = () -> INice ()
forall a. a -> StateT InterleavedState Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        -- Otherwise we try to guess which datasig the constructor is referring to
        addDataConstructors Maybe Name
Nothing (NiceDeclaration
d : [NiceDeclaration]
ds) = do
          -- get the candidate data types that are in this interleaved mutual block
          ISt m _ _ <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get
          let sigs = ((Name, InterleavedDecl) -> Maybe Name)
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n Name -> Maybe () -> Maybe Name
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedData InterleavedDecl
d) ([(Name, InterleavedDecl)] -> [Name])
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
          -- check whether this constructor matches any of them
          case isConstructor sigs d of
            Right Name
n -> do
              -- if so grab the whole block that may work and add them
              let ([NiceDeclaration]
ds0, [NiceDeclaration]
ds1) = (NiceDeclaration -> Bool)
-> [NiceDeclaration] -> ([NiceDeclaration], [NiceDeclaration])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Either (Name, [Name]) Name -> Bool
forall a b. Either a b -> Bool
isRight (Either (Name, [Name]) Name -> Bool)
-> (NiceDeclaration -> Either (Name, [Name]) Name)
-> NiceDeclaration
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor [Name
n]) [NiceDeclaration]
ds
              Maybe Name -> [NiceDeclaration] -> INice ()
addDataConstructors (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n) (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds0)
              -- and then repeat the process for the rest of the block
              Maybe Name -> [NiceDeclaration] -> INice ()
addDataConstructors Maybe Name
forall a. Maybe a
Nothing [NiceDeclaration]
ds1
            Left (Name
n, [Name]
ns) -> Nice () -> INice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT InterleavedState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> INice ()) -> Nice () -> INice ()
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 -> Name -> [Name] -> DeclarationException'
AmbiguousConstructor (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) Name
n [Name]
ns

        addFunDef :: NiceDeclaration -> INice ()
        addFunDef :: NiceDeclaration -> INice ()
addFunDef (FunDef Range
_ List1 Declaration
ds IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
cc Name
n NonEmpty Clause
cs) = do
          Name
-> List1 Declaration -> NonEmpty Clause -> MutualChecks -> INice ()
addInterleavedFun Name
n List1 Declaration
ds NonEmpty Clause
cs (MutualChecks -> INice ()) -> MutualChecks -> INice ()
forall a b. (a -> b) -> a -> b
$ [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
        addFunDef NiceDeclaration
_ = INice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        addInterleavedFun :: Name -> List1 Declaration -> List1 Clause -> MutualChecks -> INice ()
        addInterleavedFun :: Name
-> List1 Declaration -> NonEmpty Clause -> MutualChecks -> INice ()
addInterleavedFun Name
n List1 Declaration
ds NonEmpty Clause
cs MutualChecks
checks' = do
          ISt m checks i <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get
          case Map.lookup n m of
            Just (InterleavedFun Int
i0 NiceDeclaration
sig Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
cs0) -> do
              let ((Int, List1 (List1 Declaration, NonEmpty Clause))
cs', Int
i') = case Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
cs0 of
                    Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
Nothing        -> ((Int
i,  (List1 Declaration
ds, NonEmpty Clause
cs) (List1 Declaration, NonEmpty Clause)
-> [(List1 Declaration, NonEmpty Clause)]
-> List1 (List1 Declaration, NonEmpty Clause)
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    Just (Int
i1, List1 (List1 Declaration, NonEmpty Clause)
cs1) -> ((Int
i1, (List1 Declaration
ds, NonEmpty Clause
cs) (List1 Declaration, NonEmpty Clause)
-> List1 (List1 Declaration, NonEmpty Clause)
-> List1 (List1 Declaration, NonEmpty Clause)
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 (List1 Declaration, NonEmpty Clause)
cs1), Int
i)
              InterleavedState -> INice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedState -> INice ()) -> InterleavedState -> INice ()
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> MutualChecks -> Int -> InterleavedState
ISt (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 (List1 Declaration, NonEmpty Clause))
-> Maybe (Int, List1 (List1 Declaration, NonEmpty Clause))
forall a. a -> Maybe a
Just (Int, List1 (List1 Declaration, NonEmpty Clause))
cs')) InterleavedMutual
m) (MutualChecks
checks' MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) Int
i'
            Maybe InterleavedDecl
_ -> INice ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- A FunDef always come after an existing FunSig!

        addFunClauses ::
             KwRange
               -- Range of the @interleaved mutual@ keyword.
          -> [NiceDeclaration]
          -> INice [(DeclNum, NiceDeclaration)]
        addFunClauses :: KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
addFunClauses KwRange
r (nd :: NiceDeclaration
nd@(NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Catchall
_ (FunClause ArgInfo
ai LHS
lhs RHS
_ WhereClause
_ Catchall
_)) : [NiceDeclaration]
ds) = do
          -- get the candidate functions that are in this interleaved mutual block
          ISt m checks i <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get
          let sigs = ((Name, InterleavedDecl) -> Maybe Name)
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n Name -> Maybe () -> Maybe Name
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedDecl
d) ([(Name, InterleavedDecl)] -> [Name])
-> [(Name, InterleavedDecl)] -> [Name]
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> [(Name, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
          -- find the funsig candidates for the funclause of interest
          case [ (x, fits, rest)
               | x <- sigs
               , let (fits0, rest) = spanJust (couldBeNiceFunClauseOf (Map.lookup x fixs) x) (nd : ds)
               , fits <- maybeToList $ List1.nonEmpty fits0
               ] of
            -- no candidate: keep the isolated fun clause, we'll complain about it later
            [] -> do
              let check :: MutualChecks
check = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
              InterleavedState -> INice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedState -> INice ()) -> InterleavedState -> INice ()
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> MutualChecks -> Int -> InterleavedState
ISt InterleavedMutual
m (MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
              ((Int
i,NiceDeclaration
nd) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
groupByBlocks KwRange
r [NiceDeclaration]
ds
            -- exactly one candidate: attach the funclause to the definition
            [(Name
n, NonEmpty (MutualChecks, Declaration)
fits0, [NiceDeclaration]
rest)] -> do
              let (NonEmpty MutualChecks
checkss, List1 Declaration
fits) = NonEmpty (MutualChecks, Declaration)
-> (NonEmpty MutualChecks, List1 Declaration)
forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
List1.unzip NonEmpty (MutualChecks, Declaration)
fits0
              ds <- Nice (List1 Declaration)
-> StateT InterleavedState Nice (List1 Declaration)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT InterleavedState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice (List1 Declaration)
 -> StateT InterleavedState Nice (List1 Declaration))
-> Nice (List1 Declaration)
-> StateT InterleavedState Nice (List1 Declaration)
forall a b. (a -> b) -> a -> b
$ List1 Declaration -> Nice (List1 Declaration)
expandEllipsis1 List1 Declaration
fits
              cs <- lift $ mkClauses1 ai n ds empty
              addInterleavedFun n fits {- or? ds -} cs $ Fold.fold checkss
              groupByBlocks r rest
            -- more than one candidate: fail, complaining about the ambiguity!
            (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
xf:[(Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])]
xfs -> Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT InterleavedState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
                           (DeclarationException' -> Nice [(Int, NiceDeclaration)])
-> DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs
                           (List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Name -> List1 Name
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ ((Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
 -> Name)
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Name
a,NonEmpty (MutualChecks, Declaration)
_,[NiceDeclaration]
_) -> Name
a) (NonEmpty
   (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
 -> List1 Name)
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
xf (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
-> [(Name, NonEmpty (MutualChecks, Declaration),
     [NiceDeclaration])]
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])
forall a. a -> [a] -> NonEmpty a
:| [(Name, NonEmpty (MutualChecks, Declaration), [NiceDeclaration])]
xfs
        addFunClauses KwRange
_ [NiceDeclaration]
_ = StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a. HasCallStack => a
__IMPOSSIBLE__

        groupByBlocks ::
              KwRange
                -- Range of the @interleaved mutual@ keyword.
          -> [NiceDeclaration]
          -> INice [(DeclNum, NiceDeclaration)]
        groupByBlocks :: KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
groupByBlocks KwRange
_kwr []      = [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a. a -> StateT InterleavedState Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        groupByBlocks KwRange
kwr (NiceDeclaration
d : [NiceDeclaration]
ds) = do
          -- for most branches we deal with the one declaration and move on
          let oneOff :: StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff StateT InterleavedState Nice [(Int, NiceDeclaration)]
act = StateT InterleavedState Nice [(Int, NiceDeclaration)]
act StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> ([(Int, NiceDeclaration)]
    -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
StateT InterleavedState Nice a
-> (a -> StateT InterleavedState Nice b)
-> StateT InterleavedState Nice b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [(Int, NiceDeclaration)]
ns -> ([(Int, NiceDeclaration)]
ns [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
groupByBlocks KwRange
kwr [NiceDeclaration]
ds
          case NiceDeclaration
d of
            NiceDataSig{}                -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration -> INice ()
addDataType NiceDeclaration
d
            NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n [LamBinding]
_ [NiceDeclaration]
ds -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Name -> [NiceDeclaration] -> INice ()
addDataConstructors (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n) [NiceDeclaration]
ds
            NiceLoneConstructor KwRange
_ [NiceDeclaration]
ds     -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Name -> [NiceDeclaration] -> INice ()
addDataConstructors Maybe Name
forall a. Maybe a
Nothing [NiceDeclaration]
ds
            FunSig{}                     -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration -> INice ()
addFunType NiceDeclaration
d
            FunDef Range
_ List1 Declaration
_ IsAbstract
_  IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
n NonEmpty Clause
_cs
                      | Bool -> Bool
not (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n) -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceDeclaration -> INice ()
addFunDef NiceDeclaration
d
            -- It's a bit different for fun clauses because we may need to grab a lot
            -- of clauses to handle ellipses properly.
            NiceFunClause{}              -> KwRange
-> [NiceDeclaration]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
addFunClauses KwRange
kwr (NiceDeclaration
dNiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:[NiceDeclaration]
ds)
            -- We do not need to worry about RecSig vs. RecDef: we know there's exactly one
            -- of each for record definitions and leaving them in place should be enough!
            NiceDeclaration
_ -> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
oneOff (StateT InterleavedState Nice [(Int, NiceDeclaration)]
 -> StateT InterleavedState Nice [(Int, NiceDeclaration)])
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
-> StateT InterleavedState Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ do
              ISt m c i <- StateT InterleavedState Nice InterleavedState
forall s (m :: * -> *). MonadState s m => m s
get -- TODO: grab checks from c?
              put $ ISt m c (i + 1)
              pure [(i,d)]

    -- Extract the name of the return type (if any) of a potential constructor.
    -- In case of failure return the name of the constructor and the list of candidates
    -- for the return type.
    -- A `constructor' block should only contain NiceConstructors so we crash with
    -- an IMPOSSIBLE otherwise
    isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
    isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor [Name]
ns (Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
e)
       -- extract the return type & see it as an LHS-style pattern
       | Just Pattern
p <- Expr -> Pattern
exprToPatternWithHoles (Expr -> Pattern) -> Maybe Expr -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Expr
returnExpr Expr
e =
         case [ Name
x | Name
x <- [Name]
ns
                  , Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf (Name -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Fixities
fixs) Name
x Pattern
p
                  ] of
           [Name
x] -> Name -> Either (Name, [Name]) Name
forall a b. b -> Either a b
Right Name
x
           [Name]
xs  -> (Name, [Name]) -> Either (Name, [Name]) Name
forall a b. a -> Either a b
Left (Name
n, [Name]
xs)
       -- which may fail (e.g. if the "return type" is a hole
       | Bool
otherwise = (Name, [Name]) -> Either (Name, [Name]) Name
forall a b. a -> Either a b
Left (Name
n, [])
    isConstructor [Name]
_ NiceDeclaration
_ = Either (Name, [Name]) Name
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Turn an old-style mutual block into a new style mutual block
    -- by pushing the definitions to the end.
    mkOldMutual
      :: KwRange               -- Range of the @mutual@ keyword (if any).
      -> [NiceDeclaration]     -- Declarations inside the block.
      -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
    mkOldMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual KwRange
kwr [NiceDeclaration]
ds' = do
        -- Postulate the missing definitions
        let ps :: LoneSigs
ps = [(Range, Name, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames [(Range, Name, DataRecOrFun)]
loneNames
        LoneSigs -> Nice ()
checkLoneSigs LoneSigs
ps
        let ds :: [NiceDeclaration]
ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
ds'

        -- -- Remove the declarations that aren't allowed in old style mutual blocks
        -- ds <- fmap catMaybes $ forM ds $ \ d -> let success = pure (Just d) in case d of
        --   -- Andreas, 2013-11-23 allow postulates in mutual blocks
        --   Axiom{}          -> success
        --   -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
        --   -- in ConcreteToAbstract rather than here.
        --   NiceFunClause{}  -> success
        --   -- Andreas, 2018-05-11, issue #3052, allow pat.syn.s in mutual blocks
        --   NicePatternSyn{} -> success
        --   -- Otherwise, only categorized signatures and definitions are allowed:
        --   -- Data, Record, Fun
        --   _ -> if (declKind d /= OtherDecl) then success
        --        else Nothing <$ declarationWarning (NotAllowedInMutual (getRange d) $ declName d)
        -- Sort the declarations in the mutual block.
        -- Declarations of names go to the top.  (Includes module definitions.)
        -- Definitions of names go to the bottom.
        -- Some declarations are forbidden, as their positioning could confuse
        -- the user.
        (top, bottom, _invalid) <- [NiceDeclaration]
-> (NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall (m :: * -> *) a b c d.
Applicative m =>
[a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
forEither3M [NiceDeclaration]
ds ((NiceDeclaration
  -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
 -> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration]))
-> (NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall a b. (a -> b) -> a -> b
$ \ NiceDeclaration
d -> do
          let top :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top       = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. a -> Either3 a b c
In1 NiceDeclaration
d)
              bottom :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom    = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. b -> Either3 a b c
In2 NiceDeclaration
d)
              invalid :: String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
s = NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice ()
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> String -> DeclarationWarning'
NotAllowedInMutual (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) String
s
          case NiceDeclaration
d of
            -- Andreas, 2013-11-23 allow postulates in mutual blocks
            Axiom{}             -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceField{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            PrimitiveFunction{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            -- Andreas, 2019-07-23 issue #3932:
            -- Nested mutual blocks are not supported.
            NiceMutual{}        -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"mutual blocks"
            -- Andreas, 2018-10-29, issue #3246
            -- We could allow modules (top), but this is potentially confusing.
            NiceModule{}        -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Module definitions"
            -- Lone constructors are only allowed in new-style mutual blocks
            NiceLoneConstructor{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Lone constructors"
            NiceModuleMacro{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceOpen{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceImport{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceRecSig{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceDataSig{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
            -- in ConcreteToAbstract rather than here.
            NiceFunClause{}     -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            FunSig{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            FunDef{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceDataDef{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceRecDef{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            -- Andreas, 2018-05-11, issue #3051, allow pat.syn.s in mutual blocks
            -- Andreas, 2018-10-29: We shift pattern synonyms to the bottom
            -- since they might refer to constructors defined in a data types
            -- just above them.
            NicePatternSyn{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceGeneralize{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceUnquoteDecl{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceUnquoteDef{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceUnquoteData{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top

            -- Opaque blocks can not participate in old-style mutual
            -- recursion. If some of the definitions are opaque then
            -- they all need to be.
            NiceOpaque KwRange
r [QName]
_ [NiceDeclaration]
_    ->
              NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (ZonkAny 0)
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do DeclarationException' -> Nice (ZonkAny 0)
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice (ZonkAny 0))
-> DeclarationException' -> Nice (ZonkAny 0)
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationException'
OpaqueInMutual KwRange
r
            NicePragma Range
_r Pragma
pragma -> case Pragma
pragma of

              OptionsPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top     -- error thrown in the type checker

              -- Some builtins require a definition, and they affect type checking
              -- Thus, we do not handle BUILTINs in mutual blocks (at least for now).
              BuiltinPragma{}           -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"BUILTIN pragmas"

              -- The REWRITE pragma behaves differently before or after the def.
              -- and affects type checking.  Thus, we refuse it here.
              RewritePragma{}           -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"REWRITE pragmas"

              -- Compiler pragmas are not needed for type checking, thus,
              -- can go to the bottom.
              ForeignPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
              CompilePragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom

              StaticPragma{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
              InlinePragma{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
              NotProjectionLikePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom

              OverlapPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top

              ImpossiblePragma{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top     -- error thrown in scope checker
              EtaPragma{}               -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom  -- needs record definition
              WarningOnUsage{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
              WarningOnImport{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
              InjectivePragma{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top     -- only needs name, not definition
              InjectiveForInferencePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
              DisplayPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top     -- only for printing

              -- The attached pragmas have already been handled at this point.
              CatchallPragma{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              TerminationCheckPragma{}  -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoPositivityCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              PolarityPragma{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoUniverseCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoCoverageCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__


        -- -- Pull type signatures to the top
        -- let (sigs, other) = List.partition isTypeSig ds

        -- -- Push definitions to the bottom
        -- let (other, defs) = flip List.partition ds $ \case
        --       FunDef{}         -> False
        --       NiceDataDef{}    -> False
        --       NiceRecDef{}         -> False
        --       NiceFunClause{}  -> False
        --       NicePatternSyn{} -> False
        --       NiceUnquoteDef{} -> False
        --       _ -> True

        -- Compute termination checking flag for mutual block
        tc0 <- use terminationCheckPragma
        let tcs = (NiceDeclaration -> TerminationCheck)
-> [NiceDeclaration] -> [TerminationCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> TerminationCheck
termCheck [NiceDeclaration]
ds
        let r   = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
ds'
        tc <- combineTerminationChecks r (tc0:tcs)

        -- Compute coverage checking flag for mutual block
        cc0 <- use coverageCheckPragma
        let ccs = (NiceDeclaration -> CoverageCheck)
-> [NiceDeclaration] -> [CoverageCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> CoverageCheck
covCheck [NiceDeclaration]
ds
        let cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks (CoverageCheck
cc0CoverageCheck -> [CoverageCheck] -> [CoverageCheck]
forall a. a -> [a] -> [a]
:[CoverageCheck]
ccs)

        -- Compute positivity checking flag for mutual block
        pc0 <- use positivityCheckPragma
        let pcs = (NiceDeclaration -> PositivityCheck)
-> [NiceDeclaration] -> [PositivityCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> PositivityCheck
positivityCheckOldMutual [NiceDeclaration]
ds
        let pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (PositivityCheck
pc0PositivityCheck -> [PositivityCheck] -> [PositivityCheck]
forall a. a -> [a] -> [a]
:[PositivityCheck]
pcs)

        return $ NiceMutual kwr tc cc pc $ top ++ bottom

      where
        sigNames :: [(Range, Name, DataRecOrFun)]
sigNames  = [ (Range
r, Name
x, DataRecOrFun
k) | LoneSigDecl Range
r DataRecOrFun
k Name
x <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds' ]
        defNames :: [(Name, DataRecOrFun)]
defNames  = [ (Name
x, DataRecOrFun
k) | LoneDefs DataRecOrFun
k [Name]
xs <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds', Name
x <- [Name]
xs ]
        -- compute the set difference with equality just on names
        loneNames :: [(Range, Name, DataRecOrFun)]
loneNames = [ (Range
r, Name
x, DataRecOrFun
k) | (Range
r, Name
x, DataRecOrFun
k) <- [(Range, Name, DataRecOrFun)]
sigNames, ((Name, DataRecOrFun) -> Bool) -> [(Name, DataRecOrFun)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all ((Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Name -> Bool)
-> ((Name, DataRecOrFun) -> Name) -> (Name, DataRecOrFun) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, DataRecOrFun) -> Name
forall a b. (a, b) -> a
fst) [(Name, DataRecOrFun)]
defNames ]

        termCheck :: NiceDeclaration -> TerminationCheck
        -- Andreas, 2013-02-28 (issue 804):
        -- do not termination check a mutual block if any of its
        -- inner declarations comes with a {-# NO_TERMINATION_CHECK #-}
        termCheck :: NiceDeclaration -> TerminationCheck
termCheck (FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
_ Name
_ Expr
_)      = TerminationCheck
tc
        termCheck (FunDef Range
_ List1 Declaration
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
_ Name
_ NonEmpty Clause
_)          = TerminationCheck
tc
        -- ASR (28 December 2015): Is this equation necessary?
        termCheck (NiceMutual KwRange
_ TerminationCheck
tc CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
_)            = TerminationCheck
tc
        termCheck (NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
_ [Name]
_ Expr
_) = TerminationCheck
tc
        termCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
_ [Name]
_ Expr
_)    = TerminationCheck
tc
        termCheck Axiom{}               = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceField{}           = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck PrimitiveFunction{}   = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModule{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModuleMacro{}     = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceOpen{}            = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceImport{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NicePragma{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecSig{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataSig{}         = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceFunClause{}       = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataDef{}         = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecDef{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NicePatternSyn{}      = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceGeneralize{}      = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceLoneConstructor{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceUnquoteData{}     = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceOpaque{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck

        covCheck :: NiceDeclaration -> CoverageCheck
        covCheck :: NiceDeclaration -> CoverageCheck
covCheck (FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
cc Name
_ Expr
_)      = CoverageCheck
cc
        covCheck (FunDef Range
_ List1 Declaration
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
cc Name
_ NonEmpty Clause
_)          = CoverageCheck
cc
        -- ASR (28 December 2015): Is this equation necessary?
        covCheck (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
cc PositivityCheck
_ [NiceDeclaration]
_)            = CoverageCheck
cc
        covCheck (NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
cc [Name]
_ Expr
_) = CoverageCheck
cc
        covCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
cc [Name]
_ Expr
_)    = CoverageCheck
cc
        covCheck Axiom{}               = CoverageCheck
YesCoverageCheck
        covCheck NiceField{}           = CoverageCheck
YesCoverageCheck
        covCheck PrimitiveFunction{}   = CoverageCheck
YesCoverageCheck
        covCheck NiceModule{}          = CoverageCheck
YesCoverageCheck
        covCheck NiceModuleMacro{}     = CoverageCheck
YesCoverageCheck
        covCheck NiceOpen{}            = CoverageCheck
YesCoverageCheck
        covCheck NiceImport{}          = CoverageCheck
YesCoverageCheck
        covCheck NicePragma{}          = CoverageCheck
YesCoverageCheck
        covCheck NiceRecSig{}          = CoverageCheck
YesCoverageCheck
        covCheck NiceDataSig{}         = CoverageCheck
YesCoverageCheck
        covCheck NiceFunClause{}       = CoverageCheck
YesCoverageCheck
        covCheck NiceDataDef{}         = CoverageCheck
YesCoverageCheck
        covCheck NiceRecDef{}          = CoverageCheck
YesCoverageCheck
        covCheck NicePatternSyn{}      = CoverageCheck
YesCoverageCheck
        covCheck NiceGeneralize{}      = CoverageCheck
YesCoverageCheck
        covCheck NiceLoneConstructor{} = CoverageCheck
YesCoverageCheck
        covCheck NiceUnquoteData{}     = CoverageCheck
YesCoverageCheck
        covCheck NiceOpaque{}          = CoverageCheck
YesCoverageCheck

        -- ASR (26 December 2015): Do not positivity check a mutual
        -- block if any of its inner declarations comes with a
        -- NO_POSITIVITY_CHECK pragma. See Issue 1614.
        positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
        positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
positivityCheckOldMutual (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceDataSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
pc [NiceDeclaration]
_)        = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_) = PositivityCheck
pc
        positivityCheckOldMutual NiceDeclaration
_                              = PositivityCheck
YesPositivityCheck

        -- A mutual block cannot have a measure,
        -- but it can skip termination check.

    abstractBlock
      :: KwRange  -- Range of @abstract@ keyword.
      -> [NiceDeclaration]
      -> Nice [NiceDeclaration]
    abstractBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
abstractBlock KwRange
r [NiceDeclaration]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
r [NiceDeclaration]
ds
      let inherited = KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
r
      if anyChange then return ds' else do
        -- hack to avoid failing on inherited abstract blocks in where clauses
        unless inherited $ declarationWarning $ UselessAbstract r
        return ds -- no change!

    privateBlock ::
         KwRange  -- Range of @private@ keyword.
      -> Origin   -- Origin of the private block.
      -> [NiceDeclaration]
      -> Nice [NiceDeclaration]
    privateBlock :: KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o [NiceDeclaration]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
r Origin
o [NiceDeclaration]
ds
      -- Warn if user-written 'private' does not accomplish anything.
      when (o == UserWritten) do
        if anyChange then
          -- Andreas, 2025-03-29, user-written 'private' is useless in anonymous 'where' modules
          -- since Agda automatically inserts a 'private' there.
          whenM ((AnyWhere_ ==) <$> asks checkingWhere) warn
        else warn
      return $ if anyChange then ds' else ds
      where
        warn :: Nice ()
warn = HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
UselessPrivate KwRange
r

    instanceBlock ::
         KwRange  -- Range of @instance@ keyword.
      -> [NiceDeclaration]
      -> Nice [NiceDeclaration]
    instanceBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r [NiceDeclaration]
ds = do
      let ([NiceDeclaration]
ds', Bool
anyChange) = Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a. Change a -> (a, Bool)
runChange (Change [NiceDeclaration] -> ([NiceDeclaration], Bool))
-> Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r) [NiceDeclaration]
ds
      if Bool
anyChange then [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds' else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
UselessInstance KwRange
r
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds -- no change!

    -- Make a declaration eligible for instance search.
    mkInstance ::
         KwRange  -- Range of @instance@ keyword.
      -> Updater NiceDeclaration
    mkInstance :: KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0 = \case
        Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e          -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
        FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
        NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
        NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds       -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
ds
        NiceLoneConstructor KwRange
r [NiceDeclaration]
ds       -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
ds
        d :: NiceDeclaration
d@NiceFunClause{}              -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x NonEmpty Clause
cs     -> (\ IsInstance
i -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> NonEmpty Clause
-> NiceDeclaration
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x NonEmpty Clause
cs) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Updater IsInstance
setInstance KwRange
r0 IsInstance
i
        NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
i              -> (\ [NiceDeclaration]
i -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
i) ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance KwRange
r0) [NiceDeclaration]
i
        d :: NiceDeclaration
d@NiceField{}                  -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d  -- Field instance are handled by the parser
        d :: NiceDeclaration
d@PrimitiveFunction{}          -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceUnquoteDef{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecSig{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataSig{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModuleMacro{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModule{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePragma{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceOpen{}                   -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceImport{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataDef{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecDef{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePatternSyn{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceGeneralize{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceUnquoteData{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

    setInstance
      :: KwRange  -- Range of @instance@ keyword.
      -> Updater IsInstance
    setInstance :: KwRange -> Updater IsInstance
setInstance KwRange
r0 = \case
      i :: IsInstance
i@InstanceDef{} -> Updater IsInstance
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return IsInstance
i
      IsInstance
_               -> Updater IsInstance
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty Updater IsInstance -> Updater IsInstance
forall a b. (a -> b) -> a -> b
$ KwRange -> IsInstance
InstanceDef KwRange
r0

    macroBlock
      :: KwRange  -- Range of @macro@ keyword.
      -> [NiceDeclaration]
      -> Nice [NiceDeclaration]
    macroBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
macroBlock KwRange
r [NiceDeclaration]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ UpdaterT Nice [NiceDeclaration]
forall a. MakeMacro a => UpdaterT Nice a
mkMacro [NiceDeclaration]
ds
      if anyChange then return ds' else do
        declarationWarning $ UselessMacro r
        return ds -- no change!

class MakeMacro a where
  mkMacro :: UpdaterT Nice a

  default mkMacro :: (Traversable f, MakeMacro a', a ~ f a') => UpdaterT Nice a
  mkMacro = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse a' -> ChangeT Nice a'
forall a. MakeMacro a => UpdaterT Nice a
mkMacro

instance MakeMacro a => MakeMacro [a]

instance MakeMacro NiceDeclaration where
  mkMacro :: UpdaterT Nice NiceDeclaration
mkMacro = \case
    FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
MacroDef ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
    d :: NiceDeclaration
d@FunDef{}                     -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    NiceDeclaration
d                              -> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice NiceDeclaration -> ChangeT Nice NiceDeclaration)
-> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice NiceDeclaration
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice NiceDeclaration)
-> DeclarationException' -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ NiceDeclaration -> DeclarationException'
BadMacroDef NiceDeclaration
d

-- | Make a declaration abstract.
--
-- Mark computation as 'dirty' if there was a declaration that could be made abstract.
-- If no abstraction is taking place, we want to complain about 'UselessAbstract'.
--
-- Alternatively, we could only flag 'dirty' if a non-abstract thing was abstracted.
-- Then, nested @abstract@s would sometimes also be complained about.

class MakeAbstract a where
  mkAbstract ::
       KwRange
         -- ^ Range of the keyword @abstract@.
    -> UpdaterT Nice a

  default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => KwRange -> UpdaterT Nice a
  mkAbstract = (a' -> ChangeT Nice a') -> UpdaterT Nice a
(a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((a' -> ChangeT Nice a') -> UpdaterT Nice a)
-> (KwRange -> a' -> ChangeT Nice a') -> KwRange -> UpdaterT Nice a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> a' -> ChangeT Nice a'
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract

instance MakeAbstract a => MakeAbstract [a]
instance MakeAbstract a => MakeAbstract (List1 a)

-- Leads to overlap with 'WhereClause':
-- instance (Traversable f, MakeAbstract a) => MakeAbstract (f a) where
--   mkAbstract = traverse mkAbstract

instance MakeAbstract IsAbstract where
  mkAbstract :: KwRange -> UpdaterT Nice IsAbstract
mkAbstract KwRange
_ = \case
    a :: IsAbstract
a@IsAbstract
AbstractDef -> UpdaterT Nice IsAbstract
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return IsAbstract
a
    IsAbstract
ConcreteDef -> UpdaterT Nice IsAbstract
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice IsAbstract -> UpdaterT Nice IsAbstract
forall a b. (a -> b) -> a -> b
$ IsAbstract
AbstractDef

instance MakeAbstract NiceDeclaration where
  mkAbstract :: KwRange -> UpdaterT Nice NiceDeclaration
  mkAbstract :: KwRange -> UpdaterT Nice NiceDeclaration
mkAbstract KwRange
kwr = \case
    NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds      -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceDeclaration]
ds
    NiceLoneConstructor KwRange
r [NiceDeclaration]
ds             -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceDeclaration]
ds
    FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x NonEmpty Clause
cs           -> (\ IsAbstract
a -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> NonEmpty Clause
-> NiceDeclaration
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x) (IsAbstract -> NonEmpty Clause -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice (NonEmpty Clause -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr IsAbstract
a ChangeT Nice (NonEmpty Clause -> NiceDeclaration)
-> ChangeT Nice (NonEmpty Clause) -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KwRange -> UpdaterT Nice (NonEmpty Clause)
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr NonEmpty Clause
cs
    NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps [NiceDeclaration]
cs      -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps) (IsAbstract -> [NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr IsAbstract
a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KwRange -> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceDeclaration]
cs
    NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs   -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr IsAbstract
a
    NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d -> (\ IsAbstract
a -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Catchall
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr IsAbstract
a
    -- The following declarations have an @InAbstract@ field
    -- but are not really definitions, so we do count them into
    -- the declarations which can be made abstract
    -- (thus, do not notify progress with @dirty@).
    Axiom Range
r Access
p IsAbstract
_ IsInstance
i ArgInfo
rel Name
x Expr
e                -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom             Range
r Access
p IsAbstract
AbstractDef IsInstance
i ArgInfo
rel Name
x Expr
e
    FunSig Range
r Access
p IsAbstract
_ IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e       -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig            Range
r Access
p IsAbstract
AbstractDef IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
    NiceRecSig  Range
r Erased
er Access
p IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t    -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig     Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
    NiceDataSig Range
r Erased
er Access
p IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t    -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig    Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
    NiceField Range
r Access
p IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
e            -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField         Range
r Access
p IsAbstract
AbstractDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
e
    PrimitiveFunction Range
r Access
p IsAbstract
_ Name
x Arg Expr
e          -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
AbstractDef Name
x Arg Expr
e
    -- Andreas, 2016-07-17 it does have effect on unquoted defs.
    -- Need to set updater state to dirty!
    NiceUnquoteDecl Range
r Access
p IsAbstract
_ IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e    -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
AbstractDef IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
    NiceUnquoteDef Range
r Access
p IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e       -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef  Range
r Access
p IsAbstract
AbstractDef TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
    NiceUnquoteData Range
r Access
p IsAbstract
_ PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e   -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteData Range
r Access
p IsAbstract
AbstractDef PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e
    d :: NiceDeclaration
d@NiceModule{}                       -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    d :: NiceDeclaration
d@NiceModuleMacro{}                  -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    d :: NiceDeclaration
d@NicePragma{}                       -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    d :: NiceDeclaration
d@NiceOpen{}                         -> NiceDeclaration
d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
forall a b. a -> ChangeT Nice b -> ChangeT Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
      Bool -> ChangeT Nice () -> ChangeT Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
kwr) (ChangeT Nice () -> ChangeT Nice ())
-> ChangeT Nice () -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$
        Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT 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
$ Range -> KwRange -> OpenOrImport -> DeclarationWarning'
OpenImportAbstract (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) KwRange
kwr OpenOrImport
OpenNotImport
    d :: NiceDeclaration
d@NiceImport{}                       -> NiceDeclaration
d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
forall a b. a -> ChangeT Nice b -> ChangeT Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
      Bool -> ChangeT Nice () -> ChangeT Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
kwr) (ChangeT Nice () -> ChangeT Nice ())
-> ChangeT Nice () -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$
        Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT 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
$ Range -> KwRange -> OpenOrImport -> DeclarationWarning'
OpenImportAbstract (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) KwRange
kwr OpenOrImport
ImportMayOpen
    d :: NiceDeclaration
d@NicePatternSyn{}                   -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    d :: NiceDeclaration
d@NiceGeneralize{}                   -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
    NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds                   -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceDeclaration]
ds

instance MakeAbstract Clause where
  mkAbstract :: KwRange -> UpdaterT Nice Clause
mkAbstract KwRange
kwr (Clause Name
x Catchall
catchall ArgInfo
ai LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
    Name
-> Catchall
-> ArgInfo
-> LHS
-> RHS
-> WhereClause
-> [Clause]
-> Clause
Clause Name
x Catchall
catchall ArgInfo
ai LHS
lhs RHS
rhs (WhereClause -> [Clause] -> Clause)
-> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice WhereClause
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr WhereClause
wh ChangeT Nice ([Clause] -> Clause)
-> ChangeT Nice [Clause] -> ChangeT Nice Clause
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KwRange -> UpdaterT Nice [Clause]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [Clause]
with

-- | Contents of a @where@ clause are abstract if the parent is.
--
--   These are inherited 'Abstract' blocks, indicated by an empty range
--   for the @abstract@ keyword.
instance MakeAbstract WhereClause where
  mkAbstract :: KwRange -> UpdaterT Nice WhereClause
mkAbstract KwRange
_  WhereClause
NoWhere               = UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ WhereClause
forall decls. WhereClause' decls
NoWhere
  mkAbstract KwRange
_ (AnyWhere Range
r [Declaration]
ds)        = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> [Declaration] -> WhereClause
forall decls. Range -> decls -> WhereClause' decls
AnyWhere Range
r
                                                  [KwRange -> [Declaration] -> Declaration
Abstract KwRange
forall a. Null a => a
empty [Declaration]
ds]
  mkAbstract KwRange
_ (SomeWhere Range
r Erased
e Name
m Access
a [Declaration]
ds) = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Erased
e Name
m Access
a
                                                  [KwRange -> [Declaration] -> Declaration
Abstract KwRange
forall a. Null a => a
empty [Declaration]
ds]

-- | Make a declaration private.
--
-- Andreas, 2012-11-17:
-- Mark computation as 'dirty' if there was a declaration that could be privatized.
-- If no privatization is taking place, we want to complain about 'UselessPrivate'.
--
-- Alternatively, we could only flag 'dirty' if a non-private thing was privatized.
-- Then, nested @private@s would sometimes also be complained about.

class MakePrivate a where
  mkPrivate ::
       KwRange
         -- ^ Range of the @private@ keyword.
    -> Origin
         -- ^ Origin of the @private@ block.
    -> UpdaterT Nice a

  default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => KwRange -> Origin -> UpdaterT Nice a
  mkPrivate KwRange
kwr Origin
o = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a'))
-> (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> a' -> ChangeT Nice a'
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o

instance MakePrivate a => MakePrivate [a]
instance MakePrivate a => MakePrivate (List1 a)

-- Leads to overlap with 'WhereClause':
-- instance (Traversable f, MakePrivate a) => MakePrivate (f a) where
--   mkPrivate = traverse mkPrivate

instance MakePrivate Access where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice Access
mkPrivate KwRange
kwr Origin
o = \case
    p :: Access
p@PrivateAccess{} -> UpdaterT Nice Access
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return Access
p  -- OR? return $ PrivateAccess o
    Access
_                 -> UpdaterT Nice Access
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice Access -> UpdaterT Nice Access
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> Access
PrivateAccess KwRange
kwr Origin
o

instance MakePrivate NiceDeclaration where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice NiceDeclaration
mkPrivate KwRange
kwr Origin
o = \case
      Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e                    -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e)                (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e                -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e)            (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e              -> (\ Access
p -> Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e)          (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds                 -> (\ [NiceDeclaration]
ds-> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds)             ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
      NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds              -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds)          (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is         -> (\ Access
p -> Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is)     (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t         -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)     (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t        -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)    (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d     -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Catchall
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e        -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)    (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p'               -> (\ Access
p -> Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceDeclaration
NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p')           (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t             -> (\ Access
p -> Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t)         (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds                       -> (\ [NiceDeclaration]
p -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
p)                    ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
      d :: NiceDeclaration
d@NicePragma{}                           -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
r QName
_x ImportDirective
dir)                    -> NiceDeclaration
d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
forall a b. a -> ChangeT Nice b -> ChangeT Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
        Bool -> ChangeT Nice () -> ChangeT Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
kwr) (ChangeT Nice () -> ChangeT Nice ())
-> ChangeT Nice () -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$
          Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe KwRange
forall n m. ImportDirective' n m -> Maybe KwRange
publicOpen ImportDirective
dir) \ KwRange
kwrPublic ->
            Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT 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
$ Range -> KwRange -> KwRange -> OpenOrImport -> DeclarationWarning'
OpenImportPrivate Range
r KwRange
kwrPublic KwRange
kwr OpenOrImport
OpenNotImport
      d :: NiceDeclaration
d@(NiceImport Range
r QName
_x Maybe AsName
_as OpenShortHand
_open ImportDirective
dir)        -> NiceDeclaration
d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
forall a b. a -> ChangeT Nice b -> ChangeT Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
        Bool -> ChangeT Nice () -> ChangeT Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (KwRange -> Bool
forall a. Null a => a -> Bool
null KwRange
kwr) (ChangeT Nice () -> ChangeT Nice ())
-> ChangeT Nice () -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$
          Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe KwRange
forall n m. ImportDirective' n m -> Maybe KwRange
publicOpen ImportDirective
dir) \ KwRange
kwrPublic ->
            Nice () -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT 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
$ Range -> KwRange -> KwRange -> OpenOrImport -> DeclarationWarning'
OpenImportPrivate Range
r KwRange
kwrPublic KwRange
kwr OpenOrImport
ImportMayOpen
      -- Andreas, 2016-07-08, issue #2089
      -- we need to propagate 'private' to the named where modules
      FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x NonEmpty Clause
cls              -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> NonEmpty Clause
-> NiceDeclaration
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x (NonEmpty Clause -> NiceDeclaration)
-> ChangeT Nice (NonEmpty Clause) -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice (NonEmpty Clause)
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o NonEmpty Clause
cls
      d :: NiceDeclaration
d@NiceLoneConstructor{}                  -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d -- Issue #7998: constructors cannot be private
      d :: NiceDeclaration
d@NiceDataDef{}                          -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceRecDef{}                           -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceUnquoteData{}                      -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

instance MakePrivate Clause where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice Clause
mkPrivate KwRange
kwr Origin
o (Clause Name
x Catchall
catchall ArgInfo
ai LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
    Name
-> Catchall
-> ArgInfo
-> LHS
-> RHS
-> WhereClause
-> [Clause]
-> Clause
Clause Name
x Catchall
catchall ArgInfo
ai LHS
lhs RHS
rhs (WhereClause -> [Clause] -> Clause)
-> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice WhereClause
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o WhereClause
wh ChangeT Nice ([Clause] -> Clause)
-> ChangeT Nice [Clause] -> ChangeT Nice Clause
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KwRange -> Origin -> UpdaterT Nice [Clause]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [Clause]
with

instance MakePrivate WhereClause where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice WhereClause
mkPrivate KwRange
kwr Origin
o = \case
    d :: WhereClause
d@WhereClause
NoWhere    -> UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return WhereClause
d
    -- @where@-declarations are protected behind an anonymous module,
    -- thus, they are effectively private by default.
    d :: WhereClause
d@AnyWhere{} -> UpdaterT Nice WhereClause
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return WhereClause
d
    -- Andreas, 2016-07-08
    -- A named @where@-module is private if the parent function is private.
    -- The contents of this module are not private, unless declared so!
    -- Thus, we do not recurse into the @ds@ (could not anyway).
    SomeWhere Range
r Erased
e Name
m Access
a [Declaration]
ds ->
      KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
a ChangeT Nice Access
-> (Access -> WhereClause) -> ChangeT Nice WhereClause
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Access
a' -> Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Erased
e Name
m Access
a' [Declaration]
ds

-- | Make sure that the 'TacticAttribute' is empty.
dropTactic :: TacticAttribute -> Nice ()
dropTactic :: TacticAttribute -> Nice ()
dropTactic = \case
  TacticAttribute Maybe (Ranged Expr)
Nothing   -> () -> Nice ()
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  TacticAttribute (Just Ranged Expr
re) -> HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidTacticAttribute (Range -> DeclarationWarning') -> Range -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ Ranged Expr -> Range
forall a. HasRange a => a -> Range
getRange Ranged Expr
re


-- The following function is (at the time of writing) only used three
-- times: for building Lets, and for printing error messages.

-- | (Approximately) convert a 'NiceDeclaration' back to a list of
-- 'Declaration's.
notSoNiceDeclarations :: NiceDeclaration -> List1 Declaration
notSoNiceDeclarations :: NiceDeclaration -> List1 Declaration
notSoNiceDeclarations = \case
    Axiom Range
_ Access
_ IsAbstract
_ IsInstance
i ArgInfo
rel Name
x Expr
e            -> IsInstance -> Declaration -> List1 Declaration
forall {b}.
Singleton Declaration b =>
IsInstance -> Declaration -> b
inst IsInstance
i (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Null a => a
empty Name
x Expr
e
    NiceField Range
_ Access
_ IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt     -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
FieldSig IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt
    PrimitiveFunction Range
_ Access
_ IsAbstract
_ Name
x Arg Expr
e      -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
Primitive KwRange
forall a. Null a => a
empty ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> [Declaration]) -> Declaration -> [Declaration]
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (Arg Expr -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Expr
e) TacticAttribute
forall a. Null a => a
empty Name
x (Arg Expr -> Expr
forall e. Arg e -> e
unArg Arg Expr
e)
    NiceMutual KwRange
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds            -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
Mutual KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [List1 Declaration] -> [Declaration]
forall a. [List1 a] -> [a]
List1.concat ([List1 Declaration] -> [Declaration])
-> [List1 Declaration] -> [Declaration]
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> List1 Declaration)
-> [NiceDeclaration] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceDeclaration -> List1 Declaration
notSoNiceDeclarations [NiceDeclaration]
ds
    NiceLoneConstructor KwRange
r [NiceDeclaration]
ds         -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [List1 Declaration] -> [Declaration]
forall a. [List1 a] -> [a]
List1.concat ([List1 Declaration] -> [Declaration])
-> [List1 Declaration] -> [Declaration]
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> List1 Declaration)
-> [NiceDeclaration] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceDeclaration -> List1 Declaration
notSoNiceDeclarations [NiceDeclaration]
ds
    NiceModule Range
r Access
_ IsAbstract
_ Erased
e QName
x Telescope
tel [Declaration]
ds      -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r Erased
e QName
x Telescope
tel [Declaration]
ds
    NiceModuleMacro Range
r Access
_ Erased
e Name
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir
                                     -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
r Erased
e Name
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir
    NiceOpen Range
r QName
x ImportDirective
dir                 -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> QName -> ImportDirective -> Declaration
Open Range
r QName
x ImportDirective
dir
    NiceImport Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir          -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> Declaration
Import Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir
    NicePragma Range
_ Pragma
p                   -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Pragma -> Declaration
Pragma Pragma
p
    NiceRecSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e   -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e
    NiceDataSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e  -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e
    NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Catchall
_ Declaration
d      -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Declaration
d
    FunSig Range
_ Access
_ IsAbstract
_ IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
_ CoverageCheck
_ Name
x Expr
e     -> IsInstance -> Declaration -> List1 Declaration
forall {b}.
Singleton Declaration b =>
IsInstance -> Declaration -> b
inst IsInstance
i (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Null a => a
empty Name
x Expr
e
    FunDef Range
_ List1 Declaration
ds IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ NonEmpty Clause
_          -> List1 Declaration
ds
    NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs [NiceDeclaration]
cs    -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
r Name
x [LamBinding]
bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [List1 Declaration] -> [Declaration]
forall a. [List1 a] -> [a]
List1.concat ([List1 Declaration] -> [Declaration])
-> [List1 Declaration] -> [Declaration]
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> List1 Declaration)
-> [NiceDeclaration] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceDeclaration -> List1 Declaration
notSoNiceDeclarations [NiceDeclaration]
cs
    NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds
    NicePatternSyn Range
r Access
_ Name
n [WithHiding Name]
as Pattern
p        -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> Name -> [WithHiding Name] -> Pattern -> Declaration
PatternSyn Range
r Name
n [WithHiding Name]
as Pattern
p
    NiceGeneralize Range
_ Access
_ ArgInfo
i TacticAttribute
tac Name
n Expr
e     -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
Generalize KwRange
forall a. Null a => a
empty ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> [Declaration]) -> Declaration -> [Declaration]
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
i TacticAttribute
tac Name
n Expr
e
    NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
i TerminationCheck
_ CoverageCheck
_ [Name]
x Expr
e  -> IsInstance -> Declaration -> List1 Declaration
forall {b}.
Singleton Declaration b =>
IsInstance -> Declaration -> b
inst IsInstance
i (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
r [Name]
x Expr
e
    NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
x Expr
e     -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
r [Name]
x Expr
e
    NiceUnquoteData Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [Name]
xs Expr
e -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ Range -> Name -> [Name] -> Expr -> Declaration
UnquoteData Range
r Name
x [Name]
xs Expr
e
    NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds               -> Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
Opaque KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (KwRange -> [QName] -> Declaration
Unfolding KwRange
r [QName]
ns Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> [Declaration]) -> [Declaration] -> [Declaration]
forall a b. (a -> b) -> a -> b
$ [List1 Declaration] -> [Declaration]
forall a. [List1 a] -> [a]
List1.concat ([List1 Declaration] -> [Declaration])
-> [List1 Declaration] -> [Declaration]
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> List1 Declaration)
-> [NiceDeclaration] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceDeclaration -> List1 Declaration
notSoNiceDeclarations [NiceDeclaration]
ds
  where
    inst :: IsInstance -> Declaration -> b
inst (InstanceDef KwRange
r) Declaration
d = Declaration -> b
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> b) -> Declaration -> b
forall a b. (a -> b) -> a -> b
$ KwRange -> [Declaration] -> Declaration
InstanceB KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall el coll. Singleton el coll => el -> coll
singleton Declaration
d
    inst IsInstance
NotInstanceDef  Declaration
d = Declaration -> b
forall el coll. Singleton el coll => el -> coll
singleton Declaration
d

-- | Has the 'NiceDeclaration' a field of type 'IsAbstract'?
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
niceHasAbstract = \case
    Axiom{}                       -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceField Range
_ Access
_ IsAbstract
a IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_       -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    PrimitiveFunction Range
_ Access
_ IsAbstract
a Name
_ Arg Expr
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceMutual{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceLoneConstructor{}         -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceModule Range
_ Access
_ IsAbstract
a Erased
_ QName
_ Telescope
_ [Declaration]
_      -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceModuleMacro{}             -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceOpen{}                    -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceImport{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NicePragma{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceRecSig{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceDataSig{}                 -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceFunClause Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ Catchall
_ Declaration
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    FunSig{}                      -> Maybe IsAbstract
forall a. Maybe a
Nothing
    FunDef Range
_ List1 Declaration
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ NonEmpty Clause
_        -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceDataDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceRecDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NicePatternSyn{}              -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceGeneralize{}              -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceUnquoteDecl Range
_ Access
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceUnquoteDef Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_    -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceUnquoteData Range
_ Access
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [Name]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceOpaque{}                    -> Maybe IsAbstract
forall a. Maybe a
Nothing