module Agda.Syntax.Concrete.Definitions.Errors where

import Control.DeepSeq

import GHC.Generics (Generic)

import Agda.Syntax.Position
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Definitions.Types

import Agda.Interaction.Options.Warnings

import Agda.Utils.CallStack ( CallStack )
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List2 (List2, pattern List2)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty

------------------------------------------------------------------------
-- Errors

-- | Exception with internal source code callstack
data DeclarationException = DeclarationException
  { DeclarationException -> CallStack
deLocation  :: CallStack
  , DeclarationException -> DeclarationException'
deException :: DeclarationException'
  }

-- | The exception type.
data DeclarationException'
  = MultipleEllipses Pattern
  | InvalidName Name
  | DuplicateDefinition Name
  | DuplicateAnonDeclaration Range
  | MissingWithClauses Name LHS
  | WrongDefinition Name DataRecOrFun DataRecOrFun
  | DeclarationPanic String
  | WrongContentBlock KindOfBlock Range
  | AmbiguousFunClauses LHS (List1 Name)
      -- ^ In a mutual block, a clause could belong to any of the ≥2 type signatures ('Name').
  | AmbiguousConstructor Range Name [Name]
      -- ^ In an interleaved mutual block, a constructor could belong to any of the data signatures ('Name')
  | InvalidMeasureMutual Range
      -- ^ In a mutual block, all or none need a MEASURE pragma.
      --   Range is of mutual block.
  | UnquoteDefRequiresSignature (List1 Name)
  | BadMacroDef NiceDeclaration
    deriving Int -> DeclarationException' -> ShowS
[DeclarationException'] -> ShowS
DeclarationException' -> String
(Int -> DeclarationException' -> ShowS)
-> (DeclarationException' -> String)
-> ([DeclarationException'] -> ShowS)
-> Show DeclarationException'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclarationException' -> ShowS
showsPrec :: Int -> DeclarationException' -> ShowS
$cshow :: DeclarationException' -> String
show :: DeclarationException' -> String
$cshowList :: [DeclarationException'] -> ShowS
showList :: [DeclarationException'] -> ShowS
Show

------------------------------------------------------------------------
-- Warnings

data DeclarationWarning = DeclarationWarning
  { DeclarationWarning -> CallStack
dwLocation :: CallStack
  , DeclarationWarning -> DeclarationWarning'
dwWarning  :: DeclarationWarning'
  } deriving (Int -> DeclarationWarning -> ShowS
[DeclarationWarning] -> ShowS
DeclarationWarning -> String
(Int -> DeclarationWarning -> ShowS)
-> (DeclarationWarning -> String)
-> ([DeclarationWarning] -> ShowS)
-> Show DeclarationWarning
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclarationWarning -> ShowS
showsPrec :: Int -> DeclarationWarning -> ShowS
$cshow :: DeclarationWarning -> String
show :: DeclarationWarning -> String
$cshowList :: [DeclarationWarning] -> ShowS
showList :: [DeclarationWarning] -> ShowS
Show, (forall x. DeclarationWarning -> Rep DeclarationWarning x)
-> (forall x. Rep DeclarationWarning x -> DeclarationWarning)
-> Generic DeclarationWarning
forall x. Rep DeclarationWarning x -> DeclarationWarning
forall x. DeclarationWarning -> Rep DeclarationWarning x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DeclarationWarning -> Rep DeclarationWarning x
from :: forall x. DeclarationWarning -> Rep DeclarationWarning x
$cto :: forall x. Rep DeclarationWarning x -> DeclarationWarning
to :: forall x. Rep DeclarationWarning x -> DeclarationWarning
Generic)

-- | Non-fatal errors encountered in the Nicifier.
data DeclarationWarning'
  -- Please keep in alphabetical order.
  = EmptyAbstract Range    -- ^ Empty @abstract@  block.
  | EmptyConstructor Range -- ^ Empty @constructor@ block.
  | EmptyField Range       -- ^ Empty @field@     block.
  | EmptyGeneralize Range  -- ^ Empty @variable@  block.
  | EmptyInstance Range    -- ^ Empty @instance@  block
  | EmptyMacro Range       -- ^ Empty @macro@     block.
  | EmptyMutual Range      -- ^ Empty @mutual@    block.
  | EmptyPostulate Range   -- ^ Empty @postulate@ block.
  | EmptyPrivate Range     -- ^ Empty @private@   block.
  | EmptyPrimitive Range   -- ^ Empty @primitive@ block.
  | HiddenGeneralize Range
      -- ^ A 'Hidden' identifier in a @variable@ declaration.
      --   Hiding has no effect there as generalized variables are always hidden
      --   (or instance variables).
  | InvalidCatchallPragma Range
      -- ^ A {-\# CATCHALL \#-} pragma
      --   that does not precede a function clause.
  | InvalidConstructor Range
      -- ^ Invalid definition in a constructor block
  | InvalidConstructorBlock Range
      -- ^ Invalid constructor block (not inside an interleaved mutual block)
  | InvalidCoverageCheckPragma Range
      -- ^ A {-\# NON_COVERING \#-} pragma that does not apply to any function.
  | InvalidNoPositivityCheckPragma Range
      -- ^ A {-\# NO_POSITIVITY_CHECK \#-} pragma
      --   that does not apply to any data or record type.
  | InvalidNoUniverseCheckPragma Range
      -- ^ A {-\# NO_UNIVERSE_CHECK \#-} pragma
      --   that does not apply to a data or record type.
  | InvalidRecordDirective Range
      -- ^ A record directive outside of a record / below existing fields.
  | InvalidTerminationCheckPragma Range
      -- ^ A {-\# TERMINATING \#-} and {-\# NON_TERMINATING \#-} pragma
      --   that does not apply to any function.
  | MissingDeclarations [(Name, Range)]
      -- ^ Definitions (e.g. constructors or functions) without a declaration.
  | MissingDefinitions [(Name, Range)]
      -- ^ Declarations (e.g. type signatures) without a definition.
  | NotAllowedInMutual Range String
  | OpenPublicPrivate Range
      -- ^ @private@ has no effect on @open public@.  (But the user might think so.)
  | OpenPublicAbstract Range
      -- ^ @abstract@ has no effect on @open public@.  (But the user might think so.)
  | PolarityPragmasButNotPostulates [Name]
  | PragmaNoTerminationCheck Range
  -- ^ Pragma @{-\# NO_TERMINATION_CHECK \#-}@ has been replaced
  --   by @{-\# TERMINATING \#-}@ and @{-\# NON_TERMINATING \#-}@.
  | PragmaCompiled Range
  -- ^ @COMPILE@ pragmas are not allowed in safe mode
  | ShadowingInTelescope (List1 (Name, List2 Range))
  | UnknownFixityInMixfixDecl [Name]
  | UnknownNamesInFixityDecl [Name]
  | UnknownNamesInPolarityPragmas [Name]
  | UselessAbstract Range
      -- ^ @abstract@ block with nothing that can (newly) be made abstract.
  | UselessInstance Range
      -- ^ @instance@ block with nothing that can (newly) become an instance.
  | UselessPrivate Range
      -- ^ @private@ block with nothing that can (newly) be made private.
  deriving (Int -> DeclarationWarning' -> ShowS
[DeclarationWarning'] -> ShowS
DeclarationWarning' -> String
(Int -> DeclarationWarning' -> ShowS)
-> (DeclarationWarning' -> String)
-> ([DeclarationWarning'] -> ShowS)
-> Show DeclarationWarning'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclarationWarning' -> ShowS
showsPrec :: Int -> DeclarationWarning' -> ShowS
$cshow :: DeclarationWarning' -> String
show :: DeclarationWarning' -> String
$cshowList :: [DeclarationWarning'] -> ShowS
showList :: [DeclarationWarning'] -> ShowS
Show, (forall x. DeclarationWarning' -> Rep DeclarationWarning' x)
-> (forall x. Rep DeclarationWarning' x -> DeclarationWarning')
-> Generic DeclarationWarning'
forall x. Rep DeclarationWarning' x -> DeclarationWarning'
forall x. DeclarationWarning' -> Rep DeclarationWarning' x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DeclarationWarning' -> Rep DeclarationWarning' x
from :: forall x. DeclarationWarning' -> Rep DeclarationWarning' x
$cto :: forall x. Rep DeclarationWarning' x -> DeclarationWarning'
to :: forall x. Rep DeclarationWarning' x -> DeclarationWarning'
Generic)

declarationWarningName :: DeclarationWarning -> WarningName
declarationWarningName :: DeclarationWarning -> WarningName
declarationWarningName = DeclarationWarning' -> WarningName
declarationWarningName' (DeclarationWarning' -> WarningName)
-> (DeclarationWarning -> DeclarationWarning')
-> DeclarationWarning
-> WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> DeclarationWarning'
dwWarning

declarationWarningName' :: DeclarationWarning' -> WarningName
declarationWarningName' :: DeclarationWarning' -> WarningName
declarationWarningName' = \case
  -- Please keep in alphabetical order.
  EmptyAbstract{}                   -> WarningName
EmptyAbstract_
  EmptyConstructor{}                -> WarningName
EmptyConstructor_
  EmptyField{}                      -> WarningName
EmptyField_
  EmptyGeneralize{}                 -> WarningName
EmptyGeneralize_
  EmptyInstance{}                   -> WarningName
EmptyInstance_
  EmptyMacro{}                      -> WarningName
EmptyMacro_
  EmptyMutual{}                     -> WarningName
EmptyMutual_
  EmptyPrivate{}                    -> WarningName
EmptyPrivate_
  EmptyPostulate{}                  -> WarningName
EmptyPostulate_
  EmptyPrimitive{}                  -> WarningName
EmptyPrimitive_
  HiddenGeneralize{}                -> WarningName
HiddenGeneralize_
  InvalidCatchallPragma{}           -> WarningName
InvalidCatchallPragma_
  InvalidConstructor{}              -> WarningName
InvalidConstructor_
  InvalidConstructorBlock{}         -> WarningName
InvalidConstructorBlock_
  InvalidNoPositivityCheckPragma{}  -> WarningName
InvalidNoPositivityCheckPragma_
  InvalidNoUniverseCheckPragma{}    -> WarningName
InvalidNoUniverseCheckPragma_
  InvalidRecordDirective{}          -> WarningName
InvalidRecordDirective_
  InvalidTerminationCheckPragma{}   -> WarningName
InvalidTerminationCheckPragma_
  InvalidCoverageCheckPragma{}      -> WarningName
InvalidCoverageCheckPragma_
  MissingDeclarations{}             -> WarningName
MissingDeclarations_
  MissingDefinitions{}              -> WarningName
MissingDefinitions_
  NotAllowedInMutual{}              -> WarningName
NotAllowedInMutual_
  OpenPublicPrivate{}               -> WarningName
OpenPublicPrivate_
  OpenPublicAbstract{}              -> WarningName
OpenPublicAbstract_
  PolarityPragmasButNotPostulates{} -> WarningName
PolarityPragmasButNotPostulates_
  PragmaNoTerminationCheck{}        -> WarningName
PragmaNoTerminationCheck_
  PragmaCompiled{}                  -> WarningName
PragmaCompiled_
  ShadowingInTelescope{}            -> WarningName
ShadowingInTelescope_
  UnknownFixityInMixfixDecl{}       -> WarningName
UnknownFixityInMixfixDecl_
  UnknownNamesInFixityDecl{}        -> WarningName
UnknownNamesInFixityDecl_
  UnknownNamesInPolarityPragmas{}   -> WarningName
UnknownNamesInPolarityPragmas_
  UselessAbstract{}                 -> WarningName
UselessAbstract_
  UselessInstance{}                 -> WarningName
UselessInstance_
  UselessPrivate{}                  -> WarningName
UselessPrivate_

-- | Nicifier warnings turned into errors in @--safe@ mode.
unsafeDeclarationWarning :: DeclarationWarning -> Bool
unsafeDeclarationWarning :: DeclarationWarning -> Bool
unsafeDeclarationWarning = DeclarationWarning' -> Bool
unsafeDeclarationWarning' (DeclarationWarning' -> Bool)
-> (DeclarationWarning -> DeclarationWarning')
-> DeclarationWarning
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeclarationWarning -> DeclarationWarning'
dwWarning

unsafeDeclarationWarning' :: DeclarationWarning' -> Bool
unsafeDeclarationWarning' :: DeclarationWarning' -> Bool
unsafeDeclarationWarning' = \case
  -- Please keep in alphabetical order.
  EmptyAbstract{}                   -> Bool
False
  EmptyConstructor{}                -> Bool
False
  EmptyField{}                      -> Bool
False
  EmptyGeneralize{}                 -> Bool
False
  EmptyInstance{}                   -> Bool
False
  EmptyMacro{}                      -> Bool
False
  EmptyMutual{}                     -> Bool
False
  EmptyPrivate{}                    -> Bool
False
  EmptyPostulate{}                  -> Bool
False
  EmptyPrimitive{}                  -> Bool
False
  HiddenGeneralize{}                -> Bool
False
  InvalidCatchallPragma{}           -> Bool
False
  InvalidConstructor{}              -> Bool
False
  InvalidConstructorBlock{}         -> Bool
False
  InvalidNoPositivityCheckPragma{}  -> Bool
False
  InvalidNoUniverseCheckPragma{}    -> Bool
False
  InvalidRecordDirective{}          -> Bool
False
  InvalidTerminationCheckPragma{}   -> Bool
False
  InvalidCoverageCheckPragma{}      -> Bool
False
  MissingDeclarations{}             -> Bool
True  -- not safe
  MissingDefinitions{}              -> Bool
True  -- not safe
  NotAllowedInMutual{}              -> Bool
False -- really safe?
  OpenPublicPrivate{}               -> Bool
False
  OpenPublicAbstract{}              -> Bool
False
  PolarityPragmasButNotPostulates{} -> Bool
False
  PragmaNoTerminationCheck{}        -> Bool
True  -- not safe
  PragmaCompiled{}                  -> Bool
True  -- not safe
  ShadowingInTelescope{}            -> Bool
False
  UnknownFixityInMixfixDecl{}       -> Bool
False
  UnknownNamesInFixityDecl{}        -> Bool
False
  UnknownNamesInPolarityPragmas{}   -> Bool
False
  UselessAbstract{}                 -> Bool
False
  UselessInstance{}                 -> Bool
False
  UselessPrivate{}                  -> Bool
False

------------------------------------------------------------------------
-- Instances

instance HasRange DeclarationException where
  getRange :: DeclarationException -> Range
getRange (DeclarationException CallStack
_ DeclarationException'
err) = DeclarationException' -> Range
forall a. HasRange a => a -> Range
getRange DeclarationException'
err

instance HasRange DeclarationException' where
  getRange :: DeclarationException' -> Range
getRange (MultipleEllipses Pattern
d)                 = Pattern -> Range
forall a. HasRange a => a -> Range
getRange Pattern
d
  getRange (InvalidName Name
x)                      = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
  getRange (DuplicateDefinition Name
x)              = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
  getRange (DuplicateAnonDeclaration Range
r)         = Range
r
  getRange (MissingWithClauses Name
x LHS
lhs)           = LHS -> Range
forall a. HasRange a => a -> Range
getRange LHS
lhs
  getRange (WrongDefinition Name
x DataRecOrFun
k DataRecOrFun
k')             = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
  getRange (AmbiguousFunClauses LHS
lhs List1 Name
xs)         = LHS -> Range
forall a. HasRange a => a -> Range
getRange LHS
lhs
  getRange (AmbiguousConstructor Range
r Name
_ [Name]
_)         = Range
r
  getRange (DeclarationPanic String
_)                 = Range
forall a. Range' a
noRange
  getRange (WrongContentBlock KindOfBlock
_ Range
r)              = Range
r
  getRange (InvalidMeasureMutual Range
r)             = Range
r
  getRange (UnquoteDefRequiresSignature List1 Name
x)      = List1 Name -> Range
forall a. HasRange a => a -> Range
getRange List1 Name
x
  getRange (BadMacroDef NiceDeclaration
d)                      = NiceDeclaration -> Range
forall a. HasRange a => a -> Range
getRange NiceDeclaration
d

instance HasRange DeclarationWarning where
  getRange :: DeclarationWarning -> Range
getRange (DeclarationWarning CallStack
_ DeclarationWarning'
w) = DeclarationWarning' -> Range
forall a. HasRange a => a -> Range
getRange DeclarationWarning'
w

instance HasRange DeclarationWarning' where
  getRange :: DeclarationWarning' -> Range
getRange (UnknownNamesInFixityDecl [Name]
xs)        = [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
  getRange (UnknownFixityInMixfixDecl [Name]
xs)       = [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
  getRange (UnknownNamesInPolarityPragmas [Name]
xs)   = [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
  getRange (PolarityPragmasButNotPostulates [Name]
xs) = [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
  getRange (MissingDeclarations [(Name, Range)]
xs)             = [(Name, Range)] -> Range
forall a. HasRange a => a -> Range
getRange [(Name, Range)]
xs
  getRange (MissingDefinitions [(Name, Range)]
xs)              = [(Name, Range)] -> Range
forall a. HasRange a => a -> Range
getRange [(Name, Range)]
xs
  getRange (UselessPrivate Range
r)                   = Range
r
  getRange (NotAllowedInMutual Range
r String
x)             = Range
r
  getRange (UselessAbstract Range
r)                  = Range
r
  getRange (UselessInstance Range
r)                  = Range
r
  getRange (EmptyConstructor Range
r)                 = Range
r
  getRange (EmptyMutual Range
r)                      = Range
r
  getRange (EmptyAbstract Range
r)                    = Range
r
  getRange (EmptyPrivate Range
r)                     = Range
r
  getRange (EmptyInstance Range
r)                    = Range
r
  getRange (EmptyMacro Range
r)                       = Range
r
  getRange (EmptyPostulate Range
r)                   = Range
r
  getRange (EmptyGeneralize Range
r)                  = Range
r
  getRange (EmptyPrimitive Range
r)                   = Range
r
  getRange (EmptyField Range
r)                       = Range
r
  getRange (HiddenGeneralize Range
r)                 = Range
r
  getRange (InvalidTerminationCheckPragma Range
r)    = Range
r
  getRange (InvalidCoverageCheckPragma Range
r)       = Range
r
  getRange (InvalidNoPositivityCheckPragma Range
r)   = Range
r
  getRange (InvalidCatchallPragma Range
r)            = Range
r
  getRange (InvalidConstructor Range
r)               = Range
r
  getRange (InvalidConstructorBlock Range
r)          = Range
r
  getRange (InvalidNoUniverseCheckPragma Range
r)     = Range
r
  getRange (InvalidRecordDirective Range
r)           = Range
r
  getRange (PragmaNoTerminationCheck Range
r)         = Range
r
  getRange (PragmaCompiled Range
r)                   = Range
r
  getRange (OpenPublicAbstract Range
r)               = Range
r
  getRange (OpenPublicPrivate Range
r)                = Range
r
  getRange (ShadowingInTelescope List1 (Name, List2 Range)
ns)            = List1 (Name, List2 Range) -> Range
forall a. HasRange a => a -> Range
getRange List1 (Name, List2 Range)
ns

-- These error messages can (should) be terminated by a dot ".",
-- there is no error context printed after them.
instance Pretty DeclarationException' where
  pretty :: DeclarationException' -> Doc
pretty (MultipleEllipses Pattern
p) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Multiple ellipses in left-hand side" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p]
  pretty (InvalidName Name
x) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Invalid name:" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x]
  pretty (DuplicateDefinition Name
x) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Duplicate definition of" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x]
  pretty (DuplicateAnonDeclaration Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Duplicate declaration of _"
  pretty (MissingWithClauses Name
x LHS
lhs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Missing with-clauses for function" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x]

  pretty (WrongDefinition Name
x DataRecOrFun
k DataRecOrFun
k') = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
    String -> [Doc]
pwords (String
"has been declared as a " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DataRecOrFun -> String
forall a. Pretty a => a -> String
prettyShow DataRecOrFun
k String -> ShowS
forall a. [a] -> [a] -> [a]
++
      String
", but is being defined as a " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DataRecOrFun -> String
forall a. Pretty a => a -> String
prettyShow DataRecOrFun
k')
  pretty (AmbiguousFunClauses LHS
lhs List1 Name
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
    [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
        String -> [Doc]
pwords String
"More than one matching type signature for left hand side " [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [LHS -> Doc
forall a. Pretty a => a -> Doc
pretty LHS
lhs] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
        String -> [Doc]
pwords String
"it could belong to any of:"
    , NonEmpty Doc -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> List1 Name -> NonEmpty Doc
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrintRange Name -> Doc
forall a. Pretty a => a -> Doc
pretty (PrintRange Name -> Doc)
-> (Name -> PrintRange Name) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> PrintRange Name
forall a. a -> PrintRange a
PrintRange) List1 Name
xs
    ]
  pretty (AmbiguousConstructor Range
_ Name
n [Name]
ns) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
    [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (String -> [Doc]
pwords String
"Could not find a matching data signature for constructor " [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n])
    , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (case [Name]
ns of
              [] -> [[Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"There was no candidate."]
              [Name]
_  -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (String -> [Doc]
pwords String
"It could be any of:") Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrintRange Name -> Doc
forall a. Pretty a => a -> Doc
pretty (PrintRange Name -> Doc)
-> (Name -> PrintRange Name) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> PrintRange Name
forall a. a -> PrintRange a
PrintRange) [Name]
ns
           )
    ]
  pretty (WrongContentBlock KindOfBlock
b Range
_)      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc]
pwords (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    case KindOfBlock
b of
      KindOfBlock
PostulateBlock -> String
"A postulate block can only contain type signatures, possibly under keyword instance"
      KindOfBlock
DataBlock -> String
"A data definition can only contain type signatures, possibly under keyword instance"
      KindOfBlock
_ -> String
"Unexpected declaration"
  pretty (InvalidMeasureMutual Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"In a mutual block, either all functions must have the same (or no) termination checking pragma."
  pretty (UnquoteDefRequiresSignature List1 Name
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Missing type signatures for unquoteDef" [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty (List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Name
xs)
  pretty (BadMacroDef NiceDeclaration
nd) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> Doc
text (NiceDeclaration -> String
declName NiceDeclaration
nd) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: String -> [Doc]
pwords String
"are not allowed in macro blocks"
  pretty (DeclarationPanic String
s) = String -> Doc
text String
s

instance Pretty DeclarationWarning where
  pretty :: DeclarationWarning -> Doc
pretty (DeclarationWarning CallStack
_ DeclarationWarning'
w) = DeclarationWarning' -> Doc
forall a. Pretty a => a -> Doc
pretty DeclarationWarning'
w

instance Pretty DeclarationWarning' where
  pretty :: DeclarationWarning' -> Doc
pretty (UnknownNamesInFixityDecl [Name]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"The following names are not declared in the same scope as their syntax or fixity declaration (i.e., either not in scope at all, imported from another module, or declared in a super module):"
    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs)
  pretty (UnknownFixityInMixfixDecl [Name]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"The following mixfix names do not have an associated fixity declaration:"
    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs)
  pretty (UnknownNamesInPolarityPragmas [Name]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"The following names are not declared in the same scope as their polarity pragmas (they could for instance be out of scope, imported from another module, or declared in a super module):"
    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma  ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs)
  pretty (MissingDeclarations [(Name, Range)]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
   String -> [Doc]
pwords String
"The following names are defined but not accompanied by a declaration:"
   [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma (((Name, Range) -> Doc) -> [(Name, Range)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> ((Name, Range) -> Name) -> (Name, Range) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Range) -> Name
forall a b. (a, b) -> a
fst) [(Name, Range)]
xs)
  pretty (MissingDefinitions [(Name, Range)]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
   String -> [Doc]
pwords String
"The following names are declared but not accompanied by a definition:"
   [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma (((Name, Range) -> Doc) -> [(Name, Range)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> ((Name, Range) -> Name) -> (Name, Range) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Range) -> Name
forall a b. (a, b) -> a
fst) [(Name, Range)]
xs)
  pretty (NotAllowedInMutual Range
r String
nd) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> Doc
text String
nd Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: String -> [Doc]
pwords String
"in mutual blocks are not supported.  Suggestion: get rid of the mutual block by manually ordering declarations"
  pretty (PolarityPragmasButNotPostulates [Name]
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Polarity pragmas have been given for the following identifiers which are not postulates:"
    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
xs)
  pretty (UselessPrivate Range
_)      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations."
  pretty (UselessAbstract Range
_)      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Using abstract here has no effect. Abstract applies to only definitions like data definitions, record type definitions and function clauses."
  pretty (UselessInstance Range
_)      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms."
  pretty (EmptyMutual    Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty mutual block."
  pretty EmptyConstructor{}  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty constructor block."
  pretty (EmptyAbstract  Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty abstract block."
  pretty (EmptyPrivate   Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty private block."
  pretty (EmptyInstance  Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty instance block."
  pretty (EmptyMacro     Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty macro block."
  pretty (EmptyPostulate Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty postulate block."
  pretty (EmptyGeneralize Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty variable block."
  pretty (EmptyPrimitive Range
_)  = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty primitive block."
  pretty (EmptyField Range
_)      = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Empty field block."
  pretty (HiddenGeneralize Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
pwords String
"Declaring a variable as hidden has no effect in a variable block. Generalization never introduces visible arguments."
  pretty InvalidRecordDirective{} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Record directives can only be used inside record definitions and before field declarations."
  pretty (InvalidTerminationCheckPragma Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Termination checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."
  pretty InvalidConstructor{} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"`constructor' blocks may only contain type signatures for constructors."
  pretty InvalidConstructorBlock{} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"No `constructor' blocks outside of `interleaved mutual' blocks."
  pretty (InvalidCoverageCheckPragma Range
_)    = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Coverage checking pragmas can only precede a function definition or a mutual block (that contains a function definition)."
  pretty (InvalidNoPositivityCheckPragma Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"NO_POSITIVITY_CHECKING pragmas can only precede a data/record definition or a mutual block (that contains a data/record definition)."
  pretty (InvalidCatchallPragma Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"The CATCHALL pragma can only precede a function clause."
  pretty (InvalidNoUniverseCheckPragma Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"NO_UNIVERSE_CHECKING pragmas can only precede a data/record definition."
  pretty (PragmaNoTerminationCheck Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Pragma {-# NO_TERMINATION_CHECK #-} has been removed.  To skip the termination check, label your definitions either as {-# TERMINATING #-} or {-# NON_TERMINATING #-}."
  pretty (PragmaCompiled Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"COMPILE pragma not allowed in safe mode."
  pretty (OpenPublicAbstract Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"public does not have any effect in an abstract block."
  pretty (OpenPublicPrivate Range
_) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"public does not have any effect in a private block."
  pretty (ShadowingInTelescope List1 (Name, List2 Range)
nrs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    String -> [Doc]
pwords String
"Shadowing in telescope, repeated variable names:"
    [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> NonEmpty Doc -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma (((Name, List2 Range) -> Doc)
-> List1 (Name, List2 Range) -> NonEmpty Doc
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc)
-> ((Name, List2 Range) -> Name) -> (Name, List2 Range) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, List2 Range) -> Name
forall a b. (a, b) -> a
fst) List1 (Name, List2 Range)
nrs)

instance NFData DeclarationWarning
instance NFData DeclarationWarning'