-- | 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.Foldable         qualified as Fold
import Data.Function         ( on )
import Data.List             qualified as List
import Data.Map              qualified as Map
import Data.Maybe
import Data.Semigroup        ( sconcat )
import Data.Text             ( Text )

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

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 Agda.Utils.List1      qualified 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 :: NiceConstructor -> 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 Parameters
_ 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 Parameters
_ 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 DefParameters
_par [NiceConstructor]
_)  = 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]
_ DefParameters
_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 -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps = if LoneSigs -> Bool
forall k a. Map k a -> Bool
Map.null LoneSigs
ps then [NiceConstructor] -> [NiceConstructor]
forall a. a -> a
id else \case
  []     -> [NiceConstructor]
forall a. HasCallStack => a
__IMPOSSIBLE__
  (NiceConstructor
d:[NiceConstructor]
ds) ->
    case NiceConstructor -> Maybe (Name, NiceConstructor)
replaceable NiceConstructor
d of
      -- If declaration d of x is mentioned in the map of lone signatures then replace
      -- it with an axiom.
      Just (Name
x, NiceConstructor
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.
        -> NiceConstructor
axiom NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps' [NiceConstructor]
ds
      Maybe (Name, NiceConstructor)
_ -> NiceConstructor
d     NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps  [NiceConstructor]
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 :: NiceConstructor -> Maybe (Name, NiceConstructor)
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, NiceConstructor) -> Maybe (Name, NiceConstructor)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceConstructor
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 Parameters
pars Expr
t -> Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> Parameters
-> Expr
-> Maybe (Name, NiceConstructor)
forall {m :: * -> *}.
Monad m =>
Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> Parameters
-> Expr
-> m (Name, NiceConstructor)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x Parameters
pars Expr
t
      NiceDataSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x Parameters
pars Expr
t -> Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> Parameters
-> Expr
-> Maybe (Name, NiceConstructor)
forall {m :: * -> *}.
Monad m =>
Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> Parameters
-> Expr
-> m (Name, NiceConstructor)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x Parameters
pars Expr
t
      NiceConstructor
_ -> Maybe (Name, NiceConstructor)
forall a. Maybe a
Nothing
      where
        retAx :: Range
-> Erased
-> Access
-> IsAbstract
-> Name
-> Parameters
-> Expr
-> m (Name, NiceConstructor)
retAx Range
r Erased
erased Access
acc IsAbstract
abst Name
x Parameters
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 -> Parameters -> Telescope
parametersToTelescope Range
r Parameters
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, NiceConstructor) -> m (Name, NiceConstructor)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceConstructor
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 [NiceConstructor]
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 -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps [NiceConstructor]
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 :: [NiceConstructor] -> Nice [NiceConstructor]
inferMutualBlocks [] = [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    inferMutualBlocks (NiceConstructor
d : [NiceConstructor]
ds) =
      case NiceConstructor -> DeclKind
declKind NiceConstructor
d of
        DeclKind
OtherDecl    -> (NiceConstructor
d NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
:) ([NiceConstructor] -> [NiceConstructor])
-> Nice [NiceConstructor] -> Nice [NiceConstructor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceConstructor] -> Nice [NiceConstructor]
inferMutualBlocks [NiceConstructor]
ds
        LoneDefs{}   -> (NiceConstructor
d NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
:) ([NiceConstructor] -> [NiceConstructor])
-> Nice [NiceConstructor] -> Nice [NiceConstructor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceConstructor] -> Nice [NiceConstructor]
inferMutualBlocks [NiceConstructor]
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 -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps (NiceConstructor
d NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
: [NiceConstructor]
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 -> [NiceConstructor] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceConstructor]
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
-> [NiceConstructor] -> [NiceConstructor] -> InferredMutual
InferredMutual MutualChecks
checks [] [NiceConstructor]
ds)
              NiceConstructor
d : [NiceConstructor]
ds -> case NiceConstructor -> DeclKind
declKind NiceConstructor
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
                  NiceConstructor -> InferredMutual -> InferredMutual
extendInferredBlock  NiceConstructor
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceConstructor] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceConstructor]
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
                  NiceConstructor -> InferredMutual -> InferredMutual
extendInferredBlock  NiceConstructor
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceConstructor] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceConstructor]
ds
                DeclKind
OtherDecl -> NiceConstructor -> InferredMutual -> InferredMutual
extendInferredBlock NiceConstructor
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceConstructor] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceConstructor]
ds

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

    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 :: [Declaration] -> Nice ([NiceConstructor], [Declaration])
nice1 []     = ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [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 ([NiceConstructor], [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 ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__

        Generalize KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyGeneralize KwRange
r
        Generalize KwRange
_ [Declaration]
sigs -> do
          gs <- [Declaration]
-> (Declaration -> Nice NiceConstructor) -> Nice [NiceConstructor]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
sigs ((Declaration -> Nice NiceConstructor) -> Nice [NiceConstructor])
-> (Declaration -> Nice NiceConstructor) -> Nice [NiceConstructor]
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
              NiceConstructor -> Nice NiceConstructor
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceConstructor -> Nice NiceConstructor)
-> NiceConstructor -> Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceConstructor
NiceGeneralize (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
sig) Access
PublicAccess ArgInfo
info TacticAttribute
tac Name
x Expr
t
            Declaration
_ -> Nice NiceConstructor
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 [NiceConstructor]
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 [NiceConstructor])
-> List1 Declaration -> Nice [NiceConstructor]
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
                ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Catchall
-> Declaration
-> NiceConstructor
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 ([NiceConstructor], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationException' -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyField KwRange
r
        Field KwRange
_ [Declaration]
fs -> (,[Declaration]
ds) ([NiceConstructor] -> ([NiceConstructor], [Declaration]))
-> Nice [NiceConstructor]
-> Nice ([NiceConstructor], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          [Declaration]
-> (Declaration -> Nice NiceConstructor) -> Nice [NiceConstructor]
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) -> NiceConstructor -> Nice NiceConstructor
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NiceConstructor -> Nice NiceConstructor)
-> NiceConstructor -> Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceConstructor
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 NiceConstructor
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice NiceConstructor)
-> DeclarationException' -> Nice NiceConstructor
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 Parameters
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 Parameters
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
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig erased) (niceAxioms DataBlock) r
                      x (Just (tel, t)) (Just (parametersToDefParameters tel, cs))

        DataDef Range
r Name
x Parameters
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 <- retrieveTypeSig (DataName pc uc) x
          defpars <- niceDefParameters IsData tel
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig defaultErased) (niceAxioms DataBlock) r
                      x ((tel,) <$> mt) (Just (defpars, cs))

        RecordSig Range
r Erased
erased Name
x Parameters
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 Parameters
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
          (,ds) <$> dataOrRec pc uc
                      (\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x DefParameters
tel [Declaration]
cs ->
                        Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> DefParameters
-> [Declaration]
-> NiceConstructor
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir DefParameters
tel [Declaration]
cs)
                      (flip NiceRecSig erased) return r x
                      (Just (tel, t)) (Just (parametersToDefParameters tel, cs))

        RecordDef Range
r Name
x [RecordDirective]
dir Parameters
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 <- retrieveTypeSig (RecName pc uc) x
          defpars <- niceDefParameters (IsRecord ()) tel
          (,ds) <$> dataOrRec pc uc
                      (\Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x DefParameters
tel [Declaration]
cs ->
                        Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> DefParameters
-> [Declaration]
-> NiceConstructor
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir DefParameters
tel [Declaration]
cs)
                      (flip NiceRecSig defaultErased) return r x
                      ((tel,) <$> mt) (Just (defpars, 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 ([NiceConstructor], [Declaration])
DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceConstructor] -> ([NiceConstructor], [Declaration]))
-> Nice [NiceConstructor]
-> Nice ([NiceConstructor], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceConstructor -> [NiceConstructor]
forall el coll. Singleton el coll => el -> coll
singleton (NiceConstructor -> [NiceConstructor])
-> Nice NiceConstructor -> Nice [NiceConstructor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceConstructor] -> Nice NiceConstructor
mkOldMutual KwRange
r ([NiceConstructor] -> Nice NiceConstructor)
-> Nice [NiceConstructor] -> Nice NiceConstructor
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceConstructor]
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 ([NiceConstructor], [Declaration])
DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyMutual KwRange
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceConstructor] -> ([NiceConstructor], [Declaration]))
-> Nice [NiceConstructor]
-> Nice ([NiceConstructor], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceConstructor -> [NiceConstructor]
forall el coll. Singleton el coll => el -> coll
singleton (NiceConstructor -> [NiceConstructor])
-> Nice NiceConstructor -> Nice [NiceConstructor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KwRange -> [NiceConstructor] -> Nice NiceConstructor
mkInterleavedMutual KwRange
r ([NiceConstructor] -> Nice NiceConstructor)
-> Nice [NiceConstructor] -> Nice NiceConstructor
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceConstructor]
nice [Declaration]
ds'))

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

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

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

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

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

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

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

        Module Range
r Erased
erased QName
x Telescope
tel [Declaration]
ds' -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$
          ([Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceConstructor
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 -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$
          ([Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceConstructor
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
_  -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
        Syntax Name
_ Notation
_ -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [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
          ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceConstructor
NicePatternSyn Range
r Access
PublicAccess Name
n [WithHiding Name]
as Pattern
p] , [Declaration]
ds)
        Open Range
r QName
x ImportDirective
is         -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> QName -> ImportDirective -> NiceConstructor
NiceOpen Range
r QName
x ImportDirective
is] , [Declaration]
ds)
        Import Ranged OpenShortHand
opn KwRange
r QName
x Either AsName RawOpenArgs
as ImportDirective
is-> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ranged OpenShortHand
-> KwRange
-> QName
-> Either AsName RawOpenArgs
-> ImportDirective
-> NiceConstructor
NiceImport Ranged OpenShortHand
opn KwRange
r QName
x Either AsName RawOpenArgs
as 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 ([NiceConstructor], [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 [NiceConstructor]
nice [Declaration]
body
          ps <- use loneSigs
          checkLoneSigs ps
          let decls = LoneSigs -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps [NiceConstructor]
decls0
          body <- inferMutualBlocks decls
          pure ([NiceOpaque r (concat unfoldings) body], ds)

        Unfolding KwRange
r [QName]
_ -> DeclarationException' -> Nice ([NiceConstructor], [Declaration])
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ([NiceConstructor], [Declaration]))
-> DeclarationException' -> Nice ([NiceConstructor], [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 ([NiceConstructor], [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 ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma (Range -> Name -> TerminationCheck
forall m. Range -> m -> TerminationCheck m
TerminationMeasure Range
r Name
x) (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     TerminationCheckPragma Range
r TerminationCheck
tc ->
      if [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds then
        TerminationCheck
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma TerminationCheck
tc (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     NoCoverageCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveCoverageCheckPragma [Declaration]
ds then
        CoverageCheck
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma CoverageCheck
NoCoverageCheck (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     CatchallPragma Range
r ->
      if [Declaration] -> Bool
canHaveCatchallPragma [Declaration]
ds then
        Catchall
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. Catchall -> Nice a -> Nice a
withCatchallPragma (Range -> Catchall
YesCatchall Range
r) (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     NoPositivityCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveNoPositivityCheckPragma [Declaration]
ds then
        PositivityCheck
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma PositivityCheck
NoPositivityCheck (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     NoUniverseCheckPragma Range
r ->
      if [Declaration] -> Bool
canHaveNoUniverseCheckPragma [Declaration]
ds then
        UniverseCheck
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma UniverseCheck
NoUniverseCheck (Nice ([NiceConstructor], [Declaration])
 -> Nice ([NiceConstructor], [Declaration]))
-> Nice ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
nice1 [Declaration]
ds

     -- Polarity pragmas have been handled with fixity declarations, can be deleted.
     PolarityPragma{} -> ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [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 ([NiceConstructor], [Declaration])
keep
     CompilePragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     DisplayPragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     EtaPragma{}                   -> Nice ([NiceConstructor], [Declaration])
keep
     ForeignPragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     ImpossiblePragma{}            -> Nice ([NiceConstructor], [Declaration])
keep
     InjectiveForInferencePragma{} -> Nice ([NiceConstructor], [Declaration])
keep
     InjectivePragma{}             -> Nice ([NiceConstructor], [Declaration])
keep
     InlinePragma{}                -> Nice ([NiceConstructor], [Declaration])
keep
     NotProjectionLikePragma{}     -> Nice ([NiceConstructor], [Declaration])
keep
     OptionsPragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     OverlapPragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     RewritePragma{}               -> Nice ([NiceConstructor], [Declaration])
keep
     StaticPragma{}                -> Nice ([NiceConstructor], [Declaration])
keep
     WarningOnImport{}             -> Nice ([NiceConstructor], [Declaration])
keep
     WarningOnUsage{}              -> Nice ([NiceConstructor], [Declaration])
keep

     where keep :: Nice ([NiceConstructor], [Declaration])
keep = ([NiceConstructor], [Declaration])
-> Nice ([NiceConstructor], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceConstructor
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

    -- Get the data or record type signature.
    retrieveTypeSig :: DataRecOrFun -> Name -> Nice (Maybe Expr)
    retrieveTypeSig :: DataRecOrFun -> Name -> Nice (Maybe Expr)
retrieveTypeSig DataRecOrFun
k Name
x = 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 -> DefParameters -> [decl] -> NiceDeclaration)
         -- Construct definition.
      -> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> Parameters -> Expr -> NiceDeclaration)
         -- Construct signature.
      -> ([a] -> Nice [decl])        -- Constructor checking.
      -> Range
      -> Name                        -- Data/record type name.
      -> Maybe (Parameters, Expr)    -- Parameters and type.  If not @Nothing@ a signature is created.
      -> Maybe (DefParameters, [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
    -> DefParameters
    -> [decl]
    -> NiceConstructor)
-> (Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> Parameters
    -> Expr
    -> NiceConstructor)
-> ([a] -> Nice [decl])
-> Range
-> Name
-> Maybe (Parameters, Expr)
-> Maybe (DefParameters, [a])
-> Nice [NiceConstructor]
dataOrRec PositivityCheck
pc UniverseCheck
uc Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> DefParameters
-> [decl]
-> NiceConstructor
mkDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
mkSig [a] -> Nice [decl]
niceD Range
r Name
x Maybe (Parameters, Expr)
mt Maybe (DefParameters, [a])
mcs = do
      mds <- ((DefParameters, [a]) -> Nice (DefParameters, [decl]))
-> Maybe (DefParameters, [a])
-> Nice (Maybe (DefParameters, [decl]))
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) -> Maybe a -> m (Maybe b)
mapM (([a] -> Nice [decl])
-> (DefParameters, [a]) -> Nice (DefParameters, [decl])
forall (m :: * -> *) b d a.
Functor m =>
(b -> m d) -> (a, b) -> m (a, d)
secondM [a] -> Nice [decl]
niceD) Maybe (DefParameters, [a])
mcs
      -- 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 (Parameters, Expr) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Parameters, Expr)
mt Bool -> Bool -> Bool
&& Maybe (DefParameters, [a]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (DefParameters, [a])
mcs = Origin
Inserted
            | Bool
otherwise               = Origin
UserWritten
      return $ catMaybes $
        [ mt  <&> \ (Parameters
tel, Expr
t)  -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
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 Parameters
tel Expr
t
        , mds <&> \ (DefParameters
tel, [decl]
ds) -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> DefParameters
-> [decl]
-> NiceConstructor
mkDef Range
r Origin
o IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x DefParameters
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 [NiceConstructor]
niceAxioms KindOfBlock
b [Declaration]
ds = [[NiceConstructor]] -> [NiceConstructor]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[NiceConstructor]] -> [NiceConstructor])
-> Nice [[NiceConstructor]] -> Nice [NiceConstructor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> Nice [NiceConstructor])
-> [Declaration] -> Nice [[NiceConstructor]]
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 [NiceConstructor]
niceAxiom [Declaration]
ds
      where
        niceAxiom :: TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
        niceAxiom :: Declaration -> Nice [NiceConstructor]
niceAxiom = \case
          d :: Declaration
d@(TypeSig ArgInfo
rel TacticAttribute
tac Name
x Expr
t) -> do
            TacticAttribute -> Nice ()
dropTactic TacticAttribute
tac
            [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceConstructor
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 -> [NiceConstructor] -> Nice [NiceConstructor]
instanceBlock KwRange
r ([NiceConstructor] -> Nice [NiceConstructor])
-> Nice [NiceConstructor] -> Nice [NiceConstructor]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceConstructor]
niceAxioms KindOfBlock
b [Declaration]
ds
          Private KwRange
r Origin
o [Declaration]
ds | Bool
privateAllowed -> KwRange -> Origin -> [NiceConstructor] -> Nice [NiceConstructor]
privateBlock KwRange
r Origin
o ([NiceConstructor] -> Nice [NiceConstructor])
-> Nice [NiceConstructor] -> Nice [NiceConstructor]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceConstructor]
niceAxioms KindOfBlock
b [Declaration]
ds
          -- @data _ where@, @postulate@ and @primitive@ blocks exclude each other.
          Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceConstructor
NicePragma Range
r Pragma
p ]
          Pragma p :: Pragma
p@(OverlapPragma Range
r [QName]
_ OverlapMode
_) -> [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceConstructor
NicePragma Range
r Pragma
p ]
          Declaration
d -> DeclarationException' -> Nice [NiceConstructor]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [NiceConstructor])
-> DeclarationException' -> Nice [NiceConstructor]
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 -> [NiceConstructor] -> Nice [NiceConstructor]
constructorBlock KwRange
r [] = [] [NiceConstructor] -> Nice () -> Nice [NiceConstructor]
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 [NiceConstructor]
ds = [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceConstructor] -> Nice [NiceConstructor])
-> [NiceConstructor] -> Nice [NiceConstructor]
forall a b. (a -> b) -> a -> b
$ NiceConstructor -> [NiceConstructor]
forall el coll. Singleton el coll => el -> coll
singleton (NiceConstructor -> [NiceConstructor])
-> NiceConstructor -> [NiceConstructor]
forall a b. (a -> b) -> a -> b
$ KwRange -> [NiceConstructor] -> NiceConstructor
NiceLoneConstructor KwRange
r [NiceConstructor]
ds

    postulateBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    postulateBlock :: KwRange -> [NiceConstructor] -> Nice [NiceConstructor]
postulateBlock KwRange
r [] = [] [NiceConstructor] -> Nice () -> Nice [NiceConstructor]
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
_ [NiceConstructor]
ds = [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceConstructor]
ds

    primitiveBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    primitiveBlock :: KwRange -> [NiceConstructor] -> Nice [NiceConstructor]
primitiveBlock KwRange
r [] = [] [NiceConstructor] -> Nice () -> Nice [NiceConstructor]
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
_ [NiceConstructor]
ds = (NiceConstructor -> Nice NiceConstructor)
-> [NiceConstructor] -> Nice [NiceConstructor]
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 NiceConstructor -> Nice NiceConstructor
toPrim [NiceConstructor]
ds

    toPrim :: NiceDeclaration -> Nice NiceDeclaration
    toPrim :: NiceConstructor -> Nice NiceConstructor
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 ()
      NiceConstructor -> Nice NiceConstructor
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceConstructor -> Nice NiceConstructor)
-> NiceConstructor -> Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceConstructor
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 NiceConstructor
_ = Nice NiceConstructor
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 [NiceConstructor]
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 (List1 Clause)
mkClauses1 ArgInfo
info Name
x List1 Declaration
ds Catchall
ca = List1 Clause -> [Clause] -> List1 Clause
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe List1 Clause
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Clause] -> List1 Clause) -> Nice [Clause] -> Nice (List1 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 b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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 -> NiceConstructor -> 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
_ NiceConstructor
_ = 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 -> [NiceConstructor] -> Nice NiceConstructor
mkInterleavedMutual KwRange
kwr [NiceConstructor]
ds' = do
      (other, ISt m checks _) <- StateT InterleavedState Nice [(Int, NiceConstructor)]
-> InterleavedState
-> Nice ([(Int, NiceConstructor)], InterleavedState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (KwRange
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
groupByBlocks KwRange
kwr [NiceConstructor]
ds') (InterleavedState
 -> Nice ([(Int, NiceConstructor)], InterleavedState))
-> InterleavedState
-> Nice ([(Int, NiceConstructor)], 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
      idecls <- (other ++) . concat <$> mapM (uncurry interleavedDecl) (Map.toList m)
      let decls0 = ((Int, NiceConstructor) -> NiceConstructor)
-> [(Int, NiceConstructor)] -> [NiceConstructor]
forall a b. (a -> b) -> [a] -> [b]
map (Int, NiceConstructor) -> NiceConstructor
forall a b. (a, b) -> b
snd ([(Int, NiceConstructor)] -> [NiceConstructor])
-> [(Int, NiceConstructor)] -> [NiceConstructor]
forall a b. (a -> b) -> a -> b
$ ((Int, NiceConstructor) -> (Int, NiceConstructor) -> Ordering)
-> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, NiceConstructor) -> Int)
-> (Int, NiceConstructor)
-> (Int, NiceConstructor)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, NiceConstructor) -> Int
forall a b. (a, b) -> a
fst) [(Int, NiceConstructor)]
idecls
      ps <- use loneSigs
      checkLoneSigs ps
      let decls = LoneSigs -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps [NiceConstructor]
decls0
      -- process the checks
      let r = KwRange -> [NiceConstructor] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceConstructor]
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
          whenJust (Map.lookup n m) \ InterleavedDecl
y -> 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
$ Name -> Range -> DeclarationException'
DuplicateDefinition Name
n (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ InterleavedDecl -> Range
forall a. HasRange a => a -> Range
getRange InterleavedDecl
y
          put $ ISt (Map.insert n (c i) m) (mc <> checks) (i + 1)

        addFunType :: NiceConstructor -> INice ()
addFunType d :: NiceConstructor
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
-> NiceConstructor
-> Maybe (Int, List1 (List1 Declaration, List1 Clause))
-> InterleavedDecl
InterleavedFun Int
i NiceConstructor
d Maybe (Int, List1 (List1 Declaration, List1 Clause))
forall a. Maybe a
Nothing) MutualChecks
checks
        addFunType NiceConstructor
_ = INice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

        addDataConstructors ::
             Maybe (Name, DefParameters)
               -- Data type the constructors belong to, and parameter telescope of the data definition.
          -> [NiceConstructor]
               -- Constructors to add.
          -> INice ()
        -- if we know the type's name, we can go ahead
        addDataConstructors :: Maybe (Name, DefParameters) -> [NiceConstructor] -> INice ()
addDataConstructors (Just (Name
n, DefParameters
pars)) [NiceConstructor]
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 NiceConstructor
sig Maybe (Int, List1 (DefParameters, [NiceConstructor]))
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 (DefParameters, [NiceConstructor]))
cs', Int
i') = case Maybe (Int, List1 (DefParameters, [NiceConstructor]))
cs of
                    Maybe (Int, List1 (DefParameters, [NiceConstructor]))
Nothing        -> ((Int
i , (DefParameters
pars, [NiceConstructor]
ds) (DefParameters, [NiceConstructor])
-> [(DefParameters, [NiceConstructor])]
-> List1 (DefParameters, [NiceConstructor])
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    Just (Int
i1, List1 (DefParameters, [NiceConstructor])
ds1) -> ((Int
i1, (DefParameters
pars, [NiceConstructor]
ds) (DefParameters, [NiceConstructor])
-> List1 (DefParameters, [NiceConstructor])
-> List1 (DefParameters, [NiceConstructor])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 (DefParameters, [NiceConstructor])
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
-> NiceConstructor
-> Maybe (Int, List1 (DefParameters, [NiceConstructor]))
-> InterleavedDecl
InterleavedData Int
i0 NiceConstructor
sig ((Int, List1 (DefParameters, [NiceConstructor]))
-> Maybe (Int, List1 (DefParameters, [NiceConstructor]))
forall a. a -> Maybe a
Just (Int, List1 (DefParameters, [NiceConstructor]))
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, DefParameters)
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, DefParameters)
Nothing (NiceConstructor
d : [NiceConstructor]
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 ([NiceConstructor]
ds0, [NiceConstructor]
ds1) = (NiceConstructor -> Bool)
-> [NiceConstructor] -> ([NiceConstructor], [NiceConstructor])
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)
-> (NiceConstructor -> Either (Name, [Name]) Name)
-> NiceConstructor
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> NiceConstructor -> Either (Name, [Name]) Name
isConstructor [Name
n]) [NiceConstructor]
ds
              Maybe (Name, DefParameters) -> [NiceConstructor] -> INice ()
addDataConstructors ((Name, DefParameters) -> Maybe (Name, DefParameters)
forall a. a -> Maybe a
Just (Name
n, [])) (NiceConstructor
d NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
: [NiceConstructor]
ds0)
              -- and then repeat the process for the rest of the block
              Maybe (Name, DefParameters) -> [NiceConstructor] -> INice ()
addDataConstructors Maybe (Name, DefParameters)
forall a. Maybe a
Nothing [NiceConstructor]
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 (NiceConstructor -> Range
forall a. HasRange a => a -> Range
getRange NiceConstructor
d) Name
n [Name]
ns

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

        addInterleavedFun :: Name -> List1 Declaration -> List1 Clause -> MutualChecks -> INice ()
        addInterleavedFun :: Name
-> List1 Declaration -> List1 Clause -> MutualChecks -> INice ()
addInterleavedFun Name
n List1 Declaration
ds List1 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 NiceConstructor
sig Maybe (Int, List1 (List1 Declaration, List1 Clause))
cs0) -> do
              let ((Int, List1 (List1 Declaration, List1 Clause))
cs', Int
i') = case Maybe (Int, List1 (List1 Declaration, List1 Clause))
cs0 of
                    Maybe (Int, List1 (List1 Declaration, List1 Clause))
Nothing        -> ((Int
i,  (List1 Declaration
ds, List1 Clause
cs) (List1 Declaration, List1 Clause)
-> [(List1 Declaration, List1 Clause)]
-> List1 (List1 Declaration, List1 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, List1 Clause)
cs1) -> ((Int
i1, (List1 Declaration
ds, List1 Clause
cs) (List1 Declaration, List1 Clause)
-> List1 (List1 Declaration, List1 Clause)
-> List1 (List1 Declaration, List1 Clause)
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 (List1 Declaration, List1 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
-> NiceConstructor
-> Maybe (Int, List1 (List1 Declaration, List1 Clause))
-> InterleavedDecl
InterleavedFun Int
i0 NiceConstructor
sig ((Int, List1 (List1 Declaration, List1 Clause))
-> Maybe (Int, List1 (List1 Declaration, List1 Clause))
forall a. a -> Maybe a
Just (Int, List1 (List1 Declaration, List1 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
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
addFunClauses KwRange
r (nd :: NiceConstructor
nd@(NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Catchall
_ (FunClause ArgInfo
ai LHS
lhs RHS
_ WhereClause
_ Catchall
_)) : [NiceConstructor]
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,NiceConstructor
nd) (Int, NiceConstructor)
-> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceConstructor)] -> [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
groupByBlocks KwRange
r [NiceConstructor]
ds
            -- exactly one candidate: attach the funclause to the definition
            [(Name
n, NonEmpty (MutualChecks, Declaration)
fits0, [NiceConstructor]
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), [NiceConstructor])
xf:[(Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])]
xfs -> Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
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, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice [(Int, NiceConstructor)]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
                           (DeclarationException' -> Nice [(Int, NiceConstructor)])
-> DeclarationException' -> Nice [(Int, NiceConstructor)]
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), [NiceConstructor])
 -> Name)
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
-> 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)
_,[NiceConstructor]
_) -> Name
a) (NonEmpty
   (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
 -> List1 Name)
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
xf (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
-> [(Name, NonEmpty (MutualChecks, Declaration),
     [NiceConstructor])]
-> NonEmpty
     (Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])
forall a. a -> [a] -> NonEmpty a
:| [(Name, NonEmpty (MutualChecks, Declaration), [NiceConstructor])]
xfs
        addFunClauses KwRange
_ [NiceConstructor]
_ = StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a. HasCallStack => a
__IMPOSSIBLE__

        groupByBlocks ::
              KwRange
                -- Range of the @interleaved mutual@ keyword.
          -> [NiceDeclaration]
          -> INice [(DeclNum, NiceDeclaration)]
        groupByBlocks :: KwRange
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
groupByBlocks KwRange
_kwr []      = [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a. a -> StateT InterleavedState Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        groupByBlocks KwRange
kwr (NiceConstructor
d : [NiceConstructor]
ds) = do
          -- for most branches we deal with the one declaration and move on
          let oneOff :: StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff StateT InterleavedState Nice [(Int, NiceConstructor)]
act = StateT InterleavedState Nice [(Int, NiceConstructor)]
act StateT InterleavedState Nice [(Int, NiceConstructor)]
-> ([(Int, NiceConstructor)]
    -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
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, NiceConstructor)]
ns -> ([(Int, NiceConstructor)]
ns [(Int, NiceConstructor)]
-> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
forall a. [a] -> [a] -> [a]
++) ([(Int, NiceConstructor)] -> [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
groupByBlocks KwRange
kwr [NiceConstructor]
ds
          case NiceConstructor
d of
            NiceDataSig{}                -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceConstructor)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceConstructor -> INice ()
addDataType NiceConstructor
d
            NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
n DefParameters
pars [NiceConstructor]
ds
                                         -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceConstructor)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
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, DefParameters) -> [NiceConstructor] -> INice ()
addDataConstructors ((Name, DefParameters) -> Maybe (Name, DefParameters)
forall a. a -> Maybe a
Just (Name
n, DefParameters
pars)) [NiceConstructor]
ds
            NiceLoneConstructor KwRange
_ [NiceConstructor]
ds     -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceConstructor)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
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, DefParameters) -> [NiceConstructor] -> INice ()
addDataConstructors Maybe (Name, DefParameters)
forall a. Maybe a
Nothing [NiceConstructor]
ds
            FunSig{}                     -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceConstructor)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceConstructor -> INice ()
addFunType NiceConstructor
d
            FunDef Range
_ List1 Declaration
_ IsAbstract
_  IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
n List1 Clause
_cs
                      | Bool -> Bool
not (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n) -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceConstructor)]
-> INice ()
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
forall a b.
a
-> StateT InterleavedState Nice b -> StateT InterleavedState Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NiceConstructor -> INice ()
addFunDef NiceConstructor
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
-> [NiceConstructor]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
addFunClauses KwRange
kwr (NiceConstructor
dNiceConstructor -> [NiceConstructor] -> [NiceConstructor]
forall a. a -> [a] -> [a]
:[NiceConstructor]
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!
            NiceConstructor
_ -> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
oneOff (StateT InterleavedState Nice [(Int, NiceConstructor)]
 -> StateT InterleavedState Nice [(Int, NiceConstructor)])
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
-> StateT InterleavedState Nice [(Int, NiceConstructor)]
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] -> NiceConstructor -> 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]
_ NiceConstructor
_ = 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 -> [NiceConstructor] -> Nice NiceConstructor
mkOldMutual KwRange
kwr [NiceConstructor]
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 :: [NiceConstructor]
ds = LoneSigs -> [NiceConstructor] -> [NiceConstructor]
replaceSigs LoneSigs
ps [NiceConstructor]
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) <- [NiceConstructor]
-> (NiceConstructor
    -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor))
-> Nice ([NiceConstructor], [NiceConstructor], [NiceConstructor])
forall (m :: * -> *) a b c d.
Applicative m =>
[a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
forEither3M [NiceConstructor]
ds ((NiceConstructor
  -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor))
 -> Nice ([NiceConstructor], [NiceConstructor], [NiceConstructor]))
-> (NiceConstructor
    -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor))
-> Nice ([NiceConstructor], [NiceConstructor], [NiceConstructor])
forall a b. (a -> b) -> a -> b
$ \ NiceConstructor
d -> do
          let top :: Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top       = Either3 NiceConstructor NiceConstructor NiceConstructor
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceConstructor
-> Either3 NiceConstructor NiceConstructor NiceConstructor
forall a b c. a -> Either3 a b c
In1 NiceConstructor
d)
              bottom :: Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
bottom    = Either3 NiceConstructor NiceConstructor NiceConstructor
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceConstructor
-> Either3 NiceConstructor NiceConstructor NiceConstructor
forall a b c. b -> Either3 a b c
In2 NiceConstructor
d)
              invalid :: String
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
invalid String
s = NiceConstructor
-> Either3 NiceConstructor NiceConstructor NiceConstructor
forall a b c. c -> Either3 a b c
In3 NiceConstructor
d Either3 NiceConstructor NiceConstructor NiceConstructor
-> Nice ()
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
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 (NiceConstructor -> Range
forall a. HasRange a => a -> Range
getRange NiceConstructor
d) String
s
          case NiceConstructor
d of
            -- Andreas, 2013-11-23 allow postulates in mutual blocks
            Axiom{}             -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceField{}         -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            PrimitiveFunction{} -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            -- Andreas, 2019-07-23 issue #3932:
            -- Nested mutual blocks are not supported.
            NiceMutual{}        -> String
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
invalid String
"mutual blocks"
            -- Andreas, 2018-10-29, issue #3246
            -- We could allow modules (top), but this is potentially confusing.
            NiceModule{}        -> String
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
invalid String
"Module definitions"
            -- Lone constructors are only allowed in new-style mutual blocks
            NiceLoneConstructor{} -> String
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
invalid String
"Lone constructors"
            NiceModuleMacro{}   -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceOpen{}          -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceImport{}        -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceRecSig{}        -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceDataSig{}       -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
            -- in ConcreteToAbstract rather than here.
            NiceFunClause{}     -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
bottom
            FunSig{}            -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            FunDef{}            -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
bottom
            NiceDataDef{}       -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
bottom
            NiceRecDef{}        -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
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 NiceConstructor NiceConstructor NiceConstructor)
bottom
            NiceGeneralize{}    -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceUnquoteDecl{}   -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
top
            NiceUnquoteDef{}    -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
bottom
            NiceUnquoteData{}   -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
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]
_ [NiceConstructor]
_    ->
              NiceConstructor
-> Either3 NiceConstructor NiceConstructor NiceConstructor
forall a b c. c -> Either3 a b c
In3 NiceConstructor
d Either3 NiceConstructor NiceConstructor NiceConstructor
-> Nice (ZonkAny 0)
-> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
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 NiceConstructor NiceConstructor NiceConstructor)
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 NiceConstructor NiceConstructor NiceConstructor)
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 NiceConstructor NiceConstructor NiceConstructor)
invalid String
"REWRITE pragmas"

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

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

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

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

              -- The attached pragmas have already been handled at this point.
              CatchallPragma{}          -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. HasCallStack => a
__IMPOSSIBLE__
              TerminationCheckPragma{}  -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoPositivityCheckPragma{} -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. HasCallStack => a
__IMPOSSIBLE__
              PolarityPragma{}          -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoUniverseCheckPragma{}   -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoCoverageCheckPragma{}   -> Nice (Either3 NiceConstructor NiceConstructor NiceConstructor)
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 = (NiceConstructor -> TerminationCheck)
-> [NiceConstructor] -> [TerminationCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceConstructor -> TerminationCheck
termCheck [NiceConstructor]
ds
        let r   = KwRange -> [NiceConstructor] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceConstructor]
ds'
        tc <- combineTerminationChecks r (tc0:tcs)

        -- Compute coverage checking flag for mutual block
        cc0 <- use coverageCheckPragma
        let ccs = (NiceConstructor -> CoverageCheck)
-> [NiceConstructor] -> [CoverageCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceConstructor -> CoverageCheck
covCheck [NiceConstructor]
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 = (NiceConstructor -> PositivityCheck)
-> [NiceConstructor] -> [PositivityCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceConstructor -> PositivityCheck
positivityCheckOldMutual [NiceConstructor]
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 <- (NiceConstructor -> DeclKind) -> [NiceConstructor] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceConstructor -> DeclKind
declKind [NiceConstructor]
ds' ]
        defNames :: [(Name, DataRecOrFun)]
defNames  = [ (Name
x, DataRecOrFun
k) | LoneDefs DataRecOrFun
k [Name]
xs <- (NiceConstructor -> DeclKind) -> [NiceConstructor] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceConstructor -> DeclKind
declKind [NiceConstructor]
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 :: NiceConstructor -> 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
_ List1 Clause
_)          = TerminationCheck
tc
        -- ASR (28 December 2015): Is this equation necessary?
        termCheck (NiceMutual KwRange
_ TerminationCheck
tc CoverageCheck
_ PositivityCheck
_ [NiceConstructor]
_)            = 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 :: NiceConstructor -> 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
_ List1 Clause
_)          = CoverageCheck
cc
        -- ASR (28 December 2015): Is this equation necessary?
        covCheck (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
cc PositivityCheck
_ [NiceConstructor]
_)            = 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 :: NiceConstructor -> PositivityCheck
positivityCheckOldMutual (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ DefParameters
_ [NiceConstructor]
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceDataSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ Parameters
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceMutual KwRange
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
pc [NiceConstructor]
_)        = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ Parameters
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [RecordDirective]
_ DefParameters
_ [Declaration]
_) = PositivityCheck
pc
        positivityCheckOldMutual NiceConstructor
_                              = 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 -> [NiceConstructor] -> Nice [NiceConstructor]
abstractBlock KwRange
r [NiceConstructor]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool))
-> ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> UpdaterT Nice [NiceConstructor]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
r [NiceConstructor]
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 -> [NiceConstructor] -> Nice [NiceConstructor]
privateBlock KwRange
r Origin
o [NiceConstructor]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool))
-> ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> UpdaterT Nice [NiceConstructor]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
r Origin
o [NiceConstructor]
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 -> [NiceConstructor] -> Nice [NiceConstructor]
instanceBlock KwRange
r [NiceConstructor]
ds = do
      let ([NiceConstructor]
ds', Bool
anyChange) = Change [NiceConstructor] -> ([NiceConstructor], Bool)
forall a. Change a -> (a, Bool)
runChange (Change [NiceConstructor] -> ([NiceConstructor], Bool))
-> Change [NiceConstructor] -> ([NiceConstructor], Bool)
forall a b. (a -> b) -> a -> b
$ (NiceConstructor -> ChangeT Identity NiceConstructor)
-> [NiceConstructor] -> Change [NiceConstructor]
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 -> NiceConstructor -> ChangeT Identity NiceConstructor
mkInstance KwRange
r) [NiceConstructor]
ds
      if Bool
anyChange then [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceConstructor]
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
        [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceConstructor]
ds -- no change!

    -- Make a declaration eligible for instance search.
    mkInstance ::
         KwRange  -- Range of @instance@ keyword.
      -> Updater NiceDeclaration
    mkInstance :: KwRange -> NiceConstructor -> ChangeT Identity NiceConstructor
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
-> NiceConstructor
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e) (IsInstance -> NiceConstructor)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceConstructor
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
-> NiceConstructor
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e) (IsInstance -> NiceConstructor)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceConstructor
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
-> NiceConstructor
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e) (IsInstance -> NiceConstructor)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceConstructor
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 [NiceConstructor]
ds       -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceConstructor]
-> NiceConstructor
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc ([NiceConstructor] -> NiceConstructor)
-> Change [NiceConstructor] -> ChangeT Identity NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceConstructor -> ChangeT Identity NiceConstructor)
-> [NiceConstructor] -> Change [NiceConstructor]
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 -> NiceConstructor -> ChangeT Identity NiceConstructor
mkInstance KwRange
r0) [NiceConstructor]
ds
        NiceLoneConstructor KwRange
r [NiceConstructor]
ds       -> KwRange -> [NiceConstructor] -> NiceConstructor
NiceLoneConstructor KwRange
r ([NiceConstructor] -> NiceConstructor)
-> Change [NiceConstructor] -> ChangeT Identity NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceConstructor -> ChangeT Identity NiceConstructor)
-> [NiceConstructor] -> Change [NiceConstructor]
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 -> NiceConstructor -> ChangeT Identity NiceConstructor
mkInstance KwRange
r0) [NiceConstructor]
ds
        d :: NiceConstructor
d@NiceFunClause{}              -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x List1 Clause
cs     -> (\ IsInstance
i -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> List1 Clause
-> NiceConstructor
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x List1 Clause
cs) (IsInstance -> NiceConstructor)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceConstructor
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 [NiceConstructor]
i              -> (\ [NiceConstructor]
i -> KwRange -> [QName] -> [NiceConstructor] -> NiceConstructor
NiceOpaque KwRange
r [QName]
ns [NiceConstructor]
i) ([NiceConstructor] -> NiceConstructor)
-> Change [NiceConstructor] -> ChangeT Identity NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceConstructor -> ChangeT Identity NiceConstructor)
-> [NiceConstructor] -> Change [NiceConstructor]
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 -> NiceConstructor -> ChangeT Identity NiceConstructor
mkInstance KwRange
r0) [NiceConstructor]
i
        d :: NiceConstructor
d@NiceField{}                  -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d  -- Field instance are handled by the parser
        d :: NiceConstructor
d@PrimitiveFunction{}          -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceUnquoteDef{}             -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceRecSig{}                 -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceDataSig{}                -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceModuleMacro{}            -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceModule{}                 -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NicePragma{}                 -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceOpen{}                   -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceImport{}                 -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceDataDef{}                -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceRecDef{}                 -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NicePatternSyn{}             -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceGeneralize{}             -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
        d :: NiceConstructor
d@NiceUnquoteData{}            -> NiceConstructor -> ChangeT Identity NiceConstructor
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
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 -> [NiceConstructor] -> Nice [NiceConstructor]
macroBlock KwRange
r [NiceConstructor]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool))
-> ChangeT Nice [NiceConstructor] -> Nice ([NiceConstructor], Bool)
forall a b. (a -> b) -> a -> b
$ UpdaterT Nice [NiceConstructor]
forall a. MakeMacro a => UpdaterT Nice a
mkMacro [NiceConstructor]
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 NiceConstructor
mkMacro = \case
    FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> UpdaterT Nice NiceConstructor
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceConstructor
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
MacroDef ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
    d :: NiceConstructor
d@FunDef{}                     -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    NiceConstructor
d                              -> Nice NiceConstructor -> ChangeT Nice NiceConstructor
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 NiceConstructor -> ChangeT Nice NiceConstructor)
-> Nice NiceConstructor -> ChangeT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice NiceConstructor
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice NiceConstructor)
-> DeclarationException' -> Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ NiceConstructor -> DeclarationException'
BadMacroDef NiceConstructor
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 NiceConstructor
mkAbstract KwRange
kwr = \case
    NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc [NiceConstructor]
ds      -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceConstructor]
-> NiceConstructor
NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceConstructor]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceConstructor]
ds
    NiceLoneConstructor KwRange
r [NiceConstructor]
ds             -> KwRange -> [NiceConstructor] -> NiceConstructor
NiceLoneConstructor KwRange
r ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceConstructor]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceConstructor]
ds
    FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x List1 Clause
cs           -> (\ IsAbstract
a -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> List1 Clause
-> NiceConstructor
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x) (IsAbstract -> List1 Clause -> NiceConstructor)
-> ChangeT Nice IsAbstract
-> ChangeT Nice (List1 Clause -> NiceConstructor)
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 (List1 Clause -> NiceConstructor)
-> ChangeT Nice (List1 Clause) -> ChangeT Nice NiceConstructor
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 (List1 Clause)
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr List1 Clause
cs
    NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x DefParameters
ps [NiceConstructor]
cs      -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> DefParameters
-> [NiceConstructor]
-> NiceConstructor
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x DefParameters
ps) (IsAbstract -> [NiceConstructor] -> NiceConstructor)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([NiceConstructor] -> NiceConstructor)
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 ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
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 [NiceConstructor]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceConstructor]
cs
    NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir DefParameters
ps [Declaration]
cs   -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> DefParameters
-> [Declaration]
-> NiceConstructor
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir DefParameters
ps [Declaration]
cs) (IsAbstract -> NiceConstructor)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d) (IsAbstract -> NiceConstructor)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceConstructor
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 NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceConstructor
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 NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceConstructor
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 Parameters
ls Expr
t    -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
NiceRecSig     Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x Parameters
ls Expr
t
    NiceDataSig Range
r Erased
er Access
p IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x Parameters
ls Expr
t    -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
NiceDataSig    Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x Parameters
ls Expr
t
    NiceField Range
r Access
p IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
e            -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceConstructor
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 NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceConstructor -> UpdaterT Nice NiceConstructor
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceConstructor
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 NiceConstructor
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceConstructor
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 NiceConstructor
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceConstructor
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 NiceConstructor
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [Name]
-> Expr
-> NiceConstructor
NiceUnquoteData Range
r Access
p IsAbstract
AbstractDef PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e
    d :: NiceConstructor
d@NiceModule{}                       -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    d :: NiceConstructor
d@NiceModuleMacro{}                  -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    d :: NiceConstructor
d@NicePragma{}                       -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    d :: NiceConstructor
d@NiceOpen{}                         -> NiceConstructor
d NiceConstructor -> ChangeT Nice () -> ChangeT Nice NiceConstructor
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 (NiceConstructor -> Range
forall a. HasRange a => a -> Range
getRange NiceConstructor
d) KwRange
kwr OpenOrImport
OpenNotImport
    d :: NiceConstructor
d@NiceImport{}                       -> NiceConstructor
d NiceConstructor -> ChangeT Nice () -> ChangeT Nice NiceConstructor
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 (NiceConstructor -> Range
forall a. HasRange a => a -> Range
getRange NiceConstructor
d) KwRange
kwr OpenOrImport
ImportMayOpen
    d :: NiceConstructor
d@NicePatternSyn{}                   -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    d :: NiceConstructor
d@NiceGeneralize{}                   -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
    NiceOpaque KwRange
r [QName]
ns [NiceConstructor]
ds                   -> KwRange -> [QName] -> [NiceConstructor] -> NiceConstructor
NiceOpaque KwRange
r [QName]
ns ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> UpdaterT Nice [NiceConstructor]
forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
mkAbstract KwRange
kwr [NiceConstructor]
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 NiceConstructor
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
-> NiceConstructor
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e)                (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e)            (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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 -> NiceConstructor
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e)          (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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 [NiceConstructor]
ds                 -> (\ [NiceConstructor]
ds-> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceConstructor]
-> NiceConstructor
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceConstructor]
ds)             ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceConstructor]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceConstructor]
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]
-> NiceConstructor
NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds)          (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is)     (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e)       (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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 Parameters
ls Expr
t         -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x Parameters
ls Expr
t)     (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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 Parameters
ls Expr
t        -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> Parameters
-> Expr
-> NiceConstructor
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x Parameters
ls Expr
t)    (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Catchall
catchall Declaration
d) (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)    (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)       (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p')           (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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
-> NiceConstructor
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t)         (Access -> NiceConstructor)
-> ChangeT Nice Access -> ChangeT Nice NiceConstructor
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 [NiceConstructor]
ds                       -> (\ [NiceConstructor]
p -> KwRange -> [QName] -> [NiceConstructor] -> NiceConstructor
NiceOpaque KwRange
r [QName]
ns [NiceConstructor]
p)                    ([NiceConstructor] -> NiceConstructor)
-> ChangeT Nice [NiceConstructor] -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceConstructor]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceConstructor]
ds
      d :: NiceConstructor
d@NicePragma{}                           -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
      d :: NiceConstructor
d@(NiceOpen Range
r QName
_x ImportDirective
dir)                    -> NiceConstructor
d NiceConstructor -> ChangeT Nice () -> ChangeT Nice NiceConstructor
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 :: NiceConstructor
d@(NiceImport Ranged OpenShortHand
opn KwRange
impR QName
x Either AsName RawOpenArgs
args ImportDirective
dir)       -> NiceConstructor
d NiceConstructor -> ChangeT Nice () -> ChangeT Nice NiceConstructor
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 ((Ranged OpenShortHand, KwRange, QName, Either AsName RawOpenArgs,
 ImportDirective)
-> Range
forall a. HasRange a => a -> Range
getRange (Ranged OpenShortHand
opn, KwRange
impR, QName
x, Either AsName RawOpenArgs
args, ImportDirective
dir)) 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 List1 Clause
cls              -> Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> List1 Clause
-> NiceConstructor
FunDef Range
r List1 Declaration
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x (List1 Clause -> NiceConstructor)
-> ChangeT Nice (List1 Clause) -> ChangeT Nice NiceConstructor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice (List1 Clause)
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o List1 Clause
cls
      d :: NiceConstructor
d@NiceLoneConstructor{}                  -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d -- Issue #7998: constructors cannot be private
      d :: NiceConstructor
d@NiceDataDef{}                          -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
      d :: NiceConstructor
d@NiceRecDef{}                           -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
d
      d :: NiceConstructor
d@NiceUnquoteData{}                      -> UpdaterT Nice NiceConstructor
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceConstructor
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

-- | Check data/record definition parameters for parts that are not allowed
--   (allowed if at all in data/record signatures).
niceDefParameters :: DataOrRecord_ -> Parameters -> Nice DefParameters
niceDefParameters :: DataOrRecord_ -> Parameters -> Nice DefParameters
niceDefParameters DataOrRecord_
dataOrRec = (LamBinding -> Nice DefParameters)
-> Parameters -> Nice DefParameters
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM \case
    DomainFree NamedArg Binder
x ->
      WithHiding (Named_ Name) -> DefParameters
forall el coll. Singleton el coll => el -> coll
singleton (WithHiding (Named_ Name) -> DefParameters)
-> Nice (WithHiding (Named_ Name)) -> Nice DefParameters
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Binder -> Nice (WithHiding (Named_ Name))
strip NamedArg Binder
x
    DomainFull (TBind Range
_r List1 (NamedArg Binder)
xs Expr
a) -> do
      Expr -> Text -> Nice ()
forall a. HasRange a => a -> Text -> Nice ()
warn Expr
a Text
"parameter type"
      (NamedArg Binder -> Nice (WithHiding (Named_ Name)))
-> [NamedArg Binder] -> Nice DefParameters
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 NamedArg Binder -> Nice (WithHiding (Named_ Name))
strip ([NamedArg Binder] -> Nice DefParameters)
-> [NamedArg Binder] -> Nice DefParameters
forall a b. (a -> b) -> a -> b
$ List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (NamedArg Binder)
xs
    DomainFull (TLet Range
r List1 Declaration
_ds) ->
      [] DefParameters -> Nice () -> Nice DefParameters
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Range -> Text -> Nice ()
forall a. HasRange a => a -> Text -> Nice ()
warn Range
r Text
"parameter `let'"
  where
    warn  :: HasRange a => a -> Text -> Nice ()
    warn :: forall a. HasRange a => a -> Text -> Nice ()
warn a
a Text
what = HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$
      Range -> DataOrRecord_ -> Text -> Text -> DeclarationWarning'
InvalidDataOrRecDefParameter (a -> Range
forall a. HasRange a => a -> Range
getRange a
a) DataOrRecord_
dataOrRec Text
what (Text -> DeclarationWarning') -> Text -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$
      Text
"(note: parameters may not repeat information from signature)"

    strip :: NamedArg Binder -> Nice (WithHiding (Named_ Name))
    strip :: NamedArg Binder -> Nice (WithHiding (Named_ Name))
strip (Arg (ArgInfo Hiding
h Modality
m Origin
_o FreeVariables
_fv Annotation
ann) (Named Maybe (WithOrigin (Ranged String))
mn (Binder Maybe Pattern
mp BinderNameOrigin
_bo (BName Name
x Fixity'
fx TacticAttribute
tac Bool
_)))) =
      Hiding -> Named_ Name -> WithHiding (Named_ Name)
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
h (Maybe (WithOrigin (Ranged String)) -> Name -> Named_ Name
forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged String))
mn Name
x) WithHiding (Named_ Name)
-> Nice () -> Nice (WithHiding (Named_ Name))
forall a b. a -> Nice b -> Nice a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Modality -> Bool
forall a. Null a => a -> Bool
null Modality
m)   (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ Modality -> Text -> Nice ()
forall a. HasRange a => a -> Text -> Nice ()
warn Modality
m   Text
"parameter modality"
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Annotation -> Bool
forall a. Null a => a -> Bool
null Annotation
ann) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ Annotation -> Text -> Nice ()
forall a. HasRange a => a -> Text -> Nice ()
warn Annotation
ann Text
"parameter annotation"
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Maybe Pattern -> Bool
forall a. Null a => a -> Bool
null Maybe Pattern
mp)  (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ Maybe Pattern -> Text -> Nice ()
forall a. HasRange a => a -> Text -> Nice ()
warn Maybe Pattern
mp  Text
"pattern attacted to parameter"
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Fixity' -> Bool
forall a. Null a => a -> Bool
null Fixity'
fx)  (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (TacticAttribute -> Bool
forall a. Null a => a -> Bool
null TacticAttribute
tac) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- warn tac "tactic (you should not see this, please report a bug)"

-- | Emit bits attached to the given name
--   that have been accumulated during processing of the interleaved mutual block
--   as 'NiceDeclaration'.
--
--   Warns about mistakes in parameters in data definition blocks;
--   but those parameters are finally ignored, taking the parameters of
--   the data signature instead.
interleavedDecl :: Name -> InterleavedDecl -> Nice [(DeclNum, NiceDeclaration)]
interleavedDecl :: Name -> InterleavedDecl -> Nice [(Int, NiceConstructor)]
interleavedDecl Name
k = \case

  InterleavedData Int
i d :: NiceConstructor
d@(NiceDataSig Range
_ Erased
_ Access
_acc IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
_ Parameters
pars Expr
_) Maybe (Int, List1 (DefParameters, [NiceConstructor]))
ds -> do
    let
      fpars :: DefParameters
fpars   = Parameters -> DefParameters
parametersToDefParameters Parameters
pars
      r :: Range
r       = (Name, DefParameters) -> Range
forall a. HasRange a => a -> Range
getRange (Name
k, DefParameters
fpars)
      ddef :: [NiceConstructor] -> NiceConstructor
ddef [NiceConstructor]
cs = Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> DefParameters
-> [NiceConstructor]
-> NiceConstructor
NiceDataDef ((Range, [NiceConstructor]) -> Range
forall a. HasRange a => a -> Range
getRange (Range
r, [NiceConstructor]
cs)) Origin
UserWritten IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
k DefParameters
fpars [NiceConstructor]
cs
    case Maybe (Int, List1 (DefParameters, [NiceConstructor]))
ds of
      Maybe (Int, List1 (DefParameters, [NiceConstructor]))
Nothing -> [(Int, NiceConstructor)] -> Nice [(Int, NiceConstructor)]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
i, NiceConstructor
d)]  -- signature only
      Just (Int
j, List1 (DefParameters, [NiceConstructor])
dds) -> do
        dds' <- List1 (DefParameters, [NiceConstructor])
-> ((DefParameters, [NiceConstructor]) -> Nice [NiceConstructor])
-> Nice (NonEmpty [NiceConstructor])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (List1 (DefParameters, [NiceConstructor])
-> List1 (DefParameters, [NiceConstructor])
forall a. NonEmpty a -> NonEmpty a
List1.reverse List1 (DefParameters, [NiceConstructor])
dds) \ (DefParameters
defpars, [NiceConstructor]
cs) -> do
          Bool -> Nice () -> Nice ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (DefParameters -> Bool
forall a. Null a => a -> Bool
null DefParameters
defpars Bool -> Bool -> Bool
|| DefParameters
defpars DefParameters -> DefParameters -> Bool
forall a. Eq a => a -> a -> Bool
== DefParameters
fpars) (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 -> DataOrRecord_ -> Text -> Text -> DeclarationWarning'
InvalidDataOrRecDefParameter (DefParameters -> Range
forall a. HasRange a => a -> Range
getRange DefParameters
defpars) DataOrRecord_
forall p. DataOrRecord' p
IsData Text
"parameter names" (Text -> DeclarationWarning') -> Text -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$
            Text
"(in `interleaved mutual' blocks, parameters of a data definition must either be omitted or match exactly the parameters given in the data signature)"
          [NiceConstructor] -> Nice [NiceConstructor]
forall a. a -> Nice a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [NiceConstructor]
cs
        return [(i, d), (j, ddef $ sconcat dds')]

  InterleavedFun Int
i d :: NiceConstructor
d@(FunSig Range
r Access
_acc IsAbstract
abs IsInstance
inst IsMacro
_mac ArgInfo
_info TerminationCheck
tc CoverageCheck
cc Name
n Expr
_e) Maybe (Int, List1 (List1 Declaration, List1 Clause))
dcs -> do
    let
      fdef :: List1 (List1 Declaration, List1 Clause) -> NiceConstructor
fdef List1 (List1 Declaration, List1 Clause)
dcss = Range
-> List1 Declaration
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> List1 Clause
-> NiceConstructor
FunDef Range
r (NonEmpty (List1 Declaration) -> List1 Declaration
forall a. Semigroup a => NonEmpty a -> a
sconcat NonEmpty (List1 Declaration)
dss) IsAbstract
abs IsInstance
inst TerminationCheck
tc CoverageCheck
cc Name
n (NonEmpty (List1 Clause) -> List1 Clause
forall a. Semigroup a => NonEmpty a -> a
sconcat NonEmpty (List1 Clause)
css)
        where (NonEmpty (List1 Declaration)
dss, NonEmpty (List1 Clause)
css) = List1 (List1 Declaration, List1 Clause)
-> (NonEmpty (List1 Declaration), NonEmpty (List1 Clause))
forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
List1.unzip (List1 (List1 Declaration, List1 Clause)
 -> (NonEmpty (List1 Declaration), NonEmpty (List1 Clause)))
-> List1 (List1 Declaration, List1 Clause)
-> (NonEmpty (List1 Declaration), NonEmpty (List1 Clause))
forall a b. (a -> b) -> a -> b
$ List1 (List1 Declaration, List1 Clause)
-> List1 (List1 Declaration, List1 Clause)
forall a. NonEmpty a -> NonEmpty a
List1.reverse List1 (List1 Declaration, List1 Clause)
dcss
    [(Int, NiceConstructor)] -> Nice [(Int, NiceConstructor)]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, NiceConstructor)] -> Nice [(Int, NiceConstructor)])
-> (Maybe (Int, NiceConstructor) -> [(Int, NiceConstructor)])
-> Maybe (Int, NiceConstructor)
-> Nice [(Int, NiceConstructor)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int
i,NiceConstructor
d) (Int, NiceConstructor)
-> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceConstructor)] -> [(Int, NiceConstructor)])
-> (Maybe (Int, NiceConstructor) -> [(Int, NiceConstructor)])
-> Maybe (Int, NiceConstructor)
-> [(Int, NiceConstructor)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Int, NiceConstructor) -> [(Int, NiceConstructor)]
forall a. Maybe a -> [a]
maybeToList (Maybe (Int, NiceConstructor) -> Nice [(Int, NiceConstructor)])
-> Maybe (Int, NiceConstructor) -> Nice [(Int, NiceConstructor)]
forall a b. (a -> b) -> a -> b
$ ((Int, List1 (List1 Declaration, List1 Clause))
 -> (Int, NiceConstructor))
-> Maybe (Int, List1 (List1 Declaration, List1 Clause))
-> Maybe (Int, NiceConstructor)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((List1 (List1 Declaration, List1 Clause) -> NiceConstructor)
-> (Int, List1 (List1 Declaration, List1 Clause))
-> (Int, NiceConstructor)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second List1 (List1 Declaration, List1 Clause) -> NiceConstructor
fdef) Maybe (Int, List1 (List1 Declaration, List1 Clause))
dcs

  InterleavedDecl
_ -> Nice [(Int, NiceConstructor)]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- someone messed up and broke the invariant

-- | 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 :: NiceConstructor -> 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
_ [NiceConstructor]
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
$ (NiceConstructor -> List1 Declaration)
-> [NiceConstructor] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceConstructor -> List1 Declaration
notSoNiceDeclarations [NiceConstructor]
ds
    NiceLoneConstructor KwRange
r [NiceConstructor]
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
$ (NiceConstructor -> List1 Declaration)
-> [NiceConstructor] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceConstructor -> List1 Declaration
notSoNiceDeclarations [NiceConstructor]
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 Ranged OpenShortHand
o KwRange
r QName
x Either AsName RawOpenArgs
as 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
$ Ranged OpenShortHand
-> KwRange
-> QName
-> Either AsName RawOpenArgs
-> ImportDirective
-> Declaration
Import Ranged OpenShortHand
o KwRange
r QName
x Either AsName RawOpenArgs
as 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 Parameters
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 -> Parameters -> Expr -> Declaration
RecordSig Range
r Erased
er Name
x Parameters
bs Expr
e
    NiceDataSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x Parameters
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 -> Parameters -> Expr -> Declaration
DataSig Range
r Erased
er Name
x Parameters
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
_ List1 Clause
_          -> List1 Declaration
ds
    NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x DefParameters
bs [NiceConstructor]
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 -> Parameters -> [Declaration] -> Declaration
DataDef Range
r Name
x (DefParameters -> Parameters
defParametersToParameters DefParameters
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
$ (NiceConstructor -> List1 Declaration)
-> [NiceConstructor] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceConstructor -> List1 Declaration
notSoNiceDeclarations [NiceConstructor]
cs
    NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [RecordDirective]
dir DefParameters
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]
-> Parameters
-> [Declaration]
-> Declaration
RecordDef Range
r Name
x [RecordDirective]
dir (DefParameters -> Parameters
defParametersToParameters DefParameters
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 [NiceConstructor]
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
$ (NiceConstructor -> List1 Declaration)
-> [NiceConstructor] -> [List1 Declaration]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NiceConstructor -> List1 Declaration
notSoNiceDeclarations [NiceConstructor]
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 :: NiceConstructor -> 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
_ List1 Clause
_        -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceDataDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ DefParameters
_ [NiceConstructor]
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceRecDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [RecordDirective]
_ DefParameters
_ [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