module Agda.Interaction.Options.Warnings
(
WarningMode (..)
, warningSet
, warn2Error
, defaultWarningSet
, allWarnings
, usualWarnings
, noWarnings
, unsolvedWarnings
, incompleteMatchWarnings
, errorWarnings
, defaultWarningMode
, warningModeUpdate
, warningSets
, WarningName (..)
, warningName2String
, string2WarningName
, usageWarning
)
where
import Control.Arrow ( (&&&) )
import Control.Monad ( guard )
import Text.Read ( readMaybe )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe ( fromMaybe )
import Data.List ( stripPrefix, intercalate )
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Impossible
data WarningMode = WarningMode
{ WarningMode -> Set WarningName
_warningSet :: Set WarningName
, WarningMode -> Bool
_warn2Error :: Bool
} deriving (WarningMode -> WarningMode -> Bool
(WarningMode -> WarningMode -> Bool)
-> (WarningMode -> WarningMode -> Bool) -> Eq WarningMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WarningMode -> WarningMode -> Bool
$c/= :: WarningMode -> WarningMode -> Bool
== :: WarningMode -> WarningMode -> Bool
$c== :: WarningMode -> WarningMode -> Bool
Eq, Int -> WarningMode -> ShowS
[WarningMode] -> ShowS
WarningMode -> String
(Int -> WarningMode -> ShowS)
-> (WarningMode -> String)
-> ([WarningMode] -> ShowS)
-> Show WarningMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WarningMode] -> ShowS
$cshowList :: [WarningMode] -> ShowS
show :: WarningMode -> String
$cshow :: WarningMode -> String
showsPrec :: Int -> WarningMode -> ShowS
$cshowsPrec :: Int -> WarningMode -> ShowS
Show)
warningSet :: Lens' (Set WarningName) WarningMode
warningSet :: (Set WarningName -> f (Set WarningName))
-> WarningMode -> f WarningMode
warningSet f :: Set WarningName -> f (Set WarningName)
f o :: WarningMode
o = (\ ws :: Set WarningName
ws -> WarningMode
o { _warningSet :: Set WarningName
_warningSet = Set WarningName
ws }) (Set WarningName -> WarningMode)
-> f (Set WarningName) -> f WarningMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set WarningName -> f (Set WarningName)
f (WarningMode -> Set WarningName
_warningSet WarningMode
o)
warn2Error :: Lens' Bool WarningMode
warn2Error :: (Bool -> f Bool) -> WarningMode -> f WarningMode
warn2Error f :: Bool -> f Bool
f o :: WarningMode
o = (\ ws :: Bool
ws -> WarningMode
o { _warn2Error :: Bool
_warn2Error = Bool
ws }) (Bool -> WarningMode) -> f Bool -> f WarningMode
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> f Bool
f (WarningMode -> Bool
_warn2Error WarningMode
o)
defaultWarningSet :: String
defaultWarningSet :: String
defaultWarningSet = "warn"
defaultWarningMode :: WarningMode
defaultWarningMode :: WarningMode
defaultWarningMode = Set WarningName -> Bool -> WarningMode
WarningMode Set WarningName
ws Bool
False where
ws :: Set WarningName
ws = (Set WarningName, String) -> Set WarningName
forall a b. (a, b) -> a
fst ((Set WarningName, String) -> Set WarningName)
-> (Set WarningName, String) -> Set WarningName
forall a b. (a -> b) -> a -> b
$ (Set WarningName, String)
-> Maybe (Set WarningName, String) -> (Set WarningName, String)
forall a. a -> Maybe a -> a
fromMaybe (Set WarningName, String)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Set WarningName, String) -> (Set WarningName, String))
-> Maybe (Set WarningName, String) -> (Set WarningName, String)
forall a b. (a -> b) -> a -> b
$ String
-> [(String, (Set WarningName, String))]
-> Maybe (Set WarningName, String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
defaultWarningSet [(String, (Set WarningName, String))]
warningSets
warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate str :: String
str = case String
str of
"error" -> (WarningMode -> WarningMode) -> Maybe (WarningMode -> WarningMode)
forall a. a -> Maybe a
Just ((WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode))
-> (WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode)
forall a b. (a -> b) -> a -> b
$ Lens' Bool WarningMode -> LensSet Bool WarningMode
forall i o. Lens' i o -> LensSet i o
set Lens' Bool WarningMode
warn2Error Bool
True
"noerror" -> (WarningMode -> WarningMode) -> Maybe (WarningMode -> WarningMode)
forall a. a -> Maybe a
Just ((WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode))
-> (WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode)
forall a b. (a -> b) -> a -> b
$ Lens' Bool WarningMode -> LensSet Bool WarningMode
forall i o. Lens' i o -> LensSet i o
set Lens' Bool WarningMode
warn2Error Bool
False
_ | Just ws :: Set WarningName
ws <- (Set WarningName, String) -> Set WarningName
forall a b. (a, b) -> a
fst ((Set WarningName, String) -> Set WarningName)
-> Maybe (Set WarningName, String) -> Maybe (Set WarningName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> [(String, (Set WarningName, String))]
-> Maybe (Set WarningName, String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
str [(String, (Set WarningName, String))]
warningSets
-> (WarningMode -> WarningMode) -> Maybe (WarningMode -> WarningMode)
forall a. a -> Maybe a
Just ((WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode))
-> (WarningMode -> WarningMode)
-> Maybe (WarningMode -> WarningMode)
forall a b. (a -> b) -> a -> b
$ Lens' (Set WarningName) WarningMode
-> LensSet (Set WarningName) WarningMode
forall i o. Lens' i o -> LensSet i o
set Lens' (Set WarningName) WarningMode
warningSet Set WarningName
ws
_ -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "no" String
str of
Just str' :: String
str' -> (Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet LensMap (Set WarningName) WarningMode
-> (WarningName -> Set WarningName -> Set WarningName)
-> WarningName
-> WarningMode
-> WarningMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.delete) (WarningName -> WarningMode -> WarningMode)
-> Maybe WarningName -> Maybe (WarningMode -> WarningMode)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe WarningName
string2WarningName String
str'
Nothing -> (Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet LensMap (Set WarningName) WarningMode
-> (WarningName -> Set WarningName -> Set WarningName)
-> WarningName
-> WarningMode
-> WarningMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.insert) (WarningName -> WarningMode -> WarningMode)
-> Maybe WarningName -> Maybe (WarningMode -> WarningMode)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe WarningName
string2WarningName String
str
warningSets :: [(String, (Set WarningName, String))]
warningSets :: [(String, (Set WarningName, String))]
warningSets = [ ("all" , (Set WarningName
allWarnings, "All of the existing warnings"))
, ("warn" , (Set WarningName
usualWarnings, "Default warning level"))
, ("ignore", (Set WarningName
errorWarnings, "Ignore all the benign warnings"))
]
noWarnings :: Set WarningName
noWarnings :: Set WarningName
noWarnings = Set WarningName
forall a. Set a
Set.empty
unsolvedWarnings :: Set WarningName
unsolvedWarnings :: Set WarningName
unsolvedWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
UnsolvedMetaVariables_
, WarningName
UnsolvedInteractionMetas_
, WarningName
UnsolvedConstraints_
]
incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings :: Set WarningName
incompleteMatchWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList [ WarningName
CoverageIssue_ ]
errorWarnings :: Set WarningName
errorWarnings :: Set WarningName
errorWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
CoverageIssue_
, WarningName
GenericNonFatalError_
, WarningName
MissingDefinitions_
, WarningName
NotAllowedInMutual_
, WarningName
NotStrictlyPositive_
, WarningName
OverlappingTokensWarning_
, WarningName
PragmaCompiled_
, WarningName
SafeFlagPostulate_
, WarningName
SafeFlagPragma_
, WarningName
SafeFlagNonTerminating_
, WarningName
SafeFlagTerminating_
, WarningName
SafeFlagWithoutKFlagPrimEraseEquality_
, WarningName
SafeFlagNoPositivityCheck_
, WarningName
SafeFlagPolarity_
, WarningName
SafeFlagNoUniverseCheck_
, WarningName
SafeFlagEta_
, WarningName
SafeFlagInjective_
, WarningName
SafeFlagNoCoverageCheck_
, WarningName
TerminationIssue_
, WarningName
UnsolvedMetaVariables_
, WarningName
UnsolvedInteractionMetas_
, WarningName
UnsolvedConstraints_
, WarningName
InfectiveImport_
, WarningName
CoInfectiveImport_
, WarningName
RewriteNonConfluent_
, WarningName
RewriteMaybeNonConfluent_
]
allWarnings :: Set WarningName
allWarnings :: Set WarningName
allWarnings = [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound]
usualWarnings :: Set WarningName
usualWarnings :: Set WarningName
usualWarnings = Set WarningName
allWarnings Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ [WarningName] -> Set WarningName
forall a. Ord a => [a] -> Set a
Set.fromList
[ WarningName
UnknownFixityInMixfixDecl_
, WarningName
CoverageNoExactSplit_
, WarningName
ShadowingInTelescope_
]
data WarningName
=
OverlappingTokensWarning_
| LibUnknownField_
| EmptyAbstract_
| EmptyField_
| EmptyGeneralize_
| EmptyInstance_
| EmptyMacro_
| EmptyMutual_
| EmptyPostulate_
| EmptyPrimitive_
| EmptyPrivate_
| EmptyRewritePragma_
| InvalidCatchallPragma_
| InvalidCoverageCheckPragma_
| InvalidNoPositivityCheckPragma_
| InvalidNoUniverseCheckPragma_
| InvalidTerminationCheckPragma_
| MissingDefinitions_
| NotAllowedInMutual_
| OpenPublicAbstract_
| OpenPublicPrivate_
| PolarityPragmasButNotPostulates_
| PragmaCompiled_
| PragmaNoTerminationCheck_
| ShadowingInTelescope_
| UnknownFixityInMixfixDecl_
| UnknownNamesInFixityDecl_
| UnknownNamesInPolarityPragmas_
| UselessAbstract_
| UselessInstance_
| UselessPrivate_
| AbsurdPatternRequiresNoRHS_
| CantGeneralizeOverSorts_
| ClashesViaRenaming_
| CoverageIssue_
| CoverageNoExactSplit_
| DeprecationWarning_
| FixityInRenamingModule_
| GenericNonFatalError_
| GenericWarning_
| IllformedAsClause_
| InstanceArgWithExplicitArg_
| InstanceWithExplicitArg_
| InstanceNoOutputTypeName_
| InversionDepthReached_
| ModuleDoesntExport_
| NotInScope_
| NotStrictlyPositive_
| OldBuiltin_
| PragmaCompileErased_
| RewriteMaybeNonConfluent_
| RewriteNonConfluent_
| SafeFlagEta_
| SafeFlagInjective_
| SafeFlagNoCoverageCheck_
| SafeFlagNonTerminating_
| SafeFlagNoPositivityCheck_
| SafeFlagNoUniverseCheck_
| SafeFlagPolarity_
| SafeFlagPostulate_
| SafeFlagPragma_
| SafeFlagTerminating_
| SafeFlagWithoutKFlagPrimEraseEquality_
| TerminationIssue_
| UnreachableClauses_
| UnsolvedConstraints_
| UnsolvedInteractionMetas_
| UnsolvedMetaVariables_
| UselessInline_
| UselessPublic_
| UserWarning_
| WithoutKFlagPrimEraseEquality_
| WrongInstanceDeclaration_
| CoInfectiveImport_
| InfectiveImport_
deriving (WarningName -> WarningName -> Bool
(WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool) -> Eq WarningName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WarningName -> WarningName -> Bool
$c/= :: WarningName -> WarningName -> Bool
== :: WarningName -> WarningName -> Bool
$c== :: WarningName -> WarningName -> Bool
Eq, Eq WarningName
Eq WarningName =>
(WarningName -> WarningName -> Ordering)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> Bool)
-> (WarningName -> WarningName -> WarningName)
-> (WarningName -> WarningName -> WarningName)
-> Ord WarningName
WarningName -> WarningName -> Bool
WarningName -> WarningName -> Ordering
WarningName -> WarningName -> WarningName
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
min :: WarningName -> WarningName -> WarningName
$cmin :: WarningName -> WarningName -> WarningName
max :: WarningName -> WarningName -> WarningName
$cmax :: WarningName -> WarningName -> WarningName
>= :: WarningName -> WarningName -> Bool
$c>= :: WarningName -> WarningName -> Bool
> :: WarningName -> WarningName -> Bool
$c> :: WarningName -> WarningName -> Bool
<= :: WarningName -> WarningName -> Bool
$c<= :: WarningName -> WarningName -> Bool
< :: WarningName -> WarningName -> Bool
$c< :: WarningName -> WarningName -> Bool
compare :: WarningName -> WarningName -> Ordering
$ccompare :: WarningName -> WarningName -> Ordering
$cp1Ord :: Eq WarningName
Ord, Int -> WarningName -> ShowS
[WarningName] -> ShowS
WarningName -> String
(Int -> WarningName -> ShowS)
-> (WarningName -> String)
-> ([WarningName] -> ShowS)
-> Show WarningName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WarningName] -> ShowS
$cshowList :: [WarningName] -> ShowS
show :: WarningName -> String
$cshow :: WarningName -> String
showsPrec :: Int -> WarningName -> ShowS
$cshowsPrec :: Int -> WarningName -> ShowS
Show, ReadPrec [WarningName]
ReadPrec WarningName
Int -> ReadS WarningName
ReadS [WarningName]
(Int -> ReadS WarningName)
-> ReadS [WarningName]
-> ReadPrec WarningName
-> ReadPrec [WarningName]
-> Read WarningName
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [WarningName]
$creadListPrec :: ReadPrec [WarningName]
readPrec :: ReadPrec WarningName
$creadPrec :: ReadPrec WarningName
readList :: ReadS [WarningName]
$creadList :: ReadS [WarningName]
readsPrec :: Int -> ReadS WarningName
$creadsPrec :: Int -> ReadS WarningName
Read, Int -> WarningName
WarningName -> Int
WarningName -> [WarningName]
WarningName -> WarningName
WarningName -> WarningName -> [WarningName]
WarningName -> WarningName -> WarningName -> [WarningName]
(WarningName -> WarningName)
-> (WarningName -> WarningName)
-> (Int -> WarningName)
-> (WarningName -> Int)
-> (WarningName -> [WarningName])
-> (WarningName -> WarningName -> [WarningName])
-> (WarningName -> WarningName -> [WarningName])
-> (WarningName -> WarningName -> WarningName -> [WarningName])
-> Enum WarningName
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
$cenumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]
enumFromTo :: WarningName -> WarningName -> [WarningName]
$cenumFromTo :: WarningName -> WarningName -> [WarningName]
enumFromThen :: WarningName -> WarningName -> [WarningName]
$cenumFromThen :: WarningName -> WarningName -> [WarningName]
enumFrom :: WarningName -> [WarningName]
$cenumFrom :: WarningName -> [WarningName]
fromEnum :: WarningName -> Int
$cfromEnum :: WarningName -> Int
toEnum :: Int -> WarningName
$ctoEnum :: Int -> WarningName
pred :: WarningName -> WarningName
$cpred :: WarningName -> WarningName
succ :: WarningName -> WarningName
$csucc :: WarningName -> WarningName
Enum, WarningName
WarningName -> WarningName -> Bounded WarningName
forall a. a -> a -> Bounded a
maxBound :: WarningName
$cmaxBound :: WarningName
minBound :: WarningName
$cminBound :: WarningName
Bounded)
string2WarningName :: String -> Maybe WarningName
string2WarningName :: String -> Maybe WarningName
string2WarningName = String -> Maybe WarningName
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe WarningName)
-> ShowS -> String -> Maybe WarningName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_")
warningName2String :: WarningName -> String
warningName2String :: WarningName -> String
warningName2String = ShowS
forall a. [a] -> [a]
init ShowS -> (WarningName -> String) -> WarningName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName -> String
forall a. Show a => a -> String
show
usageWarning :: String
usageWarning :: String
usageWarning = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n"
[ "The -W or --warning option can be used to disable or enable\
\ different warnings. The flag -W error (or --warning=error)\
\ can be used to turn all warnings into errors, while -W noerror\
\ turns this off again."
, ""
, "A group of warnings can be enabled by -W group, where group is\
\ one of the following:"
, ""
, [(String, String)] -> String
untable (((String, (Set WarningName, String)) -> (String, String))
-> [(String, (Set WarningName, String))] -> [(String, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String, (Set WarningName, String)) -> String
forall a b. (a, b) -> a
fst ((String, (Set WarningName, String)) -> String)
-> ((String, (Set WarningName, String)) -> String)
-> (String, (Set WarningName, String))
-> (String, String)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (Set WarningName, String) -> String
forall a b. (a, b) -> b
snd ((Set WarningName, String) -> String)
-> ((String, (Set WarningName, String))
-> (Set WarningName, String))
-> (String, (Set WarningName, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, (Set WarningName, String)) -> (Set WarningName, String)
forall a b. (a, b) -> b
snd) [(String, (Set WarningName, String))]
warningSets)
, "Individual warnings can be turned on and off by -W Name and\
\ -W noName, respectively, where Name comes from the following\
\ list (warnings marked with 'd' are turned on by default, and 'b'\
\ stands for \"benign warning\"):"
, ""
, [(String, String)] -> String
untable ([(String, String)] -> String) -> [(String, String)] -> String
forall a b. (a -> b) -> a -> b
$ [WarningName]
-> (WarningName -> Maybe (String, String)) -> [(String, String)]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [WarningName
forall a. Bounded a => a
minBound..WarningName
forall a. Bounded a => a
maxBound] ((WarningName -> Maybe (String, String)) -> [(String, String)])
-> (WarningName -> Maybe (String, String)) -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ \ w :: WarningName
w ->
let wnd :: String
wnd = WarningName -> String
warningNameDescription WarningName
w in
( WarningName -> String
warningName2String WarningName
w
, (if WarningName
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
usualWarnings then "d" else " ") String -> ShowS
forall a. [a] -> [a] -> [a]
++
(if Bool -> Bool
not (WarningName
w WarningName -> Set WarningName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
errorWarnings) then "b" else " ") String -> ShowS
forall a. [a] -> [a] -> [a]
++
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
wnd
) (String, String) -> Maybe () -> Maybe (String, String)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
wnd)
]
where
untable :: [(String, String)] -> String
untable :: [(String, String)] -> String
untable rows :: [(String, String)]
rows =
let len :: Int
len = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (((String, String) -> Int) -> [(String, String)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> ((String, String) -> String) -> (String, String) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, String) -> String
forall a b. (a, b) -> a
fst) [(String, String)]
rows) in
[String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (((String, String) -> String) -> [(String, String)] -> [String])
-> [(String, String)] -> ((String, String) -> String) -> [String]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map [(String, String)]
rows (((String, String) -> String) -> [String])
-> ((String, String) -> String) -> [String]
forall a b. (a -> b) -> a -> b
$ \ (hdr :: String
hdr, cnt :: String
cnt) ->
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
hdr, Int -> Char -> String
forall a. Int -> a -> [a]
replicate (1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hdr) ' ', String
cnt ]
warningNameDescription :: WarningName -> String
warningNameDescription :: WarningName -> String
warningNameDescription w :: WarningName
w = case WarningName
w of
OverlappingTokensWarning_ -> "Multi-line comments spanning one or more literate text blocks."
LibUnknownField_ -> "Unknown field in library file."
EmptyAbstract_ -> "Empty `abstract' blocks."
EmptyField_ -> "Empty `field` blocks."
EmptyGeneralize_ -> "Empty `variable' blocks."
EmptyInstance_ -> "Empty `instance' blocks."
EmptyMacro_ -> "Empty `macro' blocks."
EmptyMutual_ -> "Empty `mutual' blocks."
EmptyPostulate_ -> "Empty `postulate' blocks."
EmptyPrimitive_ -> "Empty `primitive' blocks."
EmptyPrivate_ -> "Empty `private' blocks."
EmptyRewritePragma_ -> "Empty `REWRITE' pragmas."
InvalidCatchallPragma_ -> "`CATCHALL' pragmas before a non-function clause."
InvalidCoverageCheckPragma_ -> "Coverage checking pragmas before non-function or `mutual' blocks."
InvalidNoPositivityCheckPragma_ -> "No positivity checking pragmas before non-`data', `record' or `mutual' blocks."
InvalidNoUniverseCheckPragma_ -> "No universe checking pragmas before non-`data' or `record' declaration."
InvalidTerminationCheckPragma_ -> "Termination checking pragmas before non-function or `mutual' blocks."
MissingDefinitions_ -> "Declarations not associated to a definition."
NotAllowedInMutual_ -> "Declarations not allowed in a mutual block."
OpenPublicAbstract_ -> "'open public' directive in an 'abstract' block."
OpenPublicPrivate_ -> "'open public' directive in a 'private' block."
PolarityPragmasButNotPostulates_ -> "Polarity pragmas for non-postulates."
PragmaCompiled_ -> "'COMPILE' pragmas not allowed in safe mode."
PragmaNoTerminationCheck_ -> "`NO_TERMINATION_CHECK' pragmas are deprecated"
ShadowingInTelescope_ -> "Repeated variable name in telescope."
UnknownFixityInMixfixDecl_ -> "Mixfix names without an associated fixity declaration."
UnknownNamesInFixityDecl_ -> "Names not declared in the same scope as their syntax or fixity declaration."
UnknownNamesInPolarityPragmas_ -> "Names not declared in the same scope as their polarity pragmas."
UselessAbstract_ -> "`abstract' blocks where they have no effect."
UselessInline_ -> "`INLINE' pragmas where they have no effect."
UselessInstance_ -> "`instance' blocks where they have no effect."
UselessPrivate_ -> "`private' blocks where they have no effect."
UselessPublic_ -> "`public' blocks where they have no effect."
AbsurdPatternRequiresNoRHS_ -> "A clause with an absurd pattern does not need a Right Hand Side."
CantGeneralizeOverSorts_ -> "Attempt to generalize over sort metas in 'variable' declaration."
ClashesViaRenaming_ -> "Clashes introduced by `renaming'."
CoverageIssue_ -> "Failed coverage checks."
CoverageNoExactSplit_ -> "Failed exact split checks."
DeprecationWarning_ -> "Feature deprecation."
GenericNonFatalError_ -> ""
GenericWarning_ -> ""
IllformedAsClause_ -> "Illformed `as'-clauses in `import' statements."
InstanceNoOutputTypeName_ -> "instance arguments whose type does not end in a named or variable type are never considered by instance search."
InstanceArgWithExplicitArg_ -> "instance arguments with explicit arguments are never considered by instance search."
InstanceWithExplicitArg_ -> "`instance` declarations with explicit arguments are never considered by instance search."
InversionDepthReached_ -> "Inversions of pattern-matching failed due to exhausted inversion depth."
ModuleDoesntExport_ -> "Imported name is not actually exported."
FixityInRenamingModule_ -> "Found fixity annotation in renaming directive for module."
NotInScope_ -> "Out of scope name"
NotStrictlyPositive_ -> "Failed strict positivity checks."
OldBuiltin_ -> "Deprecated `BUILTIN' pragmas."
PragmaCompileErased_ -> "`COMPILE' pragma targeting an erased symbol."
RewriteMaybeNonConfluent_ -> "Failed confluence checks while computing overlap."
RewriteNonConfluent_ -> "Failed confluence checks while joining critical pairs."
SafeFlagEta_ -> "`ETA' pragmas with the safe flag."
SafeFlagInjective_ -> "`INJECTIVE' pragmas with the safe flag."
SafeFlagNoCoverageCheck_ -> "`NON_COVERING` pragmas with the safe flag."
SafeFlagNonTerminating_ -> "`NON_TERMINATING' pragmas with the safe flag."
SafeFlagNoPositivityCheck_ -> "`NO_POSITIVITY_CHECK' pragmas with the safe flag."
SafeFlagNoUniverseCheck_ -> "`NO_UNIVERSE_CHECK' pragmas with the safe flag."
SafeFlagPolarity_ -> "`POLARITY' pragmas with the safe flag."
SafeFlagPostulate_ -> "`postulate' blocks with the safe flag."
SafeFlagPragma_ -> "Unsafe `OPTIONS' pragmas with the safe flag."
SafeFlagTerminating_ -> "`TERMINATING' pragmas with the safe flag."
SafeFlagWithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' used with the safe and without-K flags."
TerminationIssue_ -> "Failed termination checks."
UnreachableClauses_ -> "Unreachable function clauses."
UnsolvedConstraints_ -> "Unsolved constraints."
UnsolvedInteractionMetas_ -> "Unsolved interaction meta variables."
UnsolvedMetaVariables_ -> "Unsolved meta variables."
UserWarning_ -> "User-defined warning added using one of the 'WARNING_ON_*' pragmas."
WithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' usages with the without-K flags."
WrongInstanceDeclaration_ -> "Terms marked as eligible for instance search should end with a name."
CoInfectiveImport_ -> "Importing a file not using e.g. `--safe' from one which does."
InfectiveImport_ -> "Importing a file using e.g. `--cubical' into one which doesn't."