{-# LANGUAGE GADTs              #-}

-- | 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, 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.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.Concrete.Definitions.Errors
import Agda.Syntax.Concrete.Definitions.Monad
import Agda.Syntax.Concrete.Definitions.Types

import Agda.Interaction.Options.Warnings

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.Null
import Agda.Utils.Pretty
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]
tcs = [TerminationCheck] -> Nice TerminationCheck
loop [TerminationCheck]
tcs where
  loop :: [TerminationCheck] -> Nice TerminationCheck
  loop :: [TerminationCheck] -> Nice TerminationCheck
loop []         = forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
TerminationCheck
  loop (TerminationCheck
tc : [TerminationCheck]
tcs) = do
    let failure :: Range -> Nice a
failure Range
r = forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Range -> DeclarationException'
InvalidMeasureMutual Range
r
    TerminationCheck
tc' <- [TerminationCheck] -> Nice TerminationCheck
loop [TerminationCheck]
tcs
    case (TerminationCheck
tc, TerminationCheck
tc') of
      (TerminationCheck
TerminationCheck      , TerminationCheck
tc'                   ) -> forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc'
      (TerminationCheck
tc                    , TerminationCheck
TerminationCheck      ) -> forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
      (TerminationCheck
NonTerminating        , TerminationCheck
NonTerminating        ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
NonTerminating
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
NoTerminationCheck    ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
NoTerminationCheck
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
Terminating           ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
Terminating
      (TerminationCheck
Terminating           , TerminationCheck
NoTerminationCheck    ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
Terminating
      (TerminationCheck
Terminating           , TerminationCheck
Terminating           ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall m. TerminationCheck m
Terminating
      (TerminationMeasure{}  , TerminationMeasure{}  ) -> forall (m :: * -> *) a. Monad m => a -> m a
return TerminationCheck
tc
      (TerminationMeasure Range
r Name
_, TerminationCheck
NoTerminationCheck    ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationMeasure Range
r Name
_, TerminationCheck
Terminating           ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NoTerminationCheck    , TerminationMeasure Range
r Name
_) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
Terminating           , TerminationMeasure Range
r Name
_) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationMeasure Range
r Name
_, TerminationCheck
NonTerminating        ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationMeasure Range
r Name
_) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NoTerminationCheck    , TerminationCheck
NonTerminating        ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
Terminating           , TerminationCheck
NonTerminating        ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationCheck
NoTerminationCheck    ) -> forall {a}. Range -> Nice a
failure Range
r
      (TerminationCheck
NonTerminating        , TerminationCheck
Terminating           ) -> forall {a}. Range -> Nice a
failure Range
r

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

combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
combinePositivityChecks = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeclKind -> DeclKind -> Bool
$c/= :: DeclKind -> DeclKind -> Bool
== :: DeclKind -> DeclKind -> Bool
$c== :: DeclKind -> DeclKind -> Bool
Eq, Int -> DeclKind -> ShowS
[DeclKind] -> ShowS
DeclKind -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeclKind] -> ShowS
$cshowList :: [DeclKind] -> ShowS
show :: DeclKind -> String
$cshow :: DeclKind -> String
showsPrec :: Int -> DeclKind -> ShowS
$cshowsPrec :: Int -> 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 Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
pars Expr
_)   = Range -> DataRecOrFun -> Name -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x
declKind (NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
pars 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 RecordDirectives
_ [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

-- | 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 forall k a. Map k a -> Bool
Map.null LoneSigs
ps then forall a. a -> a
id else \case
  []     -> 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') <- forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\ Name
_ LoneSig
_ -> forall a. Maybe a
Nothing) Name
x LoneSigs
ps
        , forall a. HasRange a => a -> Range
getRange Name
x forall a. Eq a => a -> a -> Bool
== 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 forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps' [NiceDeclaration]
ds
      Maybe (Name, NiceDeclaration)
_ -> NiceDeclaration
d     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 forall a. IsNoName a => a -> Bool
isNoName Name
x' then Range -> Name
noName (Name -> Range
nameRange Name
x') else Name
x' in
        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 Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        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 ArgInfo
defaultArgInfo Name
x Expr
e)
      NiceDataSig Range
r Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        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 ArgInfo
defaultArgInfo Name
x Expr
e)
      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.
  NiceEnv
st <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ NiceEnv
initNiceEnv { niceWarn :: NiceWarnings
niceWarn = NiceEnv -> NiceWarnings
niceWarn NiceEnv
st }
  [NiceDeclaration]
nds <- [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds

  -- Check that every signature got its definition.
  LoneSigs
ps <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs
  LoneSigs -> Nice ()
checkLoneSigs LoneSigs
ps
  -- We postulate the missing ones and insert them in place of the corresponding @FunSig@
  let ds :: [NiceDeclaration]
ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
nds

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

  -- Restore the old state, but keep the warnings.
  NiceWarnings
warns <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets NiceEnv -> NiceWarnings
niceWarn
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ NiceEnv
st { niceWarn :: NiceWarnings
niceWarn = NiceWarnings
warns }
  forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
res

  where

    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = 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 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds
        LoneDefs{}   -> (NiceDeclaration
d forall a. a -> [a] -> [a]
:) 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
          Name
_ <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x DataRecOrFun
k
          InferredMutual MutualChecks
checks [NiceDeclaration]
nds0 [NiceDeclaration]
ds1 <- MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k) [NiceDeclaration]
ds
          -- If we still have lone signatures without any accompanying definition,
          -- we postulate the definition and substitute the axiom for the lone signature
          LoneSigs
ps <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs
          LoneSigs -> Nice ()
checkLoneSigs LoneSigs
ps
          let ds0 :: [NiceDeclaration]
ds0 = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps (NiceDeclaration
d 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
          TerminationCheck
tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks (forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) (MutualChecks -> [TerminationCheck]
mutualTermination MutualChecks
checks)
          let cc :: CoverageCheck
cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks              (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
          let pc :: PositivityCheck
pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks            (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
          (Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual (forall a. HasRange a => a -> Range
getRange [NiceDeclaration]
ds0) TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds0 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds1
      where
        untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
        untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds = do
          Bool
done <- Nice Bool
noLoneSigs
          if Bool
done then forall (m :: * -> *) a. Monad m => a -> m a
return (MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
checks [] [NiceDeclaration]
ds) else
            case [NiceDeclaration]
ds of
              []     -> 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
                  forall (f :: * -> *) a. Functor f => f a -> f ()
void 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                LoneDefs DataRecOrFun
k [Name]
xs -> do
                  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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                DeclKind
OtherDecl -> NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    nice [Declaration]
ds = do
      ([NiceDeclaration]
xs , [Declaration]
ys) <- [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      ([NiceDeclaration]
xs forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ys

    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 []     = 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.
            forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack 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
          TerminationCheck
termCheck <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
          CoverageCheck
covCheck  <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
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 :: Range
r = forall a. HasRange a => a -> Range
getRange Name
x
          -- register x as lone type signature, to recognize clauses later
          Name
x' <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x forall a b. (a -> b) -> a -> b
$ TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
termCheck CoverageCheck
covCheck
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig Range
r Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef IsMacro
NotMacroDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x' Expr
t] , [Declaration]
ds)

        -- Should not show up: all FieldSig are part of a Field block
        FieldSig{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

        Generalize Range
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
EmptyGeneralize Range
r
        Generalize Range
r [Declaration]
sigs -> do
          [NiceDeclaration]
gs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
sigs 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@.
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) forall a b. (a -> b) -> a -> b
$
                HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
HiddenGeneralize forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Name
x
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Name
-> Expr
-> NiceDeclaration
NiceGeneralize (forall a. HasRange a => a -> Range
getRange Declaration
sig) Access
PublicAccess ArgInfo
info TacticAttribute
tac Name
x Expr
t
            Declaration
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
          forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceDeclaration]
gs, [Declaration]
ds)

        (FunClause LHS
lhs RHS
_ WhereClause
_ Bool
_)         -> do
          TerminationCheck
termCheck <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
          CoverageCheck
covCheck  <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
coverageCheckPragma
          Bool
catchall  <- Nice Bool
popCatchallPragma
          [(Name, Name)]
xs <- LoneSigs -> [(Name, Name)]
loneFuns forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs
          -- for each type signature 'x' waiting for clauses, we try
          -- if we have some clauses for 'x'
          case [ (Name
x, (Name
x', [Declaration]
fits, [Declaration]
rest))
               | (Name
x, Name
x') <- [(Name, Name)]
xs
               , let ([Declaration]
fits, [Declaration]
rest) =
                      -- Anonymous declarations only have 1 clause each!
                      if forall a. IsNoName a => a -> Bool
isNoName Name
x then ([Declaration
d], [Declaration]
ds)
                      else forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Fixities
fixs) Name
x) (Declaration
d forall a. a -> [a] -> [a]
: [Declaration]
ds)
               , Bool -> Bool
not (forall a. Null a => a -> Bool
null [Declaration]
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
                [NiceDeclaration]
d  <- ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> TacticAttribute
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
defaultArgInfo) TerminationCheck
termCheck CoverageCheck
covCheck Name
x forall a. Maybe a
Nothing [Declaration
d] -- fun def without type signature is relevant
                forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceDeclaration]
d , [Declaration]
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
                forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause (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
               [Declaration]
ds  <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
               [Clause]
cs  <- Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x' [Declaration]
ds Bool
False
               forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef (forall a. HasRange a => a -> Range
getRange [Declaration]
fits) [Declaration]
fits IsAbstract
ConcreteDef IsInstance
NotInstanceDef TerminationCheck
termCheck CoverageCheck
covCheck Name
x' [Clause]
cs] , [Declaration]
rest)

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

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

        DataSig Range
r Name
x [LamBinding]
tel Expr
t -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          Name
_ <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x forall a b. (a -> b) -> a -> b
$ PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc
          (,[Declaration]
ds) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
DataBlock) Range
r Name
x (forall a. a -> Maybe a
Just ([LamBinding]
tel, Expr
t)) forall a. Maybe a
Nothing

        Data Range
r Name
x [LamBinding]
tel Expr
t [Declaration]
cs -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
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.
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          UniverseCheck
uc <- if UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck then forall (m :: * -> *) a. Monad m => a -> m a
return UniverseCheck
uc else Name -> Nice UniverseCheck
getUniverseCheckFromSig Name
x
          TacticAttribute
mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Name
x (forall a. a -> Maybe a
Just Expr
t)
          (,[Declaration]
ds) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
DataBlock) Range
r Name
x (([LamBinding]
tel,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticAttribute
mt) (forall a. a -> Maybe a
Just ([LamBinding]
tel, [Declaration]
cs))

        DataDef Range
r Name
x [LamBinding]
tel [Declaration]
cs -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
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.
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          UniverseCheck
uc <- if UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck then forall (m :: * -> *) a. Monad m => a -> m a
return UniverseCheck
uc else Name -> Nice UniverseCheck
getUniverseCheckFromSig Name
x
          TacticAttribute
mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Name
x forall a. Maybe a
Nothing
          (,[Declaration]
ds) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
DataBlock) Range
r Name
x (([LamBinding]
tel,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticAttribute
mt) (forall a. a -> Maybe a
Just ([LamBinding]
tel, [Declaration]
cs))

        RecordSig Range
r Name
x [LamBinding]
tel Expr
t         -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          Name
_ <- Range -> Name -> DataRecOrFun -> Nice Name
addLoneSig Range
r Name
x forall a b. (a -> b) -> a -> b
$ PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel Expr
t] , [Declaration]
ds)

        Record Range
r Name
x RecordDirectives
dir [LamBinding]
tel Expr
t [Declaration]
cs   -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
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.
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          UniverseCheck
uc <- if UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck then forall (m :: * -> *) a. Monad m => a -> m a
return UniverseCheck
uc else Name -> Nice UniverseCheck
getUniverseCheckFromSig Name
x
          TacticAttribute
mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x (forall a. a -> Maybe a
Just Expr
t)
          (,[Declaration]
ds) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs) Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig
                      forall (m :: * -> *) a. Monad m => a -> m a
return Range
r Name
x (([LamBinding]
tel,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticAttribute
mt) (forall a. a -> Maybe a
Just ([LamBinding]
tel, [Declaration]
cs))

        RecordDef Range
r Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs   -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
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.
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          UniverseCheck
uc <- if UniverseCheck
uc forall a. Eq a => a -> a -> Bool
== UniverseCheck
NoUniverseCheck then forall (m :: * -> *) a. Monad m => a -> m a
return UniverseCheck
uc else Name -> Nice UniverseCheck
getUniverseCheckFromSig Name
x
          TacticAttribute
mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Name
x forall a. Maybe a
Nothing
          (,[Declaration]
ds) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
tel [Declaration]
cs -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs) Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig
                      forall (m :: * -> *) a. Monad m => a -> m a
return Range
r Name
x (([LamBinding]
tel,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticAttribute
mt) (forall a. a -> Maybe a
Just ([LamBinding]
tel, [Declaration]
cs))

        RecordDirective RecordDirective
r -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidRecordDirective (forall a. HasRange a => a -> Range
getRange RecordDirective
r)

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

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

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


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

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

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

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

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

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

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

        ModuleMacro Range
r Name
x ModuleApplication
modapp OpenShortHand
op ImportDirective
is -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          ([Range
-> Access
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
PublicAccess 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
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)
        Syntax Name
_ Notation
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Declaration]
ds)

        PatternSyn Range
r Name
n [Arg Name]
as Pattern
p -> do
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Access -> Name -> [Arg Name] -> Pattern -> NiceDeclaration
NicePatternSyn Range
r Access
PublicAccess Name
n [Arg Name]
as Pattern
p] , [Declaration]
ds)
        Open Range
r QName
x ImportDirective
is         -> 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 -> 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
          TerminationCheck
tc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
          CoverageCheck
cc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
coverageCheckPragma
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef TerminationCheck
tc CoverageCheck
cc [Name]
xs Expr
e] , [Declaration]
ds)

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

        UnquoteData Range
r Name
xs [Name]
cs Expr
e -> do
          PositivityCheck
pc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
          UniverseCheck
uc <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' UniverseCheck NiceEnv
universeCheckPragma
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [Name]
-> Expr
-> NiceDeclaration
NiceUnquoteData Range
r Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Name
xs [Name]
cs Expr
e], [Declaration]
ds)

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

    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
        forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma (forall m. Range -> m -> TerminationCheck m
TerminationMeasure Range
r Name
x) forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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 forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
PragmaNoTerminationCheck Range
r
      Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nicePragma (Range -> TerminationCheck -> Pragma
TerminationCheckPragma Range
r forall m. TerminationCheck m
NonTerminating) [Declaration]
ds

    nicePragma (TerminationCheckPragma Range
r TerminationCheck
tc) [Declaration]
ds =
      if [Declaration] -> Bool
canHaveTerminationCheckPragma [Declaration]
ds then
        forall a. TerminationCheck -> Nice a -> Nice a
withTerminationCheckPragma TerminationCheck
tc forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
        forall a. CoverageCheck -> Nice a -> Nice a
withCoverageCheckPragma CoverageCheck
NoCoverageCheck forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
        forall a. Bool -> Nice a -> Nice a
withCatchallPragma Bool
True forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
        forall a. PositivityCheck -> Nice a -> Nice a
withPositivityCheckPragma PositivityCheck
NoPositivityCheck forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
        forall a. UniverseCheck -> Nice a -> Nice a
withUniverseCheckPragma UniverseCheck
NoUniverseCheck forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds
      else do
        HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
      HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
PragmaCompiled (forall a. HasRange a => a -> Range
getRange Pragma
p)
      forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)

    nicePragma (PolarityPragma{}) [Declaration]
ds = 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
      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 Pragma
p [Declaration]
ds = forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (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 Range
_ [Declaration]
ds   -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveTerminationCheckPragma forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Range
_ [Declaration]
ds                   -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Declaration] -> Bool
canHaveNoPositivityCheckPragma forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig DataRecOrFun
k Name
x t :: TacticAttribute
t@Just{} = forall (m :: * -> *) a. Monad m => a -> m a
return TacticAttribute
t
    defaultTypeSig DataRecOrFun
k Name
x TacticAttribute
Nothing  = do
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Name -> Nice (Maybe DataRecOrFun)
getSig Name
x) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ DataRecOrFun
k' -> do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (DataRecOrFun -> DataRecOrFun -> Bool
sameKind DataRecOrFun
k DataRecOrFun
k') forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Name -> DataRecOrFun -> DataRecOrFun -> DeclarationException'
WrongDefinition Name
x DataRecOrFun
k' DataRecOrFun
k
        forall a. Maybe a
Nothing 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
      Maybe ([LamBinding], [decl])
mds <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe ([LamBinding], [a])
mcs forall a b. (a -> b) -> a -> b
$ \ ([LamBinding]
tel, [a]
cs) -> ([LamBinding]
tel,) 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 :: Origin
o | forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], Expr)
mt Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], [a])
mcs = Origin
Inserted
            | Bool
otherwise               = Origin
UserWritten
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$
        [ Maybe ([LamBinding], Expr)
mt  forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ([LamBinding]
tel, Expr
t)  -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig (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
        , Maybe ([LamBinding], [decl])
mds forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ([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 (forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ([LamBinding], Expr)
mt [LamBinding]
tel forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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
        forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Name
-> Expr
-> NiceDeclaration
Axiom (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 forall a. Eq a => a -> a -> Bool
== KindOfBlock
FieldBlock -> do
        forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Name
-> Arg Expr
-> NiceDeclaration
NiceField (forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
i TacticAttribute
tac Name
x Arg Expr
argt ]
      InstanceB Range
r [Declaration]
decls -> do
        Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock Range
r forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
InstanceBlock [Declaration]
decls
      Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> do
        forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
      Declaration
d -> forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
b forall a b. (a -> b) -> a -> b
$ 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 (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
rel Expr
t)
    toPrim NiceDeclaration
_                       = forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Create a function definition.
    mkFunDef :: ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> TacticAttribute
-> [Declaration]
-> Nice [NiceDeclaration]
mkFunDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x TacticAttribute
mt [Declaration]
ds0 = do
      [Declaration]
ds <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds0
      [Clause]
cs <- Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
ds Bool
False
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Name
-> Expr
-> NiceDeclaration
FunSig (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Expr
t) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef IsMacro
NotMacroDef ArgInfo
info TerminationCheck
termCheck CoverageCheck
covCheck Name
x Expr
t
             , Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef (forall a. HasRange a => a -> Range
getRange [Declaration]
ds0) [Declaration]
ds0 IsAbstract
ConcreteDef IsInstance
NotInstanceDef TerminationCheck
termCheck CoverageCheck
covCheck Name
x [Clause]
cs ]
        where
          t :: Expr
t = forall a. a -> Maybe a -> a
fromMaybe (Range -> Expr
underscore (forall a. HasRange a => a -> Range
getRange Name
x)) TacticAttribute
mt

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


    expandEllipsis :: [Declaration] -> Nice [Declaration]
    expandEllipsis :: [Declaration] -> Nice [Declaration]
expandEllipsis [] = 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)
      | forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p = (Declaration
d forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
ds
      | Bool
otherwise     = (Declaration
d forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (forall a. KillRange a => KillRangeT a
killRange Pattern
p) [Declaration]
ds
      where
        expand :: Pattern -> [Declaration] -> Nice [Declaration]
        expand :: Pattern -> [Declaration] -> Nice [Declaration]
expand Pattern
_ [] = 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 forall a. a -> [a] -> [a]
:) 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 forall p. CPatternLike p => p -> AffineHole Pattern p
hasEllipsis' Pattern
p0 of
                AffineHole Pattern Pattern
ManyHoles -> forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Pattern -> DeclarationException'
MultipleEllipses Pattern
p0
                OneHole Pattern -> Pattern
cxt ~(EllipsisP Range
r Maybe Pattern
Nothing) -> do
                  -- Replace the ellipsis by @p@.
                  let p1 :: Pattern
p1 = Pattern -> Pattern
cxt forall a b. (a -> b) -> a -> b
$ Range -> Maybe Pattern -> Pattern
EllipsisP Range
r forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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' forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else 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 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [Declaration] -> Nice [Declaration]
expand (if forall a. Null a => a -> Bool
null [WithExpr]
es then Pattern
p else forall a. KillRange a => KillRangeT a
killRange Pattern
p0) [Declaration]
ds
            Declaration
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    expandEllipsis [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
_ = 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 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
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null [Declaration]
cs) forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning 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
      | forall a. Null a => a -> Bool
null (LHS -> [WithExpr]
lhsWithExpr LHS
lhs) Bool -> Bool -> 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 [] forall a. a -> [a] -> [a]
:) 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
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null [Declaration]
withClauses) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Name -> LHS -> DeclarationException'
MissingWithClauses Name
x LHS
lhs
      [Clause]
wcs <- Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
withClauses Bool
False
      (Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Name
x (Bool
ca Bool -> Bool -> Bool
|| Bool
catchall) LHS
lhs RHS
rhs WhereClause
wh [Clause]
wcs forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
x [Declaration]
cs' Bool
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 = forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter 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)
         | forall a. IsEllipsis a => a -> Bool
isEllipsis Pattern
p0 Bool -> Bool -> Bool
||
           forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p0 forall a. Ord a => a -> a -> Bool
>= Int
numWith = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Declaration
cforall a. a -> [a] -> [a]
:) ([Declaration] -> ([Declaration], [Declaration])
subClauses [Declaration]
cs)
         | Bool
otherwise                           = ([], Declaration
cforall 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
cforall a. a -> [a] -> [a]
:[Declaration]
cs')
          ([Declaration]
cs, [Declaration]
cs') -> (Declaration
cforall a. a -> [a] -> [a]
:[Declaration]
cs, [Declaration]
cs')
        subClauses [] = ([],[])
        subClauses [Declaration]
_  = forall a. HasCallStack => a
__IMPOSSIBLE__
    mkClauses Name
_ [Declaration]
_ Bool
_ = 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 = 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 (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 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 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 (forall a. Null a => a -> Bool
null [String]
notStrings) Bool -> Bool -> Bool
&& ([String]
notStrings 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) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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
_ = 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
_) =
       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
      :: Range                 -- Range of the whole @mutual@ block.
      -> [NiceDeclaration]     -- Declarations inside the block.
      -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
    mkInterleavedMutual :: Range -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual Range
r [NiceDeclaration]
ds' = do
      ([(Int, NiceDeclaration)]
other, (InterleavedMutual
m, MutualChecks
checks, Int
_)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
ds') (forall a. Null a => a
empty, forall a. Monoid a => a
mempty, Int
0)
      let idecls :: [(Int, NiceDeclaration)]
idecls = [(Int, NiceDeclaration)]
other forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl) (forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m)
      let decls0 :: [NiceDeclaration]
decls0 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) [(Int, NiceDeclaration)]
idecls
      LoneSigs
ps <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' LoneSigs NiceEnv
loneSigs
      LoneSigs -> Nice ()
checkLoneSigs LoneSigs
ps
      let decls :: [NiceDeclaration]
decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps [NiceDeclaration]
decls0
      -- process the checks
      TerminationCheck
tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks Range
r (MutualChecks -> [TerminationCheck]
mutualTermination MutualChecks
checks)
      let cc :: CoverageCheck
cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks   (MutualChecks -> [CoverageCheck]
mutualCoverage MutualChecks
checks)
      let pc :: PositivityCheck
pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (MutualChecks -> [PositivityCheck]
mutualPositivity MutualChecks
checks)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
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
          (Map Name a
m, MutualChecks
checks, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name a
m) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Name -> DeclarationException'
DuplicateDefinition Name
n
          forall s (m :: * -> *). MonadState s m => s -> m ()
put (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (Int -> a
c Int
i) Map Name a
m, MutualChecks
mc forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
iforall a. Num a => a -> a -> a
+Int
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] []
           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 forall a. Maybe a
Nothing) MutualChecks
checks
        addFunType NiceDeclaration
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

        addDataType :: NiceDeclaration
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataType d :: NiceDeclaration
d@(NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Name
n [LamBinding]
_ Expr
_) = do
          let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [] [] [PositivityCheck
pc]
          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 forall a. Maybe a
Nothing) MutualChecks
checks
        addDataType NiceDeclaration
_ = 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
          (InterleavedMutual
m, MutualChecks
checks, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n InterleavedMutual
m of
            Just (InterleavedData Int
i0 NiceDeclaration
sig Maybe (Int, List1 [NiceDeclaration])
cs) -> do
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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 forall a. a -> [a] -> NonEmpty a
:| [] ), Int
iforall a. Num a => a -> a -> a
+Int
1)
                    Just (Int
i1, List1 [NiceDeclaration]
ds1) -> ((Int
i1, [NiceDeclaration]
ds forall a. a -> NonEmpty a -> NonEmpty a
<| List1 [NiceDeclaration]
ds1), Int
i)
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (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 (forall a. a -> Maybe a
Just (Int, List1 [NiceDeclaration])
cs')) InterleavedMutual
m, MutualChecks
checks, Int
i')
            Maybe InterleavedDecl
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ [(Name, Range)] -> DeclarationWarning'
MissingDeclarations forall a b. (a -> b) -> a -> b
$ case Maybe Range
mr of
                   Just Range
r -> [(Name
n, Range
r)]
                   Maybe Range
Nothing -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap [NiceDeclaration]
ds forall a b. (a -> b) -> a -> b
$ \case
                     Axiom Range
r Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
n Expr
_ -> [(Name
n, Range
r)]
                     NiceDeclaration
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

        addDataConstructors Maybe Range
mr Maybe Name
Nothing [] = 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
          (InterleavedMutual
m, MutualChecks
_, Int
_) <- forall s (m :: * -> *). MonadState s m => m s
get
          let sigs :: [Name]
sigs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedData InterleavedDecl
d) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
          -- check whether this constructor matches any of them
          case [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
isConstructor [Name]
sigs NiceDeclaration
d of
            Right Name
n -> do
              -- if so grab the whole block that may work and add them
              let ([NiceDeclaration]
ds0, [NiceDeclaration]
ds1) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a b. Either a b -> Bool
isRight 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 forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just Name
n) (NiceDeclaration
d 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 forall a. Maybe a
Nothing forall a. Maybe a
Nothing [NiceDeclaration]
ds1
            Left (Name
n, [Name]
ns) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => DeclarationException' -> Nice a
declarationException forall a b. (a -> b) -> a -> b
$ Range -> Name -> [Name] -> DeclarationException'
AmbiguousConstructor (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] []
          (InterleavedMutual
m, MutualChecks
checks, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n InterleavedMutual
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) forall a. a -> [a] -> NonEmpty a
:| [] ), Int
iforall a. Num a => a -> a -> a
+Int
1)
                    Just (Int
i1, List1 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
ds, [Clause]
cs) forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (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 (forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
check forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
            Maybe InterleavedDecl
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- A FunDef always come after an existing FunSig!
        addFunDef NiceDeclaration
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

        addFunClauses :: Range -> [NiceDeclaration]
                      -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
        addFunClauses :: Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
addFunClauses Range
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
          (InterleavedMutual
m, MutualChecks
checks, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
          let sigs :: [Name]
sigs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Name
n, InterleavedDecl
d) -> Name
n forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedDecl
d) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
          -- find the funsig candidates for the funclause of interest
          case [ (Name
x, Prefix (MutualChecks, Declaration)
fits, [NiceDeclaration]
rest)
               | Name
x <- [Name]
sigs
               , let (Prefix (MutualChecks, Declaration)
fits, [NiceDeclaration]
rest) = forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
spanJust (Maybe Fixity'
-> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Fixities
fixs) Name
x) (NiceDeclaration
nd forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds)
               , Bool -> Bool
not (forall a. Null a => a -> Bool
null Prefix (MutualChecks, Declaration)
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] []
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
check forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
iforall a. Num a => a -> a -> a
+Int
1)
              ((Int
i,NiceDeclaration
nd) forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
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) = forall a b. [(a, b)] -> ([a], [b])
unzip Prefix (MutualChecks, Declaration)
fits0
              [Declaration]
ds <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
              [Clause]
cs <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Name -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Name
n [Declaration]
ds Bool
False
              case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n InterleavedMutual
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) forall a. a -> [a] -> NonEmpty a
:| [] ), Int
iforall a. Num a => a -> a -> a
+Int
1)
                        Just (Int
i1, List1 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
fits,[Clause]
cs) forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
                  let checks' :: MutualChecks
checks' = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [MutualChecks]
checkss
                  forall s (m :: * -> *). MonadState s m => s -> m ()
put (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 (forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
checks' forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
                Maybe InterleavedDecl
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
              Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
rest
            -- more than one candidate: fail, complaining about the ambiguity!
            (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf:[(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
                           forall a b. (a -> b) -> a -> b
$ LHS -> List1 Name -> DeclarationException'
AmbiguousFunClauses LHS
lhs
                           forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> NonEmpty a
List1.reverse forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Name
a,Prefix (MutualChecks, Declaration)
_,[NiceDeclaration]
_) -> Name
a) forall a b. (a -> b) -> a -> b
$ (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf forall a. a -> [a] -> NonEmpty a
:| [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs
        addFunClauses Range
_ [NiceDeclaration]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

        groupByBlocks :: Range -> [NiceDeclaration]
                      -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
        groupByBlocks :: Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r []       = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        groupByBlocks Range
r (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [(Int, NiceDeclaration)]
ns -> ([(Int, NiceDeclaration)]
ns forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
ds
          case NiceDeclaration
d of
            NiceDataSig{}                -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff forall a b. (a -> b) -> a -> b
$ [] 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 forall a b. (a -> b) -> a -> b
$ [] forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors (forall a. a -> Maybe a
Just Range
r) (forall a. a -> Maybe a
Just Name
n) [NiceDeclaration]
ds
            NiceLoneConstructor Range
r [NiceDeclaration]
ds     -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff forall a b. (a -> b) -> a -> b
$ [] forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Name
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors forall a. Maybe a
Nothing forall a. Maybe a
Nothing [NiceDeclaration]
ds
            FunSig{}                     -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff forall a b. (a -> b) -> a -> b
$ [] 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 (forall a. IsNoName a => a -> Bool
isNoName Name
n) -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff forall a b. (a -> b) -> a -> b
$ [] 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{}              -> Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
addFunClauses Range
r (NiceDeclaration
dforall 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 forall a b. (a -> b) -> a -> b
$ do
              (InterleavedMutual
m, MutualChecks
c, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get -- TODO: grab checks from c?
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
c, Int
iforall a. Num a => a -> a -> a
+Int
1)
              forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Int
i,NiceDeclaration
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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TacticAttribute
returnExpr Expr
e =
         case [ Name
x | Name
x <- [Name]
ns
                  , Maybe Fixity' -> Name -> Pattern -> Bool
couldBeCallOf (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x Fixities
fixs) Name
x Pattern
p
                  ] of
           [Name
x] -> forall a b. b -> Either a b
Right Name
x
           [Name]
xs  -> 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 = forall a b. a -> Either a b
Left (Name
n, [])
    isConstructor [Name]
_ NiceDeclaration
_ = 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
      :: Range                 -- Range of the whole @mutual@ block.
      -> [NiceDeclaration]     -- Declarations inside the block.
      -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
    mkOldMutual :: Range -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual Range
r [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.
        ([NiceDeclaration]
top, [NiceDeclaration]
bottom, [NiceDeclaration]
invalid) <- forall (m :: * -> *) a b c d.
Applicative m =>
[a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
forEither3M [NiceDeclaration]
ds forall a b. (a -> b) -> a -> b
$ \ NiceDeclaration
d -> do
          let top :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top       = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. a -> Either3 a b c
In1 NiceDeclaration
d)
              bottom :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom    = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. b -> Either3 a b c
In2 NiceDeclaration
d)
              invalid :: String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
s = forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ Range -> String -> DeclarationWarning'
NotAllowedInMutual (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
            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

              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
              DisplayPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top     -- only for printing

              -- The attached pragmas have already been handled at this point.
              CatchallPragma{}          -> forall a. HasCallStack => a
__IMPOSSIBLE__
              TerminationCheckPragma{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
              NoPositivityCheckPragma{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
              PolarityPragma{}          -> forall a. HasCallStack => a
__IMPOSSIBLE__
              NoUniverseCheckPragma{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
              NoCoverageCheckPragma{}   -> 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
        TerminationCheck
tc0 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
        let tcs :: [TerminationCheck]
tcs = forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> TerminationCheck
termCheck [NiceDeclaration]
ds
        TerminationCheck
tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks Range
r (TerminationCheck
tc0forall a. a -> [a] -> [a]
:[TerminationCheck]
tcs)

        -- Compute coverage checking flag for mutual block
        CoverageCheck
cc0 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' CoverageCheck NiceEnv
coverageCheckPragma
        let ccs :: [CoverageCheck]
ccs = forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> CoverageCheck
covCheck [NiceDeclaration]
ds
        let cc :: CoverageCheck
cc = [CoverageCheck] -> CoverageCheck
combineCoverageChecks (CoverageCheck
cc0forall a. a -> [a] -> [a]
:[CoverageCheck]
ccs)

        -- Compute positivity checking flag for mutual block
        PositivityCheck
pc0 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' PositivityCheck NiceEnv
positivityCheckPragma
        let pcs :: [PositivityCheck]
pcs = forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> PositivityCheck
positivityCheckOldMutual [NiceDeclaration]
ds
        let pc :: PositivityCheck
pc = [PositivityCheck] -> PositivityCheck
combinePositivityChecks (PositivityCheck
pc0forall a. a -> [a] -> [a]
:[PositivityCheck]
pcs)

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc forall a b. (a -> b) -> a -> b
$ [NiceDeclaration]
top forall a. [a] -> [a] -> [a]
++ [NiceDeclaration]
bottom
        -- return $ NiceMutual r tc pc $ other ++ defs
        -- return $ NiceMutual r tc pc $ sigs ++ other
      where

        -- isTypeSig Axiom{}                     = True
        -- isTypeSig d | LoneSig{} <- declKind d = True
        -- isTypeSig _                           = False

        sigNames :: [(Range, Name, DataRecOrFun)]
sigNames  = [ (Range
r, Name
x, DataRecOrFun
k) | LoneSigDecl Range
r DataRecOrFun
k Name
x <- 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 <- 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, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all ((Name
x forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Range
_ 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{}             = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceField{}         = forall m. TerminationCheck m
TerminationCheck
        termCheck PrimitiveFunction{} = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModule{}        = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModuleMacro{}   = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceOpen{}          = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceImport{}        = forall m. TerminationCheck m
TerminationCheck
        termCheck NicePragma{}        = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecSig{}        = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataSig{}       = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceFunClause{}     = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataDef{}       = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecDef{}        = forall m. TerminationCheck m
TerminationCheck
        termCheck NicePatternSyn{}    = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceGeneralize{}    = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceLoneConstructor{} = forall m. TerminationCheck m
TerminationCheck
        termCheck NiceUnquoteData{}   = 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 Range
_ 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

        -- 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
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
pc [NiceDeclaration]
_)        = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_)  = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Name
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_) = PositivityCheck
pc
        positivityCheckOldMutual NiceDeclaration
_                              = PositivityCheck
YesPositivityCheck

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

    abstractBlock :: Range -> [a] -> Nice [a]
abstractBlock Range
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    abstractBlock Range
r [a]
ds = do
      ([a]
ds', Bool
anyChange) <- forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT forall a b. (a -> b) -> a -> b
$ forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [a]
ds
      let inherited :: Bool
inherited = Range
r forall a. Eq a => a -> a -> Bool
== forall a. Range' a
noRange
      if Bool
anyChange then forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds' else do
        -- hack to avoid failing on inherited abstract blocks in where clauses
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
inherited forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
UselessAbstract Range
r
        forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds -- no change!

    privateBlock :: Range -> Origin -> [a] -> Nice [a]
privateBlock Range
_ Origin
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    privateBlock Range
r Origin
o [a]
ds = do
      ([a]
ds', Bool
anyChange) <- forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT forall a b. (a -> b) -> a -> b
$ forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [a]
ds
      if Bool
anyChange then forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds' else do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Origin
o forall a. Eq a => a -> a -> Bool
== Origin
UserWritten) forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
UselessPrivate Range
r
        forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds -- no change!

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

    -- Make a declaration eligible for instance search.
    mkInstance
      :: Range  -- Range of @instance@ keyword.
      -> Updater NiceDeclaration
    mkInstance :: Range -> Updater NiceDeclaration
mkInstance Range
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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Updater IsInstance
setInstance Range
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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Updater IsInstance
setInstance Range
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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Updater IsInstance
setInstance Range
r0 IsInstance
i
        NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds       -> Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> Updater NiceDeclaration
mkInstance Range
r0) [NiceDeclaration]
ds
        NiceLoneConstructor Range
r [NiceDeclaration]
ds       -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> Updater NiceDeclaration
mkInstance Range
r0) [NiceDeclaration]
ds
        d :: NiceDeclaration
d@NiceFunClause{}              -> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Updater IsInstance
setInstance Range
r0 IsInstance
i
        d :: NiceDeclaration
d@NiceField{}                  -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d  -- Field instance are handled by the parser
        d :: NiceDeclaration
d@PrimitiveFunction{}          -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceUnquoteDef{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecSig{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataSig{}                -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModuleMacro{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModule{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePragma{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceOpen{}                   -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceImport{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataDef{}                -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecDef{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePatternSyn{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceGeneralize{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceUnquoteData{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

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

    macroBlock :: p -> t NiceDeclaration -> Nice (t NiceDeclaration)
macroBlock p
r t NiceDeclaration
ds = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM NiceDeclaration -> Nice NiceDeclaration
mkMacro t NiceDeclaration
ds

    mkMacro :: NiceDeclaration -> Nice NiceDeclaration
    mkMacro :: NiceDeclaration -> Nice NiceDeclaration
mkMacro = \case
        FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
_ ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Name
x Expr
e -> forall (m :: * -> *) a. Monad m => a -> m a
return 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{}                     -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        NiceDeclaration
d                              -> forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return IsAbstract
a
    IsAbstract
ConcreteDef -> forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty forall a b. (a -> b) -> a -> b
$ IsAbstract
AbstractDef

instance MakeAbstract NiceDeclaration where
  mkAbstract :: UpdaterT Nice NiceDeclaration
mkAbstract = \case
      NiceMutual Range
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds  -> Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
termCheck CoverageCheck
cc PositivityCheck
pc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
      NiceLoneConstructor Range
r [NiceDeclaration]
ds         -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
cs
      NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x RecordDirectives
dir [LamBinding]
ps [Declaration]
cs -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x RecordDirectives
dir [LamBinding]
ps [Declaration]
cs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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          -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig        Range
r Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t
      NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig       Range
r 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      -> forall (m :: * -> *) a. Monad m => a -> m a
return 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    -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall (m :: * -> *). MonadChange m => m ()
tellDirty 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    -> forall (m :: * -> *). MonadChange m => m ()
tellDirty 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 -> forall (m :: * -> *). MonadChange m => m ()
tellDirty 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{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceModuleMacro{}            -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePragma{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
directives) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> DeclarationWarning'
OpenPublicAbstract
        forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                 -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePatternSyn{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceGeneralize{}             -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract WhereClause
wh forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [Clause]
with

-- | Contents of a @where@ clause are abstract if the parent is.
instance MakeAbstract WhereClause where
  mkAbstract :: UpdaterT Nice WhereClause
mkAbstract  WhereClause
NoWhere             = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall decls. WhereClause' decls
NoWhere
  mkAbstract (AnyWhere Range
r [Declaration]
ds)      = forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty forall a b. (a -> b) -> a -> b
$ forall decls. Range -> decls -> WhereClause' decls
AnyWhere Range
r [Range -> [Declaration] -> Declaration
Abstract forall a. Range' a
noRange [Declaration]
ds]
  mkAbstract (SomeWhere Range
r Name
m Access
a [Declaration]
ds) = forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty forall a b. (a -> b) -> a -> b
$ forall decls.
Range -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Name
m Access
a [Range -> [Declaration] -> Declaration
Abstract forall a. Range' a
noRange [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 :: Origin -> UpdaterT Nice a

  default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => Origin -> UpdaterT Nice a
  mkPrivate Origin
o = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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 :: Origin -> UpdaterT Nice Access
mkPrivate Origin
o = \case
    p :: Access
p@PrivateAccess{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Access
p  -- OR? return $ PrivateAccess o
    Access
_                 -> forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty forall a b. (a -> b) -> a -> b
$ Origin -> Access
PrivateAccess Origin
o

instance MakePrivate NiceDeclaration where
  mkPrivate :: Origin -> UpdaterT Nice NiceDeclaration
mkPrivate 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)                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds                 -> (\ [NiceDeclaration]
ds-> Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds)             forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [NiceDeclaration]
ds
      NiceLoneConstructor Range
r [NiceDeclaration]
ds                 -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r                         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [NiceDeclaration]
ds
      NiceModule Range
r Access
p IsAbstract
a QName
x Telescope
tel [Declaration]
ds                -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> QName
-> Telescope
-> [Declaration]
-> NiceDeclaration
NiceModule Range
r Access
p IsAbstract
a QName
x Telescope
tel [Declaration]
ds)            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceModuleMacro Range
r Access
p Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is           -> (\ Access
p -> Range
-> Access
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
p Name
x ModuleApplication
ma OpenShortHand
op ImportDirective
is)       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceRecSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t            -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Name
x [LamBinding]
ls Expr
t)       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NicePatternSyn Range
r Access
p Name
x [Arg Name]
xs Pattern
p'               -> (\ Access
p -> Range -> Access -> Name -> [Arg Name] -> Pattern -> NiceDeclaration
NicePatternSyn Range
r Access
p Name
x [Arg Name]
xs Pattern
p')           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate 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)         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      d :: NiceDeclaration
d@NicePragma{}                           -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
directives) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
declarationWarning forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> DeclarationWarning'
OpenPublicPrivate
        forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                           -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [Clause]
cls
      d :: NiceDeclaration
d@NiceDataDef{}                          -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceRecDef{}                           -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceUnquoteData{}                      -> forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

instance MakePrivate Clause where
  mkPrivate :: Origin -> UpdaterT Nice Clause
mkPrivate 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o WhereClause
wh forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [Clause]
with

instance MakePrivate WhereClause where
  mkPrivate :: Origin -> UpdaterT Nice WhereClause
mkPrivate Origin
o = \case
    d :: WhereClause
d@WhereClause
NoWhere    -> 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{} -> 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 Name
m Access
a [Declaration]
ds -> forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
a forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Access
a' -> forall decls.
Range -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
r 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 forall a. Maybe a
Nothing 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
r Access
_ IsAbstract
_ Name
x Arg Expr
e    -> [Range -> [Declaration] -> Declaration
Primitive Range
r [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig (forall e. Arg e -> ArgInfo
argInfo Arg Expr
e) forall a. Maybe a
Nothing Name
x (forall e. Arg e -> e
unArg Arg Expr
e)]]
    NiceMutual Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds          -> [Range -> [Declaration] -> Declaration
Mutual Range
r forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceLoneConstructor Range
r [NiceDeclaration]
ds       -> [Range -> [Declaration] -> Declaration
LoneConstructor Range
r forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceModule Range
r Access
_ IsAbstract
_ QName
x Telescope
tel [Declaration]
ds      -> [Range -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r QName
x Telescope
tel [Declaration]
ds]
    NiceModuleMacro Range
r Access
_ Name
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir -> [Range
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
r 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 Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e    -> [Range -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Name
x [LamBinding]
bs Expr
e]
    NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
bs Expr
e   -> [Range -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r 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 forall a. Maybe a
Nothing 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 forall a b. (a -> b) -> a -> b
$ 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 RecordDirectives
dir [LamBinding]
bs [Declaration]
ds -> [Range
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
x RecordDirectives
dir [LamBinding]
bs [Declaration]
ds]
    NicePatternSyn Range
r Access
_ Name
n [Arg Name]
as Pattern
p      -> [Range -> Name -> [Arg Name] -> Pattern -> Declaration
PatternSyn Range
r Name
n [Arg Name]
as Pattern
p]
    NiceGeneralize Range
r Access
_ ArgInfo
i TacticAttribute
tac Name
n Expr
e   -> [Range -> [Declaration] -> Declaration
Generalize Range
r [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]
  where
    inst :: IsInstance -> [Declaration] -> [Declaration]
inst (InstanceDef Range
r) [Declaration]
ds = [Range -> [Declaration] -> Declaration
InstanceB Range
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{}                       -> forall a. Maybe a
Nothing
    NiceField Range
_ Access
_ IsAbstract
a IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_       -> forall a. a -> Maybe a
Just IsAbstract
a
    PrimitiveFunction Range
_ Access
_ IsAbstract
a Name
_ Arg Expr
_   -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceMutual{}                  -> forall a. Maybe a
Nothing
    NiceLoneConstructor{}         -> forall a. Maybe a
Nothing
    NiceModule Range
_ Access
_ IsAbstract
a QName
_ Telescope
_ [Declaration]
_        -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceModuleMacro{}             -> forall a. Maybe a
Nothing
    NiceOpen{}                    -> forall a. Maybe a
Nothing
    NiceImport{}                  -> forall a. Maybe a
Nothing
    NicePragma{}                  -> forall a. Maybe a
Nothing
    NiceRecSig{}                  -> forall a. Maybe a
Nothing
    NiceDataSig{}                 -> forall a. Maybe a
Nothing
    NiceFunClause Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_   -> forall a. a -> Maybe a
Just IsAbstract
a
    FunSig{}                      -> forall a. Maybe a
Nothing
    FunDef Range
_ [Declaration]
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_        -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceDataDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_   -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceRecDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_ -> forall a. a -> Maybe a
Just IsAbstract
a
    NicePatternSyn{}              -> forall a. Maybe a
Nothing
    NiceGeneralize{}              -> forall a. Maybe a
Nothing
    NiceUnquoteDecl Range
_ Access
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_ -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceUnquoteDef Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_    -> forall a. a -> Maybe a
Just IsAbstract
a
    NiceUnquoteData Range
_ Access
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Name
_ [Name]
_ Expr
_ -> forall a. a -> Maybe a
Just IsAbstract
a