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.Utils.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 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
  | NiceUnquoteData Range Access IsAbstract PositivityCheck UniverseCheck Name [Name] Expr
  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

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 (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
_ 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 -> Catchall
(KindOfBlock -> KindOfBlock -> Catchall)
-> (KindOfBlock -> KindOfBlock -> Catchall) -> Eq KindOfBlock
forall a. (a -> a -> Catchall) -> (a -> a -> Catchall) -> Eq a
$c== :: KindOfBlock -> KindOfBlock -> Catchall
== :: KindOfBlock -> KindOfBlock -> Catchall
$c/= :: KindOfBlock -> KindOfBlock -> Catchall
/= :: KindOfBlock -> KindOfBlock -> Catchall
Eq, Eq KindOfBlock
Eq KindOfBlock
-> (KindOfBlock -> KindOfBlock -> Ordering)
-> (KindOfBlock -> KindOfBlock -> Catchall)
-> (KindOfBlock -> KindOfBlock -> Catchall)
-> (KindOfBlock -> KindOfBlock -> Catchall)
-> (KindOfBlock -> KindOfBlock -> Catchall)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> (KindOfBlock -> KindOfBlock -> KindOfBlock)
-> Ord KindOfBlock
KindOfBlock -> KindOfBlock -> Catchall
KindOfBlock -> KindOfBlock -> Ordering
KindOfBlock -> KindOfBlock -> KindOfBlock
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Catchall)
-> (a -> a -> Catchall)
-> (a -> a -> Catchall)
-> (a -> a -> Catchall)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: KindOfBlock -> KindOfBlock -> Ordering
compare :: KindOfBlock -> KindOfBlock -> Ordering
$c< :: KindOfBlock -> KindOfBlock -> Catchall
< :: KindOfBlock -> KindOfBlock -> Catchall
$c<= :: KindOfBlock -> KindOfBlock -> Catchall
<= :: KindOfBlock -> KindOfBlock -> Catchall
$c> :: KindOfBlock -> KindOfBlock -> Catchall
> :: KindOfBlock -> KindOfBlock -> Catchall
$c>= :: KindOfBlock -> KindOfBlock -> Catchall
>= :: KindOfBlock -> KindOfBlock -> Catchall
$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)


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 Range
r TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceConstructor]
_)          = 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]
_ [NiceConstructor]
_)   = Range
r
  getRange (NiceLoneConstructor Range
r [NiceConstructor]
_)       = 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
_ 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

instance Pretty NiceDeclaration where
  pretty :: NiceConstructor -> 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]
_ [NiceConstructor]
_    -> 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
_ [NiceConstructor]
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>"
    NiceUnquoteData Range
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x [Name]
xs Expr
_ -> String -> Doc
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"


data InMutual
  = InMutual    -- ^ we are nicifying a mutual block
  | NotInMutual -- ^ we are nicifying decls not in a mutual block
    deriving (InMutual -> InMutual -> Catchall
(InMutual -> InMutual -> Catchall)
-> (InMutual -> InMutual -> Catchall) -> Eq InMutual
forall a. (a -> a -> Catchall) -> (a -> a -> Catchall) -> Eq a
$c== :: InMutual -> InMutual -> Catchall
== :: InMutual -> InMutual -> Catchall
$c/= :: InMutual -> InMutual -> Catchall
/= :: InMutual -> InMutual -> Catchall
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

-- Ignore pragmas when checking equality
instance Eq DataRecOrFun where
  DataName{} == :: DataRecOrFun -> DataRecOrFun -> Catchall
== DataName{} = Catchall
True
  RecName{}  == RecName{}  = Catchall
True
  FunName{}  == FunName{}  = Catchall
True
  DataRecOrFun
_          == DataRecOrFun
_          = Catchall
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 -> Catchall
isFunName (FunName{}) = Catchall
True
isFunName DataRecOrFun
_           = Catchall
False

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

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