{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

module Agda.Syntax.Concrete.Definitions.Types where

import Control.DeepSeq

import Data.Map (Map)

import GHC.Generics (Generic)

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

import Agda.Utils.List1 (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 (Ranged OpenShortHand) KwRange QName (Either AsName RawOpenArgs) ImportDirective
  | NicePragma Range Pragma
  | NiceRecSig Range Erased Access IsAbstract PositivityCheck
      UniverseCheck Name Parameters Expr
  | NiceDataSig Range Erased Access IsAbstract PositivityCheck
      UniverseCheck Name Parameters 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 (List1 Declaration) IsAbstract IsInstance TerminationCheck CoverageCheck Name (List1 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 DefParameters [NiceConstructor]
  | NiceLoneConstructor KwRange [NiceConstructor]
  | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [RecordDirective] DefParameters [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 -> 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
$cshowsPrec :: Int -> NiceDeclaration -> ShowS
showsPrec :: Int -> NiceDeclaration -> ShowS
$cshow :: NiceDeclaration -> String
show :: NiceDeclaration -> String
$cshowList :: [NiceDeclaration] -> ShowS
showList :: [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
$cfrom :: forall x. NiceDeclaration -> Rep NiceDeclaration x
from :: forall x. NiceDeclaration -> Rep NiceDeclaration x
$cto :: forall x. Rep NiceDeclaration x -> NiceDeclaration
to :: forall x. Rep NiceDeclaration x -> NiceDeclaration
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 ArgInfo 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

instance LensArgInfo Clause where
  getArgInfo :: Clause -> ArgInfo
getArgInfo (Clause Name
_ Catchall
_ ArgInfo
ai LHS
_ RHS
_ WhereClause
_ [Clause]
_) = ArgInfo
ai
  mapArgInfo :: (ArgInfo -> ArgInfo) -> Clause -> Clause
mapArgInfo ArgInfo -> ArgInfo
f (Clause Name
x Catchall
ca ArgInfo
ai LHS
lhs RHS
rhs WhereClause
wh [Clause]
cs) = Name
-> Catchall
-> ArgInfo
-> LHS
-> RHS
-> WhereClause
-> [Clause]
-> Clause
Clause Name
x Catchall
ca (ArgInfo -> ArgInfo
f ArgInfo
ai) LHS
lhs RHS
rhs WhereClause
wh [Clause]
cs

-- | 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
interleavedDeclNum  :: DeclNum
        -- ^ Internal number of the data signature.
    , InterleavedDecl -> NiceDeclaration
interleavedDeclSig  :: NiceDeclaration
        -- ^ The data signature.
    , InterleavedDecl
-> Maybe (Int, List1 (DefParameters, [NiceDeclaration]))
interleavedDataCons :: Maybe (DeclNum, List1 (DefParameters, [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 (List1 Declaration, List1 Clause))
interleavedFunClauses :: Maybe (DeclNum, List1 (List1 Declaration, List1 Clause))
        -- ^ Function clauses associated to the function signature.
    }

-- | Extra state for the 'Nice' monad to process interleaved mutual blocks.
data InterleavedState = ISt
  { InterleavedState -> InterleavedMutual
interleavedMutual         :: InterleavedMutual
  , InterleavedState -> MutualChecks
interleavedMutualChecks   :: MutualChecks
  , InterleavedState -> Int
interleavedCurrentDeclNum :: DeclNum
  }

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

instance HasRange InterleavedDecl where
  getRange :: InterleavedDecl -> Range
  getRange :: InterleavedDecl -> Range
getRange (InterleavedFun Int
_ NiceDeclaration
d Maybe (Int, List1 (List1 Declaration, List1 Clause))
_)  = NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d
  getRange (InterleavedData Int
_ NiceDeclaration
d Maybe (Int, List1 (DefParameters, [NiceDeclaration]))
_) = NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d

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

-- | Several declarations expect only type signatures as sub-declarations.  These are:
data KindOfBlock
  = PostulateBlock    -- ^ @postulate@.
  | PrimitiveBlock    -- ^ @primitive@.
  | 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 :: 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 KwRange
kwr TerminationCheck
_ CoverageCheck
_ PositivityCheck
_ [NiceDeclaration]
ds)       = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
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 Ranged OpenShortHand
o KwRange
r QName
x Either AsName RawOpenArgs
as ImportDirective
dir)       = (Ranged OpenShortHand, KwRange, QName, Either AsName RawOpenArgs,
 ImportDirective)
-> Range
forall a. HasRange a => a -> Range
getRange (Ranged OpenShortHand
o, KwRange
r, QName
x, Either AsName RawOpenArgs
as, ImportDirective
dir)
  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 List1 Declaration
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
_ List1 Clause
_)        = Range
r
  getRange (NiceDataDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ DefParameters
_ [NiceDeclaration]
_)   = Range
r
  getRange (NiceLoneConstructor KwRange
kwr [NiceDeclaration]
ds)    = KwRange -> [NiceDeclaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [NiceDeclaration]
ds
  getRange (NiceRecDef Range
r Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ [RecordDirective]
_ DefParameters
_ [Declaration]
_)  = Range
r
  getRange (NiceRecSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ Parameters
_ Expr
_)  = Range
r
  getRange (NiceDataSig Range
r Erased
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
_ Parameters
_ 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 [NiceDeclaration]
ds)          = (KwRange, [QName], [NiceDeclaration]) -> Range
forall a. HasRange a => a -> Range
getRange (KwRange
kwr, [QName]
xs, [NiceDeclaration]
ds)

instance Pretty NiceDeclaration where
  pretty :: NiceDeclaration -> 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]
_ [NiceDeclaration]
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 ((NiceDeclaration -> Doc) -> [NiceDeclaration] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map NiceDeclaration -> Doc
forall a. Pretty a => a -> Doc
pretty [NiceDeclaration]
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 Ranged OpenShortHand
_ KwRange
x QName
_ Either AsName RawOpenArgs
_ ImportDirective
_           -> String -> Doc
forall a. String -> Doc a
text String
"import" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> KwRange -> Doc
forall a. Pretty a => a -> Doc
pretty KwRange
x
    NicePragma{}                   -> String -> Doc
forall a. String -> Doc a
text String
"{-# ... #-}"
    NiceRecSig Range
_ Erased
_ Access
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x Parameters
_ 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 Parameters
_ 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
_ List1 Declaration
_ IsAbstract
_ IsInstance
_ TerminationCheck
_ CoverageCheck
_ Name
x List1 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 DefParameters
_ [NiceDeclaration]
_    -> 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
_ [NiceDeclaration]
_        -> String -> Doc
forall a. String -> Doc a
text String
"data _ where"
    NiceRecDef Range
_ Origin
_ IsAbstract
_ PositivityCheck
_ UniverseCheck
_ Name
x  [RecordDirective]
_ DefParameters
_ [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 :: 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 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 ArgInfo 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 ArgInfo
_ TerminationCheck
tc CoverageCheck
_) = TerminationCheck
tc
terminationCheck DataRecOrFun
_ = TerminationCheck
forall m. TerminationCheck m
TerminationCheck

coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck :: DataRecOrFun -> CoverageCheck
coverageCheck (FunName ArgInfo
_ 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 ArgInfo
_ 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 ArgInfo
_ TerminationCheck
_ CoverageCheck
_) = UniverseCheck
YesUniverseCheck