-- | Convert errors to their names.

module Mikan.TypeChecking.Errors.Names where

import Mikan.Syntax.Concrete.Definitions.Errors as N (DeclarationException'(..))
import Mikan.TypeChecking.Monad.Base            as MB
import Mikan.Interaction.Options.Errors

-- | Print the name of a 'TypeError'.
--
typeErrorString :: TypeError -> String
typeErrorString :: TypeError -> String
typeErrorString = ErrorName -> String
errorNameString (ErrorName -> String)
-> (TypeError -> ErrorName) -> TypeError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> ErrorName
typeErrorName

-- | Compute the name of a 'TypeError'.
--
typeErrorName :: TypeError -> ErrorName
typeErrorName :: TypeError -> ErrorName
typeErrorName = \case
  -- Error groups (alphabetically) with named sub errors
  ImpossibleConstructor QName
_  NegativeUnification
err -> NegativeUnification_ -> ErrorName
ImpossibleConstructor_ (NegativeUnification_ -> ErrorName)
-> NegativeUnification_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName NegativeUnification
err
  -- Parametrized errors
  CannotQuote             CannotQuote
what -> CannotQuote_ -> ErrorName
CannotQuote_           (CannotQuote_ -> ErrorName) -> CannotQuote_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ CannotQuote -> CannotQuote_
unquotableName                 CannotQuote
what
  MissingTypeSignature    MissingTypeSignatureInfo
what -> DataRecOrFun_ -> ErrorName
MissingTypeSignature_  (DataRecOrFun_ -> ErrorName) -> DataRecOrFun_ -> ErrorName
forall a b. (a -> b) -> a -> b
$ MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName   MissingTypeSignatureInfo
what
  InvalidPun            ConstructorOrPatternSynonym
kind QName
_ -> ConstructorOrPatternSynonym -> ErrorName
InvalidPun_              ConstructorOrPatternSynonym
kind
  CannotQuoteTerm         CannotQuoteTerm
what -> CannotQuoteTerm -> ErrorName
CannotQuoteTerm_         CannotQuoteTerm
what
  NotAllowedInDotPatterns NotAllowedInDotPatterns
what -> NotAllowedInDotPatterns -> ErrorName
NotAllowedInDotPatterns_ NotAllowedInDotPatterns
what
  NotAValidLetBinding     Maybe NotAValidLetBinding
what -> Maybe NotAValidLetBinding -> ErrorName
NotAValidLetBinding_     Maybe NotAValidLetBinding
what
  NotAValidLetExpression  NotAValidLetExpression
what -> NotAValidLetExpression -> ErrorName
NotAValidLetExpression_  NotAValidLetExpression
what
  -- Wrappers
  OperatorInformation [NotationSection]
_ OperatorScope
_  TypeError
err -> TypeError -> ErrorName
typeErrorName TypeError
err
  -- Generic errors (alphabetically)
  CompilationError          {} -> ErrorName
CompilationError_
  CustomBackendError        {} -> ErrorName
CustomBackendError_
  UserError                 {} -> ErrorName
UserError_
  InternalError             {} -> ErrorName
InternalError_
  LibraryError              {} -> ErrorName
LibraryError_
  NonFatalErrors            {} -> ErrorName
NonFatalErrors_
  OptionError               {} -> ErrorName
OptionError_
  SyntaxError               {} -> ErrorName
SyntaxError_
  -- Other errors (alphabetically)
  AbsentRHSRequiresAbsurdPattern                             {} -> ErrorName
AbsentRHSRequiresAbsurdPattern_
  AbstractConstructorNotInScope                              {} -> ErrorName
AbstractConstructorNotInScope_
  MB.AmbiguousConstructor                                    {} -> ErrorName
AmbiguousConstructor_
  AmbiguousField                                             {} -> ErrorName
AmbiguousField_
  AmbiguousModule                                            {} -> ErrorName
AmbiguousModule_
  AmbiguousName                                              {} -> ErrorName
AmbiguousName_
  AmbiguousOverloadedProjection                              {} -> ErrorName
AmbiguousOverloadedProjection_
  AmbiguousParseForApplication                               {} -> ErrorName
AmbiguousParseForApplication_
  AmbiguousParseForLHS                                       {} -> ErrorName
AmbiguousParseForLHS_
  AmbiguousProjection                                        {} -> ErrorName
AmbiguousProjection_
  AmbiguousTopLevelModuleName                                {} -> ErrorName
AmbiguousTopLevelModuleName_
  BackendDoesNotSupportOnlyScopeChecking                     {} -> ErrorName
BackendDoesNotSupportOnlyScopeChecking_
  BothWithAndRHS                                             {} -> ErrorName
BothWithAndRHS_
  BuiltinInParameterisedModule                               {} -> ErrorName
BuiltinInParameterisedModule_
  BuiltinMustBeConstructor                                   {} -> ErrorName
BuiltinMustBeConstructor_
  BuiltinMustBeData                                          {} -> ErrorName
BuiltinMustBeData_
  BuiltinMustBeDef                                           {} -> ErrorName
BuiltinMustBeDef_
  BuiltinMustBeFunction                                      {} -> ErrorName
BuiltinMustBeFunction_
  BuiltinMustBePostulate                                     {} -> ErrorName
BuiltinMustBePostulate_
  CannotApply                                                {} -> ErrorName
CannotApply_
  CannotGeneralizeEtaExpandable                              {} -> ErrorName
CannotGeneralizeEtaExpandable_
  CannotGenerateTransportClause                              {} -> ErrorName
CannotGenerateTransportClause_
  CannotRewriteByNonEquation                                 {} -> ErrorName
CannotRewriteByNonEquation_
  CantResolveOverloadedConstructorsTargetingSameDatatype     {} -> ErrorName
CantResolveOverloadedConstructorsTargetingSameDatatype_
  ClashingDefinition                                         {} -> ErrorName
ClashingDefinition_
  ClashingModule                                             {} -> ErrorName
ClashingModule_
  ComatchingDisabledForRecord                                {} -> ErrorName
ComatchingDisabledForRecord_
  ConstructorDoesNotTargetGivenType                          {} -> ErrorName
ConstructorDoesNotTargetGivenType_
  ConstructorNameOfNonRecord                                 {} -> ErrorName
ConstructorNameOfNonRecord_
  ConstructorPatternInWrongDatatype                          {} -> ErrorName
ConstructorPatternInWrongDatatype_
  CopatternHeadNotProjection                                 {} -> ErrorName
CopatternHeadNotProjection_
  CubicalPrimitiveNotFullyApplied                            {} -> ErrorName
CubicalPrimitiveNotFullyApplied_
  CyclicModuleDependency                                     {} -> ErrorName
CyclicModuleDependency_
  DeBruijnIndexOutOfScope                                    {} -> ErrorName
DeBruijnIndexOutOfScope_
  DeclarationsAfterTopLevelModule                            {} -> ErrorName
DeclarationsAfterTopLevelModule_
  DefinitionInDifferentModule                                {} -> ErrorName
DefinitionInDifferentModule_
  DoNotationError                                            {} -> ErrorName
DoNotationError_
  DuplicateBuiltinBinding                                    {} -> ErrorName
DuplicateBuiltinBinding_
  DuplicateConstructors                                      {} -> ErrorName
DuplicateConstructors_
  DuplicateFields                                            {} -> ErrorName
DuplicateFields_
  DuplicateImports                                           {} -> ErrorName
DuplicateImports_
  DuplicateOverlapPragma                                     {} -> ErrorName
DuplicateOverlapPragma_
  DuplicatePrimitiveBinding                                  {} -> ErrorName
DuplicatePrimitiveBinding_
  ExpectedIntervalLiteral                                    {} -> ErrorName
ExpectedIntervalLiteral_
  FaceConstraintDisjunction                                  {} -> ErrorName
FaceConstraintDisjunction_
  FaceConstraintUnsatisfiable                                {} -> ErrorName
FaceConstraintUnsatisfiable_
  FileNotFound                                               {} -> ErrorName
FileNotFound_
  ForcedConstructorNotInstantiated                           {} -> ErrorName
ForcedConstructorNotInstantiated_
  GeneralizationFailed                                       {} -> ErrorName
GeneralizationFailed_
  GeneralizationPrepruneErrorRefinedContext                  {} -> ErrorName
GeneralizationPrepruneErrorRefinedContext_
  GeneralizationPrepruneErrorCyclicDependencies              {} -> ErrorName
GeneralizationPrepruneErrorCyclicDependencies_
  GeneralizationPrepruneErrorFailedToInstantiate             {} -> ErrorName
GeneralizationPrepruneErrorFailedToInstantiate_
  GeneralizeCyclicDependency                                 {} -> ErrorName
GeneralizeCyclicDependency_
  GeneralizeNotSupportedHere                                 {} -> ErrorName
GeneralizeNotSupportedHere_
  GeneralizedVarInLetOpenedModule                            {} -> ErrorName
GeneralizedVarInLetOpenedModule_
  HidingMismatch                                             {} -> ErrorName
HidingMismatch_
  IdiomBracketError                                          {} -> ErrorName
IdiomBracketError_
  InvalidBuiltin                                             {} -> ErrorName
InvalidBuiltin_
  InvalidDottedExpression                                    {} -> ErrorName
InvalidDottedExpression_
  IllTypedPatternAfterWithAbstraction                        {} -> ErrorName
IllTypedPatternAfterWithAbstraction_
  IllegalDeclarationBeforeTopLevelModule                     {} -> ErrorName
IllegalDeclarationBeforeTopLevelModule_
  IllegalHidingInPostfixProjection                           {} -> ErrorName
IllegalHidingInPostfixProjection_
  IllegalLetInTelescope                                      {} -> ErrorName
IllegalLetInTelescope_
  IllegalPatternInTelescope                                  {} -> ErrorName
IllegalPatternInTelescope_
  IllformedProjectionPatternAbstract                         {} -> ErrorName
IllformedProjectionPatternAbstract_
  IllformedProjectionPatternConcrete                         {} -> ErrorName
IllformedProjectionPatternConcrete_
  InvalidFileName                                            {} -> ErrorName
InvalidFileName_
  InvalidPattern                                             {} -> ErrorName
InvalidPattern_
  InvalidProjectionParameter                                 {} -> ErrorName
InvalidProjectionParameter_
  InvalidTypeSort                                            {} -> ErrorName
InvalidTypeSort_
  LibTooFarDown                                              {} -> ErrorName
LibTooFarDown_
  LiteralTooBig                                              {} -> ErrorName
LiteralTooBig_
  MacroResultTypeMismatch                                    {} -> ErrorName
MacroResultTypeMismatch_
  MetaCannotDependOn                                         {} -> ErrorName
MetaCannotDependOn_
  MismatchedProjectionsError                                 {} -> ErrorName
MismatchedProjectionsError_
  MissingBindingsForTelescopeVariables                       {} -> ErrorName
MissingBindingsForTelescopeVariables_
  ModuleArityMismatch                                        {} -> ErrorName
ModuleArityMismatch_
  ModuleDefinedInOtherFile                                   {} -> ErrorName
ModuleDefinedInOtherFile_
  ModuleNameDoesntMatchFileName                              {} -> ErrorName
ModuleNameDoesntMatchFileName_
  ModuleNameHashCollision                                    {} -> ErrorName
ModuleNameHashCollision_
  ModuleNameUnexpected                                       {} -> ErrorName
ModuleNameUnexpected_
  MultipleFixityDecls                                        {} -> ErrorName
MultipleFixityDecls_
  MultiplePolarityPragmas                                    {} -> ErrorName
MultiplePolarityPragmas_
  NonLocalWhereModuleInRefinedContext                        {} -> ErrorName
NonLocalWhereModuleInRefinedContext_
  NeedOptionAllowExec                                        {} -> ErrorName
NeedOptionAllowExec_
  NeedOptionCopatterns                                       {} -> ErrorName
NeedOptionCopatterns_
  NeedOptionPatternMatching                                  {} -> ErrorName
NeedOptionPatternMatching_
  NeedOptionProp                                             {} -> ErrorName
NeedOptionProp_
  NegativeLiteralInPattern                                   {} -> ErrorName
NegativeLiteralInPattern_
  NoBindingForBuiltin                                        {} -> ErrorName
NoBindingForBuiltin_
  NoBindingForPrimitive                                      {} -> ErrorName
NoBindingForPrimitive_
  NoKnownRecordWithSuchFields                                {} -> ErrorName
NoKnownRecordWithSuchFields_
  NoParameterOfName                                          {} -> ErrorName
NoParameterOfName_
  NoParseForApplication                                      {} -> ErrorName
NoParseForApplication_
  NoParseForLHS                                              {} -> ErrorName
NoParseForLHS_
  NoSuchBuiltinName                                          {} -> ErrorName
NoSuchBuiltinName_
  NoSuchModule                                               {} -> ErrorName
NoSuchModule_
  NoSuchPrimitiveFunction                                    {} -> ErrorName
NoSuchPrimitiveFunction_
  NotAnExpression                                            {} -> ErrorName
NotAnExpression_
  NotInScope                                                 {} -> ErrorName
NotInScope_
  NotLeqSort                                                 {} -> ErrorName
NotLeqSort_
  OverlappingProjects                                        {} -> ErrorName
OverlappingProjects_
  PathAbstractionFailed                                      {} -> ErrorName
PathAbstractionFailed_
  PatternInPathLambda                                        {} -> ErrorName
PatternInPathLambda_
  PatternInSystem                                            {} -> ErrorName
PatternInSystem_
  QualifiedLocalModule                                       {} -> ErrorName
QualifiedLocalModule_
  RepeatedNamesInImportDirective                             {} -> ErrorName
RepeatedNamesInImportDirective_
  RepeatedVariablesInPattern                                 {} -> ErrorName
RepeatedVariablesInPattern_
  ShadowedModule                                             {} -> ErrorName
ShadowedModule_
  ShouldBeASort                                              {} -> ErrorName
ShouldBeASort_
  ShouldBeEmpty                                              {} -> ErrorName
ShouldBeEmpty_
  ShouldBePath                                               {} -> ErrorName
ShouldBePath_
  ShouldBePi                                                 {} -> ErrorName
ShouldBePi_
  ShouldBeRecordPattern                                      {} -> ErrorName
ShouldBeRecordPattern_
  ShouldBeRecordType                                         {} -> ErrorName
ShouldBeRecordType_
  ShouldEndInApplicationOfTheDatatype                        {} -> ErrorName
ShouldEndInApplicationOfTheDatatype_
  SolvedButOpenHoles                                         {} -> ErrorName
SolvedButOpenHoles_
  SortCannotDependOnItsIndex                                 {} -> ErrorName
SortCannotDependOnItsIndex_
  SortDoesNotAdmitDataDefinitions                            {} -> ErrorName
SortDoesNotAdmitDataDefinitions_
  TacticAttributeNotAllowed                                  {} -> ErrorName
TacticAttributeNotAllowed_
  TooFewPatternsInWithClause                                 {} -> ErrorName
TooFewPatternsInWithClause_
  TooManyFields                                              {} -> ErrorName
TooManyFields_
  TooManyPatternsInWithClause                                {} -> ErrorName
TooManyPatternsInWithClause_
  TriedToCopyConstrainedPrim                                 {} -> ErrorName
TriedToCopyConstrainedPrim_
  UnexpectedParameter                                        {} -> ErrorName
UnexpectedParameter_
  UnexpectedTypeSignatureForParameter                        {} -> ErrorName
UnexpectedTypeSignatureForParameter_
  UnexpectedWithPatterns                                     {} -> ErrorName
UnexpectedWithPatterns_
  UnknownBackend                                             {} -> ErrorName
UnknownBackend_
  WithClausePatternMismatch                                  {} -> ErrorName
WithClausePatternMismatch_
  WithOnFreeVariable                                         {} -> ErrorName
WithOnFreeVariable_
  WrongHidingInApplication                                   {} -> ErrorName
WrongHidingInApplication_
  WrongHidingInLHS                                           {} -> ErrorName
WrongHidingInLHS_
  WrongHidingInLambda                                        {} -> ErrorName
WrongHidingInLambda_
  WrongHidingInProjection                                    {} -> ErrorName
WrongHidingInProjection_
  WrongNamedArgument                                         {} -> ErrorName
WrongNamedArgument_
  WrongNumberOfConstructorArguments                          {} -> ErrorName
WrongNumberOfConstructorArguments_


impossibleConstructorErrorName :: NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName :: NegativeUnification -> NegativeUnification_
impossibleConstructorErrorName = \case
  UnifyConflict {} -> NegativeUnification_
UnifyConflict_
  UnifyCycle    {} -> NegativeUnification_
UnifyCycle_

missingTypeSignatureInfoName :: MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName :: MissingTypeSignatureInfo -> DataRecOrFun_
missingTypeSignatureInfoName = \case
  MissingDataSignature      {} -> DataRecOrFun_
DataName_
  MissingRecordSignature    {} -> DataRecOrFun_
RecName_
  MissingFunctionSignature  {} -> DataRecOrFun_
FunName_

notAHaskellTypeErrorName :: WhyNotAHaskellType -> NotAHaskellType_
notAHaskellTypeErrorName :: WhyNotAHaskellType -> NotAHaskellType_
notAHaskellTypeErrorName = \case
  BadDontCare               {} -> NotAHaskellType_
BadDontCare_
  BadLambda                 {} -> NotAHaskellType_
BadLambda_
  BadMeta                   {} -> NotAHaskellType_
BadMeta_
  NoPragmaFor               {} -> NotAHaskellType_
NoPragmaFor_
  NotCompiled               {} -> NotAHaskellType_
NotCompiled_
  WrongPragmaFor            {} -> NotAHaskellType_
WrongPragmaFor_

unquotableName :: CannotQuote -> CannotQuote_
unquotableName :: CannotQuote -> CannotQuote_
unquotableName = \case
  CannotQuoteAmbiguous         {} -> CannotQuote_
CannotQuoteAmbiguous_
  CannotQuoteExpression        {} -> CannotQuote_
CannotQuoteExpression_
  CannotQuoteHidden            {} -> CannotQuote_
CannotQuoteHidden_
  CannotQuoteNothing           {} -> CannotQuote_
CannotQuoteNothing_
  CannotQuotePattern           {} -> CannotQuote_
CannotQuotePattern_

-- -- * Printing names of errors

-- -- The following might not be used yet:

-- interactionErrorString :: InteractionError -> String
-- interactionErrorString = interactionErrorNameString . interactionErrorName

-- splitErrorString :: SplitError -> String
-- splitErrorString = splitErrorNameString . splitErrorName

-- unquoteErrorString :: UnquoteError -> String
-- unquoteErrorString = unquoteErrorNameString . unquoteErrorName