module Agda.Syntax.Concrete.Definitions.Errors where
import Control.DeepSeq
import GHC.Generics (Generic)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Definitions.Types
import Agda.Interaction.Options.Warnings
import Agda.Utils.Null ( empty )
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.Singleton
data DeclarationException = DeclarationException
{ DeclarationException -> CallStack
deLocation :: CallStack
, DeclarationException -> DeclarationException'
deException :: DeclarationException'
}
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)
| AmbiguousConstructor Range Name [Name]
| InvalidMeasureMutual Range
| UnquoteDefRequiresSignature (List1 Name)
| BadMacroDef NiceDeclaration
| UnfoldingOutsideOpaque KwRange
| OpaqueInMutual KwRange
| DisallowedInterleavedMutual KwRange String (List1 Name)
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
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)
data DeclarationWarning'
= EmptyAbstract KwRange
| EmptyConstructor KwRange
| EmptyField KwRange
| EmptyGeneralize KwRange
| EmptyInstance KwRange
| EmptyMacro KwRange
| EmptyMutual KwRange
| EmptyPostulate KwRange
| EmptyPrivate KwRange
| EmptyPrimitive KwRange
| HiddenGeneralize Range
| InvalidCatchallPragma Range
| InvalidConstructor Range
| InvalidConstructorBlock Range
| InvalidCoverageCheckPragma Range
| InvalidNoPositivityCheckPragma Range
| InvalidNoUniverseCheckPragma Range
| InvalidTerminationCheckPragma Range
| MissingDeclarations [(Name, Range)]
| MissingDefinitions [(Name, Range)]
| NotAllowedInMutual Range String
| OpenPublicPrivate KwRange
| OpenPublicAbstract KwRange
| PolarityPragmasButNotPostulates [Name]
| PragmaNoTerminationCheck Range
| PragmaCompiled Range
| SafeFlagEta Range
| SafeFlagInjective Range
| SafeFlagNoCoverageCheck Range
| SafeFlagNoPositivityCheck Range
| SafeFlagNoUniverseCheck Range
| SafeFlagNonTerminating Range
| SafeFlagPolarity Range
| SafeFlagTerminating Range
| ShadowingInTelescope (List1 (Name, List2 Range))
| UnknownFixityInMixfixDecl [Name]
| UnknownNamesInFixityDecl [Name]
| UnknownNamesInPolarityPragmas [Name]
| UselessAbstract KwRange
| UselessInstance KwRange
| UselessMacro KwRange
| UselessPrivate KwRange
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
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_
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_
SafeFlagEta {} -> WarningName
SafeFlagEta_
SafeFlagInjective {} -> WarningName
SafeFlagInjective_
SafeFlagNoCoverageCheck {} -> WarningName
SafeFlagNoCoverageCheck_
SafeFlagNoPositivityCheck {} -> WarningName
SafeFlagNoPositivityCheck_
SafeFlagNoUniverseCheck {} -> WarningName
SafeFlagNoUniverseCheck_
SafeFlagNonTerminating {} -> WarningName
SafeFlagNonTerminating_
SafeFlagPolarity {} -> WarningName
SafeFlagPolarity_
SafeFlagTerminating {} -> WarningName
SafeFlagTerminating_
ShadowingInTelescope{} -> WarningName
ShadowingInTelescope_
UnknownFixityInMixfixDecl{} -> WarningName
UnknownFixityInMixfixDecl_
UnknownNamesInFixityDecl{} -> WarningName
UnknownNamesInFixityDecl_
UnknownNamesInPolarityPragmas{} -> WarningName
UnknownNamesInPolarityPragmas_
UselessAbstract{} -> WarningName
UselessAbstract_
UselessInstance{} -> WarningName
UselessInstance_
UselessMacro{} -> WarningName
UselessMacro_
UselessPrivate{} -> WarningName
UselessPrivate_
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
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
InvalidTerminationCheckPragma{} -> Bool
False
InvalidCoverageCheckPragma{} -> Bool
False
MissingDeclarations{} -> Bool
True
MissingDefinitions{} -> Bool
True
NotAllowedInMutual{} -> Bool
False
OpenPublicPrivate{} -> Bool
False
OpenPublicAbstract{} -> Bool
False
PolarityPragmasButNotPostulates{} -> Bool
False
PragmaNoTerminationCheck{} -> Bool
True
PragmaCompiled{} -> Bool
True
SafeFlagEta {} -> Bool
True
SafeFlagInjective {} -> Bool
True
SafeFlagNoCoverageCheck {} -> Bool
True
SafeFlagNoPositivityCheck {} -> Bool
True
SafeFlagNoUniverseCheck {} -> Bool
True
SafeFlagNonTerminating {} -> Bool
True
SafeFlagPolarity {} -> Bool
True
SafeFlagTerminating {} -> Bool
True
ShadowingInTelescope{} -> Bool
False
UnknownFixityInMixfixDecl{} -> Bool
False
UnknownNamesInFixityDecl{} -> Bool
False
UnknownNamesInPolarityPragmas{} -> Bool
False
UselessAbstract{} -> Bool
False
UselessInstance{} -> Bool
False
UselessMacro{} -> Bool
False
UselessPrivate{} -> Bool
False
unsafePragma :: CMaybe DeclarationWarning' m => Pragma -> m
unsafePragma :: forall m. CMaybe DeclarationWarning' m => Pragma -> m
unsafePragma Pragma
p =
case Pragma
p of
BuiltinPragma{} -> m
forall a. Null a => a
empty
CatchallPragma{} -> m
forall a. Null a => a
empty
CompilePragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
PragmaCompiled Range
r
DisplayPragma{} -> m
forall a. Null a => a
empty
EtaPragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagEta Range
r
ForeignPragma{} -> m
forall a. Null a => a
empty
ImpossiblePragma{} -> m
forall a. Null a => a
empty
InjectivePragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagInjective Range
r
InjectiveForInferencePragma{} -> m
forall a. Null a => a
empty
InlinePragma{} -> m
forall a. Null a => a
empty
NoCoverageCheckPragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagNoCoverageCheck Range
r
NoPositivityCheckPragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagNoPositivityCheck Range
r
NoUniverseCheckPragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagNoUniverseCheck Range
r
NotProjectionLikePragma{} -> m
forall a. Null a => a
empty
OptionsPragma{} -> m
forall a. Null a => a
empty
PolarityPragma{} -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagPolarity Range
r
RewritePragma{} -> m
forall a. Null a => a
empty
StaticPragma{} -> m
forall a. Null a => a
empty
TerminationCheckPragma Range
_ TerminationCheck Name
m ->
case TerminationCheck Name
m of
TerminationCheck Name
NonTerminating -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagNonTerminating Range
r
TerminationCheck Name
Terminating -> DeclarationWarning' -> m
forall el coll. Singleton el coll => el -> coll
singleton (DeclarationWarning' -> m) -> DeclarationWarning' -> m
forall a b. (a -> b) -> a -> b
$ Range -> DeclarationWarning'
SafeFlagTerminating Range
r
TerminationCheck Name
TerminationCheck -> m
forall a. Null a => a
empty
TerminationMeasure{} -> m
forall a. Null a => a
empty
TerminationCheck Name
NoTerminationCheck -> m
forall a. Null a => a
empty
WarningOnImport{} -> m
forall a. Null a => a
empty
WarningOnUsage{} -> m
forall a. Null a => a
empty
OverlapPragma{} -> m
forall a. Null a => a
empty
where
r :: Range
r = Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p
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
getRange (UnfoldingOutsideOpaque KwRange
kwr) = KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
getRange (OpaqueInMutual KwRange
kwr) = KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
getRange (DisallowedInterleavedMutual KwRange
kwr String
_ List1 Name
_)= KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
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 = \case
EmptyAbstract KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyConstructor KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyField KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyGeneralize KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyInstance KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyMacro KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyMutual KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyPostulate KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyPrimitive KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
EmptyPrivate KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
HiddenGeneralize Range
r -> Range
r
InvalidCatchallPragma Range
r -> Range
r
InvalidConstructor Range
r -> Range
r
InvalidConstructorBlock Range
r -> Range
r
InvalidCoverageCheckPragma Range
r -> Range
r
InvalidNoPositivityCheckPragma Range
r -> Range
r
InvalidNoUniverseCheckPragma Range
r -> Range
r
InvalidTerminationCheckPragma Range
r -> Range
r
MissingDeclarations [(Name, Range)]
xs -> [(Name, Range)] -> Range
forall a. HasRange a => a -> Range
getRange [(Name, Range)]
xs
MissingDefinitions [(Name, Range)]
xs -> [(Name, Range)] -> Range
forall a. HasRange a => a -> Range
getRange [(Name, Range)]
xs
NotAllowedInMutual Range
r String
x -> Range
r
OpenPublicAbstract KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
OpenPublicPrivate KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
PolarityPragmasButNotPostulates [Name]
xs -> [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
PragmaCompiled Range
r -> Range
r
PragmaNoTerminationCheck Range
r -> Range
r
SafeFlagEta Range
r -> Range
r
SafeFlagInjective Range
r -> Range
r
SafeFlagNoCoverageCheck Range
r -> Range
r
SafeFlagNoPositivityCheck Range
r -> Range
r
SafeFlagNoUniverseCheck Range
r -> Range
r
SafeFlagNonTerminating Range
r -> Range
r
SafeFlagPolarity Range
r -> Range
r
SafeFlagTerminating Range
r -> Range
r
ShadowingInTelescope List1 (Name, List2 Range)
ns -> List1 (Name, List2 Range) -> Range
forall a. HasRange a => a -> Range
getRange List1 (Name, List2 Range)
ns
UnknownFixityInMixfixDecl [Name]
xs -> [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
UnknownNamesInFixityDecl [Name]
xs -> [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
UnknownNamesInPolarityPragmas [Name]
xs -> [Name] -> Range
forall a. HasRange a => a -> Range
getRange [Name]
xs
UselessAbstract KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
UselessInstance KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
UselessMacro KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
UselessPrivate KwRange
kwr -> KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
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:"
, List1 Doc -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (List1 Doc -> Doc) -> List1 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> List1 Name -> List1 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 keywords `instance` and `private`"
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
forall a. String -> Doc a
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
forall a. String -> Doc a
text String
s
pretty (UnfoldingOutsideOpaque KwRange
_) = [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
$
String
"Unfolding declarations can only appear as the first declaration immediately contained in an opaque block."
pretty (OpaqueInMutual KwRange
_) = [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
"Opaque blocks can not participate in mutual recursion. If the opaque definitions are to be mutually recursive, move the `mutual` block inside the `opaque` block."
pretty (DisallowedInterleavedMutual KwRange
_ String
what List1 Name
xs) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [List1 Doc] -> [Doc]
forall a. [List1 a] -> [a]
List1.concat
[ Doc -> List1 Doc
forall el coll. Singleton el coll => el -> coll
singleton (Doc -> List1 Doc) -> Doc -> List1 Doc
forall a b. (a -> b) -> a -> b
$ [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:"
, (Name -> Doc) -> List1 Name -> List1 Doc
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc
"-" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
, Doc -> List1 Doc
forall el coll. Singleton el coll => el -> coll
singleton (Doc -> List1 Doc) -> Doc -> List1 Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
fwords (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Since " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
what String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" can not participate in mutual recursion, their definition must be given before this point."
]
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 = \case
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)
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)
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)
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)
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)
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
forall a. String -> Doc a
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"
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)
UselessPrivate KwRange
_ -> [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."
UselessAbstract KwRange
_ -> [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."
UselessInstance KwRange
_ -> [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."
UselessMacro KwRange
_ -> [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 a macro block here has no effect. `macro' applies only to function definitions."
EmptyMutual KwRange
_ -> [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."
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."
EmptyAbstract KwRange
_ -> [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."
EmptyPrivate KwRange
_ -> [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."
EmptyInstance KwRange
_ -> [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."
EmptyMacro KwRange
_ -> [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."
EmptyPostulate KwRange
_ -> [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."
EmptyGeneralize KwRange
_ -> [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."
EmptyPrimitive KwRange
_ -> [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."
EmptyField KwRange
_ -> [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."
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."
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)."
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
"`data _ where' blocks may only contain type signatures for constructors."
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 `data _ where' blocks outside of `interleaved mutual' blocks."
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)."
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)."
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."
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."
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 #-}."
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."
OpenPublicAbstract KwRange
_ -> [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."
OpenPublicPrivate KwRange
_ -> [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."
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 -> List1 Doc -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma (((Name, List2 Range) -> Doc)
-> List1 (Name, List2 Range) -> List1 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)
SafeFlagEta Range
_ -> Doc -> Doc
unsafePragma Doc
"ETA"
SafeFlagInjective Range
_ -> Doc -> Doc
unsafePragma Doc
"INJECTIVE"
SafeFlagNoCoverageCheck Range
_ -> Doc -> Doc
unsafePragma Doc
"NON_COVERING"
SafeFlagNoPositivityCheck Range
_ -> Doc -> Doc
unsafePragma Doc
"NO_POSITIVITY_CHECK"
SafeFlagNoUniverseCheck Range
_ -> Doc -> Doc
unsafePragma Doc
"NO_UNIVERSE_CHECK"
SafeFlagNonTerminating Range
_ -> Doc -> Doc
unsafePragma Doc
"NON_TERMINATING"
SafeFlagPolarity Range
_ -> Doc -> Doc
unsafePragma Doc
"POLARITY"
SafeFlagTerminating Range
_ -> Doc -> Doc
unsafePragma Doc
"TERMINATING"
where
unsafePragma :: Doc -> Doc
unsafePragma Doc
s = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc
"Cannot", Doc
"use", Doc
s] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ String -> [Doc]
pwords String
"pragma with safe flag."
instance NFData DeclarationWarning
instance NFData DeclarationWarning'