{-# LANGUAGE DataKinds #-}

{-# OPTIONS_GHC -Wunused-imports #-}

-- | A module defining the types exported by "Mikan.Interaction.Options" for use in the rest of the codebase.
--
-- This is a boot module to avoid cyclic module dependencies.
-- Only put types and trivial instances here.

module Mikan.Interaction.Options.Types where

import Control.DeepSeq ( NFData )
import Data.Functor ( (<&>) )
import Data.Map ( Map )
import Data.Set ( Set )
import GHC.Generics ( Generic )

import Mikan.Syntax.Concrete.Glyph ( UnicodeOrAscii )
import Mikan.Interaction.Library ( ExeName, LibName )
import Mikan.Interaction.Options.Help ( Help )
import Mikan.Interaction.Options.Warnings ( WarningMode )
import Mikan.Termination.CutOff ( CutOff )

import Mikan.Utils.FileName ( AbsolutePath )
import Mikan.Utils.Lens ( Lens', (^.), over )
import Mikan.Utils.List1 ( String1 )
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Interaction.Options.ProfileOptions ( ProfileOptions )
import Mikan.Utils.Trie ( Trie )
import Mikan.Utils.WithDefault ( WithDefault, WithDefault' )

---------------------------------------------------------------------------
-- * Option records

-- Don't forget to update
--   doc/user-manual/tools/command-line-options.rst
-- if you make changes to the command-line options!

data CommandLineOptions = Options
  { CommandLineOptions -> Maybe FilePath
optInputFile             :: Maybe FilePath
  , CommandLineOptions -> [FilePath]
optIncludePaths          :: [FilePath]
  , CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths  :: [AbsolutePath]
      -- ^ The list should not contain duplicates.
  , CommandLineOptions -> [LibName]
optLibraries             :: [LibName]
  , CommandLineOptions -> Maybe FilePath
optOverrideLibrariesFile :: Maybe FilePath
      -- ^ Use this (if 'Just') instead of @~\/.agda\/libraries@.
  , CommandLineOptions -> Bool
optDefaultLibs           :: Bool
       -- ^ Use @~\/.agda\/defaults@.
  , CommandLineOptions -> Maybe FilePath
optOverrideDefaultsFile :: Maybe FilePath
      -- ^ Use this (if 'Just') instead of @~\/.agda\/defaults@.
  , CommandLineOptions -> Bool
optUseLibs               :: Bool
       -- ^ look for @.agda-lib@ files.
  , CommandLineOptions -> Integer
optTraceImports          :: Integer
       -- ^ Configure notifications about imported modules.
  , CommandLineOptions -> Map ExeName FilePath
optTrustedExecutables    :: Map ExeName FilePath
       -- ^ Map names of trusted executables to absolute paths.

  -- Setup and printing
  , CommandLineOptions -> Bool
optPrintDataDir          :: Bool
  , CommandLineOptions -> Bool
optPrintAppDir           :: Bool
  , CommandLineOptions -> Bool
optPrintOptions          :: Bool
      -- ^ Print all options as a simple list (for implementing bash completion).
  , CommandLineOptions -> Maybe PrintVersion
optPrintVersion          :: Maybe PrintVersion
  , CommandLineOptions -> Maybe Help
optPrintHelp             :: Maybe Help
  , CommandLineOptions -> Bool
optBuildLibrary          :: Bool
      -- ^ @--build-library@: Build all modules in the current library.
  , CommandLineOptions -> Bool
optSetup                 :: Bool
      -- ^ Force self-setup at startup.
  , CommandLineOptions -> Set EmacsModeCommand
optEmacsMode             :: Set EmacsModeCommand
      -- ^ Emacs mode administration
      --   (formerly done by the @agda-mode@ executable).
      --   Accepted subcommands: @locate@, @setup@, @compile@.
      --   Can be given several times,
      --   subcommands are accumulated in the set.

  , CommandLineOptions -> Bool
optGHCiInteraction       :: Bool
      -- ^ @--interaction@ mode.
  , CommandLineOptions -> Bool
optJSONInteraction       :: Bool
      -- ^ @--interaction-json@ mode.
  , CommandLineOptions -> Bool
optExitOnError           :: !Bool
      -- ^ Exit if an interactive command fails.
  , CommandLineOptions -> Bool
optGenerateVimFile       :: Bool
  , CommandLineOptions -> Bool
optIgnoreInterfaces      :: Bool
  , CommandLineOptions -> Bool
optIgnoreAllInterfaces   :: Bool
  , CommandLineOptions -> Bool
optWriteInterfaces       :: Bool
  , CommandLineOptions -> PragmaOptions
optPragmaOptions         :: PragmaOptions
  , CommandLineOptions -> Bool
optOnlyScopeChecking     :: Bool
      -- ^ Should the top-level module only be scope-checked, and not type-checked?
  , CommandLineOptions -> Bool
optTransliterate         :: Bool
      -- ^ Should code points that are not supported by the locale be transliterated?
  , CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour     :: DiagnosticsColours
      -- ^ Configure colour output.
  , CommandLineOptions -> Bool
optMdOnlyAgdaBlocks      :: Bool
      -- ^ In literate Markdown/Typst, only treat @```agda@ blocks as code.
  , CommandLineOptions -> Parallelism
optParallelChecking      :: Parallelism
      -- ^ Should imports be type-checked in parallel?
  }
  deriving (Int -> CommandLineOptions -> ShowS
[CommandLineOptions] -> ShowS
CommandLineOptions -> FilePath
(Int -> CommandLineOptions -> ShowS)
-> (CommandLineOptions -> FilePath)
-> ([CommandLineOptions] -> ShowS)
-> Show CommandLineOptions
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CommandLineOptions -> ShowS
showsPrec :: Int -> CommandLineOptions -> ShowS
$cshow :: CommandLineOptions -> FilePath
show :: CommandLineOptions -> FilePath
$cshowList :: [CommandLineOptions] -> ShowS
showList :: [CommandLineOptions] -> ShowS
Show, (forall x. CommandLineOptions -> Rep CommandLineOptions x)
-> (forall x. Rep CommandLineOptions x -> CommandLineOptions)
-> Generic CommandLineOptions
forall x. Rep CommandLineOptions x -> CommandLineOptions
forall x. CommandLineOptions -> Rep CommandLineOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommandLineOptions -> Rep CommandLineOptions x
from :: forall x. CommandLineOptions -> Rep CommandLineOptions x
$cto :: forall x. Rep CommandLineOptions x -> CommandLineOptions
to :: forall x. Rep CommandLineOptions x -> CommandLineOptions
Generic)

-- | Options which can be set in a pragma.

data PragmaOptions = PragmaOptions
  { PragmaOptions -> WithDefault 'False
_optShowImplicit              :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optShowGeneralized           :: WithDefault 'True
      -- ^ Show generalized parameters in Pi types
  , PragmaOptions -> WithDefault 'False
_optShowIrrelevant            :: WithDefault 'False
  , PragmaOptions -> WithDefault' UnicodeOrAscii 'True
_optUseUnicode                :: WithDefault' UnicodeOrAscii 'True -- Would like to write UnicodeOk instead of True here
  , PragmaOptions -> Verbosity
_optVerbose                   :: !Verbosity
  , PragmaOptions -> ProfileOptions
_optProfiling                 :: ProfileOptions
  , PragmaOptions -> WithDefault 'False
_optProp                      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optLevelUniverse             :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optAllowUnsolved             :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optAllowIncompleteMatch      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optPositivityCheck           :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optTerminationCheck          :: WithDefault 'True
  , PragmaOptions -> CutOff
_optTerminationDepth          :: CutOff
      -- ^ Cut off structural order comparison at some depth in termination checker?
  , PragmaOptions -> WithDefault 'True
_optCopatterns                :: WithDefault 'True
      -- ^ Allow definitions by copattern matching?
  , PragmaOptions -> WithDefault 'True
_optPatternMatching           :: WithDefault 'True
      -- ^ Is pattern matching allowed in the current file?
  , PragmaOptions -> WithDefault 'False
_optExactSplit                :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optHiddenArgumentPuns        :: WithDefault 'False
      -- ^ Should patterns of the form @{x}@ or @⦃ x ⦄@ be interpreted as puns?
  , PragmaOptions -> WithDefault 'True
_optEta                       :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optForcing                   :: WithDefault 'True
      -- ^ Perform the forcing analysis on data constructors?
  , PragmaOptions -> WithDefault 'True
_optProjectionLike            :: WithDefault 'True
      -- ^ Perform the projection-likeness analysis on functions?
  , PragmaOptions -> WithDefault 'False
_optFirstOrder                :: WithDefault 'False
      -- ^ Should we speculatively unify function applications as if they were injective? Implies
      --   optRequireUniqueMetaSolutions.
  , PragmaOptions -> WithDefault 'True
_optRequireUniqueMetaSolutions :: WithDefault 'True
      -- ^ Forbid non-unique meta solutions allowed. For instance from INJECTIVE_FOR_INFERENCE pragmas.
  , PragmaOptions -> WithDefault 'True
_optPostfixProjections        :: WithDefault 'True
      -- ^ Should system generated projections 'ProjSystem' be printed
      --   postfix (True) or prefix (False).
  , PragmaOptions -> WithDefault 'True
_optKeepPatternVariables      :: WithDefault 'True
      -- ^ Should case splitting replace variables with dot patterns
      --   (False) or keep them as variables (True).
  , PragmaOptions -> WithDefault 'True
_optInferAbsurdClauses        :: WithDefault 'True
      -- ^ Should case splitting and coverage checking try to discharge absurd clauses?
      --   Default: 'True', but 'False' might make coverage checking considerably faster in some cases.
  , PragmaOptions -> Int
_optInstanceSearchDepth       :: Int
  , PragmaOptions -> WithDefault 'False
_optBacktrackingInstances     :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optQualifiedInstances        :: WithDefault 'True
      -- ^ Should instance search consider instances with qualified names?
  , PragmaOptions -> Int
_optInversionMaxDepth         :: Int
  , PragmaOptions -> WithDefault 'False
_optSafe                      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optDoubleCheck               :: WithDefault 'False
  , PragmaOptions -> WarningMode
_optWarningMode               :: WarningMode
  , PragmaOptions -> WithDefault 'True
_optCompileMain               :: WithDefault 'True
      -- ^ Treat the module given at the command line or via interaction as main module in compilation?
  , PragmaOptions -> WithDefault 'True
_optCaching                   :: WithDefault 'True
  , PragmaOptions -> WithDefault 'False
_optCountClusters             :: WithDefault 'False
      -- ^ Count extended grapheme clusters rather than code points
      --   when generating LaTeX.
  , PragmaOptions -> WithDefault 'False
_optAutoInline                :: WithDefault 'False
      -- ^ Automatic compile-time inlining for simple definitions
      --   (unless marked @NOINLINE@).
  , PragmaOptions -> WithDefault 'True
_optPrintPatternSynonyms      :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optFastReduce                :: WithDefault 'True
      -- ^ Use the abstract machine ('fastReduce')?
  , PragmaOptions -> WithDefault 'False
_optCallByName                :: WithDefault 'False
      -- ^ Use call-by-name instead of call-by-need.
  , PragmaOptions -> WithDefault 'True
_optOccurrence                :: WithDefault 'True
      -- ^ Perform automated occurrence analysis for functions?
  , PragmaOptions -> WithDefault 'True
_optImportSorts               :: WithDefault 'True
      -- ^ Should every top-level module start with an implicit statement
      --   @open import Agda.Primitive using (Type; Prop)@?
  , PragmaOptions -> WithDefault 'True
_optLoadPrimitives            :: WithDefault 'True
      -- ^ Should we load the primitive modules at all?
      --   This is a stronger form of 'optImportSorts'.
  , PragmaOptions -> WithDefault 'False
_optAllowExec                 :: WithDefault 'False
      -- ^ Allow running external @executables@ from meta programs.
  , PragmaOptions -> WithDefault 'False
_optSaveMetas                 :: WithDefault 'False
      -- ^ Save meta-variables to interface files.
  , PragmaOptions -> WithDefault 'False
_optShowIdentitySubstitutions :: WithDefault 'False
      -- ^ Show identity substitutions when pretty-printing terms
      --   (i.e. always show all arguments of a metavariable).
  , PragmaOptions -> WithDefault 'False
_optKeepCoveringClauses       :: WithDefault 'False
      -- ^ Do not discard clauses constructed by the coverage checker
      --   (needed for some external backends).
  , PragmaOptions -> WithDefault 'False
_optExperimentalLazyInstances :: WithDefault 'False
      -- ^ Defer instance search based on discrimination tree results
  , PragmaOptions -> WithDefault 'False
_optQuoteMetas                :: WithDefault 'False
  }
  deriving (Int -> PragmaOptions -> ShowS
[PragmaOptions] -> ShowS
PragmaOptions -> FilePath
(Int -> PragmaOptions -> ShowS)
-> (PragmaOptions -> FilePath)
-> ([PragmaOptions] -> ShowS)
-> Show PragmaOptions
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PragmaOptions -> ShowS
showsPrec :: Int -> PragmaOptions -> ShowS
$cshow :: PragmaOptions -> FilePath
show :: PragmaOptions -> FilePath
$cshowList :: [PragmaOptions] -> ShowS
showList :: [PragmaOptions] -> ShowS
Show, PragmaOptions -> PragmaOptions -> Bool
(PragmaOptions -> PragmaOptions -> Bool)
-> (PragmaOptions -> PragmaOptions -> Bool) -> Eq PragmaOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PragmaOptions -> PragmaOptions -> Bool
== :: PragmaOptions -> PragmaOptions -> Bool
$c/= :: PragmaOptions -> PragmaOptions -> Bool
/= :: PragmaOptions -> PragmaOptions -> Bool
Eq, (forall x. PragmaOptions -> Rep PragmaOptions x)
-> (forall x. Rep PragmaOptions x -> PragmaOptions)
-> Generic PragmaOptions
forall x. Rep PragmaOptions x -> PragmaOptions
forall x. PragmaOptions -> Rep PragmaOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PragmaOptions -> Rep PragmaOptions x
from :: forall x. PragmaOptions -> Rep PragmaOptions x
$cto :: forall x. Rep PragmaOptions x -> PragmaOptions
to :: forall x. Rep PragmaOptions x -> PragmaOptions
Generic)

---------------------------------------------------------------------------
-- * Auxiliary structures (by default in alphabetic order)

data DiagnosticsColours
  = AlwaysColour
  | NeverColour
  | AutoColour
  deriving (Int -> DiagnosticsColours -> ShowS
[DiagnosticsColours] -> ShowS
DiagnosticsColours -> FilePath
(Int -> DiagnosticsColours -> ShowS)
-> (DiagnosticsColours -> FilePath)
-> ([DiagnosticsColours] -> ShowS)
-> Show DiagnosticsColours
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiagnosticsColours -> ShowS
showsPrec :: Int -> DiagnosticsColours -> ShowS
$cshow :: DiagnosticsColours -> FilePath
show :: DiagnosticsColours -> FilePath
$cshowList :: [DiagnosticsColours] -> ShowS
showList :: [DiagnosticsColours] -> ShowS
Show, (forall x. DiagnosticsColours -> Rep DiagnosticsColours x)
-> (forall x. Rep DiagnosticsColours x -> DiagnosticsColours)
-> Generic DiagnosticsColours
forall x. Rep DiagnosticsColours x -> DiagnosticsColours
forall x. DiagnosticsColours -> Rep DiagnosticsColours x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DiagnosticsColours -> Rep DiagnosticsColours x
from :: forall x. DiagnosticsColours -> Rep DiagnosticsColours x
$cto :: forall x. Rep DiagnosticsColours x -> DiagnosticsColours
to :: forall x. Rep DiagnosticsColours x -> DiagnosticsColours
Generic)

data Parallelism
  = Sequential
  | Parallel (Maybe Int)
  deriving (Int -> Parallelism -> ShowS
[Parallelism] -> ShowS
Parallelism -> FilePath
(Int -> Parallelism -> ShowS)
-> (Parallelism -> FilePath)
-> ([Parallelism] -> ShowS)
-> Show Parallelism
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Parallelism -> ShowS
showsPrec :: Int -> Parallelism -> ShowS
$cshow :: Parallelism -> FilePath
show :: Parallelism -> FilePath
$cshowList :: [Parallelism] -> ShowS
showList :: [Parallelism] -> ShowS
Show, (forall x. Parallelism -> Rep Parallelism x)
-> (forall x. Rep Parallelism x -> Parallelism)
-> Generic Parallelism
forall x. Rep Parallelism x -> Parallelism
forall x. Parallelism -> Rep Parallelism x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Parallelism -> Rep Parallelism x
from :: forall x. Parallelism -> Rep Parallelism x
$cto :: forall x. Rep Parallelism x -> Parallelism
to :: forall x. Rep Parallelism x -> Parallelism
Generic)

-- | If several @--emacs-mode@ commands are given,
--   they are executed in the order as given in this datatype.
data EmacsModeCommand
  = EmacsModeCompile
      -- ^ Compile the @.el@ files to @.elc@.
  | EmacsModeSetup
      -- ^ Add the initialization lines to @.emacs@.
  | EmacsModeLocate
      -- ^ Print the installation location of @agda2.el@.
  deriving (EmacsModeCommand -> EmacsModeCommand -> Bool
(EmacsModeCommand -> EmacsModeCommand -> Bool)
-> (EmacsModeCommand -> EmacsModeCommand -> Bool)
-> Eq EmacsModeCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EmacsModeCommand -> EmacsModeCommand -> Bool
== :: EmacsModeCommand -> EmacsModeCommand -> Bool
$c/= :: EmacsModeCommand -> EmacsModeCommand -> Bool
/= :: EmacsModeCommand -> EmacsModeCommand -> Bool
Eq, Eq EmacsModeCommand
Eq EmacsModeCommand =>
(EmacsModeCommand -> EmacsModeCommand -> Ordering)
-> (EmacsModeCommand -> EmacsModeCommand -> Bool)
-> (EmacsModeCommand -> EmacsModeCommand -> Bool)
-> (EmacsModeCommand -> EmacsModeCommand -> Bool)
-> (EmacsModeCommand -> EmacsModeCommand -> Bool)
-> (EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand)
-> (EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand)
-> Ord EmacsModeCommand
EmacsModeCommand -> EmacsModeCommand -> Bool
EmacsModeCommand -> EmacsModeCommand -> Ordering
EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: EmacsModeCommand -> EmacsModeCommand -> Ordering
compare :: EmacsModeCommand -> EmacsModeCommand -> Ordering
$c< :: EmacsModeCommand -> EmacsModeCommand -> Bool
< :: EmacsModeCommand -> EmacsModeCommand -> Bool
$c<= :: EmacsModeCommand -> EmacsModeCommand -> Bool
<= :: EmacsModeCommand -> EmacsModeCommand -> Bool
$c> :: EmacsModeCommand -> EmacsModeCommand -> Bool
> :: EmacsModeCommand -> EmacsModeCommand -> Bool
$c>= :: EmacsModeCommand -> EmacsModeCommand -> Bool
>= :: EmacsModeCommand -> EmacsModeCommand -> Bool
$cmax :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand
max :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand
$cmin :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand
min :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand
Ord, Int -> EmacsModeCommand -> ShowS
[EmacsModeCommand] -> ShowS
EmacsModeCommand -> FilePath
(Int -> EmacsModeCommand -> ShowS)
-> (EmacsModeCommand -> FilePath)
-> ([EmacsModeCommand] -> ShowS)
-> Show EmacsModeCommand
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EmacsModeCommand -> ShowS
showsPrec :: Int -> EmacsModeCommand -> ShowS
$cshow :: EmacsModeCommand -> FilePath
show :: EmacsModeCommand -> FilePath
$cshowList :: [EmacsModeCommand] -> ShowS
showList :: [EmacsModeCommand] -> ShowS
Show, (forall x. EmacsModeCommand -> Rep EmacsModeCommand x)
-> (forall x. Rep EmacsModeCommand x -> EmacsModeCommand)
-> Generic EmacsModeCommand
forall x. Rep EmacsModeCommand x -> EmacsModeCommand
forall x. EmacsModeCommand -> Rep EmacsModeCommand x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EmacsModeCommand -> Rep EmacsModeCommand x
from :: forall x. EmacsModeCommand -> Rep EmacsModeCommand x
$cto :: forall x. Rep EmacsModeCommand x -> EmacsModeCommand
to :: forall x. Rep EmacsModeCommand x -> EmacsModeCommand
Generic)

-- | Infective or coinfective?
data InfectiveCoinfective
  = Infective
  | Coinfective
  deriving (InfectiveCoinfective -> InfectiveCoinfective -> Bool
(InfectiveCoinfective -> InfectiveCoinfective -> Bool)
-> (InfectiveCoinfective -> InfectiveCoinfective -> Bool)
-> Eq InfectiveCoinfective
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
$c/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
Eq, Int -> InfectiveCoinfective -> ShowS
[InfectiveCoinfective] -> ShowS
InfectiveCoinfective -> FilePath
(Int -> InfectiveCoinfective -> ShowS)
-> (InfectiveCoinfective -> FilePath)
-> ([InfectiveCoinfective] -> ShowS)
-> Show InfectiveCoinfective
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InfectiveCoinfective -> ShowS
showsPrec :: Int -> InfectiveCoinfective -> ShowS
$cshow :: InfectiveCoinfective -> FilePath
show :: InfectiveCoinfective -> FilePath
$cshowList :: [InfectiveCoinfective] -> ShowS
showList :: [InfectiveCoinfective] -> ShowS
Show, (forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x)
-> (forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective)
-> Generic InfectiveCoinfective
forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
from :: forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
$cto :: forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
to :: forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
Generic)

-- | Options @--version@ and @--numeric-version@ (last wins).
data PrintVersion
  = PrintVersion
      -- ^ Print version information.
  | PrintNumericVersion
      -- ^ Print version number.
  deriving (Int -> PrintVersion -> ShowS
[PrintVersion] -> ShowS
PrintVersion -> FilePath
(Int -> PrintVersion -> ShowS)
-> (PrintVersion -> FilePath)
-> ([PrintVersion] -> ShowS)
-> Show PrintVersion
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PrintVersion -> ShowS
showsPrec :: Int -> PrintVersion -> ShowS
$cshow :: PrintVersion -> FilePath
show :: PrintVersion -> FilePath
$cshowList :: [PrintVersion] -> ShowS
showList :: [PrintVersion] -> ShowS
Show, (forall x. PrintVersion -> Rep PrintVersion x)
-> (forall x. Rep PrintVersion x -> PrintVersion)
-> Generic PrintVersion
forall x. Rep PrintVersion x -> PrintVersion
forall x. PrintVersion -> Rep PrintVersion x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrintVersion -> Rep PrintVersion x
from :: forall x. PrintVersion -> Rep PrintVersion x
$cto :: forall x. Rep PrintVersion x -> PrintVersion
to :: forall x. Rep PrintVersion x -> PrintVersion
Generic)

type VerboseKey     = String
type VerboseKeyItem = String1
type VerboseLevel   = Int

-- | 'Strict.Nothing' is used if no verbosity options have been given,
-- thus making it possible to handle the default case relatively
-- quickly. Note that 'Strict.Nothing' corresponds to a trie with
-- verbosity level 1 for the empty path.
type Verbosity = Strict.Maybe (Trie VerboseKeyItem VerboseLevel)

---------------------------------------------------------------------------
-- * Lenses

class LensPragmaOptions a where
  getPragmaOptions  :: a -> PragmaOptions
  setPragmaOptions  :: PragmaOptions -> a -> a
  mapPragmaOptions  :: (PragmaOptions -> PragmaOptions) -> a -> a
  lensPragmaOptions :: Lens' a PragmaOptions

  {-# MINIMAL lensPragmaOptions #-}
  getPragmaOptions = (a -> Getting PragmaOptions a PragmaOptions -> PragmaOptions
forall s a. s -> Getting a s a -> a
^. Getting PragmaOptions a PragmaOptions
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' a PragmaOptions
lensPragmaOptions)
  setPragmaOptions = (PragmaOptions -> PragmaOptions) -> a -> a
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions) -> a -> a)
-> (PragmaOptions -> PragmaOptions -> PragmaOptions)
-> PragmaOptions
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> PragmaOptions -> PragmaOptions
forall a b. a -> b -> a
const
  mapPragmaOptions = ASetter a a PragmaOptions PragmaOptions
-> (PragmaOptions -> PragmaOptions) -> a -> a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter a a PragmaOptions PragmaOptions
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' a PragmaOptions
lensPragmaOptions

instance LensPragmaOptions CommandLineOptions where
  lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) f PragmaOptions
-> (PragmaOptions -> CommandLineOptions) -> f CommandLineOptions
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions = opts }

---------------------------------------------------------------------------
-- NFData instances

instance NFData CommandLineOptions
instance NFData PragmaOptions

instance NFData Parallelism
instance NFData DiagnosticsColours
instance NFData EmacsModeCommand
instance NFData InfectiveCoinfective
instance NFData PrintVersion