-- | Types related to warnings raised by Agda.

module Agda.TypeChecking.Monad.Base.Warning where

import           Control.DeepSeq            (NFData)
import           GHC.Generics               (Generic)

import           Agda.Syntax.Abstract.Name
import           Agda.Syntax.Position       (Range)
import qualified Agda.Syntax.Concrete.Name  as C

import           Agda.Utils.List1           (List1)

data RecordFieldWarning
  = DuplicateFields (List1 (C.Name, Range))
      -- ^ Each redundant field comes with a range of associated dead code.
  | TooManyFields QName [C.Name] (List1 (C.Name, Range))
      -- ^ Record type, fields not supplied by user, non-fields but supplied.
      --   The redundant fields come with a range of associated dead code.
  deriving (Int -> RecordFieldWarning -> ShowS
[RecordFieldWarning] -> ShowS
RecordFieldWarning -> String
(Int -> RecordFieldWarning -> ShowS)
-> (RecordFieldWarning -> String)
-> ([RecordFieldWarning] -> ShowS)
-> Show RecordFieldWarning
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RecordFieldWarning -> ShowS
showsPrec :: Int -> RecordFieldWarning -> ShowS
$cshow :: RecordFieldWarning -> String
show :: RecordFieldWarning -> String
$cshowList :: [RecordFieldWarning] -> ShowS
showList :: [RecordFieldWarning] -> ShowS
Show, (forall x. RecordFieldWarning -> Rep RecordFieldWarning x)
-> (forall x. Rep RecordFieldWarning x -> RecordFieldWarning)
-> Generic RecordFieldWarning
forall x. Rep RecordFieldWarning x -> RecordFieldWarning
forall x. RecordFieldWarning -> Rep RecordFieldWarning x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RecordFieldWarning -> Rep RecordFieldWarning x
from :: forall x. RecordFieldWarning -> Rep RecordFieldWarning x
$cto :: forall x. Rep RecordFieldWarning x -> RecordFieldWarning
to :: forall x. Rep RecordFieldWarning x -> RecordFieldWarning
Generic)

data UselessPublicReason
  = UselessPublicPreamble
  | UselessPublicLet
  | UselessPublicNoOpen
  | UselessPublicAnonymousModule
  deriving (Int -> UselessPublicReason -> ShowS
[UselessPublicReason] -> ShowS
UselessPublicReason -> String
(Int -> UselessPublicReason -> ShowS)
-> (UselessPublicReason -> String)
-> ([UselessPublicReason] -> ShowS)
-> Show UselessPublicReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UselessPublicReason -> ShowS
showsPrec :: Int -> UselessPublicReason -> ShowS
$cshow :: UselessPublicReason -> String
show :: UselessPublicReason -> String
$cshowList :: [UselessPublicReason] -> ShowS
showList :: [UselessPublicReason] -> ShowS
Show, (forall x. UselessPublicReason -> Rep UselessPublicReason x)
-> (forall x. Rep UselessPublicReason x -> UselessPublicReason)
-> Generic UselessPublicReason
forall x. Rep UselessPublicReason x -> UselessPublicReason
forall x. UselessPublicReason -> Rep UselessPublicReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UselessPublicReason -> Rep UselessPublicReason x
from :: forall x. UselessPublicReason -> Rep UselessPublicReason x
$cto :: forall x. Rep UselessPublicReason x -> UselessPublicReason
to :: forall x. Rep UselessPublicReason x -> UselessPublicReason
Generic, Int -> UselessPublicReason
UselessPublicReason -> Int
UselessPublicReason -> [UselessPublicReason]
UselessPublicReason -> UselessPublicReason
UselessPublicReason -> UselessPublicReason -> [UselessPublicReason]
UselessPublicReason
-> UselessPublicReason
-> UselessPublicReason
-> [UselessPublicReason]
(UselessPublicReason -> UselessPublicReason)
-> (UselessPublicReason -> UselessPublicReason)
-> (Int -> UselessPublicReason)
-> (UselessPublicReason -> Int)
-> (UselessPublicReason -> [UselessPublicReason])
-> (UselessPublicReason
    -> UselessPublicReason -> [UselessPublicReason])
-> (UselessPublicReason
    -> UselessPublicReason -> [UselessPublicReason])
-> (UselessPublicReason
    -> UselessPublicReason
    -> UselessPublicReason
    -> [UselessPublicReason])
-> Enum UselessPublicReason
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: UselessPublicReason -> UselessPublicReason
succ :: UselessPublicReason -> UselessPublicReason
$cpred :: UselessPublicReason -> UselessPublicReason
pred :: UselessPublicReason -> UselessPublicReason
$ctoEnum :: Int -> UselessPublicReason
toEnum :: Int -> UselessPublicReason
$cfromEnum :: UselessPublicReason -> Int
fromEnum :: UselessPublicReason -> Int
$cenumFrom :: UselessPublicReason -> [UselessPublicReason]
enumFrom :: UselessPublicReason -> [UselessPublicReason]
$cenumFromThen :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason]
enumFromThen :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason]
$cenumFromTo :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason]
enumFromTo :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason]
$cenumFromThenTo :: UselessPublicReason
-> UselessPublicReason
-> UselessPublicReason
-> [UselessPublicReason]
enumFromThenTo :: UselessPublicReason
-> UselessPublicReason
-> UselessPublicReason
-> [UselessPublicReason]
Enum, UselessPublicReason
UselessPublicReason
-> UselessPublicReason -> Bounded UselessPublicReason
forall a. a -> a -> Bounded a
$cminBound :: UselessPublicReason
minBound :: UselessPublicReason
$cmaxBound :: UselessPublicReason
maxBound :: UselessPublicReason
Bounded)

instance NFData UselessPublicReason