module Agda.Syntax.Concrete.Definitions.Types where

import Control.DeepSeq

import Data.Data
import Data.Map (Map)
import Data.Semigroup ( Semigroup(..) )

import GHC.Generics (Generic)

import Agda.Syntax.Position
import Agda.Syntax.Common hiding (TerminationCheck())
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Pretty

import Agda.Utils.Pretty
import Agda.Utils.Impossible

{--------------------------------------------------------------------------
    Types
 --------------------------------------------------------------------------}

{-| The nice declarations. No fixity declarations and function definitions are
    contained in a single constructor instead of spread out between type
    signatures and clauses. The @private@, @postulate@, @abstract@ and @instance@
    modifiers have been distributed to the individual declarations.

    Observe the order of components:

      Range
      Fixity'
      Access
      IsAbstract
      IsInstance
      TerminationCheck
      PositivityCheck

      further attributes

      (Q)Name

      content (Expr, Declaration ...)
-}
data NiceDeclaration
  = Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
      -- ^ 'IsAbstract' argument: We record whether a declaration was made in an @abstract@ block.
      --
      --   'ArgInfo' argument: Axioms and functions can be declared irrelevant.
      --   ('Hiding' should be 'NotHidden'.)
  | NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
  | PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
  | NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
  | NiceModule Range Access IsAbstract QName Telescope [Declaration]
  | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
  | NiceOpen Range QName ImportDirective
  | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
  | NicePragma Range Pragma
  | NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  | NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  | NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
    -- ^ An uncategorized function clause, could be a function clause
    --   without type signature or a pattern lhs (e.g. for irrefutable let).
    --   The 'Declaration' is the actual 'FunClause'.
  | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
  | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
      -- ^ Block of function clauses (we have seen the type signature before).
      --   The 'Declaration's are the original declarations that were processed
      --   into this 'FunDef' and are only used in 'notSoNiceDeclaration'.
      --   Andreas, 2017-01-01: Because of issue #2372, we add 'IsInstance' here.
      --   An alias should know that it is an instance.
  | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
  | NiceLoneConstructor Range [NiceConstructor]
  | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]
      -- ^ @(Maybe Range)@ gives range of the 'pattern' declaration.
  | NicePatternSyn Range Access Name [Arg Name] Pattern
  | NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
  | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
  | NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
  deriving (Typeable NiceDeclaration
DataType
Constr
Typeable NiceDeclaration
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NiceDeclaration)
-> (NiceDeclaration -> Constr)
-> (NiceDeclaration -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NiceDeclaration))
-> ((forall b. Data b => b -> b)
    -> NiceDeclaration -> NiceDeclaration)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> NiceDeclaration -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NiceDeclaration -> m NiceDeclaration)
-> Data NiceDeclaration
NiceDeclaration -> DataType
NiceDeclaration -> Constr
(forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
$cNiceUnquoteDef :: Constr
$cNiceUnquoteDecl :: Constr
$cNiceGeneralize :: Constr
$cNicePatternSyn :: Constr
$cNiceRecDef :: Constr
$cNiceLoneConstructor :: Constr
$cNiceDataDef :: Constr
$cFunDef :: Constr
$cFunSig :: Constr
$cNiceFunClause :: Constr
$cNiceDataSig :: Constr
$cNiceRecSig :: Constr
$cNicePragma :: Constr
$cNiceImport :: Constr
$cNiceOpen :: Constr
$cNiceModuleMacro :: Constr
$cNiceModule :: Constr
$cNiceMutual :: Constr
$cPrimitiveFunction :: Constr
$cNiceField :: Constr
$cAxiom :: Constr
$tNiceDeclaration :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapMp :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapM :: (forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NiceDeclaration -> m NiceDeclaration
gmapQi :: Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u
gmapQ :: (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NiceDeclaration -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r
gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
$cgmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NiceDeclaration)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)
dataTypeOf :: NiceDeclaration -> DataType
$cdataTypeOf :: NiceDeclaration -> DataType
toConstr :: NiceDeclaration -> Constr
$ctoConstr :: NiceDeclaration -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NiceDeclaration
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration
$cp1Data :: Typeable NiceDeclaration
Data, Int -> NiceDeclaration -> ShowS
[NiceDeclaration] -> ShowS
NiceDeclaration -> String
(Int -> NiceDeclaration -> ShowS)
-> (NiceDeclaration -> String)
-> ([NiceDeclaration] -> ShowS)
-> Show NiceDeclaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NiceDeclaration] -> ShowS
$cshowList :: [NiceDeclaration] -> ShowS
show :: NiceDeclaration -> String
$cshow :: NiceDeclaration -> String
showsPrec :: Int -> NiceDeclaration -> ShowS
$cshowsPrec :: Int -> NiceDeclaration -> ShowS
Show, (forall x. NiceDeclaration -> Rep NiceDeclaration x)
-> (forall x. Rep NiceDeclaration x -> NiceDeclaration)
-> Generic NiceDeclaration
forall x. Rep NiceDeclaration x -> NiceDeclaration
forall x. NiceDeclaration -> Rep NiceDeclaration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NiceDeclaration x -> NiceDeclaration
$cfrom :: forall x. NiceDeclaration -> Rep NiceDeclaration x
Generic)

instance NFData NiceDeclaration

type TerminationCheck = Common.TerminationCheck Measure

-- | Termination measure is, for now, a variable name.
type Measure = Name

type Catchall = Bool

-- | Only 'Axiom's.
type NiceConstructor = NiceTypeSignature

-- | Only 'Axiom's.
type NiceTypeSignature  = NiceDeclaration

-- | One clause in a function definition. There is no guarantee that the 'LHS'
--   actually declares the 'Name'. We will have to check that later.
data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
    deriving (Typeable Clause
DataType
Constr
Typeable Clause
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Clause -> c Clause)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Clause)
-> (Clause -> Constr)
-> (Clause -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Clause))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause))
-> ((forall b. Data b => b -> b) -> Clause -> Clause)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Clause -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Clause -> r)
-> (forall u. (forall d. Data d => d -> u) -> Clause -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Clause -> m Clause)
-> Data Clause
Clause -> DataType
Clause -> Constr
(forall b. Data b => b -> b) -> Clause -> Clause
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
forall u. (forall d. Data d => d -> u) -> Clause -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
$cClause :: Constr
$tClause :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapMp :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapM :: (forall d. Data d => d -> m d) -> Clause -> m Clause
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Clause -> m Clause
gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Clause -> u
gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Clause -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r
gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
$cgmapT :: (forall b. Data b => b -> b) -> Clause -> Clause
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Clause)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Clause)
dataTypeOf :: Clause -> DataType
$cdataTypeOf :: Clause -> DataType
toConstr :: Clause -> Constr
$ctoConstr :: Clause -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Clause
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Clause -> c Clause
$cp1Data :: Typeable Clause
Data, Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> String
$cshow :: Clause -> String
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, (forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Clause x -> Clause
$cfrom :: forall x. Clause -> Rep Clause x
Generic)

instance NFData Clause

-- | When processing a mutual block we collect the various checks present in the block
--   before combining them.

data MutualChecks = MutualChecks
  { MutualChecks -> [TerminationCheck]
mutualTermination :: [TerminationCheck]
  , MutualChecks -> [CoverageCheck]
mutualCoverage    :: [CoverageCheck]
  , MutualChecks -> [PositivityCheck]
mutualPositivity  :: [PositivityCheck]
  }

instance Semigroup MutualChecks where
  MutualChecks [TerminationCheck]
a [CoverageCheck]
b [PositivityCheck]
c <> :: MutualChecks -> MutualChecks -> MutualChecks
<> MutualChecks [TerminationCheck]
a' [CoverageCheck]
b' [PositivityCheck]
c'
    = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks ([TerminationCheck]
a [TerminationCheck] -> [TerminationCheck] -> [TerminationCheck]
forall a. Semigroup a => a -> a -> a
<> [TerminationCheck]
a') ([CoverageCheck]
b [CoverageCheck] -> [CoverageCheck] -> [CoverageCheck]
forall a. Semigroup a => a -> a -> a
<> [CoverageCheck]
b') ([PositivityCheck]
c [PositivityCheck] -> [PositivityCheck] -> [PositivityCheck]
forall a. Semigroup a => a -> a -> a
<> [PositivityCheck]
c')

instance Monoid MutualChecks where
  mempty :: MutualChecks
mempty = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [] [] []
  mappend :: MutualChecks -> MutualChecks -> MutualChecks
mappend = MutualChecks -> MutualChecks -> MutualChecks
forall a. Semigroup a => a -> a -> a
(<>)

-- | In an inferred `mutual' block we keep accumulating nice declarations until all
--   of the lone signatures have an attached definition. The type is therefore a bit
--   span-like: we return an initial segment (the inferred mutual block) together
--   with leftovers.

data InferredMutual = InferredMutual
  { InferredMutual -> MutualChecks
inferredChecks    :: MutualChecks       -- checks for this block
  , InferredMutual -> [NiceDeclaration]
inferredBlock     :: [NiceDeclaration]  -- mutual block
  , InferredMutual -> [NiceDeclaration]
inferredLeftovers :: [NiceDeclaration]  -- leftovers
  }

extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
extendInferredBlock NiceDeclaration
d (InferredMutual MutualChecks
cs [NiceDeclaration]
ds [NiceDeclaration]
left) = MutualChecks
-> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
InferredMutual MutualChecks
cs (NiceDeclaration
d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
forall a. a -> [a] -> [a]
: [NiceDeclaration]
ds) [NiceDeclaration]
left

-- | In an `interleaved mutual' block we collect the data signatures, function signatures,
--   as well as their associated constructors and function clauses respectively.
--   Each signature is given a position in the block (from 0 onwards) and each set
--   of constructor / clauses is given a *distinct* one. This allows for interleaved
--   forward declarations similar to what one gets in a new-style mutual block.
type InterleavedMutual = Map Name InterleavedDecl

data InterleavedDecl
  = InterleavedData
    { InterleavedDecl -> (Int, NiceDeclaration)
infixDataSig  :: (Int, NiceDeclaration)           -- a data signature
    , InterleavedDecl -> Maybe (Int, [[NiceDeclaration]])
infixDataCons :: Maybe (Int, [[NiceConstructor]]) -- and associated constructors
    }
  | InterleavedFun
    { InterleavedDecl -> (Int, NiceDeclaration)
infixFunSig     :: (Int, NiceDeclaration)                  -- a fun signature
    , InterleavedDecl -> Maybe (Int, [([Declaration], [Clause])])
infixFunClauses :: Maybe (Int, [([Declaration],[Clause])]) -- and associated fun clauses
    }

isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedFun :: InterleavedDecl -> Maybe ()
isInterleavedFun InterleavedFun{} = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isInterleavedFun InterleavedDecl
_ = Maybe ()
forall a. Maybe a
Nothing

isInterleavedData :: InterleavedDecl -> Maybe ()
isInterleavedData :: InterleavedDecl -> Maybe ()
isInterleavedData InterleavedData{} = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isInterleavedData InterleavedDecl
_ = Maybe ()
forall a. Maybe a
Nothing

interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
interleavedDecl Name
k = \case
  InterleavedData (Int
i, d :: NiceDeclaration
d@(NiceDataSig Range
_ Access
acc IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
_ [LamBinding]
pars Expr
_)) Maybe (Int, [[NiceDeclaration]])
ds ->
    let fpars :: [LamBinding]
fpars = (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LamBinding -> [LamBinding]
dropTypeAndModality [LamBinding]
pars
        ddef :: [NiceDeclaration] -> NiceDeclaration
ddef  = Range
-> Origin
-> IsAbstract
-> PositivityCheck
-> UniverseCheck
-> Name
-> [LamBinding]
-> [NiceDeclaration]
-> NiceDeclaration
NiceDataDef Range
forall a. Range' a
noRange Origin
UserWritten IsAbstract
abs PositivityCheck
pc UniverseCheck
uc Name
k [LamBinding]
fpars
    in (Int
i,NiceDeclaration
d) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
: [(Int, NiceDeclaration)]
-> ((Int, [[NiceDeclaration]]) -> [(Int, NiceDeclaration)])
-> Maybe (Int, [[NiceDeclaration]])
-> [(Int, NiceDeclaration)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ (Int
j, [[NiceDeclaration]]
dss) -> [(Int
j, [NiceDeclaration] -> NiceDeclaration
ddef ([[NiceDeclaration]] -> [NiceDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[NiceDeclaration]] -> [[NiceDeclaration]]
forall a. [a] -> [a]
reverse [[NiceDeclaration]]
dss)))]) Maybe (Int, [[NiceDeclaration]])
ds
  InterleavedFun (Int
i, d :: NiceDeclaration
d@(FunSig Range
r Access
acc IsAbstract
abs IsInstance
inst IsMacro
mac ArgInfo
info TerminationCheck
tc CoverageCheck
cc Name
n Expr
e)) Maybe (Int, [([Declaration], [Clause])])
dcs ->
    let fdef :: [([Declaration], [Clause])] -> NiceDeclaration
fdef [([Declaration], [Clause])]
dcss = let ([[Declaration]]
dss, [[Clause]]
css) = [([Declaration], [Clause])] -> ([[Declaration]], [[Clause]])
forall a b. [(a, b)] -> ([a], [b])
unzip [([Declaration], [Clause])]
dcss in
                    Range
-> [Declaration]
-> IsAbstract
-> IsInstance
-> TerminationCheck
-> CoverageCheck
-> Name
-> [Clause]
-> NiceDeclaration
FunDef Range
r ([[Declaration]] -> [Declaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Declaration]]
dss) IsAbstract
abs IsInstance
inst TerminationCheck
tc CoverageCheck
cc Name
n ([[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Clause]]
css)
    in (Int
i,NiceDeclaration
d) (Int, NiceDeclaration)
-> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
forall a. a -> [a] -> [a]
: [(Int, NiceDeclaration)]
-> ((Int, [([Declaration], [Clause])]) -> [(Int, NiceDeclaration)])
-> Maybe (Int, [([Declaration], [Clause])])
-> [(Int, NiceDeclaration)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ (Int
j, [([Declaration], [Clause])]
dcss) -> [(Int
j, [([Declaration], [Clause])] -> NiceDeclaration
fdef ([([Declaration], [Clause])] -> [([Declaration], [Clause])]
forall a. [a] -> [a]
reverse [([Declaration], [Clause])]
dcss))]) Maybe (Int, [([Declaration], [Clause])])
dcs
  InterleavedDecl
_ -> [(Int, NiceDeclaration)]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- someone messed up and broke the invariant

-- | Several declarations expect only type signatures as sub-declarations.  These are:
data KindOfBlock
  = PostulateBlock  -- ^ @postulate@
  | PrimitiveBlock  -- ^ @primitive@.  Ensured by parser.
  | InstanceBlock   -- ^ @instance@.  Actually, here all kinds of sub-declarations are allowed a priori.
  | FieldBlock      -- ^ @field@.  Ensured by parser.
  | DataBlock       -- ^ @data ... where@.  Here we got a bad error message for Agda-2.5 (Issue 1698).
  | ConstructorBlock  -- ^ @constructor@, in @interleaved mutual@.
  deriving (Typeable KindOfBlock
DataType
Constr
Typeable KindOfBlock
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KindOfBlock)
-> (KindOfBlock -> Constr)
-> (KindOfBlock -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c KindOfBlock))
-> ((forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r)
-> (forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock)
-> Data KindOfBlock
KindOfBlock -> DataType
KindOfBlock -> Constr
(forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
$cConstructorBlock :: Constr
$cDataBlock :: Constr
$cFieldBlock :: Constr
$cInstanceBlock :: Constr
$cPrimitiveBlock :: Constr
$cPostulateBlock :: Constr
$tKindOfBlock :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapMp :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapM :: (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock
gmapQi :: Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u
gmapQ :: (forall d. Data d => d -> u) -> KindOfBlock -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KindOfBlock -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r
gmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
$cgmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c KindOfBlock)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KindOfBlock)
dataTypeOf :: KindOfBlock -> DataType
$cdataTypeOf :: KindOfBlock -> DataType
toConstr :: KindOfBlock -> Constr
$ctoConstr :: KindOfBlock -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KindOfBlock
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock
$cp1Data :: Typeable KindOfBlock
Data, KindOfBlock -> KindOfBlock -> Bool
(KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool) -> Eq KindOfBlock
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KindOfBlock -> KindOfBlock -> Bool
$c/= :: KindOfBlock -> KindOfBlock -> Bool
== :: KindOfBlock -> KindOfBlock -> Bool
$c== :: KindOfBlock -> KindOfBlock -> Bool
Eq, Eq KindOfBlock
Eq KindOfBlock
-> (KindOfBlock -> KindOfBlock -> Ordering)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> Bool)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> Ord KindOfBlock
KindOfBlock -> KindOfBlock -> Bool
KindOfBlock -> KindOfBlock -> Ordering
KindOfBlock -> KindOfBlock -> KindOfBlock
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: KindOfBlock -> KindOfBlock -> KindOfBlock
$cmin :: KindOfBlock -> KindOfBlock -> KindOfBlock
max :: KindOfBlock -> KindOfBlock -> KindOfBlock
$cmax :: KindOfBlock -> KindOfBlock -> KindOfBlock
>= :: KindOfBlock -> KindOfBlock -> Bool
$c>= :: KindOfBlock -> KindOfBlock -> Bool
> :: KindOfBlock -> KindOfBlock -> Bool
$c> :: KindOfBlock -> KindOfBlock -> Bool
<= :: KindOfBlock -> KindOfBlock -> Bool
$c<= :: KindOfBlock -> KindOfBlock -> Bool
< :: KindOfBlock -> KindOfBlock -> Bool
$c< :: KindOfBlock -> KindOfBlock -> Bool
compare :: KindOfBlock -> KindOfBlock -> Ordering
$ccompare :: KindOfBlock -> KindOfBlock -> Ordering
$cp1Ord :: Eq KindOfBlock
Ord, Int -> KindOfBlock -> ShowS
[KindOfBlock] -> ShowS
KindOfBlock -> String
(Int -> KindOfBlock -> ShowS)
-> (KindOfBlock -> String)
-> ([KindOfBlock] -> ShowS)
-> Show KindOfBlock
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KindOfBlock] -> ShowS
$cshowList :: [KindOfBlock] -> ShowS
show :: KindOfBlock -> String
$cshow :: KindOfBlock -> String
showsPrec :: Int -> KindOfBlock -> ShowS
$cshowsPrec :: Int -> KindOfBlock -> ShowS
Show)


instance HasRange NiceDeclaration where
  getRange :: NiceDeclaration -> Range
getRange (Axiom Range
r Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
_ Expr
_)           = Range
r
  getRange (NiceField Range
r Access
_ IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_)       = Range
r
  getRange (NiceMutual Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
_)          = Range
r
  getRange (NiceModule Range
r Access
_ IsAbstract
_ QName
_ Telescope
_ [Declaration]
_ )       = Range
r
  getRange (NiceModuleMacro Range
r Access
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_)   = Range
r
  getRange (NiceOpen Range
r QName
_ ImportDirective
_)                = Range
r
  getRange (NiceImport Range
r QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_)          = Range
r
  getRange (NicePragma Range
r Pragma
_)                = Range
r
  getRange (PrimitiveFunction Range
r Access
_ IsAbstract
_ Name
_ Arg Expr
_)   = Range
r
  getRange (FunSig Range
r Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
_ Expr
_)    = Range
r
  getRange (FunDef Range
r [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ [Clause]
_)        = Range
r
  getRange (NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ [NiceDeclaration]
_)   = Range
r
  getRange (NiceLoneConstructor Range
r [NiceDeclaration]
_)       = Range
r
  getRange (NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ RecordDirectives
_ [LamBinding]
_ [Declaration]
_)  = Range
r
  getRange (NiceRecSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_)    = Range
r
  getRange (NiceDataSig Range
r Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [LamBinding]
_ Expr
_)   = Range
r
  getRange (NicePatternSyn Range
r Access
_ Name
_ [Arg Name]
_ Pattern
_)      = Range
r
  getRange (NiceGeneralize Range
r Access
_ ArgInfo
_ TacticAttribute
_ Name
_ Expr
_)    = Range
r
  getRange (NiceFunClause Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ Bool
_ Declaration
_)   = Range
r
  getRange (NiceUnquoteDecl Range
r Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_) = Range
r
  getRange (NiceUnquoteDef Range
r Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
_ Expr
_)    = Range
r

instance Pretty NiceDeclaration where
  pretty :: NiceDeclaration -> Doc
pretty = \case
    Axiom Range
_ Access
_ IsAbstract
_ IsInstance
_ ArgInfo
_ Name
x Expr
_            -> String -> Doc
text String
"postulate" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text String
"_"
    NiceField Range
_ Access
_ IsAbstract
_ IsInstance
_ TacticAttribute
_ Name
x Arg Expr
_        -> String -> Doc
text String
"field" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    PrimitiveFunction Range
_ Access
_ IsAbstract
_ Name
x Arg Expr
_    -> String -> Doc
text String
"primitive" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    NiceMutual{}                   -> String -> Doc
text String
"mutual"
    NiceModule Range
_ Access
_ IsAbstract
_ QName
x Telescope
_ [Declaration]
_         -> String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
    NiceModuleMacro Range
_ Access
_ Name
x ModuleApplication
_ OpenShortHand
_ ImportDirective
_    -> String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"= ..."
    NiceOpen Range
_ QName
x ImportDirective
_                 -> String -> Doc
text String
"open" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
    NiceImport Range
_ QName
x Maybe AsName
_ OpenShortHand
_ ImportDirective
_           -> String -> Doc
text String
"import" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
    NicePragma{}                   -> String -> Doc
text String
"{-# ... #-}"
    NiceRecSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ Expr
_     -> String -> Doc
text String
"record" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    NiceDataSig Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ Expr
_    -> String -> Doc
text String
"data" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    NiceFunClause{}                -> String -> Doc
text String
"<function clause>"
    FunSig Range
_ Access
_ IsAbstract
_ IsInstance
_ IsMacro
_ ArgInfo
_ TerminationCheck
_ CoverageCheck
_ Name
x Expr
_     -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text String
"_"
    FunDef Range
_ [Declaration]
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
x [Clause]
_         -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"= _"
    NiceDataDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [LamBinding]
_ [NiceDeclaration]
_    -> String -> Doc
text String
"data" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
    NiceLoneConstructor Range
_ [NiceDeclaration]
ds       -> String -> Doc
text String
"constructor"
    NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x  RecordDirectives
_ [LamBinding]
_ [Declaration]
_  -> String -> Doc
text String
"record" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"where"
    NicePatternSyn Range
_ Access
_ Name
x [Arg Name]
_ Pattern
_       -> String -> Doc
text String
"pattern" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    NiceGeneralize Range
_ Access
_ ArgInfo
_ TacticAttribute
_ Name
x Expr
_     -> String -> Doc
text String
"variable" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    NiceUnquoteDecl Range
_ Access
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ [Name]
xs Expr
_ -> String -> Doc
text String
"<unquote declarations>"
    NiceUnquoteDef Range
_ Access
_ IsAbstract
_ TerminationCheck
_ CoverageCheck
_ [Name]
xs Expr
_    -> String -> Doc
text String
"<unquote definitions>"

declName :: NiceDeclaration -> String
declName :: NiceDeclaration -> String
declName Axiom{}             = String
"Postulates"
declName NiceField{}         = String
"Fields"
declName NiceMutual{}        = String
"Mutual blocks"
declName NiceModule{}        = String
"Modules"
declName NiceModuleMacro{}   = String
"Modules"
declName NiceOpen{}          = String
"Open declarations"
declName NiceImport{}        = String
"Import statements"
declName NicePragma{}        = String
"Pragmas"
declName PrimitiveFunction{} = String
"Primitive declarations"
declName NicePatternSyn{}    = String
"Pattern synonyms"
declName NiceGeneralize{}    = String
"Generalized variables"
declName NiceUnquoteDecl{}   = String
"Unquoted declarations"
declName NiceUnquoteDef{}    = String
"Unquoted definitions"
declName NiceRecSig{}        = String
"Records"
declName NiceDataSig{}       = String
"Data types"
declName NiceFunClause{}     = String
"Functions without a type signature"
declName FunSig{}            = String
"Type signatures"
declName FunDef{}            = String
"Function definitions"
declName NiceRecDef{}        = String
"Records"
declName NiceDataDef{}       = String
"Data types"
declName NiceLoneConstructor{} = String
"Constructors"


data InMutual
  = InMutual    -- ^ we are nicifying a mutual block
  | NotInMutual -- ^ we are nicifying decls not in a mutual block
    deriving (InMutual -> InMutual -> Bool
(InMutual -> InMutual -> Bool)
-> (InMutual -> InMutual -> Bool) -> Eq InMutual
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InMutual -> InMutual -> Bool
$c/= :: InMutual -> InMutual -> Bool
== :: InMutual -> InMutual -> Bool
$c== :: InMutual -> InMutual -> Bool
Eq, Int -> InMutual -> ShowS
[InMutual] -> ShowS
InMutual -> String
(Int -> InMutual -> ShowS)
-> (InMutual -> String) -> ([InMutual] -> ShowS) -> Show InMutual
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InMutual] -> ShowS
$cshowList :: [InMutual] -> ShowS
show :: InMutual -> String
$cshow :: InMutual -> String
showsPrec :: Int -> InMutual -> ShowS
$cshowsPrec :: Int -> InMutual -> ShowS
Show)

-- | The kind of the forward declaration.

data DataRecOrFun
  = DataName
    { DataRecOrFun -> PositivityCheck
_kindPosCheck :: PositivityCheck
    , DataRecOrFun -> UniverseCheck
_kindUniCheck :: UniverseCheck
    }
    -- ^ Name of a data type
  | RecName
    { _kindPosCheck :: PositivityCheck
    , _kindUniCheck :: UniverseCheck
    }
    -- ^ Name of a record type
  | FunName TerminationCheck CoverageCheck
    -- ^ Name of a function.
  deriving (Typeable DataRecOrFun
DataType
Constr
Typeable DataRecOrFun
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DataRecOrFun)
-> (DataRecOrFun -> Constr)
-> (DataRecOrFun -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DataRecOrFun))
-> ((forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r)
-> (forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun)
-> Data DataRecOrFun
DataRecOrFun -> DataType
DataRecOrFun -> Constr
(forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
$cFunName :: Constr
$cRecName :: Constr
$cDataName :: Constr
$tDataRecOrFun :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapMp :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapM :: (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun
gmapQi :: Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u
gmapQ :: (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DataRecOrFun -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r
gmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
$cgmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DataRecOrFun)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun)
dataTypeOf :: DataRecOrFun -> DataType
$cdataTypeOf :: DataRecOrFun -> DataType
toConstr :: DataRecOrFun -> Constr
$ctoConstr :: DataRecOrFun -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataRecOrFun
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun
$cp1Data :: Typeable DataRecOrFun
Data, Int -> DataRecOrFun -> ShowS
[DataRecOrFun] -> ShowS
DataRecOrFun -> String
(Int -> DataRecOrFun -> ShowS)
-> (DataRecOrFun -> String)
-> ([DataRecOrFun] -> ShowS)
-> Show DataRecOrFun
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataRecOrFun] -> ShowS
$cshowList :: [DataRecOrFun] -> ShowS
show :: DataRecOrFun -> String
$cshow :: DataRecOrFun -> String
showsPrec :: Int -> DataRecOrFun -> ShowS
$cshowsPrec :: Int -> DataRecOrFun -> ShowS
Show)

-- Ignore pragmas when checking equality
instance Eq DataRecOrFun where
  DataName{} == :: DataRecOrFun -> DataRecOrFun -> Bool
== DataName{} = Bool
True
  RecName{}  == RecName{}  = Bool
True
  FunName{}  == FunName{}  = Bool
True
  DataRecOrFun
_          == DataRecOrFun
_          = Bool
False

instance Pretty DataRecOrFun where
  pretty :: DataRecOrFun -> Doc
pretty DataName{} = Doc
"data type"
  pretty RecName{}  = Doc
"record type"
  pretty FunName{}  = Doc
"function"

isFunName :: DataRecOrFun -> Bool
isFunName :: DataRecOrFun -> Bool
isFunName (FunName{}) = Bool
True
isFunName DataRecOrFun
_           = Bool
False

sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
sameKind = DataRecOrFun -> DataRecOrFun -> Bool
forall a. Eq a => a -> a -> Bool
(==)

terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck :: DataRecOrFun -> TerminationCheck
terminationCheck (FunName TerminationCheck
tc CoverageCheck
_) = TerminationCheck
tc
terminationCheck DataRecOrFun
_ = TerminationCheck
forall m. TerminationCheck m
TerminationCheck

coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck (FunName TerminationCheck
_ CoverageCheck
cc) = CoverageCheck
cc
coverageCheck DataRecOrFun
_ = CoverageCheck
YesCoverageCheck

positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck :: DataRecOrFun -> PositivityCheck
positivityCheck (DataName PositivityCheck
pc UniverseCheck
_) = PositivityCheck
pc
positivityCheck (RecName PositivityCheck
pc UniverseCheck
_)  = PositivityCheck
pc
positivityCheck (FunName TerminationCheck
_ CoverageCheck
_)   = PositivityCheck
YesPositivityCheck

mutualChecks :: DataRecOrFun -> MutualChecks
mutualChecks :: DataRecOrFun -> MutualChecks
mutualChecks DataRecOrFun
k = [TerminationCheck]
-> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
MutualChecks [DataRecOrFun -> TerminationCheck
terminationCheck DataRecOrFun
k] [DataRecOrFun -> CoverageCheck
coverageCheck DataRecOrFun
k] [DataRecOrFun -> PositivityCheck
positivityCheck DataRecOrFun
k]

universeCheck :: DataRecOrFun -> UniverseCheck
universeCheck :: DataRecOrFun -> UniverseCheck
universeCheck (DataName PositivityCheck
_ UniverseCheck
uc) = UniverseCheck
uc
universeCheck (RecName PositivityCheck
_ UniverseCheck
uc)  = UniverseCheck
uc
universeCheck (FunName TerminationCheck
_ CoverageCheck
_)   = UniverseCheck
YesUniverseCheck