{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances.Errors where
import Data.Maybe
import Control.Monad
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common
import Agda.TypeChecking.Serialise.Instances.Internal ()
import Agda.TypeChecking.Serialise.Instances.Abstract ()
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Definitions (DeclarationWarning(..))
import Agda.Syntax.Abstract.Name (ModuleName)
import Agda.TypeChecking.Monad.Base
import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Interaction.Library
import Agda.Interaction.Library.Parse
import Agda.Termination.CutOff
import Agda.TypeChecking.Positivity.Occurrence ()
import Agda.Syntax.Parser.Monad (ParseWarning( OverlappingTokensWarning ))
import Agda.Utils.Pretty
import Agda.Utils.FileName ()
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
instance EmbPrj TCWarning where
icod_ (TCWarning a b c d) = icodeN' TCWarning a b c d
value = valueN TCWarning
instance EmbPrj Warning where
icod_ (TerminationIssue a) = __IMPOSSIBLE__
icod_ (UnreachableClauses a b) = icodeN 0 UnreachableClauses a b
icod_ (CoverageIssue a b) = __IMPOSSIBLE__
icod_ (NotStrictlyPositive a b) = __IMPOSSIBLE__
icod_ (UnsolvedMetaVariables a) = __IMPOSSIBLE__
icod_ (UnsolvedInteractionMetas a) = __IMPOSSIBLE__
icod_ (UnsolvedConstraints a) = __IMPOSSIBLE__
icod_ (OldBuiltin a b) = icodeN 1 OldBuiltin a b
icod_ EmptyRewritePragma = icodeN 2 EmptyRewritePragma
icod_ UselessPublic = icodeN 3 UselessPublic
icod_ (UselessInline a) = icodeN 4 UselessInline a
icod_ (GenericWarning a) = icodeN 5 GenericWarning a
icod_ (GenericNonFatalError a) = __IMPOSSIBLE__
icod_ (SafeFlagPostulate a) = __IMPOSSIBLE__
icod_ (SafeFlagPragma a) = __IMPOSSIBLE__
icod_ SafeFlagNonTerminating = __IMPOSSIBLE__
icod_ SafeFlagTerminating = __IMPOSSIBLE__
icod_ SafeFlagWithoutKFlagPrimEraseEquality = __IMPOSSIBLE__
icod_ SafeFlagNoPositivityCheck = __IMPOSSIBLE__
icod_ SafeFlagPolarity = __IMPOSSIBLE__
icod_ SafeFlagNoUniverseCheck = __IMPOSSIBLE__
icod_ (ParseWarning a) = __IMPOSSIBLE__
icod_ (DeprecationWarning a b c) = icodeN 6 DeprecationWarning a b c
icod_ (NicifierIssue a) = icodeN 7 NicifierIssue a
icod_ (InversionDepthReached a) = icodeN 8 InversionDepthReached a
icod_ (UserWarning a) = icodeN 9 UserWarning a
icod_ (AbsurdPatternRequiresNoRHS a) = icodeN 10 AbsurdPatternRequiresNoRHS a
icod_ (ModuleDoesntExport a b) = icodeN 11 ModuleDoesntExport a b
icod_ (LibraryWarning a) = icodeN 12 LibraryWarning a
icod_ (CoverageNoExactSplit a b) = icodeN 13 CoverageNoExactSplit a b
icod_ (CantGeneralizeOverSorts a) = icodeN 14 CantGeneralizeOverSorts a
icod_ (IllformedAsClause a) = icodeN 15 IllformedAsClause a
icod_ WithoutKFlagPrimEraseEquality = icodeN 16 WithoutKFlagPrimEraseEquality
icod_ (InstanceWithExplicitArg a) = icodeN 17 InstanceWithExplicitArg a
icod_ (InfectiveImport a b) = icodeN 18 InfectiveImport a b
icod_ (CoInfectiveImport a b) = icodeN 19 CoInfectiveImport a b
icod_ (InstanceNoOutputTypeName a) = icodeN 20 InstanceNoOutputTypeName a
icod_ (InstanceArgWithExplicitArg a) = icodeN 21 InstanceArgWithExplicitArg a
icod_ WrongInstanceDeclaration = icodeN 22 WrongInstanceDeclaration
value = vcase valu where
valu [0, a, b] = valuN UnreachableClauses a b
valu [1, a, b] = valuN OldBuiltin a b
valu [2] = valuN EmptyRewritePragma
valu [3] = valuN UselessPublic
valu [4, a] = valuN UselessInline a
valu [5, a] = valuN GenericWarning a
valu [6, a, b, c] = valuN DeprecationWarning a b c
valu [7, a] = valuN NicifierIssue a
valu [8, a] = valuN InversionDepthReached a
valu [9, a] = valuN UserWarning a
valu [10, a] = valuN AbsurdPatternRequiresNoRHS a
valu [11, a, b] = valuN ModuleDoesntExport a b
valu [12, a] = valuN LibraryWarning a
valu [13, a, b] = valuN CoverageNoExactSplit a b
valu [14, a] = valuN CantGeneralizeOverSorts a
valu [15, a] = valuN IllformedAsClause a
valu [16] = valuN WithoutKFlagPrimEraseEquality
valu [17, a] = valuN InstanceWithExplicitArg a
valu [18, a, b] = valuN InfectiveImport a b
valu [19, a, b] = valuN CoInfectiveImport a b
valu [20, a] = valuN InstanceNoOutputTypeName a
valu [21, a] = valuN InstanceArgWithExplicitArg a
valu _ = malformed
instance EmbPrj DeclarationWarning where
icod_ = \case
UnknownNamesInFixityDecl a -> icodeN 0 UnknownNamesInFixityDecl a
UnknownNamesInPolarityPragmas a -> icodeN 1 UnknownNamesInPolarityPragmas a
PolarityPragmasButNotPostulates a -> icodeN 2 PolarityPragmasButNotPostulates a
UselessPrivate a -> icodeN 3 UselessPrivate a
UselessAbstract a -> icodeN 4 UselessAbstract a
UselessInstance a -> icodeN 5 UselessInstance a
EmptyMutual a -> icodeN 6 EmptyMutual a
EmptyAbstract a -> icodeN 7 EmptyAbstract a
EmptyPrivate a -> icodeN 8 EmptyPrivate a
EmptyInstance a -> icodeN 9 EmptyInstance a
EmptyMacro a -> icodeN 10 EmptyMacro a
EmptyPostulate a -> icodeN 11 EmptyPostulate a
InvalidTerminationCheckPragma a -> icodeN 12 InvalidTerminationCheckPragma a
InvalidNoPositivityCheckPragma a -> icodeN 13 InvalidNoPositivityCheckPragma a
InvalidCatchallPragma a -> icodeN 14 InvalidCatchallPragma a
InvalidNoUniverseCheckPragma a -> icodeN 15 InvalidNoUniverseCheckPragma a
UnknownFixityInMixfixDecl a -> icodeN 16 UnknownFixityInMixfixDecl a
MissingDefinitions a -> icodeN 17 MissingDefinitions a
NotAllowedInMutual r a -> icodeN 18 NotAllowedInMutual r a
PragmaNoTerminationCheck r -> icodeN 19 PragmaNoTerminationCheck r
EmptyGeneralize a -> icodeN 20 EmptyGeneralize a
PragmaCompiled r -> icodeN 21 PragmaCompiled r
EmptyPrimitive a -> icodeN 22 EmptyPrimitive a
value = vcase $ \case
[0, a] -> valuN UnknownNamesInFixityDecl a
[1, a] -> valuN UnknownNamesInPolarityPragmas a
[2, a] -> valuN PolarityPragmasButNotPostulates a
[3, a] -> valuN UselessPrivate a
[4, a] -> valuN UselessAbstract a
[5, a] -> valuN UselessInstance a
[6, a] -> valuN EmptyMutual a
[7, a] -> valuN EmptyAbstract a
[8, a] -> valuN EmptyPrivate a
[9, a] -> valuN EmptyInstance a
[10,a] -> valuN EmptyMacro a
[11,a] -> valuN EmptyPostulate a
[12,a] -> valuN InvalidTerminationCheckPragma a
[13,a] -> valuN InvalidNoPositivityCheckPragma a
[14,a] -> valuN InvalidCatchallPragma a
[15,a] -> valuN InvalidNoUniverseCheckPragma a
[16,a] -> valuN UnknownFixityInMixfixDecl a
[17,a] -> valuN MissingDefinitions a
[18,r,a] -> valuN NotAllowedInMutual r a
[19,r] -> valuN PragmaNoTerminationCheck r
[20,a] -> valuN EmptyGeneralize a
[21,a] -> valuN PragmaCompiled a
[22,a] -> valuN EmptyPrimitive a
_ -> malformed
instance EmbPrj LibWarning where
icod_ = \case
LibWarning a b -> icodeN 0 LibWarning a b
value = vcase $ \case
[0, a, b] -> valuN LibWarning a b
_ -> malformed
instance EmbPrj LibWarning' where
icod_ = \case
UnknownField a -> icodeN 0 UnknownField a
value = vcase $ \case
[0, a] -> valuN UnknownField a
_ -> malformed
instance EmbPrj LibPositionInfo where
icod_ = \case
LibPositionInfo a b c -> icodeN 0 LibPositionInfo a b c
value = vcase $ \case
[0, a, b, c] -> valuN LibPositionInfo a b c
_ -> malformed
instance EmbPrj Doc where
icod_ d = icodeN' (undefined :: String -> Doc) (render d)
value = valueN text
instance EmbPrj PragmaOptions where
icod_ = \case
PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm -> icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm
value = vcase $ \case
[a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm] -> valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm
_ -> malformed
instance EmbPrj WarningMode where
icod_ = \case
WarningMode a b -> icodeN' WarningMode a b
value = vcase $ \case
[a, b] -> valuN WarningMode a b
_ -> malformed
instance EmbPrj WarningName where
icod_ x = icod_ (warningName2String x)
value = (maybe malformed return . string2WarningName) <=< value
instance EmbPrj CutOff where
icod_ = \case
DontCutOff -> icodeN' DontCutOff
CutOff a -> icodeN 0 CutOff a
value = vcase valu where
valu [] = valuN DontCutOff
valu [0,a] = valuN CutOff a
valu _ = malformed