-- | Provide names for the errors Agda throws.Options/Er

module Mikan.Interaction.Options.Errors where

import Control.DeepSeq        ( NFData )
import Data.List              ( sort )
import Generic.Data           ( FiniteEnumeration(..) )
import GHC.Generics           ( Generic )

import Mikan.Syntax.Common     ( ConstructorOrPatternSynonym(..), Hiding )

import Mikan.Utils.Function    ( applyWhenJust )
import Mikan.Utils.List        ( initWithDefault )
import Mikan.Utils.Impossible  ( __IMPOSSIBLE__ )

-- | Extra information for error 'CannotQuoteTerm'.

data CannotQuoteTerm
  = CannotQuoteTermHidden Hiding
  | CannotQuoteTermNothing
  deriving (Int -> CannotQuoteTerm -> ShowS
[CannotQuoteTerm] -> ShowS
CannotQuoteTerm -> [Char]
(Int -> CannotQuoteTerm -> ShowS)
-> (CannotQuoteTerm -> [Char])
-> ([CannotQuoteTerm] -> ShowS)
-> Show CannotQuoteTerm
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CannotQuoteTerm -> ShowS
showsPrec :: Int -> CannotQuoteTerm -> ShowS
$cshow :: CannotQuoteTerm -> [Char]
show :: CannotQuoteTerm -> [Char]
$cshowList :: [CannotQuoteTerm] -> ShowS
showList :: [CannotQuoteTerm] -> ShowS
Show, (forall x. CannotQuoteTerm -> Rep CannotQuoteTerm x)
-> (forall x. Rep CannotQuoteTerm x -> CannotQuoteTerm)
-> Generic CannotQuoteTerm
forall x. Rep CannotQuoteTerm x -> CannotQuoteTerm
forall x. CannotQuoteTerm -> Rep CannotQuoteTerm x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CannotQuoteTerm -> Rep CannotQuoteTerm x
from :: forall x. CannotQuoteTerm -> Rep CannotQuoteTerm x
$cto :: forall x. Rep CannotQuoteTerm x -> CannotQuoteTerm
to :: forall x. Rep CannotQuoteTerm x -> CannotQuoteTerm
Generic)
  deriving (Int -> CannotQuoteTerm
CannotQuoteTerm -> Int
CannotQuoteTerm -> [CannotQuoteTerm]
CannotQuoteTerm -> CannotQuoteTerm
CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
CannotQuoteTerm
-> CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
(CannotQuoteTerm -> CannotQuoteTerm)
-> (CannotQuoteTerm -> CannotQuoteTerm)
-> (Int -> CannotQuoteTerm)
-> (CannotQuoteTerm -> Int)
-> (CannotQuoteTerm -> [CannotQuoteTerm])
-> (CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm])
-> (CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm])
-> (CannotQuoteTerm
    -> CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm])
-> Enum CannotQuoteTerm
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 :: CannotQuoteTerm -> CannotQuoteTerm
succ :: CannotQuoteTerm -> CannotQuoteTerm
$cpred :: CannotQuoteTerm -> CannotQuoteTerm
pred :: CannotQuoteTerm -> CannotQuoteTerm
$ctoEnum :: Int -> CannotQuoteTerm
toEnum :: Int -> CannotQuoteTerm
$cfromEnum :: CannotQuoteTerm -> Int
fromEnum :: CannotQuoteTerm -> Int
$cenumFrom :: CannotQuoteTerm -> [CannotQuoteTerm]
enumFrom :: CannotQuoteTerm -> [CannotQuoteTerm]
$cenumFromThen :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
enumFromThen :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
$cenumFromTo :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
enumFromTo :: CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
$cenumFromThenTo :: CannotQuoteTerm
-> CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
enumFromThenTo :: CannotQuoteTerm
-> CannotQuoteTerm -> CannotQuoteTerm -> [CannotQuoteTerm]
Enum, CannotQuoteTerm
CannotQuoteTerm -> CannotQuoteTerm -> Bounded CannotQuoteTerm
forall a. a -> a -> Bounded a
$cminBound :: CannotQuoteTerm
minBound :: CannotQuoteTerm
$cmaxBound :: CannotQuoteTerm
maxBound :: CannotQuoteTerm
Bounded) via (FiniteEnumeration CannotQuoteTerm)

-- | What kind of declaration?
--
--   See also 'Agda.Syntax.Concrete.Definitions.Types.DataRecOrFun'.

data DataRecOrFun_
  = DataName_  -- ^ Name of a data type.
  | RecName_   -- ^ Name of a record type.
  | FunName_   -- ^ Name of a function.
  deriving (Int -> DataRecOrFun_ -> ShowS
[DataRecOrFun_] -> ShowS
DataRecOrFun_ -> [Char]
(Int -> DataRecOrFun_ -> ShowS)
-> (DataRecOrFun_ -> [Char])
-> ([DataRecOrFun_] -> ShowS)
-> Show DataRecOrFun_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataRecOrFun_ -> ShowS
showsPrec :: Int -> DataRecOrFun_ -> ShowS
$cshow :: DataRecOrFun_ -> [Char]
show :: DataRecOrFun_ -> [Char]
$cshowList :: [DataRecOrFun_] -> ShowS
showList :: [DataRecOrFun_] -> ShowS
Show, (forall x. DataRecOrFun_ -> Rep DataRecOrFun_ x)
-> (forall x. Rep DataRecOrFun_ x -> DataRecOrFun_)
-> Generic DataRecOrFun_
forall x. Rep DataRecOrFun_ x -> DataRecOrFun_
forall x. DataRecOrFun_ -> Rep DataRecOrFun_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DataRecOrFun_ -> Rep DataRecOrFun_ x
from :: forall x. DataRecOrFun_ -> Rep DataRecOrFun_ x
$cto :: forall x. Rep DataRecOrFun_ x -> DataRecOrFun_
to :: forall x. Rep DataRecOrFun_ x -> DataRecOrFun_
Generic, Int -> DataRecOrFun_
DataRecOrFun_ -> Int
DataRecOrFun_ -> [DataRecOrFun_]
DataRecOrFun_ -> DataRecOrFun_
DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
DataRecOrFun_ -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
(DataRecOrFun_ -> DataRecOrFun_)
-> (DataRecOrFun_ -> DataRecOrFun_)
-> (Int -> DataRecOrFun_)
-> (DataRecOrFun_ -> Int)
-> (DataRecOrFun_ -> [DataRecOrFun_])
-> (DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_])
-> (DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_])
-> (DataRecOrFun_
    -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_])
-> Enum DataRecOrFun_
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 :: DataRecOrFun_ -> DataRecOrFun_
succ :: DataRecOrFun_ -> DataRecOrFun_
$cpred :: DataRecOrFun_ -> DataRecOrFun_
pred :: DataRecOrFun_ -> DataRecOrFun_
$ctoEnum :: Int -> DataRecOrFun_
toEnum :: Int -> DataRecOrFun_
$cfromEnum :: DataRecOrFun_ -> Int
fromEnum :: DataRecOrFun_ -> Int
$cenumFrom :: DataRecOrFun_ -> [DataRecOrFun_]
enumFrom :: DataRecOrFun_ -> [DataRecOrFun_]
$cenumFromThen :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
enumFromThen :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
$cenumFromTo :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
enumFromTo :: DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
$cenumFromThenTo :: DataRecOrFun_ -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
enumFromThenTo :: DataRecOrFun_ -> DataRecOrFun_ -> DataRecOrFun_ -> [DataRecOrFun_]
Enum, DataRecOrFun_
DataRecOrFun_ -> DataRecOrFun_ -> Bounded DataRecOrFun_
forall a. a -> a -> Bounded a
$cminBound :: DataRecOrFun_
minBound :: DataRecOrFun_
$cmaxBound :: DataRecOrFun_
maxBound :: DataRecOrFun_
Bounded)

-- | Things not allowed in dot patterns.

data NotAllowedInDotPatterns
  = LetExpressions
  | PatternLambdas
  deriving (Int -> NotAllowedInDotPatterns -> ShowS
[NotAllowedInDotPatterns] -> ShowS
NotAllowedInDotPatterns -> [Char]
(Int -> NotAllowedInDotPatterns -> ShowS)
-> (NotAllowedInDotPatterns -> [Char])
-> ([NotAllowedInDotPatterns] -> ShowS)
-> Show NotAllowedInDotPatterns
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotAllowedInDotPatterns -> ShowS
showsPrec :: Int -> NotAllowedInDotPatterns -> ShowS
$cshow :: NotAllowedInDotPatterns -> [Char]
show :: NotAllowedInDotPatterns -> [Char]
$cshowList :: [NotAllowedInDotPatterns] -> ShowS
showList :: [NotAllowedInDotPatterns] -> ShowS
Show, (forall x.
 NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x)
-> (forall x.
    Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns)
-> Generic NotAllowedInDotPatterns
forall x. Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns
forall x. NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x
from :: forall x. NotAllowedInDotPatterns -> Rep NotAllowedInDotPatterns x
$cto :: forall x. Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns
to :: forall x. Rep NotAllowedInDotPatterns x -> NotAllowedInDotPatterns
Generic, Int -> NotAllowedInDotPatterns
NotAllowedInDotPatterns -> Int
NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
NotAllowedInDotPatterns -> NotAllowedInDotPatterns
NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> [NotAllowedInDotPatterns]
(NotAllowedInDotPatterns -> NotAllowedInDotPatterns)
-> (NotAllowedInDotPatterns -> NotAllowedInDotPatterns)
-> (Int -> NotAllowedInDotPatterns)
-> (NotAllowedInDotPatterns -> Int)
-> (NotAllowedInDotPatterns -> [NotAllowedInDotPatterns])
-> (NotAllowedInDotPatterns
    -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns])
-> (NotAllowedInDotPatterns
    -> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns])
-> (NotAllowedInDotPatterns
    -> NotAllowedInDotPatterns
    -> NotAllowedInDotPatterns
    -> [NotAllowedInDotPatterns])
-> Enum NotAllowedInDotPatterns
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 :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns
succ :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns
$cpred :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns
pred :: NotAllowedInDotPatterns -> NotAllowedInDotPatterns
$ctoEnum :: Int -> NotAllowedInDotPatterns
toEnum :: Int -> NotAllowedInDotPatterns
$cfromEnum :: NotAllowedInDotPatterns -> Int
fromEnum :: NotAllowedInDotPatterns -> Int
$cenumFrom :: NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
enumFrom :: NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
$cenumFromThen :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
enumFromThen :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
$cenumFromTo :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
enumFromTo :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> [NotAllowedInDotPatterns]
$cenumFromThenTo :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> [NotAllowedInDotPatterns]
enumFromThenTo :: NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> NotAllowedInDotPatterns
-> [NotAllowedInDotPatterns]
Enum, NotAllowedInDotPatterns
NotAllowedInDotPatterns
-> NotAllowedInDotPatterns -> Bounded NotAllowedInDotPatterns
forall a. a -> a -> Bounded a
$cminBound :: NotAllowedInDotPatterns
minBound :: NotAllowedInDotPatterns
$cmaxBound :: NotAllowedInDotPatterns
maxBound :: NotAllowedInDotPatterns
Bounded)

-- | Reasons for error 'NotAValidLetBinding'.

data NotAValidLetBinding
  = MissingRHS
  | NotAValidLetPattern
  | WhereClausesNotAllowed
  | CopatternsNotAllowed
  -- These cannot be triggered:
  -- -- | EllipsisNotAllowed
  -- -- | WithPatternsNotAllowed
  deriving (Int -> NotAValidLetBinding -> ShowS
[NotAValidLetBinding] -> ShowS
NotAValidLetBinding -> [Char]
(Int -> NotAValidLetBinding -> ShowS)
-> (NotAValidLetBinding -> [Char])
-> ([NotAValidLetBinding] -> ShowS)
-> Show NotAValidLetBinding
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotAValidLetBinding -> ShowS
showsPrec :: Int -> NotAValidLetBinding -> ShowS
$cshow :: NotAValidLetBinding -> [Char]
show :: NotAValidLetBinding -> [Char]
$cshowList :: [NotAValidLetBinding] -> ShowS
showList :: [NotAValidLetBinding] -> ShowS
Show, (forall x. NotAValidLetBinding -> Rep NotAValidLetBinding x)
-> (forall x. Rep NotAValidLetBinding x -> NotAValidLetBinding)
-> Generic NotAValidLetBinding
forall x. Rep NotAValidLetBinding x -> NotAValidLetBinding
forall x. NotAValidLetBinding -> Rep NotAValidLetBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotAValidLetBinding -> Rep NotAValidLetBinding x
from :: forall x. NotAValidLetBinding -> Rep NotAValidLetBinding x
$cto :: forall x. Rep NotAValidLetBinding x -> NotAValidLetBinding
to :: forall x. Rep NotAValidLetBinding x -> NotAValidLetBinding
Generic, Int -> NotAValidLetBinding
NotAValidLetBinding -> Int
NotAValidLetBinding -> [NotAValidLetBinding]
NotAValidLetBinding -> NotAValidLetBinding
NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding]
NotAValidLetBinding
-> NotAValidLetBinding
-> NotAValidLetBinding
-> [NotAValidLetBinding]
(NotAValidLetBinding -> NotAValidLetBinding)
-> (NotAValidLetBinding -> NotAValidLetBinding)
-> (Int -> NotAValidLetBinding)
-> (NotAValidLetBinding -> Int)
-> (NotAValidLetBinding -> [NotAValidLetBinding])
-> (NotAValidLetBinding
    -> NotAValidLetBinding -> [NotAValidLetBinding])
-> (NotAValidLetBinding
    -> NotAValidLetBinding -> [NotAValidLetBinding])
-> (NotAValidLetBinding
    -> NotAValidLetBinding
    -> NotAValidLetBinding
    -> [NotAValidLetBinding])
-> Enum NotAValidLetBinding
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 :: NotAValidLetBinding -> NotAValidLetBinding
succ :: NotAValidLetBinding -> NotAValidLetBinding
$cpred :: NotAValidLetBinding -> NotAValidLetBinding
pred :: NotAValidLetBinding -> NotAValidLetBinding
$ctoEnum :: Int -> NotAValidLetBinding
toEnum :: Int -> NotAValidLetBinding
$cfromEnum :: NotAValidLetBinding -> Int
fromEnum :: NotAValidLetBinding -> Int
$cenumFrom :: NotAValidLetBinding -> [NotAValidLetBinding]
enumFrom :: NotAValidLetBinding -> [NotAValidLetBinding]
$cenumFromThen :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding]
enumFromThen :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding]
$cenumFromTo :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding]
enumFromTo :: NotAValidLetBinding -> NotAValidLetBinding -> [NotAValidLetBinding]
$cenumFromThenTo :: NotAValidLetBinding
-> NotAValidLetBinding
-> NotAValidLetBinding
-> [NotAValidLetBinding]
enumFromThenTo :: NotAValidLetBinding
-> NotAValidLetBinding
-> NotAValidLetBinding
-> [NotAValidLetBinding]
Enum, NotAValidLetBinding
NotAValidLetBinding
-> NotAValidLetBinding -> Bounded NotAValidLetBinding
forall a. a -> a -> Bounded a
$cminBound :: NotAValidLetBinding
minBound :: NotAValidLetBinding
$cmaxBound :: NotAValidLetBinding
maxBound :: NotAValidLetBinding
Bounded)

-- | Reasons for error 'NotAValidLetExpression'.

data NotAValidLetExpression
  = MissingBody
  deriving (Int -> NotAValidLetExpression -> ShowS
[NotAValidLetExpression] -> ShowS
NotAValidLetExpression -> [Char]
(Int -> NotAValidLetExpression -> ShowS)
-> (NotAValidLetExpression -> [Char])
-> ([NotAValidLetExpression] -> ShowS)
-> Show NotAValidLetExpression
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotAValidLetExpression -> ShowS
showsPrec :: Int -> NotAValidLetExpression -> ShowS
$cshow :: NotAValidLetExpression -> [Char]
show :: NotAValidLetExpression -> [Char]
$cshowList :: [NotAValidLetExpression] -> ShowS
showList :: [NotAValidLetExpression] -> ShowS
Show, (forall x. NotAValidLetExpression -> Rep NotAValidLetExpression x)
-> (forall x.
    Rep NotAValidLetExpression x -> NotAValidLetExpression)
-> Generic NotAValidLetExpression
forall x. Rep NotAValidLetExpression x -> NotAValidLetExpression
forall x. NotAValidLetExpression -> Rep NotAValidLetExpression x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotAValidLetExpression -> Rep NotAValidLetExpression x
from :: forall x. NotAValidLetExpression -> Rep NotAValidLetExpression x
$cto :: forall x. Rep NotAValidLetExpression x -> NotAValidLetExpression
to :: forall x. Rep NotAValidLetExpression x -> NotAValidLetExpression
Generic, Int -> NotAValidLetExpression
NotAValidLetExpression -> Int
NotAValidLetExpression -> [NotAValidLetExpression]
NotAValidLetExpression -> NotAValidLetExpression
NotAValidLetExpression
-> NotAValidLetExpression -> [NotAValidLetExpression]
NotAValidLetExpression
-> NotAValidLetExpression
-> NotAValidLetExpression
-> [NotAValidLetExpression]
(NotAValidLetExpression -> NotAValidLetExpression)
-> (NotAValidLetExpression -> NotAValidLetExpression)
-> (Int -> NotAValidLetExpression)
-> (NotAValidLetExpression -> Int)
-> (NotAValidLetExpression -> [NotAValidLetExpression])
-> (NotAValidLetExpression
    -> NotAValidLetExpression -> [NotAValidLetExpression])
-> (NotAValidLetExpression
    -> NotAValidLetExpression -> [NotAValidLetExpression])
-> (NotAValidLetExpression
    -> NotAValidLetExpression
    -> NotAValidLetExpression
    -> [NotAValidLetExpression])
-> Enum NotAValidLetExpression
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 :: NotAValidLetExpression -> NotAValidLetExpression
succ :: NotAValidLetExpression -> NotAValidLetExpression
$cpred :: NotAValidLetExpression -> NotAValidLetExpression
pred :: NotAValidLetExpression -> NotAValidLetExpression
$ctoEnum :: Int -> NotAValidLetExpression
toEnum :: Int -> NotAValidLetExpression
$cfromEnum :: NotAValidLetExpression -> Int
fromEnum :: NotAValidLetExpression -> Int
$cenumFrom :: NotAValidLetExpression -> [NotAValidLetExpression]
enumFrom :: NotAValidLetExpression -> [NotAValidLetExpression]
$cenumFromThen :: NotAValidLetExpression
-> NotAValidLetExpression -> [NotAValidLetExpression]
enumFromThen :: NotAValidLetExpression
-> NotAValidLetExpression -> [NotAValidLetExpression]
$cenumFromTo :: NotAValidLetExpression
-> NotAValidLetExpression -> [NotAValidLetExpression]
enumFromTo :: NotAValidLetExpression
-> NotAValidLetExpression -> [NotAValidLetExpression]
$cenumFromThenTo :: NotAValidLetExpression
-> NotAValidLetExpression
-> NotAValidLetExpression
-> [NotAValidLetExpression]
enumFromThenTo :: NotAValidLetExpression
-> NotAValidLetExpression
-> NotAValidLetExpression
-> [NotAValidLetExpression]
Enum, NotAValidLetExpression
NotAValidLetExpression
-> NotAValidLetExpression -> Bounded NotAValidLetExpression
forall a. a -> a -> Bounded a
$cminBound :: NotAValidLetExpression
minBound :: NotAValidLetExpression
$cmaxBound :: NotAValidLetExpression
maxBound :: NotAValidLetExpression
Bounded)

-- | Symbolic name of an Agda error.

data ErrorName
  -- Error groups (alphabetically) with named sub errors
  = ExecError_             ExecError_
  | ImpossibleConstructor_ NegativeUnification_
  | SplitError_            SplitError_
  -- Generic errors (alphabetically)
  | CompilationError_
  | CustomBackendError_
  | InternalError_
  | LibraryError_
  | NonFatalErrors_
  | OptionError_
  | SyntaxError_
  | UserError_
  -- Other errors (alphabetically)
  | AbsentRHSRequiresAbsurdPattern_
  | AbstractConstructorNotInScope_
  | AmbiguousConstructor_
  | AmbiguousField_
  | AmbiguousModule_
  | AmbiguousName_
  | AmbiguousOverloadedProjection_
  | AmbiguousParseForApplication_
  | AmbiguousParseForLHS_
  | AmbiguousProjection_
  | AmbiguousTopLevelModuleName_
  | AsPatternInPatternSynonym_
  | BackendDoesNotSupportOnlyScopeChecking_
  | BadArgumentsToPatternSynonym_
  | BothWithAndRHS_
  | BuiltinInParameterisedModule_
  | BuiltinMustBeConstructor_
  | BuiltinMustBeData_
  | BuiltinMustBeDef_
  | BuiltinMustBeFunction_
  | BuiltinMustBePostulate_
  | CannotApply_
  | CannotGeneralizeEtaExpandable_
  | CannotGenerateTransportClause_
  | CannotQuote_ CannotQuote_
  | CannotQuoteTerm_ CannotQuoteTerm
  | CannotResolveAmbiguousPatternSynonym_
  | CannotRewriteByNonEquation_
  | CantResolveOverloadedConstructorsTargetingSameDatatype_
  | ClashingDefinition_
  | ClashingModule_
  | ComatchingDisabledForRecord_
  | ConstructorDoesNotTargetGivenType_
  | ConstructorPatternInWrongDatatype_
  | CopatternHeadNotProjection_
  | CubicalPrimitiveNotFullyApplied_
  | CyclicModuleDependency_
  | DeBruijnIndexOutOfScope_
  | DeclarationsAfterTopLevelModule_
  | DefinitionInDifferentModule_
  | DoNotationError_
  | DotPatternInPatternSynonym_
  | DuplicateBuiltinBinding_
  | DuplicateConstructors_
  | DuplicateFields_
  | DuplicateImports_
  | DuplicateOverlapPragma_
  | DuplicatePrimitiveBinding_
  | ExpectedBindingForParameter_
  | ExpectedIntervalLiteral_
  | FieldOutsideRecord_
  | FaceConstraintDisjunction_
  | FaceConstraintUnsatisfiable_
  | FileNotFound_
  | ForcedConstructorNotInstantiated_
  | GeneralizationFailed_
  | GeneralizationPrepruneErrorRefinedContext_
  | GeneralizationPrepruneErrorCyclicDependencies_
  | GeneralizationPrepruneErrorFailedToInstantiate_
  | GeneralizeCyclicDependency_
  | GeneralizeNotSupportedHere_
  | GeneralizedVarInLetOpenedModule_
  | ModuleNameHashCollision_
  | HidingMismatch_
  | IdiomBracketError_
  | InvalidBuiltin_
  | InvalidDottedExpression_
  | IllTypedPatternAfterWithAbstraction_
  | IllegalDeclarationBeforeTopLevelModule_
  | IllegalHidingInPostfixProjection_
  | IllegalInstanceVariableInPatternSynonym_
  | IllegalLetInTelescope_
  | IllegalPatternInTelescope_
  | IllformedProjectionPatternAbstract_
  | IllformedProjectionPatternConcrete_
  | InvalidFileName_
  | InvalidPattern_
  | InvalidProjectionParameter_
  | InvalidPun_ ConstructorOrPatternSynonym
  | InvalidTypeSort_
  | LibTooFarDown_
  | LiteralTooBig_
  | MacroResultTypeMismatch_
  | MetaCannotDependOn_
  | MismatchedProjectionsError_
  | MissingBindingsForTelescopeVariables_
  | MissingTypeSignature_ DataRecOrFun_
  | ModuleArityMismatch_
  | ModuleDefinedInOtherFile_
  | ModuleNameDoesntMatchFileName_
  | ModuleNameUnexpected_
  | MultipleFixityDecls_
  | MultiplePolarityPragmas_
  | ConstructorNameOfNonRecord_
  | NonLocalWhereModuleInRefinedContext_
  | NeedOptionAllowExec_
  | NeedOptionCopatterns_
  | NeedOptionCubical_
  | NeedOptionPatternMatching_
  | NeedOptionProp_
  | NegativeLiteralInPattern_
  | NoBindingForBuiltin_
  | NoBindingForPrimitive_
  | NoKnownRecordWithSuchFields_
  | NoParameterOfName_
  | NoParseForApplication_
  | NoParseForLHS_
  | NoSuchBuiltinName_
  | NoSuchModule_
  | NoSuchPrimitiveFunction_
  | NotAValidLetBinding_ (Maybe NotAValidLetBinding)
  | NotAValidLetExpression_ NotAValidLetExpression
  | NotAllowedInDotPatterns_ NotAllowedInDotPatterns
  | NotAnExpression_
  | NotInScope_
  | NotLeqSort_
  | NotValidBeforeField_
  | OverlappingProjects_
  | PathAbstractionFailed_
  | PatternInPathLambda_
  | PatternInSystem_
  | PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym
  | PrivateRecordField_
  | QualifiedLocalModule_
  | ReferencesFutureVariables_
  | RepeatedNamesInImportDirective_
  | RepeatedVariablesInPattern_
  | ShadowedModule_
  | ShouldBeASort_
  | ShouldBeEmpty_
  | ShouldBePath_
  | ShouldBePi_
  | ShouldBeRecordPattern_
  | ShouldBeRecordType_
  | ShouldEndInApplicationOfTheDatatype_
  | SolvedButOpenHoles_
  | SortCannotDependOnItsIndex_
  | SortDoesNotAdmitDataDefinitions_
  | TacticAttributeNotAllowed_
  | TooFewArgumentsToPatternSynonym_
  | TooFewPatternsInWithClause_
  | TooManyFields_
  | TooManyPatternsInWithClause_
  | TriedToCopyConstrainedPrim_
  | UnboundVariablesInPatternSynonym_
  | UnequalTerms_
  | UnequalTypes_
  | UnexpectedParameter_
  | UnexpectedTypeSignatureForParameter_
  | UnexpectedWithPatterns_
  | UnknownBackend_
  | UnusedVariableInPatternSynonym_
  | WithClausePatternMismatch_
  | WithOnFreeVariable_
  | WrongAnnotationInLambda_
  | WrongHidingInApplication_
  | WrongHidingInLHS_
  | WrongHidingInLambda_
  | WrongHidingInProjection_
  | WrongNamedArgument_
  | WrongNumberOfConstructorArguments_
  deriving (Int -> ErrorName -> ShowS
[ErrorName] -> ShowS
ErrorName -> [Char]
(Int -> ErrorName -> ShowS)
-> (ErrorName -> [Char])
-> ([ErrorName] -> ShowS)
-> Show ErrorName
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ErrorName -> ShowS
showsPrec :: Int -> ErrorName -> ShowS
$cshow :: ErrorName -> [Char]
show :: ErrorName -> [Char]
$cshowList :: [ErrorName] -> ShowS
showList :: [ErrorName] -> ShowS
Show, (forall x. ErrorName -> Rep ErrorName x)
-> (forall x. Rep ErrorName x -> ErrorName) -> Generic ErrorName
forall x. Rep ErrorName x -> ErrorName
forall x. ErrorName -> Rep ErrorName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ErrorName -> Rep ErrorName x
from :: forall x. ErrorName -> Rep ErrorName x
$cto :: forall x. Rep ErrorName x -> ErrorName
to :: forall x. Rep ErrorName x -> ErrorName
Generic)
  deriving (Int -> ErrorName
ErrorName -> Int
ErrorName -> [ErrorName]
ErrorName -> ErrorName
ErrorName -> ErrorName -> [ErrorName]
ErrorName -> ErrorName -> ErrorName -> [ErrorName]
(ErrorName -> ErrorName)
-> (ErrorName -> ErrorName)
-> (Int -> ErrorName)
-> (ErrorName -> Int)
-> (ErrorName -> [ErrorName])
-> (ErrorName -> ErrorName -> [ErrorName])
-> (ErrorName -> ErrorName -> [ErrorName])
-> (ErrorName -> ErrorName -> ErrorName -> [ErrorName])
-> Enum ErrorName
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 :: ErrorName -> ErrorName
succ :: ErrorName -> ErrorName
$cpred :: ErrorName -> ErrorName
pred :: ErrorName -> ErrorName
$ctoEnum :: Int -> ErrorName
toEnum :: Int -> ErrorName
$cfromEnum :: ErrorName -> Int
fromEnum :: ErrorName -> Int
$cenumFrom :: ErrorName -> [ErrorName]
enumFrom :: ErrorName -> [ErrorName]
$cenumFromThen :: ErrorName -> ErrorName -> [ErrorName]
enumFromThen :: ErrorName -> ErrorName -> [ErrorName]
$cenumFromTo :: ErrorName -> ErrorName -> [ErrorName]
enumFromTo :: ErrorName -> ErrorName -> [ErrorName]
$cenumFromThenTo :: ErrorName -> ErrorName -> ErrorName -> [ErrorName]
enumFromThenTo :: ErrorName -> ErrorName -> ErrorName -> [ErrorName]
Enum, ErrorName
ErrorName -> ErrorName -> Bounded ErrorName
forall a. a -> a -> Bounded a
$cminBound :: ErrorName
minBound :: ErrorName
$cmaxBound :: ErrorName
maxBound :: ErrorName
Bounded) via (FiniteEnumeration ErrorName)

data NegativeUnification_
  = UnifyConflict_
  | UnifyCycle_
  deriving (Int -> NegativeUnification_ -> ShowS
[NegativeUnification_] -> ShowS
NegativeUnification_ -> [Char]
(Int -> NegativeUnification_ -> ShowS)
-> (NegativeUnification_ -> [Char])
-> ([NegativeUnification_] -> ShowS)
-> Show NegativeUnification_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NegativeUnification_ -> ShowS
showsPrec :: Int -> NegativeUnification_ -> ShowS
$cshow :: NegativeUnification_ -> [Char]
show :: NegativeUnification_ -> [Char]
$cshowList :: [NegativeUnification_] -> ShowS
showList :: [NegativeUnification_] -> ShowS
Show, (forall x. NegativeUnification_ -> Rep NegativeUnification_ x)
-> (forall x. Rep NegativeUnification_ x -> NegativeUnification_)
-> Generic NegativeUnification_
forall x. Rep NegativeUnification_ x -> NegativeUnification_
forall x. NegativeUnification_ -> Rep NegativeUnification_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NegativeUnification_ -> Rep NegativeUnification_ x
from :: forall x. NegativeUnification_ -> Rep NegativeUnification_ x
$cto :: forall x. Rep NegativeUnification_ x -> NegativeUnification_
to :: forall x. Rep NegativeUnification_ x -> NegativeUnification_
Generic, Int -> NegativeUnification_
NegativeUnification_ -> Int
NegativeUnification_ -> [NegativeUnification_]
NegativeUnification_ -> NegativeUnification_
NegativeUnification_
-> NegativeUnification_ -> [NegativeUnification_]
NegativeUnification_
-> NegativeUnification_
-> NegativeUnification_
-> [NegativeUnification_]
(NegativeUnification_ -> NegativeUnification_)
-> (NegativeUnification_ -> NegativeUnification_)
-> (Int -> NegativeUnification_)
-> (NegativeUnification_ -> Int)
-> (NegativeUnification_ -> [NegativeUnification_])
-> (NegativeUnification_
    -> NegativeUnification_ -> [NegativeUnification_])
-> (NegativeUnification_
    -> NegativeUnification_ -> [NegativeUnification_])
-> (NegativeUnification_
    -> NegativeUnification_
    -> NegativeUnification_
    -> [NegativeUnification_])
-> Enum NegativeUnification_
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 :: NegativeUnification_ -> NegativeUnification_
succ :: NegativeUnification_ -> NegativeUnification_
$cpred :: NegativeUnification_ -> NegativeUnification_
pred :: NegativeUnification_ -> NegativeUnification_
$ctoEnum :: Int -> NegativeUnification_
toEnum :: Int -> NegativeUnification_
$cfromEnum :: NegativeUnification_ -> Int
fromEnum :: NegativeUnification_ -> Int
$cenumFrom :: NegativeUnification_ -> [NegativeUnification_]
enumFrom :: NegativeUnification_ -> [NegativeUnification_]
$cenumFromThen :: NegativeUnification_
-> NegativeUnification_ -> [NegativeUnification_]
enumFromThen :: NegativeUnification_
-> NegativeUnification_ -> [NegativeUnification_]
$cenumFromTo :: NegativeUnification_
-> NegativeUnification_ -> [NegativeUnification_]
enumFromTo :: NegativeUnification_
-> NegativeUnification_ -> [NegativeUnification_]
$cenumFromThenTo :: NegativeUnification_
-> NegativeUnification_
-> NegativeUnification_
-> [NegativeUnification_]
enumFromThenTo :: NegativeUnification_
-> NegativeUnification_
-> NegativeUnification_
-> [NegativeUnification_]
Enum, NegativeUnification_
NegativeUnification_
-> NegativeUnification_ -> Bounded NegativeUnification_
forall a. a -> a -> Bounded a
$cminBound :: NegativeUnification_
minBound :: NegativeUnification_
$cmaxBound :: NegativeUnification_
maxBound :: NegativeUnification_
Bounded)

data NotAHaskellType_
  = BadDontCare_
  | BadLambda_
  | BadMeta_
  | NoPragmaFor_
  | NotCompiled_
  | WrongPragmaFor_
  deriving (Int -> NotAHaskellType_ -> ShowS
[NotAHaskellType_] -> ShowS
NotAHaskellType_ -> [Char]
(Int -> NotAHaskellType_ -> ShowS)
-> (NotAHaskellType_ -> [Char])
-> ([NotAHaskellType_] -> ShowS)
-> Show NotAHaskellType_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotAHaskellType_ -> ShowS
showsPrec :: Int -> NotAHaskellType_ -> ShowS
$cshow :: NotAHaskellType_ -> [Char]
show :: NotAHaskellType_ -> [Char]
$cshowList :: [NotAHaskellType_] -> ShowS
showList :: [NotAHaskellType_] -> ShowS
Show, (forall x. NotAHaskellType_ -> Rep NotAHaskellType_ x)
-> (forall x. Rep NotAHaskellType_ x -> NotAHaskellType_)
-> Generic NotAHaskellType_
forall x. Rep NotAHaskellType_ x -> NotAHaskellType_
forall x. NotAHaskellType_ -> Rep NotAHaskellType_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotAHaskellType_ -> Rep NotAHaskellType_ x
from :: forall x. NotAHaskellType_ -> Rep NotAHaskellType_ x
$cto :: forall x. Rep NotAHaskellType_ x -> NotAHaskellType_
to :: forall x. Rep NotAHaskellType_ x -> NotAHaskellType_
Generic, Int -> NotAHaskellType_
NotAHaskellType_ -> Int
NotAHaskellType_ -> [NotAHaskellType_]
NotAHaskellType_ -> NotAHaskellType_
NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
NotAHaskellType_
-> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
(NotAHaskellType_ -> NotAHaskellType_)
-> (NotAHaskellType_ -> NotAHaskellType_)
-> (Int -> NotAHaskellType_)
-> (NotAHaskellType_ -> Int)
-> (NotAHaskellType_ -> [NotAHaskellType_])
-> (NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_])
-> (NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_])
-> (NotAHaskellType_
    -> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_])
-> Enum NotAHaskellType_
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 :: NotAHaskellType_ -> NotAHaskellType_
succ :: NotAHaskellType_ -> NotAHaskellType_
$cpred :: NotAHaskellType_ -> NotAHaskellType_
pred :: NotAHaskellType_ -> NotAHaskellType_
$ctoEnum :: Int -> NotAHaskellType_
toEnum :: Int -> NotAHaskellType_
$cfromEnum :: NotAHaskellType_ -> Int
fromEnum :: NotAHaskellType_ -> Int
$cenumFrom :: NotAHaskellType_ -> [NotAHaskellType_]
enumFrom :: NotAHaskellType_ -> [NotAHaskellType_]
$cenumFromThen :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
enumFromThen :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
$cenumFromTo :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
enumFromTo :: NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
$cenumFromThenTo :: NotAHaskellType_
-> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
enumFromThenTo :: NotAHaskellType_
-> NotAHaskellType_ -> NotAHaskellType_ -> [NotAHaskellType_]
Enum, NotAHaskellType_
NotAHaskellType_ -> NotAHaskellType_ -> Bounded NotAHaskellType_
forall a. a -> a -> Bounded a
$cminBound :: NotAHaskellType_
minBound :: NotAHaskellType_
$cmaxBound :: NotAHaskellType_
maxBound :: NotAHaskellType_
Bounded)

data SplitError_
  = GenericSplitError_
  -- Specific errors
  | BlockedType_
  | CannotCreateMissingClause_
  | CannotEliminateWithPattern_
  | CannotEliminateWithProjection_
  | CoinductiveDatatype_
  | CosplitNoRecordType_
  | CosplitNoTarget_
  | NotADatatype_
  | UnificationStuck_
  | SortOfSplitVarError_
  | SplitInProp_
  | SplitOnAbstract_
  | SplitOnCoinductive_
  | SplitOnNonEtaRecord_
  | SplitOnNonVariable_
  | SplitOnPartial_
  | SplitOnUnchecked_
  deriving (Int -> SplitError_ -> ShowS
[SplitError_] -> ShowS
SplitError_ -> [Char]
(Int -> SplitError_ -> ShowS)
-> (SplitError_ -> [Char])
-> ([SplitError_] -> ShowS)
-> Show SplitError_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitError_ -> ShowS
showsPrec :: Int -> SplitError_ -> ShowS
$cshow :: SplitError_ -> [Char]
show :: SplitError_ -> [Char]
$cshowList :: [SplitError_] -> ShowS
showList :: [SplitError_] -> ShowS
Show, (forall x. SplitError_ -> Rep SplitError_ x)
-> (forall x. Rep SplitError_ x -> SplitError_)
-> Generic SplitError_
forall x. Rep SplitError_ x -> SplitError_
forall x. SplitError_ -> Rep SplitError_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SplitError_ -> Rep SplitError_ x
from :: forall x. SplitError_ -> Rep SplitError_ x
$cto :: forall x. Rep SplitError_ x -> SplitError_
to :: forall x. Rep SplitError_ x -> SplitError_
Generic)
  deriving (Int -> SplitError_
SplitError_ -> Int
SplitError_ -> [SplitError_]
SplitError_ -> SplitError_
SplitError_ -> SplitError_ -> [SplitError_]
SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_]
(SplitError_ -> SplitError_)
-> (SplitError_ -> SplitError_)
-> (Int -> SplitError_)
-> (SplitError_ -> Int)
-> (SplitError_ -> [SplitError_])
-> (SplitError_ -> SplitError_ -> [SplitError_])
-> (SplitError_ -> SplitError_ -> [SplitError_])
-> (SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_])
-> Enum SplitError_
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 :: SplitError_ -> SplitError_
succ :: SplitError_ -> SplitError_
$cpred :: SplitError_ -> SplitError_
pred :: SplitError_ -> SplitError_
$ctoEnum :: Int -> SplitError_
toEnum :: Int -> SplitError_
$cfromEnum :: SplitError_ -> Int
fromEnum :: SplitError_ -> Int
$cenumFrom :: SplitError_ -> [SplitError_]
enumFrom :: SplitError_ -> [SplitError_]
$cenumFromThen :: SplitError_ -> SplitError_ -> [SplitError_]
enumFromThen :: SplitError_ -> SplitError_ -> [SplitError_]
$cenumFromTo :: SplitError_ -> SplitError_ -> [SplitError_]
enumFromTo :: SplitError_ -> SplitError_ -> [SplitError_]
$cenumFromThenTo :: SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_]
enumFromThenTo :: SplitError_ -> SplitError_ -> SplitError_ -> [SplitError_]
Enum, SplitError_
SplitError_ -> SplitError_ -> Bounded SplitError_
forall a. a -> a -> Bounded a
$cminBound :: SplitError_
minBound :: SplitError_
$cmaxBound :: SplitError_
maxBound :: SplitError_
Bounded) via (FiniteEnumeration SplitError_)

data CannotQuote_
  = CannotQuoteAmbiguous_
  | CannotQuoteExpression_
  | CannotQuoteHidden_
  | CannotQuoteNothing_
  | CannotQuotePattern_
  deriving (Int -> CannotQuote_ -> ShowS
[CannotQuote_] -> ShowS
CannotQuote_ -> [Char]
(Int -> CannotQuote_ -> ShowS)
-> (CannotQuote_ -> [Char])
-> ([CannotQuote_] -> ShowS)
-> Show CannotQuote_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CannotQuote_ -> ShowS
showsPrec :: Int -> CannotQuote_ -> ShowS
$cshow :: CannotQuote_ -> [Char]
show :: CannotQuote_ -> [Char]
$cshowList :: [CannotQuote_] -> ShowS
showList :: [CannotQuote_] -> ShowS
Show, (forall x. CannotQuote_ -> Rep CannotQuote_ x)
-> (forall x. Rep CannotQuote_ x -> CannotQuote_)
-> Generic CannotQuote_
forall x. Rep CannotQuote_ x -> CannotQuote_
forall x. CannotQuote_ -> Rep CannotQuote_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CannotQuote_ -> Rep CannotQuote_ x
from :: forall x. CannotQuote_ -> Rep CannotQuote_ x
$cto :: forall x. Rep CannotQuote_ x -> CannotQuote_
to :: forall x. Rep CannotQuote_ x -> CannotQuote_
Generic, Int -> CannotQuote_
CannotQuote_ -> Int
CannotQuote_ -> [CannotQuote_]
CannotQuote_ -> CannotQuote_
CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
(CannotQuote_ -> CannotQuote_)
-> (CannotQuote_ -> CannotQuote_)
-> (Int -> CannotQuote_)
-> (CannotQuote_ -> Int)
-> (CannotQuote_ -> [CannotQuote_])
-> (CannotQuote_ -> CannotQuote_ -> [CannotQuote_])
-> (CannotQuote_ -> CannotQuote_ -> [CannotQuote_])
-> (CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_])
-> Enum CannotQuote_
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 :: CannotQuote_ -> CannotQuote_
succ :: CannotQuote_ -> CannotQuote_
$cpred :: CannotQuote_ -> CannotQuote_
pred :: CannotQuote_ -> CannotQuote_
$ctoEnum :: Int -> CannotQuote_
toEnum :: Int -> CannotQuote_
$cfromEnum :: CannotQuote_ -> Int
fromEnum :: CannotQuote_ -> Int
$cenumFrom :: CannotQuote_ -> [CannotQuote_]
enumFrom :: CannotQuote_ -> [CannotQuote_]
$cenumFromThen :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
enumFromThen :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
$cenumFromTo :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
enumFromTo :: CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
$cenumFromThenTo :: CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
enumFromThenTo :: CannotQuote_ -> CannotQuote_ -> CannotQuote_ -> [CannotQuote_]
Enum, CannotQuote_
CannotQuote_ -> CannotQuote_ -> Bounded CannotQuote_
forall a. a -> a -> Bounded a
$cminBound :: CannotQuote_
minBound :: CannotQuote_
$cmaxBound :: CannotQuote_
maxBound :: CannotQuote_
Bounded)

data ExecError_
  = ExeNotTrusted_
  | ExeNotFound_
  | ExeNotExecutable_
  deriving (Int -> ExecError_ -> ShowS
[ExecError_] -> ShowS
ExecError_ -> [Char]
(Int -> ExecError_ -> ShowS)
-> (ExecError_ -> [Char])
-> ([ExecError_] -> ShowS)
-> Show ExecError_
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExecError_ -> ShowS
showsPrec :: Int -> ExecError_ -> ShowS
$cshow :: ExecError_ -> [Char]
show :: ExecError_ -> [Char]
$cshowList :: [ExecError_] -> ShowS
showList :: [ExecError_] -> ShowS
Show, (forall x. ExecError_ -> Rep ExecError_ x)
-> (forall x. Rep ExecError_ x -> ExecError_) -> Generic ExecError_
forall x. Rep ExecError_ x -> ExecError_
forall x. ExecError_ -> Rep ExecError_ x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExecError_ -> Rep ExecError_ x
from :: forall x. ExecError_ -> Rep ExecError_ x
$cto :: forall x. Rep ExecError_ x -> ExecError_
to :: forall x. Rep ExecError_ x -> ExecError_
Generic, Int -> ExecError_
ExecError_ -> Int
ExecError_ -> [ExecError_]
ExecError_ -> ExecError_
ExecError_ -> ExecError_ -> [ExecError_]
ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_]
(ExecError_ -> ExecError_)
-> (ExecError_ -> ExecError_)
-> (Int -> ExecError_)
-> (ExecError_ -> Int)
-> (ExecError_ -> [ExecError_])
-> (ExecError_ -> ExecError_ -> [ExecError_])
-> (ExecError_ -> ExecError_ -> [ExecError_])
-> (ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_])
-> Enum ExecError_
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 :: ExecError_ -> ExecError_
succ :: ExecError_ -> ExecError_
$cpred :: ExecError_ -> ExecError_
pred :: ExecError_ -> ExecError_
$ctoEnum :: Int -> ExecError_
toEnum :: Int -> ExecError_
$cfromEnum :: ExecError_ -> Int
fromEnum :: ExecError_ -> Int
$cenumFrom :: ExecError_ -> [ExecError_]
enumFrom :: ExecError_ -> [ExecError_]
$cenumFromThen :: ExecError_ -> ExecError_ -> [ExecError_]
enumFromThen :: ExecError_ -> ExecError_ -> [ExecError_]
$cenumFromTo :: ExecError_ -> ExecError_ -> [ExecError_]
enumFromTo :: ExecError_ -> ExecError_ -> [ExecError_]
$cenumFromThenTo :: ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_]
enumFromThenTo :: ExecError_ -> ExecError_ -> ExecError_ -> [ExecError_]
Enum, ExecError_
ExecError_ -> ExecError_ -> Bounded ExecError_
forall a. a -> a -> Bounded a
$cminBound :: ExecError_
minBound :: ExecError_
$cmaxBound :: ExecError_
maxBound :: ExecError_
Bounded)

-- * Printing error names
------------------------------------------------------------------------

defaultErrorNameString :: Show a => a -> String
defaultErrorNameString :: forall a. Show a => a -> [Char]
defaultErrorNameString = [Char] -> ShowS
forall a. [a] -> [a] -> [a]
initWithDefault [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ ShowS -> (a -> [Char]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Show a => a -> [Char]
show

errorNameString :: ErrorName -> String
errorNameString :: ErrorName -> [Char]
errorNameString = \case
  ExecError_              ExecError_
err -> [Char]
"Exec." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ExecError_ -> [Char]
execErrorNameString ExecError_
err
  ImpossibleConstructor_  NegativeUnification_
err -> [Char]
"ImpossibleConstructor." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ NegativeUnification_ -> [Char]
negativeUnificationErrorNameString NegativeUnification_
err
  SplitError_             SplitError_
err -> [Char]
"SplitError." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SplitError_ -> [Char]
splitErrorNameString SplitError_
err
  CannotQuote_             CannotQuote_
err -> [Char]
"CannotQuote." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CannotQuote_ -> [Char]
cannotQuoteNameString CannotQuote_
err
  CannotQuoteTerm_         CannotQuoteTerm
err -> [Char]
"CannotQuoteTerm." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CannotQuoteTerm -> [Char]
cannotQuoteTermNameString CannotQuoteTerm
err
  InvalidPun_              ConstructorOrPatternSynonym
err -> [Char]
"InvalidPun." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ConstructorOrPatternSynonym -> [Char]
constructorOrPatternSynonymNameString ConstructorOrPatternSynonym
err
  MissingTypeSignature_    DataRecOrFun_
err -> [Char]
"MissingTypeSignature." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ DataRecOrFun_ -> [Char]
dataRecOrFunString DataRecOrFun_
err
  NotAllowedInDotPatterns_ NotAllowedInDotPatterns
err -> [Char]
"NotAllowedInDotPatterns." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ NotAllowedInDotPatterns -> [Char]
notAllowedInDotPatternsString NotAllowedInDotPatterns
err
  NotAValidLetBinding_    Maybe NotAValidLetBinding
merr -> Maybe NotAValidLetBinding
-> (NotAValidLetBinding -> ShowS) -> ShowS
forall b a. Maybe b -> (b -> a -> a) -> a -> a
applyWhenJust Maybe NotAValidLetBinding
merr (\ NotAValidLetBinding
err [Char]
hd -> [Char]
hd [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ NotAValidLetBinding -> [Char]
notAValidLetBindingString NotAValidLetBinding
err) [Char]
"NotAValidLetBinding"
  NotAValidLetExpression_  NotAValidLetExpression
err -> [Char]
"NotAValidLetExpression." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ NotAValidLetExpression -> [Char]
notAValidLetExpressionString NotAValidLetExpression
err
  PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym
err -> [Char]
"PatternSynonymArgumentShadows." [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ConstructorOrPatternSynonym -> [Char]
constructorOrPatternSynonymNameString ConstructorOrPatternSynonym
err
  ErrorName
err -> ErrorName -> [Char]
forall a. Show a => a -> [Char]
defaultErrorNameString ErrorName
err

constructorOrPatternSynonymNameString :: ConstructorOrPatternSynonym -> String
constructorOrPatternSynonymNameString :: ConstructorOrPatternSynonym -> [Char]
constructorOrPatternSynonymNameString = \case
  ConstructorOrPatternSynonym
IsConstructor    -> [Char]
"Constructor"
  ConstructorOrPatternSynonym
IsPatternSynonym -> [Char]
"PatternSynonym"

dataRecOrFunString :: DataRecOrFun_ -> String
dataRecOrFunString :: DataRecOrFun_ -> [Char]
dataRecOrFunString = \case
  DataRecOrFun_
DataName_ -> [Char]
"Data"
  DataRecOrFun_
RecName_  -> [Char]
"Record"
  DataRecOrFun_
FunName_  -> [Char]
"Function"

negativeUnificationErrorNameString :: NegativeUnification_ -> String
negativeUnificationErrorNameString :: NegativeUnification_ -> [Char]
negativeUnificationErrorNameString = NegativeUnification_ -> [Char]
forall a. Show a => a -> [Char]
defaultErrorNameString

notAHaskellTypeErrorNameString :: NotAHaskellType_ -> String
notAHaskellTypeErrorNameString :: NotAHaskellType_ -> [Char]
notAHaskellTypeErrorNameString = NotAHaskellType_ -> [Char]
forall a. Show a => a -> [Char]
defaultErrorNameString

notAValidLetBindingString :: NotAValidLetBinding -> String
notAValidLetBindingString :: NotAValidLetBinding -> [Char]
notAValidLetBindingString = NotAValidLetBinding -> [Char]
forall a. Show a => a -> [Char]
show

notAValidLetExpressionString :: NotAValidLetExpression -> String
notAValidLetExpressionString :: NotAValidLetExpression -> [Char]
notAValidLetExpressionString = NotAValidLetExpression -> [Char]
forall a. Show a => a -> [Char]
show

notAllowedInDotPatternsString :: NotAllowedInDotPatterns -> String
notAllowedInDotPatternsString :: NotAllowedInDotPatterns -> [Char]
notAllowedInDotPatternsString = NotAllowedInDotPatterns -> [Char]
forall a. Show a => a -> [Char]
show

splitErrorNameString :: SplitError_ -> String
splitErrorNameString :: SplitError_ -> [Char]
splitErrorNameString = \case
  SplitError_
err -> SplitError_ -> [Char]
forall a. Show a => a -> [Char]
defaultErrorNameString SplitError_
err

cannotQuoteNameString :: CannotQuote_ -> String
cannotQuoteNameString :: CannotQuote_ -> [Char]
cannotQuoteNameString = \case
  CannotQuote_
CannotQuoteAmbiguous_  -> [Char]
"Ambiguous"
  CannotQuote_
CannotQuoteExpression_ -> [Char]
"Expression"
  CannotQuote_
CannotQuoteHidden_     -> [Char]
"Hidden"
  CannotQuote_
CannotQuoteNothing_    -> [Char]
"Nothing"
  CannotQuote_
CannotQuotePattern_    -> [Char]
"Pattern"

cannotQuoteTermNameString :: CannotQuoteTerm -> String
cannotQuoteTermNameString :: CannotQuoteTerm -> [Char]
cannotQuoteTermNameString = \case
  CannotQuoteTermHidden Hiding
_    -> [Char]
"Hidden"
  CannotQuoteTerm
CannotQuoteTermNothing     -> [Char]
"Nothing"

execErrorNameString :: ExecError_ -> String
execErrorNameString :: ExecError_ -> [Char]
execErrorNameString = ExecError_ -> [Char]
forall a. Show a => a -> [Char]
defaultErrorNameString

-- | Print list of errors.

helpErrors :: String
helpErrors :: [Char]
helpErrors = [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[[Char]]] -> [[Char]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ [Char]
"Agda's errors:"
    , [Char]
""
    ]
  , [[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (ErrorName -> [Char]) -> [ErrorName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ErrorName -> [Char]
errorNameString [ErrorName
forall a. Bounded a => a
minBound..ErrorName
forall a. Bounded a => a
maxBound]
  ]

-- * Print error messages
------------------------------------------------------------------------

verbalizeNotAValidLetBinding :: NotAValidLetBinding -> String
verbalizeNotAValidLetBinding :: NotAValidLetBinding -> [Char]
verbalizeNotAValidLetBinding = \case
  NotAValidLetBinding
MissingRHS             -> [Char]
"Missing right hand side in let binding"
  NotAValidLetBinding
NotAValidLetPattern    -> [Char]
"Not a valid let pattern"
  NotAValidLetBinding
WhereClausesNotAllowed -> [Char]
"`where` clauses not allowed in let bindings"
  NotAValidLetBinding
CopatternsNotAllowed   -> [Char]
"Copatterns not allowed in let bindings"
  -- These cannot be triggered:
  -- EllipsisNotAllowed     -> "`...` not allowed in let bindings"
  -- WithPatternsNotAllowed -> "`with` patterns not allowed in let bindings"

verbalizeNotAValidLetExpression :: NotAValidLetExpression -> String
verbalizeNotAValidLetExpression :: NotAValidLetExpression -> [Char]
verbalizeNotAValidLetExpression = \case
  NotAValidLetExpression
MissingBody -> [Char]
"Missing body in let-expression"

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

deriving via (FiniteEnumeration (Maybe a))
  instance (Bounded a, Enum a) => Enum (Maybe a)
deriving via (FiniteEnumeration (Maybe a))
  instance (Bounded a) => Bounded (Maybe a)

instance NFData CannotQuoteTerm
instance NFData NotAllowedInDotPatterns
instance NFData NotAValidLetBinding
instance NFData NotAValidLetExpression