{-# LANGUAGE CPP #-}

module Agda.Interaction.Options.Warnings
       (
         WarningMode (..)
       , warningSet
       , warn2Error
       , defaultWarningSet
       , allWarnings
       , usualWarnings
       , noWarnings
       , unsolvedWarnings
       , errorWarnings
       , defaultWarningMode
       , warningModeUpdate
       , warningSets
       , WarningName (..)
       , warningName2String
       , string2WarningName
       , usageWarning
       )
where

import Control.Arrow ( (&&&) )
import Control.Monad ( guard )

import Data.Traversable ( for )

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

#include "undefined.h"
import Agda.Utils.Impossible


-- | A @WarningMode@ has two components: a set of warnings to be displayed
-- and a flag stating whether warnings should be turned into fatal errors.
data WarningMode = WarningMode
  { _warningSet :: Set WarningName
  , _warn2Error :: Bool
  } deriving (Eq, Show)

warningSet :: Lens' (Set WarningName) WarningMode
warningSet f o = (\ ws -> o { _warningSet = ws }) <$> f (_warningSet o)

warn2Error :: Lens' Bool WarningMode
warn2Error f o = (\ ws -> o { _warn2Error = ws }) <$> f (_warn2Error o)

-- | The @defaultWarningMode@ is a curated set of warnings covering non-fatal
-- errors and disabling style-related ones

defaultWarningSet :: String
defaultWarningSet = "warn"

defaultWarningMode :: WarningMode
defaultWarningMode = WarningMode ws False where
  ws = fst $ fromMaybe __IMPOSSIBLE__ $ lookup defaultWarningSet warningSets

-- | @warningModeUpdate str@ computes the action of @str@ over the current
-- @WarningMode@: it may reset the set of warnings, add or remove a specific
-- flag or demand that any warning be turned into an error

warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate str = case str of
  "error"   -> Just $ set warn2Error True
  "noerror" -> Just $ set warn2Error False
  _ | Just ws <- fst <$> lookup str warningSets
            -> Just $ set warningSet ws
  _ -> case stripPrefix "no" str of
    Just str' -> (over warningSet . Set.delete) <$> string2WarningName str'
    Nothing   -> (over warningSet . Set.insert) <$> string2WarningName str

-- | Common sets of warnings

warningSets :: [(String, (Set WarningName, String))]
warningSets = [ ("all"   , (allWarnings, "All of the existing warnings"))
              , ("warn"  , (usualWarnings, "Default warning level"))
              , ("ignore", (errorWarnings, "Ignore all the benign warnings"))
              ]

noWarnings :: Set WarningName
noWarnings = Set.empty

unsolvedWarnings :: Set WarningName
unsolvedWarnings = Set.fromList
                 [ UnsolvedMetaVariables_
                 , UnsolvedInteractionMetas_
                 , UnsolvedConstraints_
                 ]

errorWarnings :: Set WarningName
errorWarnings = Set.fromList
  [ CoverageIssue_
  , GenericNonFatalError_
  , MissingDefinitions_
  , NotAllowedInMutual_
  , NotStrictlyPositive_
  , OverlappingTokensWarning_
  , PragmaCompiled_
  , SafeFlagPostulate_
  , SafeFlagPragma_
  , SafeFlagNonTerminating_
  , SafeFlagTerminating_
  , SafeFlagWithoutKFlagPrimEraseEquality_
  , SafeFlagNoPositivityCheck_
  , SafeFlagPolarity_
  , SafeFlagNoUniverseCheck_
  , TerminationIssue_
  , UnsolvedMetaVariables_
  , UnsolvedInteractionMetas_
  , UnsolvedConstraints_
  , InfectiveImport_
  , CoInfectiveImport_
  ]

allWarnings :: Set WarningName
allWarnings = Set.fromList [minBound..maxBound]

usualWarnings :: Set WarningName
usualWarnings = allWarnings Set.\\ Set.fromList
              [ UnknownFixityInMixfixDecl_
              , CoverageNoExactSplit_
              ]

-- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance
-- to existing warnings in the codebase.

data WarningName
  =
  -- Parser Warnings
    OverlappingTokensWarning_
  -- Library Warnings
  | LibUnknownField_
  -- Nicifer Warnings
  | EmptyAbstract_
  | EmptyInstance_
  | EmptyMacro_
  | EmptyMutual_
  | EmptyPostulate_
  | EmptyPrivate_
  | EmptyGeneralize_
  | EmptyPrimitive_
  | InvalidCatchallPragma_
  | InvalidNoUniverseCheckPragma_
  | InvalidTerminationCheckPragma_
  | InvalidNoPositivityCheckPragma_
  | MissingDefinitions_
  | NotAllowedInMutual_
  | PolarityPragmasButNotPostulates_
  | PragmaNoTerminationCheck_
  | PragmaCompiled_
  | UnknownFixityInMixfixDecl_
  | UnknownNamesInFixityDecl_
  | UnknownNamesInPolarityPragmas_
  | UselessAbstract_
  | UselessInstance_
  | UselessPrivate_
  -- Scope and Type Checking Warnings
  | OldBuiltin_
  | EmptyRewritePragma_
  | IllformedAsClause_
  | UselessPublic_
  | UnreachableClauses_
  | UselessInline_
  | WrongInstanceDeclaration_
  | InstanceWithExplicitArg_
  | InstanceNoOutputTypeName_
  | InstanceArgWithExplicitArg_
  | GenericWarning_
  | DeprecationWarning_
  | InversionDepthReached_
  | TerminationIssue_
  | CoverageIssue_
  | CoverageNoExactSplit_
  | ModuleDoesntExport_
  | NotStrictlyPositive_
  | UnsolvedMetaVariables_
  | UnsolvedInteractionMetas_
  | UnsolvedConstraints_
  | GenericNonFatalError_
  | SafeFlagPostulate_
  | SafeFlagPragma_
  | SafeFlagNonTerminating_
  | SafeFlagTerminating_
  | SafeFlagWithoutKFlagPrimEraseEquality_
  | SafeFlagNoPositivityCheck_
  | SafeFlagPolarity_
  | SafeFlagNoUniverseCheck_
  | UserWarning_
  | WithoutKFlagPrimEraseEquality_
  | CantGeneralizeOverSorts_
  | AbsurdPatternRequiresNoRHS_
  -- Checking consistency of options
  | InfectiveImport_
  | CoInfectiveImport_
  deriving (Eq, Ord, Show, Read, Enum, Bounded)

-- | The flag corresponding to a warning is precisely the name of the constructor
-- minus the trailing underscore.

-- sorry
string2WarningName :: String -> Maybe WarningName
string2WarningName = readMaybe . (++ "_")

warningName2String :: WarningName -> String
warningName2String = init . show

-- | @warningUsage@ generated using @warningNameDescription@

usageWarning :: String
usageWarning = intercalate "\n"
  -- Looks like CPP doesn't like multiline string literals
  [ concat [ "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."
           ]
  , ""
  , concat [ "A group of warnings can be enabled by -W group, where group is "
           , "one of the following:"
           ]
  , ""
  , untable (fmap (fst &&& snd . snd) warningSets)
  , concat [ "Individual warnings can be turned on and off by -W Name and "
           , "-W noName respectively. The flags available are:"
           ]
  , ""
  , untable $ forMaybe [minBound..maxBound] $ \ w ->
    let wnd = warningNameDescription w in
    (warningName2String w, wnd) <$ guard (not $ null wnd)
  ]

  where

    untable :: [(String, String)] -> String
    untable rows =
      let len = maximum (map (length . fst) rows) in
      unlines $ flip map rows $ \ (hdr, cnt) ->
        concat [ hdr, replicate (1 + len - length hdr) ' ', cnt ]

-- | @WarningName@ descriptions used for generating usage information
-- Leave String empty to skip that name.

warningNameDescription :: WarningName -> String
warningNameDescription w = case w of
  OverlappingTokensWarning_        -> "Multi-line comments spanning one or more literate text blocks."
  -- Library Warnings
  LibUnknownField_                 -> "Unknown field in library file"
  -- Nicifer Warnings
  EmptyAbstract_                   -> "Empty `abstract' blocks."
  EmptyInstance_                   -> "Empty `instance' blocks."
  EmptyMacro_                      -> "Empty `macro' blocks."
  EmptyMutual_                     -> "Empty `mutual' blocks."
  EmptyPostulate_                  -> "Empty `postulate' blocks."
  EmptyPrivate_                    -> "Empty `private' blocks."
  EmptyGeneralize_                 -> "Empty `variable' blocks."
  EmptyPrimitive_                  -> "Empty `primitive' blocks."
  InvalidCatchallPragma_           -> "`CATCHALL' pragmas before a non-function clause."
  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."
  PolarityPragmasButNotPostulates_ -> "Polarity pragmas for non-postulates."
  PragmaNoTerminationCheck_        -> "`NO_TERMINATION_CHECK' pragmas are deprecated"
  PragmaCompiled_                  -> "'COMPILE' pragmas not allowed in safe mode."
  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."
  UselessInstance_                 -> "`instance' blocks where they have no effect."
  UselessPrivate_                  -> "`private' blocks where they have no effect."
  -- Scope and Type Checking Warnings
  OldBuiltin_                      -> "Deprecated `BUILTIN' pragmas."
  EmptyRewritePragma_              -> "Empty `REWRITE' pragmas."
  IllformedAsClause_               -> "Illformed `as'-clauses in `import' statements."
  UselessPublic_                   -> "`public' blocks where they have no effect."
  UselessInline_                   -> "`INLINE' pragmas where they have no effect."
  WrongInstanceDeclaration_        -> "Terms marked as eligible for instance search should end with a name."
  InstanceWithExplicitArg_         -> "`instance` declarations with explicit arguments are never considered by instance search."
  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."
  UnreachableClauses_              -> "Unreachable function clauses."
  GenericWarning_                  -> ""
  DeprecationWarning_              -> "Feature deprecation."
  InversionDepthReached_           -> "Inversions of pattern-matching failed due to exhausted inversion depth."
  TerminationIssue_                -> "Failed termination checks."
  CoverageIssue_                   -> "Failed coverage checks."
  CoverageNoExactSplit_            -> "Failed exact split checks."
  ModuleDoesntExport_              -> "Imported name is not actually exported."
  NotStrictlyPositive_             -> "Failed strict positivity checks."
  UnsolvedMetaVariables_           -> "Unsolved meta variables."
  UnsolvedInteractionMetas_        -> "Unsolved interaction meta variables."
  UnsolvedConstraints_             -> "Unsolved constraints."
  GenericNonFatalError_            -> ""
  SafeFlagPostulate_               -> "`postulate' blocks with the safe flag"
  SafeFlagPragma_                  -> "Unsafe `OPTIONS' pragmas with the safe flag."
  SafeFlagNonTerminating_          -> "`NON_TERMINATING' pragmas with the safe flag."
  SafeFlagTerminating_             -> "`TERMINATING' pragmas with the safe flag."
  SafeFlagWithoutKFlagPrimEraseEquality_ -> "`primEraseEquality' usages with the safe and without-K flags."
  SafeFlagNoPositivityCheck_       -> "`NO_POSITIVITY_CHECK' pragmas with the safe flag."
  SafeFlagPolarity_                -> "`POLARITY' pragmas with the safe flag."
  SafeFlagNoUniverseCheck_         -> "`NO_UNIVERSE_CHECK' pragmas with the safe flag."
  UserWarning_                     -> "User-defined warning added using the 'WARNING_ON_USAGE' pragma."
  AbsurdPatternRequiresNoRHS_      -> "A clause with an absurd pattern does not need a Right Hand Side."
  CantGeneralizeOverSorts_         -> "Attempt to generalize over sort metas in 'variable' declaration."
  WithoutKFlagPrimEraseEquality_   -> "`primEraseEquality' usages with the without-K flags."
  InfectiveImport_                 -> "Importing a file using e.g. `--cubical' into one which doesn't"
  CoInfectiveImport_               -> "Importing a file not using e.g. `--safe'  from one which does"