    module Agda.Syntax.Concrete.Definitions.Types where

    import Control.DeepSeq

    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.Syntax.Common.Pretty
    import Agda.Utils.Impossible
    import Agda.Utils.List1 (List1)
    import qualified Agda.Utils.List1 as List1

    {--------------------------------------------------------------------------
        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 KwRange TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
      | NiceModule Range Access IsAbstract Erased QName Telescope
          [Declaration]
      | NiceModuleMacro Range Access Erased Name ModuleApplication
          OpenShortHand ImportDirective
      | NiceOpen Range QName ImportDirective
      | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
      | NicePragma Range Pragma
      | NiceRecSig Range Erased Access IsAbstract PositivityCheck
          UniverseCheck Name [LamBinding] Expr
      | NiceDataSig Range Erased 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 KwRange [NiceConstructor]
      | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [RecordDirective] [LamBinding] [Declaration]
          -- ^ @(Maybe Range)@ gives range of the 'pattern' declaration.
      | NicePatternSyn Range Access Name [WithHiding 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
      | NiceUnquoteData Range Access IsAbstract PositivityCheck UniverseCheck Name [Name] Expr
      | NiceOpaque KwRange [QName] [NiceDeclaration]
      deriving (Int -> NiceConstructor -> ShowS
    [NiceConstructor] -> ShowS
    NiceConstructor -> String
    (Int -> NiceConstructor -> ShowS)
    -> (NiceConstructor -> String)
    -> ([NiceConstructor] -> ShowS)
    -> Show NiceConstructor
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NiceConstructor -> ShowS
    showsPrec :: Int -> NiceConstructor -> ShowS
    $cshow :: NiceConstructor -> String
    show :: NiceConstructor -> String
    $cshowList :: [NiceConstructor] -> ShowS
    showList :: [NiceConstructor] -> ShowS
    Show, (forall x. NiceConstructor -> Rep NiceConstructor x)
    -> (forall x. Rep NiceConstructor x -> NiceConstructor)
    -> Generic NiceConstructor
    forall x. Rep NiceConstructor x -> NiceConstructor
    forall x. NiceConstructor -> Rep NiceConstructor x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. NiceConstructor -> Rep NiceConstructor x
    from :: forall x. NiceConstructor -> Rep NiceConstructor x
    $cto :: forall x. Rep NiceConstructor x -> NiceConstructor
    to :: forall x. Rep NiceConstructor x -> NiceConstructor
    Generic)

    instance NFData NiceDeclaration

    type TerminationCheck = Common.TerminationCheck Measure

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

    -- | 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 (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
    $cshowsPrec :: Int -> Clause -> ShowS
    showsPrec :: Int -> Clause -> ShowS
    $cshow :: Clause -> String
    show :: Clause -> String
    $cshowList :: [Clause] -> ShowS
    showList :: [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
    $cfrom :: forall x. Clause -> Rep Clause x
    from :: forall x. Clause -> Rep Clause x
    $cto :: forall x. Rep Clause x -> Clause
    to :: forall x. Rep Clause x -> Clause
    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 -> [NiceConstructor]
    inferredBlock     :: [NiceDeclaration]  -- mutual block
      , InferredMutual -> [NiceConstructor]
    inferredLeftovers :: [NiceDeclaration]  -- leftovers
      }

    extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock :: NiceConstructor -> InferredMutual -> InferredMutual
    extendInferredBlock NiceConstructor
    d (InferredMutual MutualChecks
    cs [NiceConstructor]
    ds [NiceConstructor]
    left) = MutualChecks
    -> [NiceConstructor] -> [NiceConstructor] -> InferredMutual
    InferredMutual MutualChecks
    cs (NiceConstructor
    d NiceConstructor -> [NiceConstructor] -> [NiceConstructor]
    forall a. a -> [a] -> [a]
    : [NiceConstructor]
    ds) [NiceConstructor]
    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
    interleavedDeclNum  :: DeclNum
            -- ^ Internal number of the data signature.
        , InterleavedDecl -> NiceConstructor
    interleavedDeclSig  :: NiceDeclaration
            -- ^ The data signature.
        , InterleavedDecl -> Maybe (Int, List1 [NiceConstructor])
    interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])
            -- ^ Constructors associated to the data signature.
        }
      | InterleavedFun
        { interleavedDeclNum  :: DeclNum
            -- ^ Internal number of the function signature.
        , interleavedDeclSig  :: NiceDeclaration
            -- ^ The function signature.
        , InterleavedDecl -> Maybe (Int, List1 ([Declaration], [Clause]))
    interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration],[Clause]))
            -- ^ Function clauses associated to the function signature.
        }

    -- | Numbering declarations in an @interleaved mutual@ block.
    type DeclNum = Int

    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 -> [(DeclNum, NiceDeclaration)]
    interleavedDecl :: Name -> InterleavedDecl -> [(Int, NiceConstructor)]
    interleavedDecl Name
    k = \case
      InterleavedData Int
    i d :: NiceConstructor
    d@(NiceDataSig Range
    _ Erased
    _ Access
    acc IsAbstract
    abs PositivityCheck
    pc UniverseCheck
    uc Name
    _ [LamBinding]
    pars Expr
    _) Maybe (Int, List1 [NiceConstructor])
    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
            r :: Range
    r       = (Name, [LamBinding]) -> Range
    forall a. HasRange a => a -> Range
    getRange (Name
    k, [LamBinding]
    fpars)
            ddef :: [NiceConstructor] -> NiceConstructor
    ddef [NiceConstructor]
    cs = Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [NiceConstructor]
    -> NiceConstructor
    NiceDataDef ((Range, [NiceConstructor]) -> Range
    forall a. HasRange a => a -> Range
    getRange (Range
    r, [NiceConstructor]
    cs)) Origin
    UserWritten
                        IsAbstract
    abs PositivityCheck
    pc UniverseCheck
    uc Name
    k [LamBinding]
    fpars [NiceConstructor]
    cs
        in (Int
    i,NiceConstructor
    d) (Int, NiceConstructor)
    -> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
    forall a. a -> [a] -> [a]
    : [(Int, NiceConstructor)]
    -> ((Int, List1 [NiceConstructor]) -> [(Int, NiceConstructor)])
    -> Maybe (Int, List1 [NiceConstructor])
    -> [(Int, NiceConstructor)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\ (Int
    j, List1 [NiceConstructor]
    dss) -> [(Int
    j, [NiceConstructor] -> NiceConstructor
    ddef (List1 [NiceConstructor] -> [NiceConstructor]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (List1 [NiceConstructor] -> List1 [NiceConstructor]
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse List1 [NiceConstructor]
    dss)))]) Maybe (Int, List1 [NiceConstructor])
    ds
      InterleavedFun Int
    i d :: NiceConstructor
    d@(FunSig Range
    r Access
    acc IsAbstract
    abs IsInstance
    inst IsMacro
    mac ArgInfo
    info TerminationCheck
    tc CoverageCheck
    cc Name
    n Expr
    e) Maybe (Int, List1 ([Declaration], [Clause]))
    dcs ->
        let fdef :: List1 ([Declaration], [Clause]) -> NiceConstructor
    fdef List1 ([Declaration], [Clause])
    dcss = let (NonEmpty [Declaration]
    dss, NonEmpty [Clause]
    css) = List1 ([Declaration], [Clause])
    -> (NonEmpty [Declaration], NonEmpty [Clause])
    forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
    List1.unzip List1 ([Declaration], [Clause])
    dcss in
                        Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceConstructor
    FunDef Range
    r (NonEmpty [Declaration] -> [Declaration]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat NonEmpty [Declaration]
    dss) IsAbstract
    abs IsInstance
    inst TerminationCheck
    tc CoverageCheck
    cc Name
    n (NonEmpty [Clause] -> [Clause]
    forall a. Semigroup a => NonEmpty a -> a
    sconcat NonEmpty [Clause]
    css)
        in (Int
    i,NiceConstructor
    d) (Int, NiceConstructor)
    -> [(Int, NiceConstructor)] -> [(Int, NiceConstructor)]
    forall a. a -> [a] -> [a]
    : [(Int, NiceConstructor)]
    -> ((Int, List1 ([Declaration], [Clause]))
        -> [(Int, NiceConstructor)])
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    -> [(Int, NiceConstructor)]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\ (Int
    j, List1 ([Declaration], [Clause])
    dcss) -> [(Int
    j, List1 ([Declaration], [Clause]) -> NiceConstructor
    fdef (List1 ([Declaration], [Clause]) -> List1 ([Declaration], [Clause])
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse List1 ([Declaration], [Clause])
    dcss))]) Maybe (Int, List1 ([Declaration], [Clause]))
    dcs
      InterleavedDecl
    _ -> [(Int, NiceConstructor)]
    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 (KindOfBlock -> KindOfBlock -> Bool
    (KindOfBlock -> KindOfBlock -> Bool)
    -> (KindOfBlock -> KindOfBlock -> Bool) -> Eq KindOfBlock
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: KindOfBlock -> KindOfBlock -> Bool
    == :: KindOfBlock -> KindOfBlock -> Bool
    $c/= :: KindOfBlock -> KindOfBlock -> Bool
    /= :: 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
    $ccompare :: KindOfBlock -> KindOfBlock -> Ordering
    compare :: KindOfBlock -> KindOfBlock -> Ordering
    $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
    >= :: KindOfBlock -> KindOfBlock -> Bool
    $cmax :: KindOfBlock -> KindOfBlock -> KindOfBlock
    max :: KindOfBlock -> KindOfBlock -> KindOfBlock
    $cmin :: KindOfBlock -> KindOfBlock -> KindOfBlock
    min :: KindOfBlock -> KindOfBlock -> 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
    $cshowsPrec :: Int -> KindOfBlock -> ShowS
    showsPrec :: Int -> KindOfBlock -> ShowS
    $cshow :: KindOfBlock -> String
    show :: KindOfBlock -> String
    $cshowList :: [KindOfBlock] -> ShowS
    showList :: [KindOfBlock] -> ShowS
    Show, (forall x. KindOfBlock -> Rep KindOfBlock x)
    -> (forall x. Rep KindOfBlock x -> KindOfBlock)
    -> Generic KindOfBlock
    forall x. Rep KindOfBlock x -> KindOfBlock
    forall x. KindOfBlock -> Rep KindOfBlock x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. KindOfBlock -> Rep KindOfBlock x
    from :: forall x. KindOfBlock -> Rep KindOfBlock x
    $cto :: forall x. Rep KindOfBlock x -> KindOfBlock
    to :: forall x. Rep KindOfBlock x -> KindOfBlock
    Generic)

    instance NFData KindOfBlock

    instance HasRange NiceDeclaration where
      getRange :: NiceConstructor -> 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 KwRange
    kwr TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    _ [NiceConstructor]
    ds)       = KwRange -> [NiceConstructor] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [NiceConstructor]
    ds
      getRange (NiceModule Range
    r Access
    _ IsAbstract
    _ Erased
    _ QName
    _ Telescope
    _ [Declaration]
    _ )     = Range
    r
      getRange (NiceModuleMacro Range
    r Access
    _ Erased
    _ 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]
    _ [NiceConstructor]
    _)   = Range
    r
      getRange (NiceLoneConstructor KwRange
    kwr [NiceConstructor]
    ds)    = KwRange -> [NiceConstructor] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [NiceConstructor]
    ds
      getRange (NiceRecDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _)  = Range
    r
      getRange (NiceRecSig Range
    r Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _)  = Range
    r
      getRange (NiceDataSig Range
    r Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _) = Range
    r
      getRange (NicePatternSyn Range
    r Access
    _ Name
    _ [WithHiding Name]
    _ Pattern
    _)      = Range
    r
      getRange (NiceGeneralize Range
    r Access
    _ ArgInfo
    _ TacticAttribute
    _ Name
    _ Expr
    _)    = Range
    r
      getRange (NiceFunClause Range
    r Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ Catchall
    _ 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
      getRange (NiceUnquoteData Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    _ [Name]
    _ Expr
    _) = Range
    r
      getRange (NiceOpaque KwRange
    kwr [QName]
    xs [NiceConstructor]
    ds)          = (KwRange, [QName], [NiceConstructor]) -> Range
    forall a. HasRange a => a -> Range
    getRange (KwRange
    kwr, [QName]
    xs, [NiceConstructor]
    ds)

    instance Pretty NiceDeclaration where
      pretty :: NiceConstructor -> Doc
    pretty = \case
        Axiom Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ ArgInfo
    _ Name
    x Expr
    _            -> String -> Doc
    forall a. String -> Doc a
    text String
    "postulate" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    colon Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "_"
        NiceField Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TacticAttribute
    _ Name
    x Arg Expr
    _        -> String -> Doc
    forall a. String -> Doc a
    text String
    "field" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        PrimitiveFunction Range
    _ Access
    _ IsAbstract
    _ Name
    x Arg Expr
    _    -> String -> Doc
    forall a. String -> Doc a
    text String
    "primitive" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceMutual{}                   -> String -> Doc
    forall a. String -> Doc a
    text String
    "mutual"
        NiceOpaque KwRange
    _ [QName]
    _ [NiceConstructor]
    ds              -> String -> Doc
    forall a. String -> Doc a
    text String
    "opaque" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ((NiceConstructor -> Doc) -> [NiceConstructor] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceConstructor -> Doc
    forall a. Pretty a => a -> Doc
    pretty [NiceConstructor]
    ds))
        NiceModule Range
    _ Access
    _ IsAbstract
    _ Erased
    _ QName
    x Telescope
    _ [Declaration]
    _       -> String -> Doc
    forall a. String -> Doc a
    text String
    "module" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "where"
        NiceModuleMacro Range
    _ Access
    _ Erased
    _ Name
    x ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _  -> String -> Doc
    forall a. String -> Doc a
    text String
    "module" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "= ..."
        NiceOpen Range
    _ QName
    x ImportDirective
    _                 -> String -> Doc
    forall a. String -> Doc a
    text String
    "open" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
        NiceImport Range
    _ QName
    x Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _           -> String -> Doc
    forall a. String -> Doc a
    text String
    "import" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
        NicePragma{}                   -> String -> Doc
    forall a. String -> Doc a
    text String
    "{-# ... #-}"
        NiceRecSig Range
    _ Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ Expr
    _   -> String -> Doc
    forall a. String -> Doc a
    text String
    "record" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceDataSig Range
    _ Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ Expr
    _  -> String -> Doc
    forall a. String -> Doc a
    text String
    "data" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceFunClause{}                -> String -> Doc
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    colon Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "= _"
        NiceDataDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    _ [NiceConstructor]
    _    -> String -> Doc
    forall a. String -> Doc a
    text String
    "data" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "where"
        NiceLoneConstructor KwRange
    _ [NiceConstructor]
    _        -> String -> Doc
    forall a. String -> Doc a
    text String
    "data _ where"
        NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x  [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _  -> String -> Doc
    forall a. String -> Doc a
    text String
    "record" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "where"
        NicePatternSyn Range
    _ Access
    _ Name
    x [WithHiding Name]
    _ Pattern
    _       -> String -> Doc
    forall a. String -> Doc a
    text String
    "pattern" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceGeneralize Range
    _ Access
    _ ArgInfo
    _ TacticAttribute
    _ Name
    x Expr
    _     -> String -> Doc
    forall a. String -> Doc a
    text String
    "variable" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Name -> Doc
    forall a. Pretty a => a -> Doc
    pretty Name
    x
        NiceUnquoteDecl Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    xs Expr
    _ -> String -> Doc
    forall a. String -> Doc a
    text String
    "<unquote declarations>"
        NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    xs Expr
    _    -> String -> Doc
    forall a. String -> Doc a
    text String
    "<unquote definitions>"
        NiceUnquoteData Range
    _ Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [Name]
    xs Expr
    _ -> String -> Doc
    forall a. String -> Doc a
    text String
    "<unquote data types>"

    declName :: NiceDeclaration -> String
    declName :: NiceConstructor -> 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 NiceUnquoteData{}   = String
    "Unquoted data types"
    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"
    declName NiceOpaque{}          = String
    "Opaque blocks"

    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
    $c== :: InMutual -> InMutual -> Bool
    == :: InMutual -> InMutual -> Bool
    $c/= :: InMutual -> InMutual -> Bool
    /= :: 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
    $cshowsPrec :: Int -> InMutual -> ShowS
    showsPrec :: Int -> InMutual -> ShowS
    $cshow :: InMutual -> String
    show :: InMutual -> String
    $cshowList :: [InMutual] -> ShowS
    showList :: [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 (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
    $cshowsPrec :: Int -> DataRecOrFun -> ShowS
    showsPrec :: Int -> DataRecOrFun -> ShowS
    $cshow :: DataRecOrFun -> String
    show :: DataRecOrFun -> String
    $cshowList :: [DataRecOrFun] -> ShowS
    showList :: [DataRecOrFun] -> ShowS
    Show, (forall x. DataRecOrFun -> Rep DataRecOrFun x)
    -> (forall x. Rep DataRecOrFun x -> DataRecOrFun)
    -> Generic DataRecOrFun
    forall x. Rep DataRecOrFun x -> DataRecOrFun
    forall x. DataRecOrFun -> Rep DataRecOrFun x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. DataRecOrFun -> Rep DataRecOrFun x
    from :: forall x. DataRecOrFun -> Rep DataRecOrFun x
    $cto :: forall x. Rep DataRecOrFun x -> DataRecOrFun
    to :: forall x. Rep DataRecOrFun x -> DataRecOrFun
    Generic)

    instance NFData DataRecOrFun

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