-- | 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.


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         ( forM, guard, unless, void, when )
import Control.Monad.Except  ( )
import Control.Monad.Reader  ( asks )
import Control.Monad.State   ( MonadState(..), gets, StateT, runStateT )
import Control.Monad.Trans   ( lift )

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

import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Common hiding (TerminationCheck())
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Position
import Agda.Syntax.Notation
import Agda.Syntax.Concrete.Pretty () --instance only
import Agda.Syntax.Concrete.Fixity
import Agda.Syntax.Common.Pretty

import Agda.Syntax.Concrete.Definitions.Errors
import Agda.Syntax.Concrete.Definitions.Monad
import Agda.Syntax.Concrete.Definitions.Types

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

import Agda.Utils.Impossible

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

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

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

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

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

declKind :: NiceDeclaration -> DeclKind
declKind :: NiceDeclaration -> DeclKind
declKind (FunSig Range
r Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
tc CoverageCheck
cc Name
x Expr
_)      = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) Name
x
declKind (NiceRecSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_)    = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (NiceDataSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
_ Expr
_)   = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (FunDef Range
r [Declaration]
_ IsAbstract
abs IsInstance
ins TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
_)      = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) [Name
x]
declKind (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
pars [NiceDeclaration]
_)  = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceUnquoteData Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [Name]
_ Expr
_) = DataRecOrFun -> [Name] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Name
x]
declKind (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
_ [LamBinding]
pars [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 (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName 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 Axioms for postulated names
--   The first argument is a list of axioms only.
replaceSigs
  :: LoneSigs               -- ^ Lone signatures to be turned into Axioms
  -> [NiceDeclaration]      -- ^ Declarations containing them
  -> [NiceDeclaration]      -- ^ In the output, everything should be defined
replaceSigs :: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps = if LoneSigs -> Bool
forall k a. Map k a -> Bool
Map.null LoneSigs
ps then [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> a
id else \case
  []     -> [NiceDeclaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
  (NiceDeclaration
d:[NiceDeclaration]
ds) ->
    case NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable NiceDeclaration
d of
      -- If declaration d of x is mentioned in the map of lone signatures then replace
      -- it with an axiom
      Just (Name
x, NiceDeclaration
axiom)
        | (Just (LoneSig Range
_ Name
x' DataRecOrFun
_), LoneSigs
ps') <- (Name -> LoneSig -> Maybe LoneSig)
-> Name -> LoneSigs -> (Maybe LoneSig, LoneSigs)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\ Name
_ LoneSig
_ -> Maybe LoneSig
forall a. Maybe a
Nothing) Name
x LoneSigs
ps
        , Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x'
            -- Use the range as UID to ensure we do not replace the wrong signature.
            -- This could happen if the user wrote a duplicate definition.
        -> NiceDeclaration
axiom NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps' [NiceDeclaration]
ds
      Maybe (Name, NiceDeclaration)
_ -> NiceDeclaration
d     NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps  [NiceDeclaration]
ds

  where

    -- A @replaceable@ declaration is a signature. It has a name and we can make an
    -- @Axiom@ out of it.
    replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
    replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
replaceable = \case
      FunSig Range
r Access
acc IsAbstract
abst IsInstance
inst IsMacro
_ ArgInfo
argi TerminationCheck
_ CoverageCheck
_ Name
x' Expr
e ->
        -- #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' in
        (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
inst ArgInfo
argi Name
x' Expr
e)
      NiceRecSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef
                   (Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (Erased -> Quantity
asQuantity Erased
erased) ArgInfo
defaultArgInfo) Name
x Expr
e)
      NiceDataSig Range
r Erased
erased Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
forall a. a -> Maybe a
Just (Name
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef
                   (Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (Erased -> Quantity
asQuantity Erased
erased) ArgInfo
defaultArgInfo) Name
x Expr
e)
      NiceDeclaration
_ -> Maybe (Name, NiceDeclaration)
forall a. Maybe a
Nothing

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

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

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

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

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

  where

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

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

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

      case Declaration
d of

        TypeSig ArgInfo
info TacticAttribute
_tac Name
x Expr
t -> do
          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 termCheck covCheck
          return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x' t] , ds)

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

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

        (FunClause LHS
lhs RHS
_ WhereClause
_ Bool
_)         -> 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 (fits, rest) =
                      -- Anonymous declarations only have 1 clause each!
                      if isNoName x then ([d], ds)
                      else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
               , not (null fits)
               ] 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
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
defaultArgInfo) TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
forall a. Maybe a
Nothing [Declaration
d] -- fun def without type signature is relevant
                return (d , ds)
              -- Subcase: The lhs is a proper pattern.
              -- This could be a let-pattern binding. Pass it on.
              -- A missing type signature error might be raise in ConcreteToAbstract
              LHS
_ -> do
                ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef TerminationCheck
termCheck CoverageCheck
covCheck Bool
catchall Declaration
d] , [Declaration]
ds)

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

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

        Field KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyField KwRange
r
        Field KwRange
_ [Declaration]
fs -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
FieldBlock [Declaration]
fs

        DataSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
          pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
          uc <- use universeCheckPragma
          _ <- addLoneSig r x $ DataName pc uc
          (,ds) <$> dataOrRec pc uc NiceDataDef
                      (flip NiceDataSig erased) (niceAxioms DataBlock) r
                      x (Just (tel, t)) Nothing

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

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

        RecordSig Range
r Erased
erased Name
x [LamBinding]
tel Expr
t -> do
          pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
          uc <- use universeCheckPragma
          _ <- addLoneSig r x $ RecName pc uc
          return ( [NiceRecSig r erased PublicAccess ConcreteDef pc uc x
                      tel t]
                 , ds
                 )

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

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

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

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

        LoneConstructor KwRange
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyConstructor KwRange
r
        LoneConstructor KwRange
r [Declaration]
ds' ->
          ((,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> ([NiceDeclaration] -> [NiceDeclaration])
-> [NiceDeclaration]
-> ([NiceDeclaration], [Declaration])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> ([NiceDeclaration] -> NiceDeclaration)
-> [NiceDeclaration]
-> [NiceDeclaration]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
ConstructorBlock [Declaration]
ds'


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

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

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

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

        Postulate KwRange
r []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPostulate KwRange
r
        Postulate KwRange
_ [Declaration]
ds' ->
          (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PostulateBlock [Declaration]
ds'

        Primitive KwRange
r []  -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ KwRange -> DeclarationWarning'
EmptyPrimitive KwRange
r
        Primitive KwRange
_ [Declaration]
ds' -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NiceDeclaration -> NiceDeclaration)
-> [NiceDeclaration] -> [NiceDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> NiceDeclaration
toPrim ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
PrimitiveBlock [Declaration]
ds')

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

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

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

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

        UnquoteDecl Range
r [Name]
xs Expr
e -> do
          tc <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (TerminationCheck -> f TerminationCheck)
-> NiceState -> f NiceState
Lens' NiceState TerminationCheck
terminationCheckPragma
          cc <- use coverageCheckPragma
          return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds)

        UnquoteDef Range
r [Name]
xs Expr
e -> do
          sigs <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)] -> [Name])
-> (LoneSigs -> [(Name, Name)]) -> LoneSigs -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoneSigs -> [(Name, Name)]
loneFuns (LoneSigs -> [Name]) -> Nice LoneSigs -> Nice [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' NiceState LoneSigs -> Nice LoneSigs
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
Lens' NiceState LoneSigs
loneSigs
          List1.ifNotNull (filter (`notElem` sigs) xs)
            {-then-} (declarationException . UnquoteDefRequiresSignature)
            {-else-} $ do
              mapM_ removeLoneSig xs
              return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds)

        UnquoteData Range
r Name
xs [Name]
cs Expr
e -> do
          pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
Lens' NiceState PositivityCheck
positivityCheckPragma
          uc <- use universeCheckPragma
          return ([NiceUnquoteData r PublicAccess ConcreteDef pc uc xs cs e], ds)

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

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

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

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

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

    nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])

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

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

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

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

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

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

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

    nicePragma p :: Pragma
p@CompilePragma{} [Declaration]
ds = do
      ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)

    nicePragma (PolarityPragma{}) [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)

    nicePragma (BuiltinPragma Range
r RString
str qn :: QName
qn@(QName Name
x)) [Declaration]
ds = do
      ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma Range
r (Range -> RString -> QName -> Pragma
BuiltinPragma Range
r RString
str QName
qn)], [Declaration]
ds)

    nicePragma p :: Pragma
p@RewritePragma{} [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)
    nicePragma Pragma
p [Declaration]
ds = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)

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

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

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

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

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

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

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

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

    dataOrRec
      :: forall a decl
      .  PositivityCheck
      -> UniverseCheck
      -> (Range -> Origin -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> [decl] -> NiceDeclaration)
         -- Construct definition.
      -> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration)
         -- Construct signature.
      -> ([a] -> Nice [decl])        -- Constructor checking.
      -> Range
      -> Name                        -- Data/record type name.
      -> Maybe ([LamBinding], Expr)  -- Parameters and type.  If not @Nothing@ a signature is created.
      -> Maybe ([LamBinding], [a])   -- Parameters and constructors.  If not @Nothing@, a definition body is created.
      -> Nice [NiceDeclaration]
    dataOrRec :: forall a decl.
PositivityCheck
-> UniverseCheck
-> (Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [decl]
    -> NiceDeclaration)
-> (Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration)
-> ([a] -> Nice [decl])
-> Range
-> Name
-> Maybe ([LamBinding], Expr)
-> Maybe ([LamBinding], [a])
-> Nice [NiceDeclaration]
dataOrRec PositivityCheck
pc UniverseCheck
uc Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig [a] -> Nice [decl]
niceD Range
r Name
x Maybe ([LamBinding], Expr)
mt Maybe ([LamBinding], [a])
mcs = do
      mds <- Maybe ([LamBinding], [a])
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe ([LamBinding], [a])
mcs ((([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
 -> Nice (Maybe ([LamBinding], [decl])))
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall a b. (a -> b) -> a -> b
$ \ ([LamBinding]
tel, [a]
cs) -> ([LamBinding]
tel,) ([decl] -> ([LamBinding], [decl]))
-> Nice [decl] -> Nice ([LamBinding], [decl])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Nice [decl]
niceD [a]
cs
      -- We set origin to UserWritten if the user split the data/rec herself,
      -- and to Inserted if the she wrote a single declaration that we're
      -- splitting up here. We distinguish these because the scoping rules for
      -- generalizable variables differ in these cases.
      let o | Maybe ([LamBinding], Expr) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], Expr)
mt Bool -> Bool -> Bool
&& Maybe ([LamBinding], [a]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], [a])
mcs = Origin
Inserted
            | Bool
otherwise               = Origin
UserWritten
      return $ catMaybes $
        [ mt  <&> \ ([LamBinding]
tel, Expr
t)  -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig (Name -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Expr
t) Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel Expr
t
        , mds <&> \ ([LamBinding]
tel, [decl]
ds) -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
r Origin
o IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x (Maybe ([LamBinding], Expr)
-> [LamBinding]
-> (([LamBinding], Expr) -> [LamBinding])
-> [LamBinding]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ([LamBinding], Expr)
mt [LamBinding]
tel ((([LamBinding], Expr) -> [LamBinding]) -> [LamBinding])
-> (([LamBinding], Expr) -> [LamBinding]) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. a -> b -> a
const ([LamBinding] -> ([LamBinding], Expr) -> [LamBinding])
-> [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
tel) [decl]
ds
          -- If a type is given (mt /= Nothing), we have to delete the types in @tel@
          -- for the data definition, lest we duplicate them. And also drop modalities (#1886).
        ]
    -- Translate axioms
    niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
    niceAxioms :: KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds = [[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[NiceDeclaration]] -> [NiceDeclaration])
-> Nice [[NiceDeclaration]] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> Nice [NiceDeclaration])
-> [Declaration] -> Nice [[NiceDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (KindOfBlock -> Declaration -> Nice [NiceDeclaration]
niceAxiom KindOfBlock
b) [Declaration]
ds

    niceAxiom :: KindOfBlock -> TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
    niceAxiom :: KindOfBlock -> Declaration -> Nice [NiceDeclaration]
niceAxiom KindOfBlock
b = \case
      d :: Declaration
d@(TypeSig ArgInfo
rel TacticAttribute
_tac Name
x Expr
t) -> do
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef ArgInfo
rel Name
x Expr
t ]
      d :: Declaration
d@(FieldSig IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt) | KindOfBlock
b KindOfBlock -> KindOfBlock -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfBlock
FieldBlock -> do
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt ]
      InstanceB KwRange
r [Declaration]
decls -> do
        KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock KwRange
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
InstanceBlock [Declaration]
decls
      Private KwRange
r Origin
o [Declaration]
decls | KindOfBlock
PostulateBlock <- KindOfBlock
b -> do
        KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
decls
      Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
      Pragma p :: Pragma
p@(OverlapPragma Range
r [QName]
_ OverlapMode
_) -> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
      Declaration
d -> DeclarationException' -> Nice [NiceDeclaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [NiceDeclaration])
-> DeclarationException' -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
b (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d

    toPrim :: NiceDeclaration -> NiceDeclaration
    toPrim :: NiceDeclaration -> NiceDeclaration
toPrim (Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
t) = Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x (ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
rel Expr
t)
    toPrim NiceDeclaration
_                       = NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Create a function definition.
    mkFunDef :: ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Maybe Expr
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x Maybe Expr
mt [Declaration]
ds0 = do
      ds <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds0
      cs <- mkClauses x ds False
      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


    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 (d :: Declaration
d@(FunClause lhs :: LHS
lhs@(LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) : [Declaration]
ds)
      | Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p = (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
<$> [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds
      | Bool
otherwise     = (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 (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 (LHS Pattern
p0 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Bool
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' = LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
LHS Pattern
p1 [RewriteEqn]
eqs [WithExpr]
es) RHS
rhs WhereClause
wh Bool
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__
    expandEllipsis [Declaration]
_ = Nice [Declaration]
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Turn function clauses into nice function clauses.
    mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses :: Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
_ [] Bool
_ = [Clause] -> Nice [Clause]
forall a. a -> Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    mkClauses Name
x (Pragma (CatchallPragma Range
r) : [Declaration]
cs) Bool
True  = do
      HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidCatchallPragma Range
r
      Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
True
    mkClauses Name
x (Pragma (CatchallPragma Range
r) : [Declaration]
cs) Bool
False = do
      Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Declaration] -> Bool
forall a. Null a => a -> Bool
null [Declaration]
cs) (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
      Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
True

    mkClauses Name
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
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  =
      (Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x (Bool
ca Bool -> Bool -> Bool
|| Bool
catchall) LHS
lhs RHS
rhs WhereClause
wh [] Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
:) ([Clause] -> [Clause]) -> Nice [Clause] -> Nice [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs Bool
False   -- Will result in an error later.

    mkClauses Name
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
catchall = do
      Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Declaration] -> Bool
forall a. Null a => a -> Bool
null [Declaration]
withClauses) (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 -> LHS -> DeclarationException'
MissingWithClauses Name
x LHS
lhs
      wcs <- Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
withClauses Bool
False
      (Clause x (ca || catchall) lhs rhs wh wcs :) <$> mkClauses x cs' False
      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 (LHS Pattern
p0 [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) : [Declaration]
cs)
         | Pattern -> Bool
forall a. IsEllipsis a => a -> Bool
isEllipsis Pattern
p0 Bool -> Bool -> Bool
||
           Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
numWith = ([Declaration] -> [Declaration])
-> ([Declaration], [Declaration]) -> ([Declaration], [Declaration])
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:) ([Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs)
         | Bool
otherwise                           = ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs)
        subClauses (c :: Declaration
c@(Pragma (CatchallPragma Range
r)) : [Declaration]
cs) = case [Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs of
          ([], [Declaration]
cs') -> ([], Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs')
          ([Declaration]
cs, [Declaration]
cs') -> (Declaration
cDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:[Declaration]
cs, [Declaration]
cs')
        subClauses [] = ([],[])
        subClauses [Declaration]
_  = ([Declaration], [Declaration])
forall a. HasCallStack => a
__IMPOSSIBLE__
    mkClauses Name
_ [Declaration]
_ Bool
_ = Nice [Clause]
forall a. HasCallStack => a
__IMPOSSIBLE__

    couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Name
x Pattern
p =
      let
      pns :: [Name]
pns        = Pattern -> [Name]
patternNames 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]
pns
      in
--          trace ("x = " ++ prettyShow x) $
--          trace ("pns = " ++ show pns) $
--          trace ("xStrings = " ++ show xStrings) $
--          trace ("patStrings = " ++ show patStrings) $
--          trace ("mFixity = " ++ show mFixity) $
      case ([Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe [Name]
pns, Maybe Fixity'
mFixity) of
        -- first identifier in the patterns is the fun.symbol?
        (Just Name
y, Maybe Fixity'
_) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y -> Bool
True -- trace ("couldBe since y = " ++ prettyShow y) $ True
        -- are the parts of x contained in p
        (Maybe Name, Maybe Fixity')
_ | [String]
xStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` [String]
patStrings -> Bool
True -- trace ("couldBe since isSublistOf") $ True
        -- looking for a mixfix fun.symb
        (Maybe Name
_, 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
`isSublistOf` [String]
patStrings)
        -- not a notation, not first id: give up
        (Maybe Name, Maybe Fixity')
_ -> Bool
False -- trace ("couldBe not (case default)") $ False


    -- for finding nice clauses for a type sig in mutual blocks
    couldBeNiceFunClauseOf :: Maybe Fixity' -> Name -> NiceDeclaration
                           -> Maybe (MutualChecks, Declaration)
    couldBeNiceFunClauseOf :: Maybe Fixity'
-> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf Maybe Fixity'
mf Name
n (NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Bool
_ 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 (f :: * -> *). Alternative f => Bool -> f ()
guard (Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mf Name
n Declaration
d)
    couldBeNiceFunClauseOf Maybe Fixity'
_ Name
_ NiceDeclaration
_ = Maybe (MutualChecks, Declaration)
forall a. Maybe a
Nothing

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

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

      where

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

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

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

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

        addDataConstructors :: Maybe Range        -- Range of the `data A where` (if any)
                            -> Maybe Name         -- Data type the constructors belong to
                            -> [NiceConstructor]  -- Constructors to add
                            -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
        -- if we know the type's name, we can go ahead
        addDataConstructors :: Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
mr (Just Name
n) [NiceDeclaration]
ds = do
          (m, checks, i) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  (InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
          case Map.lookup n m of
            Just (InterleavedData Int
i0 NiceDeclaration
sig Maybe (Int, List1 [NiceDeclaration])
cs) -> do
              Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
-> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ Name -> Nice ()
removeLoneSig Name
n
              -- add the constructors to the existing ones (if any)
              let ((Int, List1 [NiceDeclaration])
cs', Int
i') = case Maybe (Int, List1 [NiceDeclaration])
cs of
                    Maybe (Int, List1 [NiceDeclaration])
Nothing        -> ((Int
i , [NiceDeclaration]
ds [NiceDeclaration] -> [[NiceDeclaration]] -> List1 [NiceDeclaration]
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    Just (Int
i1, List1 [NiceDeclaration]
ds1) -> ((Int
i1, [NiceDeclaration]
ds [NiceDeclaration]
-> List1 [NiceDeclaration] -> List1 [NiceDeclaration]
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 [NiceDeclaration]
ds1), Int
i)
              (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 [NiceDeclaration])
-> InterleavedDecl
InterleavedData Int
i0 NiceDeclaration
sig ((Int, List1 [NiceDeclaration])
-> Maybe (Int, List1 [NiceDeclaration])
forall a. a -> Maybe a
Just (Int, List1 [NiceDeclaration])
cs')) InterleavedMutual
m, MutualChecks
checks, Int
i')
            Maybe InterleavedDecl
_ -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
-> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> DeclarationWarning'
MissingDeclarations ([(Name, Range)] -> DeclarationWarning')
-> [(Name, Range)] -> DeclarationWarning'
forall a b. (a -> b) -> a -> b
$ case Maybe Range
mr of
                   Just Range
r -> [(Name
n, Range
r)]
                   Maybe Range
Nothing -> ((NiceDeclaration -> [(Name, Range)])
 -> [NiceDeclaration] -> [(Name, Range)])
-> [NiceDeclaration]
-> (NiceDeclaration -> [(Name, Range)])
-> [(Name, Range)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (NiceDeclaration -> [(Name, Range)])
-> [NiceDeclaration] -> [(Name, Range)]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [NiceDeclaration]
ds ((NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)])
-> (NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)]
forall a b. (a -> b) -> a -> b
$ \case
                     Axiom Range
r Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
_ -> [(Name
n, Range
r)]
                     NiceDeclaration
_ -> [(Name, Range)]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

        addFunDef :: NiceDeclaration -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
        addFunDef :: NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addFunDef (FunDef Range
_ [Declaration]
ds IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
cc Name
n [Clause]
cs) = do
          let check :: MutualChecks
check = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
          (m, checks, i) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  (InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
          case Map.lookup n m of
            Just (InterleavedFun Int
i0 NiceDeclaration
sig Maybe (Int, List1 ([Declaration], [Clause]))
cs0) -> do
              let ((Int, List1 ([Declaration], [Clause]))
cs', Int
i') = case Maybe (Int, List1 ([Declaration], [Clause]))
cs0 of
                    Maybe (Int, List1 ([Declaration], [Clause]))
Nothing        -> ((Int
i,  ([Declaration]
ds, [Clause]
cs) ([Declaration], [Clause])
-> [([Declaration], [Clause])] -> List1 ([Declaration], [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 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
ds, [Clause]
cs) ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
              (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 ([Declaration], [Clause]))
-> Maybe (Int, List1 ([Declaration], [Clause]))
forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
            Maybe InterleavedDecl
_ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- A FunDef always come after an existing FunSig!
        addFunDef NiceDeclaration
_ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

        addFunClauses ::
             KwRange
          -> [NiceDeclaration]
          -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
        addFunClauses :: KwRange
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
addFunClauses KwRange
r (nd :: NiceDeclaration
nd@(NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Bool
_ d :: Declaration
d@(FunClause LHS
lhs RHS
_ WhereClause
_ Bool
_)) : [NiceDeclaration]
ds) = do
          -- get the candidate functions that are in this interleaved mutual block
          (m, checks, i) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  (InterleavedMutual, MutualChecks, Int)
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 (fits, rest) = spanJust (couldBeNiceFunClauseOf (Map.lookup x fixs) x) (nd : ds)
               , not (null fits)
               ] 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] []
              (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
              ((Int
i,NiceDeclaration
nd) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks KwRange
r [NiceDeclaration]
ds
            -- exactly one candidate: attach the funclause to the definition
            [(Name
n, Prefix (MutualChecks, Declaration)
fits0, [NiceDeclaration]
rest)] -> do
              let ([MutualChecks]
checkss, [Declaration]
fits) = Prefix (MutualChecks, Declaration)
-> ([MutualChecks], [Declaration])
forall a b. [(a, b)] -> ([a], [b])
unzip Prefix (MutualChecks, Declaration)
fits0
              ds <- Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [Declaration]
 -> StateT
      (InterleavedMutual, MutualChecks, Int) Nice [Declaration])
-> Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
              cs <- lift $ mkClauses n ds False
              case Map.lookup n m of
                Just (InterleavedFun Int
i0 NiceDeclaration
sig Maybe (Int, List1 ([Declaration], [Clause]))
cs0) -> do
                  let ((Int, List1 ([Declaration], [Clause]))
cs', Int
i') = case Maybe (Int, List1 ([Declaration], [Clause]))
cs0 of
                        Maybe (Int, List1 ([Declaration], [Clause]))
Nothing        -> ((Int
i,  ([Declaration]
fits,[Clause]
cs) ([Declaration], [Clause])
-> [([Declaration], [Clause])] -> List1 ([Declaration], [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 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
fits,[Clause]
cs) ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
                  let checks' :: MutualChecks
checks' = [MutualChecks] -> MutualChecks
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [MutualChecks]
checkss
                  (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 ([Declaration], [Clause]))
-> Maybe (Int, List1 ([Declaration], [Clause]))
forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
checks' MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
                Maybe InterleavedDecl
_ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
              groupByBlocks r rest
            -- more than one candidate: fail, complaining about the ambiguity!
            (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf:[(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs -> Nice [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> Nice [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
                           (DeclarationException' -> Nice [(Int, NiceDeclaration)])
-> DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs
                           (List1 Name -> DeclarationException')
-> List1 Name -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Name -> List1 Name
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
forall a b. (a -> b) -> a -> b
$ ((Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
 -> Name)
-> NonEmpty
     (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Name
a,Prefix (MutualChecks, Declaration)
_,[NiceDeclaration]
_) -> Name
a) (NonEmpty
   (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
 -> List1 Name)
-> NonEmpty
     (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Name
forall a b. (a -> b) -> a -> b
$ (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
-> NonEmpty
     (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
forall a. a -> [a] -> NonEmpty a
:| [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs
        addFunClauses KwRange
_ [NiceDeclaration]
_ = StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

    privateBlock
      :: KwRange  -- Range of @private@ keyword.
      -> Origin   -- Origin of the private block.
      -> [NiceDeclaration]
      -> Nice [NiceDeclaration]
    privateBlock :: KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
privateBlock KwRange
r Origin
o [NiceDeclaration]
ds = do
      (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
-> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
r Origin
o [NiceDeclaration]
ds
      if anyChange then return ds' else do
        when (o == UserWritten) $ declarationWarning $ UselessPrivate r
        return ds -- no change!

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

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

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

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

class MakeMacro a where
  mkMacro :: UpdaterT Nice a

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

instance MakeMacro a => MakeMacro [a]

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

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

class MakeAbstract a where
  mkAbstract :: UpdaterT Nice a

  default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => UpdaterT Nice a
  mkAbstract = (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. MakeAbstract a => UpdaterT Nice a
mkAbstract

instance MakeAbstract a => MakeAbstract [a]

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

instance MakeAbstract IsAbstract where
  mkAbstract :: UpdaterT Nice IsAbstract
mkAbstract = \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 :: UpdaterT Nice NiceDeclaration
mkAbstract = \case
      NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds  -> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
      NiceLoneConstructor KwRange
r [NiceDeclaration]
ds         -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
      FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cs       -> (\ IsAbstract
a -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x) (IsAbstract -> [Clause] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([Clause] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [Clause]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [Clause]
cs
      NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps [NiceDeclaration]
cs  -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ps) (IsAbstract -> [NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall a b.
ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
cs
      NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [RecordDirective]
dir [LamBinding]
ps [Declaration]
cs) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a
      NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d  -> (\ IsAbstract
a -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract 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
a IsInstance
i ArgInfo
rel Name
x Expr
e          -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom             Range
r Access
p IsAbstract
AbstractDef IsInstance
i ArgInfo
rel Name
x Expr
e
      FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig            Range
r Access
p IsAbstract
AbstractDef IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e
      NiceRecSig  Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig  Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
      NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Erased
er Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
      NiceField Range
r Access
p IsAbstract
_ IsInstance
i TacticAttribute
tac Name
x Arg Expr
e      -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField         Range
r Access
p IsAbstract
AbstractDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
e
      PrimitiveFunction Range
r Access
p IsAbstract
_ Name
x Arg Expr
e    -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
AbstractDef Name
x Arg Expr
e
      -- Andreas, 2016-07-17 it does have effect on unquoted defs.
      -- Need to set updater state to dirty!
      NiceUnquoteDecl Range
r Access
p IsAbstract
_ IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
AbstractDef IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
      NiceUnquoteDef Range
r Access
p IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e    -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
AbstractDef TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e
      NiceUnquoteData Range
r Access
p IsAbstract
_ PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteData Range
r Access
p IsAbstract
AbstractDef PositivityCheck
tc UniverseCheck
cc Name
x [Name]
xs Expr
e
      d :: NiceDeclaration
d@NiceModule{}                 -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceModuleMacro{}            -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePragma{}                 -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        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
directives) ((KwRange -> ChangeT Nice ()) -> ChangeT Nice ())
-> (KwRange -> 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 ())
-> (KwRange -> Nice ()) -> KwRange -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (KwRange -> DeclarationWarning') -> KwRange -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> DeclarationWarning'
OpenPublicAbstract
        UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                 -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePatternSyn{}             -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceGeneralize{}             -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds             -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds

instance MakeAbstract Clause where
  mkAbstract :: UpdaterT Nice Clause
mkAbstract (Clause Name
x Bool
catchall LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
    Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x Bool
catchall 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
<$> UpdaterT Nice WhereClause
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract 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
<*> UpdaterT Nice [Clause]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [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 :: UpdaterT Nice WhereClause
mkAbstract  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 (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 (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 -> Origin -> 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]

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

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

instance MakePrivate NiceDeclaration where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice NiceDeclaration
mkPrivate KwRange
kwr Origin
o = \case
      Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e                    -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Name
x Expr
e)                (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e                -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Name
x Arg Expr
e)            (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e              -> (\ Access
p -> Range
-> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Name
x Arg Expr
e)          (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds                 -> (\ [NiceDeclaration]
ds-> KwRange
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual KwRange
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds)             ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
      NiceLoneConstructor KwRange
r [NiceDeclaration]
ds                 -> KwRange -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor KwRange
r                         ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
      NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds              -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> Erased
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
p IsAbstract
a Erased
e QName
x Telescope
tel [Declaration]
ds)          (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is         -> (\ Access
p -> Range
-> Access
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
p Erased
e Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is)     (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t         -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)     (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t        -> (\ Access
p -> Range
-> Erased
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Erased
er Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)    (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d     -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e        -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)    (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Name]
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p'               -> (\ Access
p -> Range
-> Access
-> Name
-> [WithHiding Name]
-> Pattern
-> NiceDeclaration
NicePatternSyn Range
r Access
p Name
x [WithHiding Name]
xs Pattern
p')           (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t             -> (\ Access
p -> Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Name
x Expr
t)         (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o Access
p
      NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds                       -> (\ [NiceDeclaration]
p -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
p)                    ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
mkPrivate KwRange
kwr Origin
o [NiceDeclaration]
ds
      d :: NiceDeclaration
d@NicePragma{}                           -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        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
directives) ((KwRange -> ChangeT Nice ()) -> ChangeT Nice ())
-> (KwRange -> 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 ())
-> (KwRange -> Nice ()) -> KwRange -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (KwRange -> DeclarationWarning') -> KwRange -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KwRange -> DeclarationWarning'
OpenPublicPrivate
        UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                           -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      -- Andreas, 2016-07-08, issue #2089
      -- we need to propagate 'private' to the named where modules
      FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x [Clause]
cls              -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Name
x ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor 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]
cls
      d :: NiceDeclaration
d@NiceDataDef{}                          -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceRecDef{}                           -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceUnquoteData{}                      -> UpdaterT Nice NiceDeclaration
forall a. a -> ChangeT Nice a
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

instance MakePrivate Clause where
  mkPrivate :: KwRange -> Origin -> UpdaterT Nice Clause
mkPrivate KwRange
kwr Origin
o (Clause Name
x Bool
catchall LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
    Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x Bool
catchall 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 @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

-- 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 -> [Declaration]
notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
notSoNiceDeclarations = \case
    Axiom Range
_ Access
_ IsAbstract
_ IsInstance
i ArgInfo
rel Name
x Expr
e          -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [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   -> [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    -> [KwRange -> [Declaration] -> Declaration
Primitive KwRange
forall a. Null a => a
empty [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (Arg Expr -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Expr
e) TacticAttribute
forall a. Null a => a
empty Name
x (Arg Expr -> Expr
forall e. Arg e -> e
unArg Arg Expr
e)]]
    NiceMutual KwRange
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds          -> [KwRange -> [Declaration] -> Declaration
Mutual KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceLoneConstructor KwRange
r [NiceDeclaration]
ds       -> [KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceModule Range
r Access
_ IsAbstract
_ Erased
e QName
x Telescope
tel [Declaration]
ds    -> [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
                                   -> [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               -> [Range -> QName -> ImportDirective -> Declaration
Open Range
r QName
x ImportDirective
dir]
    NiceImport Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir        -> [Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> Declaration
Import Range
r QName
x Maybe AsName
as OpenShortHand
o ImportDirective
dir]
    NicePragma Range
_ Pragma
p                 -> [Pragma -> Declaration
Pragma Pragma
p]
    NiceRecSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e -> [Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e]
    NiceDataSig Range
r Erased
er Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e -> [Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e]
    NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
d    -> [Declaration
d]
    FunSig Range
_ Access
_ IsAbstract
_ IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
_ CoverageCheck
_ Name
x Expr
e   -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Null a => a
empty Name
x Expr
e]
    FunDef Range
_ [Declaration]
ds IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_        -> [Declaration]
ds
    NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs [NiceDeclaration]
cs  -> [Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
r Name
x [LamBinding]
bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
cs]
    NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds -> [Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
x [RecordDirective]
dir [LamBinding]
bs [Declaration]
ds]
    NicePatternSyn Range
r Access
_ Name
n [WithHiding Name]
as Pattern
p      -> [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   -> [KwRange -> [Declaration] -> Declaration
Generalize KwRange
forall a. Null a => a
empty [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] -> [Declaration]
inst IsInstance
i [Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
r [Name]
x Expr
e]
    NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
x Expr
e    -> [Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
r [Name]
x Expr
e]
    NiceUnquoteData Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [Name]
xs Expr
e  -> [Range -> Name -> [Name] -> Expr -> Declaration
UnquoteData Range
r Name
x [Name]
xs Expr
e]
    NiceOpaque KwRange
r [QName]
ns [NiceDeclaration]
ds                -> [KwRange -> [Declaration] -> Declaration
Opaque KwRange
r (KwRange -> [QName] -> Declaration
Unfolding KwRange
r [QName]
nsDeclaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
:(NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds)]
  where
    inst :: IsInstance -> [Declaration] -> [Declaration]
inst (InstanceDef KwRange
r) [Declaration]
ds = [KwRange -> [Declaration] -> Declaration
InstanceB KwRange
r [Declaration]
ds]
    inst IsInstance
NotInstanceDef  [Declaration]
ds = [Declaration]
ds

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