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

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

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

data DeclKind
    = LoneSigDecl Range DataRecOrFun Name
    | LoneDefs DataRecOrFun [Name]
    | OtherDecl
  deriving (DeclKind -> DeclKind -> Bool
(DeclKind -> DeclKind -> Bool)
-> (DeclKind -> DeclKind -> Bool) -> Eq DeclKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeclKind -> DeclKind -> Bool
$c/= :: DeclKind -> DeclKind -> Bool
== :: DeclKind -> DeclKind -> Bool
$c== :: DeclKind -> DeclKind -> Bool
Eq, Int -> DeclKind -> ShowS
[DeclKind] -> ShowS
DeclKind -> String
(Int -> DeclKind -> ShowS)
-> (DeclKind -> String) -> ([DeclKind] -> ShowS) -> Show DeclKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
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 Measure
x Expr
_)     = Range -> DataRecOrFun -> Measure -> DeclKind
LoneSigDecl Range
r (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) Measure
x
declKind (NiceRecSig Range
r Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
pars Expr
_)  = Range -> DataRecOrFun -> Measure -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) Measure
x
declKind (NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
pars Expr
_) = Range -> DataRecOrFun -> Measure -> DeclKind
LoneSigDecl Range
r (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) Measure
x
declKind (FunDef Range
r [Declaration]
_ IsAbstract
abs IsInstance
ins TerminationCheck
tc CoverageCheck
cc Measure
x [Clause]
_)     = DataRecOrFun -> [Measure] -> DeclKind
LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) [Measure
x]
declKind (NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
pars [NiceDeclaration]
_) = DataRecOrFun -> [Measure] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
DataName PositivityCheck
pc UniverseCheck
uc) [Measure
x]
declKind (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
uc Measure
x RecordDirectives
_ [LamBinding]
pars [Declaration]
_) = DataRecOrFun -> [Measure] -> DeclKind
LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
RecName PositivityCheck
pc UniverseCheck
uc) [Measure
x]
declKind (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Measure]
xs Expr
_)  = DataRecOrFun -> [Measure] -> DeclKind
LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
FunName TerminationCheck
tc CoverageCheck
cc) [Measure]
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 LoneSigs -> Bool
forall k a. Map k a -> Bool
Map.null LoneSigs
ps then [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> a
id else \case
  []     -> [NiceDeclaration]
forall a. HasCallStack => a
__IMPOSSIBLE__
  (NiceDeclaration
d:[NiceDeclaration]
ds) ->
    case NiceDeclaration -> Maybe (Measure, 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 (Measure
x, NiceDeclaration
axiom)
        | (Just (LoneSig Range
_ Measure
x' DataRecOrFun
_), LoneSigs
ps') <- (Measure -> LoneSig -> Maybe LoneSig)
-> Measure -> LoneSigs -> (Maybe LoneSig, LoneSigs)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\ Measure
_ LoneSig
_ -> Maybe LoneSig
forall a. Maybe a
Nothing) Measure
x LoneSigs
ps
        , Measure -> Range
forall a. HasRange a => a -> Range
getRange Measure
x Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Measure -> Range
forall a. HasRange a => a -> Range
getRange Measure
x'
            -- Use the range as UID to ensure we do not replace the wrong signature.
            -- This could happen if the user wrote a duplicate definition.
        -> NiceDeclaration
axiom NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps' [NiceDeclaration]
ds
      Maybe (Measure, NiceDeclaration)
_ -> NiceDeclaration
d     NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
replaceSigs LoneSigs
ps  [NiceDeclaration]
ds

  where

    -- A @replaceable@ declaration is a signature. It has a name and we can make an
    -- @Axiom@ out of it.
    replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
    replaceable :: NiceDeclaration -> Maybe (Measure, NiceDeclaration)
replaceable = \case
      FunSig Range
r Access
acc IsAbstract
abst IsInstance
inst IsMacro
_ ArgInfo
argi TerminationCheck
_ CoverageCheck
_ Measure
x' Expr
e ->
        -- #4881: Don't use the unique NameId for NoName lookups.
        let x :: Measure
x = if Measure -> Bool
forall a. IsNoName a => a -> Bool
isNoName Measure
x' then Range -> Measure
noName (Measure -> Range
nameRange Measure
x') else Measure
x' in
        (Measure, NiceDeclaration) -> Maybe (Measure, NiceDeclaration)
forall a. a -> Maybe a
Just (Measure
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
inst ArgInfo
argi Measure
x' Expr
e)
      NiceRecSig Range
r Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Measure
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        (Measure, NiceDeclaration) -> Maybe (Measure, NiceDeclaration)
forall a. a -> Maybe a
Just (Measure
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef ArgInfo
defaultArgInfo Measure
x Expr
e)
      NiceDataSig Range
r Access
acc IsAbstract
abst PositivityCheck
_ UniverseCheck
_ Measure
x [LamBinding]
pars Expr
t ->
        let e :: Expr
e = Expr -> Expr
Generalized (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
makePi (Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r [LamBinding]
pars) Expr
t in
        (Measure, NiceDeclaration) -> Maybe (Measure, NiceDeclaration)
forall a. a -> Maybe a
Just (Measure
x, Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom Range
r Access
acc IsAbstract
abst IsInstance
NotInstanceDef ArgInfo
defaultArgInfo Measure
x Expr
e)
      NiceDeclaration
_ -> Maybe (Measure, 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 <- Nice NiceEnv
forall s (m :: * -> *). MonadState s m => m s
get
  NiceEnv -> Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (NiceEnv -> Nice ()) -> NiceEnv -> Nice ()
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 <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
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 <- (NiceEnv -> NiceWarnings) -> Nice NiceWarnings
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets NiceEnv -> NiceWarnings
niceWarn
  NiceEnv -> Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (NiceEnv -> Nice ()) -> NiceEnv -> Nice ()
forall a b. (a -> b) -> a -> b
$ NiceEnv
st { niceWarn :: NiceWarnings
niceWarn = NiceWarnings
warns }
  [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
res

  where

    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    inferMutualBlocks (NiceDeclaration
d : [NiceDeclaration]
ds) =
      case NiceDeclaration -> DeclKind
declKind NiceDeclaration
d of
        DeclKind
OtherDecl    -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds
        LoneDefs{}   -> (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
ds  -- Andreas, 2017-10-09, issue #2576: report error in ConcreteToAbstract
        LoneSigDecl Range
r DataRecOrFun
k Measure
x  -> do
          Measure
_ <- Range -> Measure -> DataRecOrFun -> Nice Measure
addLoneSig Range
r Measure
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 <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
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 NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
nds0) -- NB: don't forget the LoneSig the block started with!
          -- We then keep processing the rest of the block
          TerminationCheck
tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks (NiceDeclaration -> Range
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 ([NiceDeclaration] -> Range
forall a. HasRange a => a -> Range
getRange [NiceDeclaration]
ds0) TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc [NiceDeclaration]
ds0 NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NiceDeclaration] -> Nice [NiceDeclaration]
inferMutualBlocks [NiceDeclaration]
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 InferredMutual -> Nice InferredMutual
forall (m :: * -> *) a. Monad m => a -> m a
return (MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
checks [] [NiceDeclaration]
ds) else
            case [NiceDeclaration]
ds of
              []     -> InferredMutual -> Nice InferredMutual
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 Measure
x -> do
                  Nice Measure -> Nice ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Nice Measure -> Nice ()) -> Nice Measure -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> Measure -> DataRecOrFun -> Nice Measure
addLoneSig Range
r Measure
x DataRecOrFun
k
                  NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock  NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                LoneDefs DataRecOrFun
k [Measure]
xs -> do
                  (Measure -> Nice ()) -> [Measure] -> Nice ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Measure -> Nice ()
removeLoneSig [Measure]
xs
                  NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock  NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined (DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks) [NiceDeclaration]
ds
                DeclKind
OtherDecl -> NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual -> InferredMutual)
-> Nice InferredMutual -> Nice InferredMutual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
untilAllDefined MutualChecks
checks [NiceDeclaration]
ds

    nice :: [Declaration] -> Nice [NiceDeclaration]
    nice :: [Declaration] -> Nice [NiceDeclaration]
nice [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall (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 [NiceDeclaration] -> [NiceDeclaration] -> [NiceDeclaration]
forall a. [a] -> [a] -> [a]
++) ([NiceDeclaration] -> [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ys

    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 []     = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
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 :: DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning DeclarationWarning'
w = do
            -- NOTE: This is the location of the invoker of justWarning, not here.
            (CallStack -> Nice ()) -> Nice ()
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
-> (CallStack -> Nice ()) -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationWarning' -> CallStack -> Nice ()
declarationWarning' DeclarationWarning'
w
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
nice1 [Declaration]
ds

      case Declaration
d of

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

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

        Generalize Range
r [] -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
EmptyGeneralize Range
r
        Generalize Range
r [Declaration]
sigs -> do
          [NiceDeclaration]
gs <- [Declaration]
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declaration]
sigs ((Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration])
-> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ \case
            sig :: Declaration
sig@(TypeSig ArgInfo
info TacticAttribute
tac Measure
x Expr
t) -> do
              NiceDeclaration -> Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Measure
-> Expr
-> NiceDeclaration
NiceGeneralize (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
sig) Access
PublicAccess ArgInfo
info TacticAttribute
tac Measure
x Expr
t
            Declaration
_ -> Nice NiceDeclaration
forall a. HasCallStack => a
__IMPOSSIBLE__
          ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceDeclaration]
gs, [Declaration]
ds)

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

            -- case: clauses match exactly one of the sigs
            [(Measure
x,(Measure
x',[Declaration]
fits,[Declaration]
rest))] -> do
               -- The x'@NoName{} is the unique version of x@NoName{}.
               Measure -> Nice ()
removeLoneSig Measure
x
               [Declaration]
ds  <- [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
               [Clause]
cs  <- Measure -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Measure
x' [Declaration]
ds Bool
False
               ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Measure
-> [Clause]
-> NiceDeclaration
FunDef ([Declaration] -> Range
forall a. HasRange a => a -> Range
getRange [Declaration]
fits) [Declaration]
fits IsAbstract
ConcreteDef IsInstance
NotInstanceDef TerminationCheck
termCheck CoverageCheck
covCheck Measure
x' [Clause]
cs] , [Declaration]
rest)

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

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

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

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

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

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

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

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

        RecordDirective RecordDirective
r -> HasCallStack =>
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
InvalidRecordDirective (RecordDirective -> Range
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])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
EmptyMutual Range
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Range -> [NiceDeclaration] -> Nice NiceDeclaration
mkOldMutual Range
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))

        InterleavedMutual 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])
DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
-> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
EmptyMutual Range
r
            [Declaration]
_  -> (,[Declaration]
ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
-> Nice [NiceDeclaration]
-> Nice ([NiceDeclaration], [Declaration])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> [NiceDeclaration]
forall el coll. Singleton el coll => el -> coll
singleton (NiceDeclaration -> [NiceDeclaration])
-> Nice NiceDeclaration -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Range -> [NiceDeclaration] -> Nice NiceDeclaration
mkInterleavedMutual Range
r ([NiceDeclaration] -> Nice NiceDeclaration)
-> Nice [NiceDeclaration] -> Nice NiceDeclaration
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Declaration] -> Nice [NiceDeclaration]
nice [Declaration]
ds'))

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    nicePragma (BuiltinPragma Range
r RString
str qn :: QName
qn@(QName Measure
x)) [Declaration]
ds = do
      ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
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 = ([NiceDeclaration], [Declaration])
-> Nice ([NiceDeclaration], [Declaration])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Range -> Pragma -> NiceDeclaration
NicePragma (Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p) Pragma
p], [Declaration]
ds)

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

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

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

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

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

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

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

    -- We could add a default type signature here, but at the moment we can't
    -- infer the type of a record or datatype, so better to just fail here.
    defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
    defaultTypeSig :: DataRecOrFun -> Measure -> TacticAttribute -> Nice TacticAttribute
defaultTypeSig DataRecOrFun
k Measure
x t :: TacticAttribute
t@Just{} = TacticAttribute -> Nice TacticAttribute
forall (m :: * -> *) a. Monad m => a -> m a
return TacticAttribute
t
    defaultTypeSig DataRecOrFun
k Measure
x TacticAttribute
Nothing  = do
      Nice (Maybe DataRecOrFun)
-> Nice TacticAttribute
-> (DataRecOrFun -> Nice TacticAttribute)
-> Nice TacticAttribute
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Measure -> Nice (Maybe DataRecOrFun)
getSig Measure
x) (TacticAttribute -> Nice TacticAttribute
forall (m :: * -> *) a. Monad m => a -> m a
return TacticAttribute
forall a. Maybe a
Nothing) ((DataRecOrFun -> Nice TacticAttribute) -> Nice TacticAttribute)
-> (DataRecOrFun -> Nice TacticAttribute) -> Nice TacticAttribute
forall a b. (a -> b) -> a -> b
$ \ DataRecOrFun
k' -> do
        Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (DataRecOrFun -> DataRecOrFun -> Bool
sameKind DataRecOrFun
k DataRecOrFun
k') (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Measure -> DataRecOrFun -> DataRecOrFun -> DeclarationException'
WrongDefinition Measure
x DataRecOrFun
k' DataRecOrFun
k
        TacticAttribute
forall a. Maybe a
Nothing TacticAttribute -> Nice () -> Nice TacticAttribute
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Measure -> Nice ()
removeLoneSig Measure
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 :: PositivityCheck
-> UniverseCheck
-> (Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Measure
    -> [LamBinding]
    -> [decl]
    -> NiceDeclaration)
-> (Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Measure
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration)
-> ([a] -> Nice [decl])
-> Range
-> Measure
-> Maybe ([LamBinding], Expr)
-> Maybe ([LamBinding], [a])
-> Nice [NiceDeclaration]
dataOrRec PositivityCheck
pc UniverseCheck
uc Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig [a] -> Nice [decl]
niceD Range
r Measure
x Maybe ([LamBinding], Expr)
mt Maybe ([LamBinding], [a])
mcs = do
      Maybe ([LamBinding], [decl])
mds <- Maybe ([LamBinding], [a])
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
Trav.forM Maybe ([LamBinding], [a])
mcs ((([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
 -> Nice (Maybe ([LamBinding], [decl])))
-> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
-> Nice (Maybe ([LamBinding], [decl]))
forall a b. (a -> b) -> a -> b
$ \ ([LamBinding]
tel, [a]
cs) -> ([LamBinding]
tel,) ([decl] -> ([LamBinding], [decl]))
-> Nice [decl] -> Nice ([LamBinding], [decl])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Nice [decl]
niceD [a]
cs
      -- We set origin to UserWritten if the user split the data/rec herself,
      -- and to Inserted if the she wrote a single declaration that we're
      -- splitting up here. We distinguish these because the scoping rules for
      -- generalizable variables differ in these cases.
      let o :: Origin
o | Maybe ([LamBinding], Expr) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], Expr)
mt Bool -> Bool -> Bool
&& Maybe ([LamBinding], [a]) -> Bool
forall a. Maybe a -> Bool
isJust Maybe ([LamBinding], [a])
mcs = Origin
Inserted
            | Bool
otherwise               = Origin
UserWritten
      [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return ([NiceDeclaration] -> Nice [NiceDeclaration])
-> [NiceDeclaration] -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ [Maybe NiceDeclaration] -> [NiceDeclaration]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe NiceDeclaration] -> [NiceDeclaration])
-> [Maybe NiceDeclaration] -> [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$
        [ Maybe ([LamBinding], Expr)
mt  Maybe ([LamBinding], Expr)
-> (([LamBinding], Expr) -> NiceDeclaration)
-> Maybe NiceDeclaration
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ([LamBinding]
tel, Expr
t)  -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
mkSig (Measure -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Measure
x Expr
t) Access
PublicAccess IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
tel Expr
t
        , Maybe ([LamBinding], [decl])
mds Maybe ([LamBinding], [decl])
-> (([LamBinding], [decl]) -> NiceDeclaration)
-> Maybe NiceDeclaration
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ ([LamBinding]
tel, [decl]
ds) -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> [decl]
-> NiceDeclaration
mkDef Range
r Origin
o IsAbstract
ConcreteDef PositivityCheck
pc UniverseCheck
uc Measure
x (Maybe ([LamBinding], Expr)
-> [LamBinding]
-> (([LamBinding], Expr) -> [LamBinding])
-> [LamBinding]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ([LamBinding], Expr)
mt [LamBinding]
tel ((([LamBinding], Expr) -> [LamBinding]) -> [LamBinding])
-> (([LamBinding], Expr) -> [LamBinding]) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. a -> b -> a
const ([LamBinding] -> ([LamBinding], Expr) -> [LamBinding])
-> [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
tel) [decl]
ds
          -- If a type is given (mt /= Nothing), we have to delete the types in @tel@
          -- for the data definition, lest we duplicate them. And also drop modalities (#1886).
        ]
    -- Translate axioms
    niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
    niceAxioms :: KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
b [Declaration]
ds = [[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[NiceDeclaration]] -> [NiceDeclaration])
-> Nice [[NiceDeclaration]] -> Nice [NiceDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> Nice [NiceDeclaration])
-> [Declaration] -> Nice [[NiceDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
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 Measure
x Expr
t) -> do
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
NotInstanceDef ArgInfo
rel Measure
x Expr
t ]
      d :: Declaration
d@(FieldSig IsInstance
i TacticAttribute
tac Measure
x Arg Expr
argt) | KindOfBlock
b KindOfBlock -> KindOfBlock -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfBlock
FieldBlock -> do
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Measure
-> Arg Expr
-> NiceDeclaration
NiceField (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d) Access
PublicAccess IsAbstract
ConcreteDef IsInstance
i TacticAttribute
tac Measure
x Arg Expr
argt ]
      InstanceB Range
r [Declaration]
decls -> do
        Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
instanceBlock Range
r ([NiceDeclaration] -> Nice [NiceDeclaration])
-> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
niceAxioms KindOfBlock
InstanceBlock [Declaration]
decls
      Pragma p :: Pragma
p@(RewritePragma Range
r Range
_ [QName]
_) -> do
        [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Pragma -> NiceDeclaration
NicePragma Range
r Pragma
p ]
      Declaration
d -> DeclarationException' -> Nice [NiceDeclaration]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice [NiceDeclaration])
-> DeclarationException' -> Nice [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ KindOfBlock -> Range -> DeclarationException'
WrongContentBlock KindOfBlock
b (Range -> DeclarationException') -> Range -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d

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

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

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


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

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

    mkClauses Measure
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
catchall
      | [WithExpr] -> Bool
forall a. Null a => a -> Bool
null (LHS -> [WithExpr]
lhsWithExpr LHS
lhs) Bool -> Bool -> Bool
|| LHS -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis LHS
lhs  =
      (Measure -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Measure
x (Bool
ca Bool -> Bool -> Bool
|| Bool
catchall) LHS
lhs RHS
rhs WhereClause
wh [] Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
:) ([Clause] -> [Clause]) -> Nice [Clause] -> Nice [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Measure -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Measure
x [Declaration]
cs Bool
False   -- Will result in an error later.

    mkClauses Measure
x (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca : [Declaration]
cs) Bool
catchall = do
      Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Declaration] -> Bool
forall a. Null a => a -> Bool
null [Declaration]
withClauses) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Measure -> LHS -> DeclarationException'
MissingWithClauses Measure
x LHS
lhs
      [Clause]
wcs <- Measure -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Measure
x [Declaration]
withClauses Bool
False
      (Measure -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Measure
x (Bool
ca Bool -> Bool -> Bool
|| Bool
catchall) LHS
lhs RHS
rhs WhereClause
wh [Clause]
wcs Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
:) ([Clause] -> [Clause]) -> Nice [Clause] -> Nice [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Measure -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Measure
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 = Pattern -> Int
forall p. CPatternLike p => p -> Int
numberOfWithPatterns Pattern
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [WithExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((WithExpr -> Bool) -> [WithExpr] -> [WithExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter WithExpr -> Bool
forall a. LensHiding a => a -> Bool
visible [WithExpr]
es) where LHS Pattern
p [RewriteEqn]
_ [WithExpr]
es = LHS
lhs

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

    couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf :: Maybe Fixity' -> Measure -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Measure
x Pattern
p =
      let
      pns :: [Measure]
pns        = Pattern -> [Measure]
patternNames Pattern
p
      xStrings :: [String]
xStrings   = Measure -> [String]
nameStringParts Measure
x
      patStrings :: [String]
patStrings = (Measure -> [String]) -> [Measure] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure -> [String]
nameStringParts [Measure]
pns
      in
--          trace ("x = " ++ prettyShow x) $
--          trace ("pns = " ++ show pns) $
--          trace ("xStrings = " ++ show xStrings) $
--          trace ("patStrings = " ++ show patStrings) $
--          trace ("mFixity = " ++ show mFixity) $
      case ([Measure] -> Maybe Measure
forall a. [a] -> Maybe a
listToMaybe [Measure]
pns, Maybe Fixity'
mFixity) of
        -- first identifier in the patterns is the fun.symbol?
        (Just Measure
y, Maybe Fixity'
_) | Measure
x Measure -> Measure -> Bool
forall a. Eq a => a -> a -> Bool
== Measure
y -> Bool
True -- trace ("couldBe since y = " ++ prettyShow y) $ True
        -- are the parts of x contained in p
        (Maybe Measure, Maybe Fixity')
_ | [String]
xStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` [String]
patStrings -> Bool
True -- trace ("couldBe since isSublistOf") $ True
        -- looking for a mixfix fun.symb
        (Maybe Measure
_, Just Fixity'
fix) ->  -- also matches in case of a postfix
           let notStrings :: [String]
notStrings = Notation -> [String]
stringParts (Fixity' -> Notation
theNotation Fixity'
fix)
           in  -- trace ("notStrings = " ++ show notStrings) $
               -- trace ("patStrings = " ++ show patStrings) $
               Bool -> Bool
not ([String] -> Bool
forall a. Null a => a -> Bool
null [String]
notStrings) Bool -> Bool -> Bool
&& ([String]
notStrings [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` [String]
patStrings)
        -- not a notation, not first id: give up
        (Maybe Measure, 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'
-> Measure -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf Maybe Fixity'
mf Measure
n (NiceFunClause Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
cc Bool
_ Declaration
d)
      = ([TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] [], Declaration
d) (MutualChecks, Declaration)
-> Maybe () -> Maybe (MutualChecks, Declaration)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Maybe Fixity' -> Measure -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mf Measure
n Declaration
d)
    couldBeNiceFunClauseOf Maybe Fixity'
_ Measure
_ NiceDeclaration
_ = Maybe (MutualChecks, Declaration)
forall a. Maybe a
Nothing

    -- for finding clauses for a type sig in mutual blocks
    couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
    couldBeFunClauseOf :: Maybe Fixity' -> Measure -> Declaration -> Bool
couldBeFunClauseOf Maybe Fixity'
mFixity Measure
x (Pragma (CatchallPragma{})) = Bool
True
    couldBeFunClauseOf Maybe Fixity'
mFixity Measure
x (FunClause (LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_) RHS
_ WhereClause
_ Bool
_) =
       Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p Bool -> Bool -> Bool
|| Maybe Fixity' -> Measure -> Pattern -> Bool
couldBeCallOf Maybe Fixity'
mFixity Measure
x Pattern
p
    couldBeFunClauseOf Maybe Fixity'
_ Measure
_ 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
_)) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> (InterleavedMutual, MutualChecks, Int)
-> Nice
     ([(Int, NiceDeclaration)], (InterleavedMutual, MutualChecks, Int))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
ds') (InterleavedMutual
forall a. Null a => a
empty, MutualChecks
forall a. Monoid a => a
mempty, Int
0)
      let idecls :: [(Int, NiceDeclaration)]
idecls = [(Int, NiceDeclaration)]
other [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++ ((Measure, InterleavedDecl) -> [(Int, NiceDeclaration)])
-> [(Measure, InterleavedDecl)] -> [(Int, NiceDeclaration)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Measure -> InterleavedDecl -> [(Int, NiceDeclaration)])
-> (Measure, InterleavedDecl) -> [(Int, NiceDeclaration)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Measure -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl) (InterleavedMutual -> [(Measure, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m)
      let decls0 :: [NiceDeclaration]
decls0 = ((Int, NiceDeclaration) -> NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map (Int, NiceDeclaration) -> NiceDeclaration
forall a b. (a, b) -> b
snd ([(Int, NiceDeclaration)] -> [NiceDeclaration])
-> [(Int, NiceDeclaration)] -> [NiceDeclaration]
forall a b. (a -> b) -> a -> b
$ ((Int, NiceDeclaration) -> (Int, NiceDeclaration) -> Ordering)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, NiceDeclaration) -> Int)
-> (Int, NiceDeclaration)
-> (Int, NiceDeclaration)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, NiceDeclaration) -> Int
forall a b. (a, b) -> a
fst) [(Int, NiceDeclaration)]
idecls
      LoneSigs
ps <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
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)
      NiceDeclaration -> Nice NiceDeclaration
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
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 :: Measure
-> (Int -> a)
-> MutualChecks
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
addType Measure
n Int -> a
c MutualChecks
mc = do
          (Map Measure a
m, MutualChecks
checks, Int
i) <- StateT
  (Map Measure a, MutualChecks, Int)
  Nice
  (Map Measure a, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
          Bool
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> Maybe a -> Bool
forall a b. (a -> b) -> a -> b
$ Measure -> Map Measure a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Measure
n Map Measure a
m) (StateT (Map Measure a, MutualChecks, Int) Nice ()
 -> StateT (Map Measure a, MutualChecks, Int) Nice ())
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ Nice () -> StateT (Map Measure a, MutualChecks, Int) Nice ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> StateT (Map Measure a, MutualChecks, Int) Nice ())
-> Nice () -> StateT (Map Measure a, MutualChecks, Int) Nice ()
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice ()
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException (DeclarationException' -> Nice ())
-> DeclarationException' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Measure -> DeclarationException'
DuplicateDefinition Measure
n
          (Map Measure a, MutualChecks, Int)
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Measure -> a -> Map Measure a -> Map Measure a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Measure
n (Int -> a
c Int
i) Map Measure a
m, MutualChecks
mc MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
iInt -> Int -> Int
forall 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 Measure
n Expr
_) = do
           let checks :: MutualChecks
checks = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [TerminationCheck
tc] [CoverageCheck
cc] []
           Measure
-> (Int -> InterleavedDecl)
-> MutualChecks
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a.
Measure
-> (Int -> a)
-> MutualChecks
-> StateT (Map Measure a, MutualChecks, Int) Nice ()
addType Measure
n (\ Int
i -> Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i NiceDeclaration
d Maybe (Int, List1 ([Declaration], [Clause]))
forall a. Maybe a
Nothing) MutualChecks
checks
        addFunType NiceDeclaration
_ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

        addFunClauses :: 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) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  (InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get
          let sigs :: [Measure]
sigs = ((Measure, InterleavedDecl) -> Maybe Measure)
-> [(Measure, InterleavedDecl)] -> [Measure]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (Measure
n, InterleavedDecl
d) -> Measure
n Measure -> Maybe () -> Maybe Measure
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedDecl
d) ([(Measure, InterleavedDecl)] -> [Measure])
-> [(Measure, InterleavedDecl)] -> [Measure]
forall a b. (a -> b) -> a -> b
$ InterleavedMutual -> [(Measure, InterleavedDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList InterleavedMutual
m
          -- find the funsig candidates for the funclause of interest
          case [ (Measure
x, Prefix (MutualChecks, Declaration)
fits, [NiceDeclaration]
rest)
               | Measure
x <- [Measure]
sigs
               , let (Prefix (MutualChecks, Declaration)
fits, [NiceDeclaration]
rest) = (NiceDeclaration -> Maybe (MutualChecks, Declaration))
-> [NiceDeclaration]
-> (Prefix (MutualChecks, Declaration), [NiceDeclaration])
forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
spanJust (Maybe Fixity'
-> Measure -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
couldBeNiceFunClauseOf (Measure -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Measure
x Fixities
fixs) Measure
x) (NiceDeclaration
nd NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds)
               , Bool -> Bool
not (Prefix (MutualChecks, Declaration) -> Bool
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] []
              (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
check MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
              ((Int
i,NiceDeclaration
nd) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
:) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
ds
            -- exactly one candidate: attach the funclause to the definition
            [(Measure
n, Prefix (MutualChecks, Declaration)
fits0, [NiceDeclaration]
rest)] -> do
              let ([MutualChecks]
checkss, [Declaration]
fits) = Prefix (MutualChecks, Declaration)
-> ([MutualChecks], [Declaration])
forall a b. [(a, b)] -> ([a], [b])
unzip Prefix (MutualChecks, Declaration)
fits0
              [Declaration]
ds <- Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [Declaration]
 -> StateT
      (InterleavedMutual, MutualChecks, Int) Nice [Declaration])
-> Nice [Declaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Nice [Declaration]
expandEllipsis [Declaration]
fits
              [Clause]
cs <- Nice [Clause]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [Clause]
 -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause])
-> Nice [Clause]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause]
forall a b. (a -> b) -> a -> b
$ Measure -> [Declaration] -> Bool -> Nice [Clause]
mkClauses Measure
n [Declaration]
ds Bool
False
              case Measure -> InterleavedMutual -> Maybe InterleavedDecl
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Measure
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) ([Declaration], [Clause])
-> [([Declaration], [Clause])] -> List1 ([Declaration], [Clause])
forall a. a -> [a] -> NonEmpty a
:| [] ), Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
                        Just (Int
i1, List1 ([Declaration], [Clause])
cs1) -> ((Int
i1, ([Declaration]
fits,[Clause]
cs) ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
-> List1 ([Declaration], [Clause])
forall a. a -> NonEmpty a -> NonEmpty a
<| List1 ([Declaration], [Clause])
cs1), Int
i)
                  let checks' :: MutualChecks
checks' = [MutualChecks] -> MutualChecks
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [MutualChecks]
checkss
                  (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Measure
-> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Measure
n (Int
-> NiceDeclaration
-> Maybe (Int, List1 ([Declaration], [Clause]))
-> InterleavedDecl
InterleavedFun Int
i0 NiceDeclaration
sig ((Int, List1 ([Declaration], [Clause]))
-> Maybe (Int, List1 ([Declaration], [Clause]))
forall a. a -> Maybe a
Just (Int, List1 ([Declaration], [Clause]))
cs')) InterleavedMutual
m, MutualChecks
checks' MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
<> MutualChecks
checks, Int
i')
                Maybe InterleavedDecl
_ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall a. HasCallStack => a
__IMPOSSIBLE__
              Range
-> [NiceDeclaration]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
groupByBlocks Range
r [NiceDeclaration]
rest
            -- more than one candidate: fail, complaining about the ambiguity!
            (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf:[(Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs -> Nice [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> Nice [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a. HasCallStack => DeclarationException' -> Nice a
declarationException
                           (DeclarationException' -> Nice [(Int, NiceDeclaration)])
-> DeclarationException' -> Nice [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ LHS -> List1 Measure -> DeclarationException'
AmbiguousFunClauses LHS
lhs
                           (List1 Measure -> DeclarationException')
-> List1 Measure -> DeclarationException'
forall a b. (a -> b) -> a -> b
$ List1 Measure -> List1 Measure
forall a. NonEmpty a -> NonEmpty a
List1.reverse (List1 Measure -> List1 Measure) -> List1 Measure -> List1 Measure
forall a b. (a -> b) -> a -> b
$ ((Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
 -> Measure)
-> NonEmpty
     (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Measure
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Measure
a,Prefix (MutualChecks, Declaration)
_,[NiceDeclaration]
_) -> Measure
a) (NonEmpty
   (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
 -> List1 Measure)
-> NonEmpty
     (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> List1 Measure
forall a b. (a -> b) -> a -> b
$ (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
xf (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
-> [(Measure, Prefix (MutualChecks, Declaration),
     [NiceDeclaration])]
-> NonEmpty
     (Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])
forall a. a -> [a] -> NonEmpty a
:| [(Measure, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
xfs
        addFunClauses Range
_ [NiceDeclaration]
_ = StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, 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 []       = [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
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 StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> ([(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [(Int, NiceDeclaration)]
ns -> ([(Int, NiceDeclaration)]
ns [(Int, NiceDeclaration)]
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. [a] -> [a] -> [a]
++) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (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
_ Measure
n [LamBinding]
_ [NiceDeclaration]
ds -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Measure
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Measure -> Maybe Measure
forall a. a -> Maybe a
Just Measure
n) [NiceDeclaration]
ds
            NiceLoneConstructor Range
r [NiceDeclaration]
ds     -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Range
-> Maybe Measure
-> [NiceDeclaration]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
addDataConstructors Maybe Range
forall a. Maybe a
Nothing Maybe Measure
forall a. Maybe a
Nothing [NiceDeclaration]
ds
            FunSig{}                     -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (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
_ Measure
n [Clause]
cs
                      | Bool -> Bool
not (Measure -> Bool
forall a. IsNoName a => a -> Bool
isNoName Measure
n) -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ [] [(Int, NiceDeclaration)]
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall (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
dNiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
:[NiceDeclaration]
ds)
            -- We do not need to worry about RecSig vs. RecDef: we know there's exactly one
            -- of each for record definitions and leaving them in place should be enough!
            NiceDeclaration
_ -> StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
oneOff (StateT
   (InterleavedMutual, MutualChecks, Int)
   Nice
   [(Int, NiceDeclaration)]
 -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)])
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
forall a b. (a -> b) -> a -> b
$ do
              (InterleavedMutual
m, MutualChecks
c, Int
i) <- StateT
  (InterleavedMutual, MutualChecks, Int)
  Nice
  (InterleavedMutual, MutualChecks, Int)
forall s (m :: * -> *). MonadState s m => m s
get -- TODO: grab checks from c?
              (InterleavedMutual, MutualChecks, Int)
-> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (InterleavedMutual
m, MutualChecks
c, Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
              [(Int, NiceDeclaration)]
-> StateT
     (InterleavedMutual, MutualChecks, Int)
     Nice
     [(Int, NiceDeclaration)]
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 :: [Measure] -> NiceDeclaration -> Either (Measure, [Measure]) Measure
isConstructor [Measure]
ns (Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Measure
n Expr
e)
       -- extract the return type & see it as an LHS-style pattern
       | Just Pattern
p <- Expr -> Pattern
exprToPatternWithHoles (Expr -> Pattern) -> TacticAttribute -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TacticAttribute
returnExpr Expr
e =
         case [ Measure
x | Measure
x <- [Measure]
ns
                  , Maybe Fixity' -> Measure -> Pattern -> Bool
couldBeCallOf (Measure -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Measure
x Fixities
fixs) Measure
x Pattern
p
                  ] of
           [Measure
x] -> Measure -> Either (Measure, [Measure]) Measure
forall a b. b -> Either a b
Right Measure
x
           [Measure]
xs  -> (Measure, [Measure]) -> Either (Measure, [Measure]) Measure
forall a b. a -> Either a b
Left (Measure
n, [Measure]
xs)
       -- which may fail (e.g. if the "return type" is a hole
       | Bool
otherwise = (Measure, [Measure]) -> Either (Measure, [Measure]) Measure
forall a b. a -> Either a b
Left (Measure
n, [])
    isConstructor [Measure]
_ NiceDeclaration
_ = Either (Measure, [Measure]) Measure
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, Measure, DataRecOrFun)] -> LoneSigs
loneSigsFromLoneNames [(Range, Measure, 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) <- [NiceDeclaration]
-> (NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall (m :: * -> *) a b c d.
Applicative m =>
[a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
forEither3M [NiceDeclaration]
ds ((NiceDeclaration
  -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
 -> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration]))
-> (NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
-> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
forall a b. (a -> b) -> a -> b
$ \ NiceDeclaration
d -> do
          let top :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top       = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. a -> Either3 a b c
In1 NiceDeclaration
d)
              bottom :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom    = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. b -> Either3 a b c
In2 NiceDeclaration
d)
              invalid :: String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
s = NiceDeclaration
-> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
forall a b c. c -> Either3 a b c
In3 NiceDeclaration
d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
-> Nice ()
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> String -> DeclarationWarning'
NotAllowedInMutual (NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d) String
s
          case NiceDeclaration
d of
            -- Andreas, 2013-11-23 allow postulates in mutual blocks
            Axiom{}             -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceField{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            PrimitiveFunction{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            -- Andreas, 2019-07-23 issue #3932:
            -- Nested mutual blocks are not supported.
            NiceMutual{}        -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"mutual blocks"
            -- Andreas, 2018-10-29, issue #3246
            -- We could allow modules (top), but this is potentially confusing.
            NiceModule{}        -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Module definitions"
            -- Lone constructors are only allowed in new-style mutual blocks
            NiceLoneConstructor{} -> String
-> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
invalid String
"Lone constructors"
            NiceModuleMacro{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceOpen{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceImport{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceRecSig{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceDataSig{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
            -- in ConcreteToAbstract rather than here.
            NiceFunClause{}     -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            FunSig{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            FunDef{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceDataDef{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceRecDef{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            -- Andreas, 2018-05-11, issue #3051, allow pat.syn.s in mutual blocks
            -- Andreas, 2018-10-29: We shift pattern synonyms to the bottom
            -- since they might refer to constructors defined in a data types
            -- just above them.
            NicePatternSyn{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            NiceGeneralize{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceUnquoteDecl{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
top
            NiceUnquoteDef{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
bottom
            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

              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{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              TerminationCheckPragma{}  -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoPositivityCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              PolarityPragma{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoUniverseCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__
              NoCoverageCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

        -- Compute termination checking flag for mutual block
        TerminationCheck
tc0 <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' TerminationCheck NiceEnv
terminationCheckPragma
        let tcs :: [TerminationCheck]
tcs = (NiceDeclaration -> TerminationCheck)
-> [NiceDeclaration] -> [TerminationCheck]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> TerminationCheck
termCheck [NiceDeclaration]
ds
        TerminationCheck
tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
combineTerminationChecks Range
r (TerminationCheck
tc0TerminationCheck -> [TerminationCheck] -> [TerminationCheck]
forall a. a -> [a] -> [a]
:[TerminationCheck]
tcs)

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

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

        NiceDeclaration -> Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> TerminationCheck
-> CoverageCheck
-> PositivityCheck
-> [NiceDeclaration]
-> NiceDeclaration
NiceMutual Range
r TerminationCheck
tc CoverageCheck
cc PositivityCheck
pc ([NiceDeclaration] -> NiceDeclaration)
-> [NiceDeclaration] -> NiceDeclaration
forall a b. (a -> b) -> a -> b
$ [NiceDeclaration]
top [NiceDeclaration] -> [NiceDeclaration] -> [NiceDeclaration]
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, Measure, DataRecOrFun)]
sigNames  = [ (Range
r, Measure
x, DataRecOrFun
k) | LoneSigDecl Range
r DataRecOrFun
k Measure
x <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds' ]
        defNames :: [(Measure, DataRecOrFun)]
defNames  = [ (Measure
x, DataRecOrFun
k) | LoneDefs DataRecOrFun
k [Measure]
xs <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> DeclKind
declKind [NiceDeclaration]
ds', Measure
x <- [Measure]
xs ]
        -- compute the set difference with equality just on names
        loneNames :: [(Range, Measure, DataRecOrFun)]
loneNames = [ (Range
r, Measure
x, DataRecOrFun
k) | (Range
r, Measure
x, DataRecOrFun
k) <- [(Range, Measure, DataRecOrFun)]
sigNames, ((Measure, DataRecOrFun) -> Bool)
-> [(Measure, DataRecOrFun)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all ((Measure
x Measure -> Measure -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Measure -> Bool)
-> ((Measure, DataRecOrFun) -> Measure)
-> (Measure, DataRecOrFun)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Measure, DataRecOrFun) -> Measure
forall a b. (a, b) -> a
fst) [(Measure, 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
_ Measure
_ Expr
_)      = TerminationCheck
tc
        termCheck (FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
tc CoverageCheck
_ Measure
_ [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
_ [Measure]
_ Expr
_) = TerminationCheck
tc
        termCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
tc CoverageCheck
_ [Measure]
_ Expr
_)    = TerminationCheck
tc
        termCheck Axiom{}             = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceField{}         = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck PrimitiveFunction{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModule{}        = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceModuleMacro{}   = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceOpen{}          = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceImport{}        = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NicePragma{}        = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecSig{}        = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataSig{}       = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceFunClause{}     = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceDataDef{}       = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceRecDef{}        = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NicePatternSyn{}    = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceGeneralize{}    = TerminationCheck
forall m. TerminationCheck m
TerminationCheck
        termCheck NiceLoneConstructor{} = TerminationCheck
forall m. TerminationCheck m
TerminationCheck

        covCheck :: NiceDeclaration -> CoverageCheck
        covCheck :: NiceDeclaration -> CoverageCheck
covCheck (FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
cc Measure
_ Expr
_)      = CoverageCheck
cc
        covCheck (FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
cc Measure
_ [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 [Measure]
_ Expr
_) = CoverageCheck
cc
        covCheck (NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
cc [Measure]
_ 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

        -- 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
_ Measure
_ [LamBinding]
_ [NiceDeclaration]
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Measure
_ [LamBinding]
_ Expr
_) = PositivityCheck
pc
        positivityCheckOldMutual (NiceMutual Range
_ TerminationCheck
_ CoverageCheck
_ PositivityCheck
pc [NiceDeclaration]
_)        = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Measure
_ [LamBinding]
_ Expr
_)  = PositivityCheck
pc
        positivityCheckOldMutual (NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
pc UniverseCheck
_ Measure
_ 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
_ [] = [a] -> Nice [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    abstractBlock Range
r [a]
ds = do
      ([a]
ds', Bool
anyChange) <- ChangeT Nice [a] -> Nice ([a], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [a] -> Nice ([a], Bool))
-> ChangeT Nice [a] -> Nice ([a], Bool)
forall a b. (a -> b) -> a -> b
$ UpdaterT Nice [a]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [a]
ds
      let inherited :: Bool
inherited = Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
forall a. Range' a
noRange
      if Bool
anyChange then [a] -> Nice [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds' else do
        -- hack to avoid failing on inherited abstract blocks in where clauses
        Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
inherited (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
UselessAbstract Range
r
        [a] -> Nice [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds -- no change!

    privateBlock :: Range -> Origin -> [a] -> Nice [a]
privateBlock Range
_ Origin
_ [] = [a] -> Nice [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    privateBlock Range
r Origin
o [a]
ds = do
      ([a]
ds', Bool
anyChange) <- ChangeT Nice [a] -> Nice ([a], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT Nice [a] -> Nice ([a], Bool))
-> ChangeT Nice [a] -> Nice ([a], Bool)
forall a b. (a -> b) -> a -> b
$ Origin -> UpdaterT Nice [a]
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [a]
ds
      if Bool
anyChange then [a] -> Nice [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ds' else do
        Bool -> Nice () -> Nice ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Origin
o Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
UserWritten) (Nice () -> Nice ()) -> Nice () -> Nice ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
UselessPrivate Range
r
        [a] -> Nice [a]
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
_ [] = [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    instanceBlock Range
r [NiceDeclaration]
ds = do
      let ([NiceDeclaration]
ds', Bool
anyChange) = Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a. Change a -> (a, Bool)
runChange (Change [NiceDeclaration] -> ([NiceDeclaration], Bool))
-> Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance Range
r) [NiceDeclaration]
ds
      if Bool
anyChange then [NiceDeclaration] -> Nice [NiceDeclaration]
forall (m :: * -> *) a. Monad m => a -> m a
return [NiceDeclaration]
ds' else do
        HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
UselessInstance Range
r
        [NiceDeclaration] -> Nice [NiceDeclaration]
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 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance Range
r0 = \case
        Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Measure
x Expr
e          -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Measure
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
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 Measure
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Measure
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Measure
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
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 [Measure]
x Expr
e -> (\ IsInstance
i -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Measure]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
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 ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance Range
r0) [NiceDeclaration]
ds
        NiceLoneConstructor Range
r [NiceDeclaration]
ds       -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r ([NiceDeclaration] -> NiceDeclaration)
-> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
-> [NiceDeclaration] -> Change [NiceDeclaration]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
mkInstance Range
r0) [NiceDeclaration]
ds
        d :: NiceDeclaration
d@NiceFunClause{}              -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Measure
x [Clause]
cs     -> (\ IsInstance
i -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Measure
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Measure
x [Clause]
cs) (IsInstance -> NiceDeclaration)
-> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Updater IsInstance
setInstance Range
r0 IsInstance
i
        d :: NiceDeclaration
d@NiceField{}                  -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d  -- Field instance are handled by the parser
        d :: NiceDeclaration
d@PrimitiveFunction{}          -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceUnquoteDef{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecSig{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataSig{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModuleMacro{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceModule{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePragma{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceOpen{}                   -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceImport{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceDataDef{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceRecDef{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NicePatternSyn{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        d :: NiceDeclaration
d@NiceGeneralize{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
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{} -> Updater IsInstance
forall (m :: * -> *) a. Monad m => a -> m a
return IsInstance
i
      IsInstance
_               -> Updater IsInstance
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty Updater IsInstance -> Updater IsInstance
forall a b. (a -> b) -> a -> b
$ Range -> IsInstance
InstanceDef Range
r0

    macroBlock :: p -> t NiceDeclaration -> Nice (t NiceDeclaration)
macroBlock p
r t NiceDeclaration
ds = (NiceDeclaration -> Nice NiceDeclaration)
-> t NiceDeclaration -> Nice (t NiceDeclaration)
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 Measure
x Expr
e -> NiceDeclaration -> Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return (NiceDeclaration -> Nice NiceDeclaration)
-> NiceDeclaration -> Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Measure
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
MacroDef ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Measure
x Expr
e
        d :: NiceDeclaration
d@FunDef{}                     -> NiceDeclaration -> Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
        NiceDeclaration
d                              -> DeclarationException' -> Nice NiceDeclaration
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 = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a' -> ChangeT Nice a'
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract

instance MakeAbstract a => MakeAbstract [a]

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

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

instance MakeAbstract NiceDeclaration where
  mkAbstract :: UpdaterT Nice NiceDeclaration
mkAbstract = \case
      NiceMutual 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 ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
      NiceLoneConstructor Range
r [NiceDeclaration]
ds         -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
ds
      FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Measure
x [Clause]
cs       -> (\ IsAbstract
a -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Measure
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Measure
x) (IsAbstract -> [Clause] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([Clause] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [Clause]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [Clause]
cs
      NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ps [NiceDeclaration]
cs  -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ps) (IsAbstract -> [NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice IsAbstract
-> ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UpdaterT Nice [NiceDeclaration]
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract [NiceDeclaration]
cs
      NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x RecordDirectives
dir [LamBinding]
ps [Declaration]
cs -> (\ IsAbstract
a -> Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> NiceDeclaration
NiceRecDef Range
r Origin
o IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x RecordDirectives
dir [LamBinding]
ps [Declaration]
cs) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a
      NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d  -> (\ IsAbstract
a -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> Bool
-> Declaration
-> NiceDeclaration
NiceFunClause Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc Bool
catchall Declaration
d) (IsAbstract -> NiceDeclaration)
-> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UpdaterT Nice IsAbstract
forall a. MakeAbstract a => UpdaterT Nice a
mkAbstract IsAbstract
a
      -- The following declarations have an @InAbstract@ field
      -- but are not really definitions, so we do count them into
      -- the declarations which can be made abstract
      -- (thus, do not notify progress with @dirty@).
      Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Measure
x Expr
e          -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom             Range
r Access
p IsAbstract
AbstractDef IsInstance
i ArgInfo
rel Measure
x Expr
e
      FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Measure
x Expr
e -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Measure
-> Expr
-> NiceDeclaration
FunSig            Range
r Access
p IsAbstract
AbstractDef IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Measure
x Expr
e
      NiceRecSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t  -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig        Range
r Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t
      NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig       Range
r Access
p IsAbstract
AbstractDef PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t
      NiceField Range
r Access
p IsAbstract
_ IsInstance
i TacticAttribute
tac Measure
x Arg Expr
e      -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Measure
-> Arg Expr
-> NiceDeclaration
NiceField         Range
r Access
p IsAbstract
AbstractDef IsInstance
i TacticAttribute
tac Measure
x Arg Expr
e
      PrimitiveFunction Range
r Access
p IsAbstract
_ Measure
x Arg Expr
e    -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
forall a b. (a -> b) -> a -> b
$ Range
-> Access -> IsAbstract -> Measure -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
AbstractDef Measure
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 [Measure]
x Expr
e -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Measure]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
AbstractDef IsInstance
i TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e
      NiceUnquoteDef Range
r Access
p IsAbstract
_ TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e    -> ChangeT Nice ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Measure]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
AbstractDef TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e
      d :: NiceDeclaration
d@NiceModule{}                 -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceModuleMacro{}            -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePragma{}                 -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        Maybe Range -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
directives) ((Range -> ChangeT Nice ()) -> ChangeT Nice ())
-> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$ Nice () -> ChangeT Nice ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ())
-> (Range -> Nice ()) -> Range -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (Range -> DeclarationWarning') -> Range -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> DeclarationWarning'
OpenPublicAbstract
        UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                 -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NicePatternSyn{}             -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceGeneralize{}             -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

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

-- | Contents of a @where@ clause are abstract if the parent is.
instance MakeAbstract WhereClause where
  mkAbstract :: UpdaterT Nice WhereClause
mkAbstract  WhereClause
NoWhere             = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ WhereClause
forall decls. WhereClause' decls
NoWhere
  mkAbstract (AnyWhere Range
r [Declaration]
ds)      = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> [Declaration] -> WhereClause
forall decls. Range -> decls -> WhereClause' decls
AnyWhere Range
r [Range -> [Declaration] -> Declaration
Abstract Range
forall a. Range' a
noRange [Declaration]
ds]
  mkAbstract (SomeWhere Range
r Measure
m Access
a [Declaration]
ds) = UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
forall a b. (a -> b) -> a -> b
$ Range -> Measure -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Measure -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Measure
m Access
a [Range -> [Declaration] -> Declaration
Abstract Range
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 = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a'))
-> (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
forall a b. (a -> b) -> a -> b
$ Origin -> a' -> ChangeT Nice a'
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{} -> UpdaterT Nice Access
forall (m :: * -> *) a. Monad m => a -> m a
return Access
p  -- OR? return $ PrivateAccess o
    Access
_                 -> UpdaterT Nice Access
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Nice Access -> UpdaterT Nice Access
forall a b. (a -> b) -> a -> b
$ 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 Measure
x Expr
e                    -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> ArgInfo
-> Measure
-> Expr
-> NiceDeclaration
Axiom Range
r Access
p IsAbstract
a IsInstance
i ArgInfo
rel Measure
x Expr
e)                (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Measure
x Arg Expr
e                -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TacticAttribute
-> Measure
-> Arg Expr
-> NiceDeclaration
NiceField Range
r Access
p IsAbstract
a IsInstance
i TacticAttribute
tac Measure
x Arg Expr
e)            (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      PrimitiveFunction Range
r Access
p IsAbstract
a Measure
x Arg Expr
e              -> (\ Access
p -> Range
-> Access -> IsAbstract -> Measure -> Arg Expr -> NiceDeclaration
PrimitiveFunction Range
r Access
p IsAbstract
a Measure
x Arg Expr
e)          (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
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)             ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice [NiceDeclaration]
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [NiceDeclaration]
ds
      NiceLoneConstructor Range
r [NiceDeclaration]
ds                 -> Range -> [NiceDeclaration] -> NiceDeclaration
NiceLoneConstructor Range
r                         ([NiceDeclaration] -> NiceDeclaration)
-> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice [NiceDeclaration]
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)            (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceModuleMacro Range
r Access
p Measure
x ModuleApplication
ma OpenShortHand
op ImportDirective
is           -> (\ Access
p -> Range
-> Access
-> Measure
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> NiceDeclaration
NiceModuleMacro Range
r Access
p Measure
x ModuleApplication
ma OpenShortHand
op ImportDirective
is)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
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 Measure
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> ArgInfo
-> TerminationCheck
-> CoverageCheck
-> Measure
-> Expr
-> NiceDeclaration
FunSig Range
r Access
p IsAbstract
a IsInstance
i IsMacro
m ArgInfo
rel TerminationCheck
tc CoverageCheck
cc Measure
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceRecSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t            -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceRecSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t)        (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Measure
-> [LamBinding]
-> Expr
-> NiceDeclaration
NiceDataSig Range
r Access
p IsAbstract
a PositivityCheck
pc UniverseCheck
uc Measure
x [LamBinding]
ls Expr
t)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
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) (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
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 [Measure]
x Expr
e        -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> [Measure]
-> Expr
-> NiceDeclaration
NiceUnquoteDecl Range
r Access
p IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e)    (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e           -> (\ Access
p -> Range
-> Access
-> IsAbstract
-> TerminationCheck
-> CoverageCheck
-> [Measure]
-> Expr
-> NiceDeclaration
NiceUnquoteDef Range
r Access
p IsAbstract
a TerminationCheck
tc CoverageCheck
cc [Measure]
x Expr
e)       (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NicePatternSyn Range
r Access
p Measure
x [Arg Measure]
xs Pattern
p'               -> (\ Access
p -> Range
-> Access -> Measure -> [Arg Measure] -> Pattern -> NiceDeclaration
NicePatternSyn Range
r Access
p Measure
x [Arg Measure]
xs Pattern
p')           (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Measure
x Expr
t             -> (\ Access
p -> Range
-> Access
-> ArgInfo
-> TacticAttribute
-> Measure
-> Expr
-> NiceDeclaration
NiceGeneralize Range
r Access
p ArgInfo
i TacticAttribute
tac Measure
x Expr
t)         (Access -> NiceDeclaration)
-> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
p
      d :: NiceDeclaration
d@NicePragma{}                           -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@(NiceOpen Range
_ QName
_ ImportDirective
directives)              -> do
        Maybe Range -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (ImportDirective -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective
directives) ((Range -> ChangeT Nice ()) -> ChangeT Nice ())
-> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
forall a b. (a -> b) -> a -> b
$ Nice () -> ChangeT Nice ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nice () -> ChangeT Nice ())
-> (Range -> Nice ()) -> Range -> ChangeT Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => DeclarationWarning' -> Nice ()
DeclarationWarning' -> Nice ()
declarationWarning (DeclarationWarning' -> Nice ())
-> (Range -> DeclarationWarning') -> Range -> Nice ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> DeclarationWarning'
OpenPublicPrivate
        UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceImport{}                           -> UpdaterT Nice NiceDeclaration
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 Measure
x [Clause]
cls              -> Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Measure
-> [Clause]
-> NiceDeclaration
FunDef Range
r [Declaration]
ds IsAbstract
a IsInstance
i TerminationCheck
tc CoverageCheck
cc Measure
x ([Clause] -> NiceDeclaration)
-> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice [Clause]
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o [Clause]
cls
      d :: NiceDeclaration
d@NiceDataDef{}                          -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d
      d :: NiceDeclaration
d@NiceRecDef{}                           -> UpdaterT Nice NiceDeclaration
forall (m :: * -> *) a. Monad m => a -> m a
return NiceDeclaration
d

instance MakePrivate Clause where
  mkPrivate :: Origin -> UpdaterT Nice Clause
mkPrivate Origin
o (Clause Measure
x Bool
catchall LHS
lhs RHS
rhs WhereClause
wh [Clause]
with) = do
    Measure -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
Clause Measure
x Bool
catchall LHS
lhs RHS
rhs (WhereClause -> [Clause] -> Clause)
-> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Origin -> UpdaterT Nice WhereClause
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o WhereClause
wh ChangeT Nice ([Clause] -> Clause)
-> ChangeT Nice [Clause] -> ChangeT Nice Clause
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Origin -> UpdaterT Nice [Clause]
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    -> UpdaterT Nice WhereClause
forall (m :: * -> *) a. Monad m => a -> m a
return WhereClause
d
    -- @where@-declarations are protected behind an anonymous module,
    -- thus, they are effectively private by default.
    d :: WhereClause
d@AnyWhere{} -> UpdaterT Nice WhereClause
forall (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 Measure
m Access
a [Declaration]
ds -> Origin -> UpdaterT Nice Access
forall a. MakePrivate a => Origin -> UpdaterT Nice a
mkPrivate Origin
o Access
a ChangeT Nice Access
-> (Access -> WhereClause) -> ChangeT Nice WhereClause
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Access
a' -> Range -> Measure -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Measure -> Access -> decls -> WhereClause' decls
SomeWhere Range
r Measure
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 Measure
x Expr
e          -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [ArgInfo -> TacticAttribute -> Measure -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Maybe a
Nothing Measure
x Expr
e]
    NiceField Range
_ Access
_ IsAbstract
_ IsInstance
i TacticAttribute
tac Measure
x Arg Expr
argt   -> [IsInstance -> TacticAttribute -> Measure -> Arg Expr -> Declaration
FieldSig IsInstance
i TacticAttribute
tac Measure
x Arg Expr
argt]
    PrimitiveFunction Range
r Access
_ IsAbstract
_ Measure
x Arg Expr
e    -> [Range -> [Declaration] -> Declaration
Primitive Range
r [ArgInfo -> TacticAttribute -> Measure -> Expr -> Declaration
TypeSig (Arg Expr -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Expr
e) TacticAttribute
forall a. Maybe a
Nothing Measure
x (Arg Expr -> Expr
forall e. Arg e -> e
unArg Arg Expr
e)]]
    NiceMutual Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds          -> [Range -> [Declaration] -> Declaration
Mutual Range
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceLoneConstructor Range
r [NiceDeclaration]
ds       -> [Range -> [Declaration] -> Declaration
LoneConstructor Range
r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
ds]
    NiceModule Range
r Access
_ IsAbstract
_ QName
x Telescope
tel [Declaration]
ds      -> [Range -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r QName
x Telescope
tel [Declaration]
ds]
    NiceModuleMacro Range
r Access
_ Measure
x ModuleApplication
ma OpenShortHand
o ImportDirective
dir -> [Range
-> Measure
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
r Measure
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
_ Measure
x [LamBinding]
bs Expr
e    -> [Range -> Measure -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Measure
x [LamBinding]
bs Expr
e]
    NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Measure
x [LamBinding]
bs Expr
e   -> [Range -> Measure -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Measure
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
_ Measure
x Expr
e   -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [ArgInfo -> TacticAttribute -> Measure -> Expr -> Declaration
TypeSig ArgInfo
rel TacticAttribute
forall a. Maybe a
Nothing Measure
x Expr
e]
    FunDef Range
_ [Declaration]
ds IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Measure
_ [Clause]
_        -> [Declaration]
ds
    NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Measure
x [LamBinding]
bs [NiceDeclaration]
cs  -> [Range -> Measure -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
r Measure
x [LamBinding]
bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (NiceDeclaration -> [Declaration])
-> [NiceDeclaration] -> [Declaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NiceDeclaration -> [Declaration]
notSoNiceDeclarations [NiceDeclaration]
cs]
    NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Measure
x RecordDirectives
dir [LamBinding]
bs [Declaration]
ds -> [Range
-> Measure
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Measure
x RecordDirectives
dir [LamBinding]
bs [Declaration]
ds]
    NicePatternSyn Range
r Access
_ Measure
n [Arg Measure]
as Pattern
p      -> [Range -> Measure -> [Arg Measure] -> Pattern -> Declaration
PatternSyn Range
r Measure
n [Arg Measure]
as Pattern
p]
    NiceGeneralize Range
r Access
_ ArgInfo
i TacticAttribute
tac Measure
n Expr
e   -> [Range -> [Declaration] -> Declaration
Generalize Range
r [ArgInfo -> TacticAttribute -> Measure -> Expr -> Declaration
TypeSig ArgInfo
i TacticAttribute
tac Measure
n Expr
e]]
    NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
i TerminationCheck
_ CoverageCheck
_ [Measure]
x Expr
e -> IsInstance -> [Declaration] -> [Declaration]
inst IsInstance
i [Range -> [Measure] -> Expr -> Declaration
UnquoteDecl Range
r [Measure]
x Expr
e]
    NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Measure]
x Expr
e    -> [Range -> [Measure] -> Expr -> Declaration
UnquoteDef Range
r [Measure]
x 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{}                       -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceField Range
_ Access
_ IsAbstract
a IsInstance
_ TacticAttribute
_ Measure
_ Arg Expr
_       -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    PrimitiveFunction Range
_ Access
_ IsAbstract
a Measure
_ Arg Expr
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceMutual{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceLoneConstructor{}         -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceModule Range
_ Access
_ IsAbstract
a QName
_ Telescope
_ [Declaration]
_        -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceModuleMacro{}             -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceOpen{}                    -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceImport{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NicePragma{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceRecSig{}                  -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceDataSig{}                 -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceFunClause Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    FunSig{}                      -> Maybe IsAbstract
forall a. Maybe a
Nothing
    FunDef Range
_ [Declaration]
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ Measure
_ [Clause]
_        -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceDataDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Measure
_ [LamBinding]
_ [NiceDeclaration]
_   -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceRecDef Range
_ Origin
_ IsAbstract
a PositivityCheck
_ UniverseCheck
_ Measure
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NicePatternSyn{}              -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceGeneralize{}              -> Maybe IsAbstract
forall a. Maybe a
Nothing
    NiceUnquoteDecl Range
_ Access
_ IsAbstract
a IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Measure]
_ Expr
_ -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a
    NiceUnquoteDef Range
_ Access
_ IsAbstract
a TerminationCheck
_ CoverageCheck
_ [Measure]
_ Expr
_    -> IsAbstract -> Maybe IsAbstract
forall a. a -> Maybe a
Just IsAbstract
a