    {-# LANGUAGE DataKinds #-}

    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | A module defining the types exported by "Agda.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 Agda.Interaction.Options.Types where

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

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

    import           Agda.Utils.FileName               ( AbsolutePath )
    import           Agda.Utils.Lens                   ( Lens', (^.), over )
    import           Agda.Utils.List1                  ( String1 )
    import qualified Agda.Utils.Maybe.Strict           as Strict
    import           Agda.Utils.ProfileOptions         ( ProfileOptions )
    import           Agda.Utils.Trie                   ( Trie )
    import           Agda.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 -> String
    optProgramName           :: String
      , CommandLineOptions -> Maybe String
    optInputFile             :: Maybe FilePath
      , CommandLineOptions -> [String]
    optIncludePaths          :: [FilePath]
      , CommandLineOptions -> [AbsolutePath]
    optAbsoluteIncludePaths  :: [AbsolutePath]
          -- ^ The list should not contain duplicates.
      , CommandLineOptions -> [LibName]
    optLibraries             :: [LibName]
      , CommandLineOptions -> Maybe String
    optOverrideLibrariesFile :: Maybe FilePath
          -- ^ Use this (if 'Just') instead of @~\/.agda\/libraries@.
      , CommandLineOptions -> Bool
    optDefaultLibs           :: Bool
           -- ^ Use @~\/.agda\/defaults@.
      , CommandLineOptions -> Bool
    optUseLibs               :: Bool
           -- ^ look for @.agda-lib@ files.
      , CommandLineOptions -> Integer
    optTraceImports          :: Integer
           -- ^ Configure notifications about imported modules.
      , CommandLineOptions -> Map ExeName String
    optTrustedExecutables    :: Map ExeName FilePath
           -- ^ Map names of trusted executables to absolute paths.

      -- Setup and printing
      , CommandLineOptions -> Bool
    optPrintAgdaDataDir      :: Bool
      , CommandLineOptions -> Bool
    optPrintAgdaAppDir       :: Bool
      , CommandLineOptions -> Maybe PrintAgdaVersion
    optPrintVersion          :: Maybe PrintAgdaVersion
      , CommandLineOptions -> Maybe Help
    optPrintHelp             :: Maybe Help
      , CommandLineOptions -> Bool
    optBuildLibrary          :: Bool
          -- ^ @--build-library@: Build all modules in the current library.
      , CommandLineOptions -> Bool
    optSetup                 :: Bool
          -- ^ Force Agda to 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
    optInteractive           :: Bool
          -- ^ Agda REPL (@-I@).
      , CommandLineOptions -> Bool
    optGHCiInteraction       :: Bool
          -- ^ @--interaction@ mode.
      , CommandLineOptions -> Bool
    optJSONInteraction       :: Bool
          -- ^ @--interaction-json@ mode.
      , CommandLineOptions -> Bool
    optExitOnError           :: !Bool
          -- ^ Exit if an interactive command fails.
      , CommandLineOptions -> Maybe String
    optCompileDir            :: Maybe FilePath
          -- ^ In the absence of a path the project root is used.
      , CommandLineOptions -> Bool
    optGenerateVimFile       :: Bool
      , CommandLineOptions -> Bool
    optIgnoreInterfaces      :: Bool
      , CommandLineOptions -> Bool
    optIgnoreAllInterfaces   :: 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.
      }
      deriving (Int -> CommandLineOptions -> ShowS
    [CommandLineOptions] -> ShowS
    CommandLineOptions -> String
    (Int -> CommandLineOptions -> ShowS)
    -> (CommandLineOptions -> String)
    -> ([CommandLineOptions] -> ShowS)
    -> Show CommandLineOptions
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CommandLineOptions -> ShowS
    showsPrec :: Int -> CommandLineOptions -> ShowS
    $cshow :: CommandLineOptions -> String
    show :: CommandLineOptions -> String
    $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
    _optTwoLevel                  :: 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
    _optUniverseCheck             :: WithDefault 'True
      , PragmaOptions -> WithDefault 'False
    _optOmegaInOmega              :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    _optCumulativity              :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    _optSizedTypes                :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    _optGuardedness               :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    _optInjectiveTypeConstructors :: WithDefault 'False
      , PragmaOptions -> WithDefault 'True
    _optUniversePolymorphism      :: WithDefault 'True
      , PragmaOptions -> WithDefault 'False
    _optIrrelevantProjections     :: WithDefault 'False
          -- off by default in > 2.5.4, see issue #2170
      , PragmaOptions -> WithDefault 'False
    _optExperimentalIrrelevance   :: WithDefault 'False
          -- ^ irrelevant levels, irrelevant data matching
      , PragmaOptions -> WithDefault 'False
    _optWithoutK                  :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    _optCubicalCompatible         :: WithDefault 'False
      , 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
    _optErasure                   :: WithDefault 'False
      , PragmaOptions -> WithDefault 'True
    _optErasedMatches             :: WithDefault 'True
          -- ^ Allow matching in erased positions for single-constructor,
          -- non-indexed data/record types. (This kind of matching is always
          -- allowed for record types with η-equality.)
      , PragmaOptions -> WithDefault 'False
    _optEraseRecordParameters     :: WithDefault 'False
          -- ^ Mark parameters of record modules as erased?
      , PragmaOptions -> WithDefault 'False
    _optRewriting                 :: WithDefault 'False
          -- ^ Can rewrite rules be added and used?
      , PragmaOptions -> Maybe Cubical
    _optCubical                   :: Maybe Cubical
      , PragmaOptions -> WithDefault 'False
    _optGuarded                   :: WithDefault 'False
      , 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 -> Maybe Int
    _optSyntacticEquality         :: !(Strict.Maybe Int)
          -- ^ Should the conversion checker use the syntactic equality shortcut?
          -- 'Nothing' means that it should.
          -- @'Just' n@, for a non-negative number @n@, means that syntactic equality
          -- checking gets @n@ units of fuel.
          -- If the fuel becomes zero, then syntactic equality checking is turned off.
          -- The fuel counter is decreased in the failure continuation of
          -- 'Agda.TypeChecking.SyntacticEquality.checkSyntacticEquality'.
      , 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 Agda abstract machine ('fastReduce')?
      , PragmaOptions -> WithDefault 'False
    _optCallByName                :: WithDefault 'False
          -- ^ Use call-by-name instead of call-by-need.
      , PragmaOptions -> Maybe ConfluenceCheck
    _optConfluenceCheck           :: Maybe ConfluenceCheck
          -- ^ Check confluence of rewrite rules?
      , PragmaOptions -> WithDefault 'False
    _optCohesion                  :: WithDefault 'False
          -- ^ Are the cohesion modalities available?
      , PragmaOptions -> WithDefault 'False
    _optFlatSplit                 :: WithDefault 'False
          -- ^ Can we split on a @(\@flat x : A)@ argument?
      , PragmaOptions -> WithDefault 'False
    _optPolarity                  :: WithDefault 'False
          -- ^ Can we use modal polarities (@++, @+, etc.)?
      , PragmaOptions -> WithDefault 'True
    _optImportSorts               :: WithDefault 'True
          -- ^ Should every top-level module start with an implicit statement
          --   @open import Agda.Primitive using (Set; 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
    _optLargeIndices              :: WithDefault 'False
          -- ^ Allow large indices, and large forced arguments in
          -- constructors.
      , PragmaOptions -> WithDefault 'True
    _optForcedArgumentRecursion   :: WithDefault 'True
          -- ^ Allow recursion on forced constructor arguments.
      , PragmaOptions -> WithDefault 'False
    _optExperimentalLazyInstances :: WithDefault 'False
          -- ^ Defer instance search based on discrimination tree results
      }
      deriving (Int -> PragmaOptions -> ShowS
    [PragmaOptions] -> ShowS
    PragmaOptions -> String
    (Int -> PragmaOptions -> ShowS)
    -> (PragmaOptions -> String)
    -> ([PragmaOptions] -> ShowS)
    -> Show PragmaOptions
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PragmaOptions -> ShowS
    showsPrec :: Int -> PragmaOptions -> ShowS
    $cshow :: PragmaOptions -> String
    show :: PragmaOptions -> String
    $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 ConfluenceCheck
      = LocalConfluenceCheck
      | GlobalConfluenceCheck
      deriving (Int -> ConfluenceCheck -> ShowS
    [ConfluenceCheck] -> ShowS
    ConfluenceCheck -> String
    (Int -> ConfluenceCheck -> ShowS)
    -> (ConfluenceCheck -> String)
    -> ([ConfluenceCheck] -> ShowS)
    -> Show ConfluenceCheck
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ConfluenceCheck -> ShowS
    showsPrec :: Int -> ConfluenceCheck -> ShowS
    $cshow :: ConfluenceCheck -> String
    show :: ConfluenceCheck -> String
    $cshowList :: [ConfluenceCheck] -> ShowS
    showList :: [ConfluenceCheck] -> ShowS
    Show, ConfluenceCheck -> ConfluenceCheck -> Bool
    (ConfluenceCheck -> ConfluenceCheck -> Bool)
    -> (ConfluenceCheck -> ConfluenceCheck -> Bool)
    -> Eq ConfluenceCheck
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ConfluenceCheck -> ConfluenceCheck -> Bool
    == :: ConfluenceCheck -> ConfluenceCheck -> Bool
    $c/= :: ConfluenceCheck -> ConfluenceCheck -> Bool
    /= :: ConfluenceCheck -> ConfluenceCheck -> Bool
    Eq, (forall x. ConfluenceCheck -> Rep ConfluenceCheck x)
    -> (forall x. Rep ConfluenceCheck x -> ConfluenceCheck)
    -> Generic ConfluenceCheck
    forall x. Rep ConfluenceCheck x -> ConfluenceCheck
    forall x. ConfluenceCheck -> Rep ConfluenceCheck x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ConfluenceCheck -> Rep ConfluenceCheck x
    from :: forall x. ConfluenceCheck -> Rep ConfluenceCheck x
    $cto :: forall x. Rep ConfluenceCheck x -> ConfluenceCheck
    to :: forall x. Rep ConfluenceCheck x -> ConfluenceCheck
    Generic)

    data DiagnosticsColours
      = AlwaysColour
      | NeverColour
      | AutoColour
      deriving (Int -> DiagnosticsColours -> ShowS
    [DiagnosticsColours] -> ShowS
    DiagnosticsColours -> String
    (Int -> DiagnosticsColours -> ShowS)
    -> (DiagnosticsColours -> String)
    -> ([DiagnosticsColours] -> ShowS)
    -> Show DiagnosticsColours
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DiagnosticsColours -> ShowS
    showsPrec :: Int -> DiagnosticsColours -> ShowS
    $cshow :: DiagnosticsColours -> String
    show :: DiagnosticsColours -> String
    $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)

    -- | 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 -> String
    (Int -> EmacsModeCommand -> ShowS)
    -> (EmacsModeCommand -> String)
    -> ([EmacsModeCommand] -> ShowS)
    -> Show EmacsModeCommand
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> EmacsModeCommand -> ShowS
    showsPrec :: Int -> EmacsModeCommand -> ShowS
    $cshow :: EmacsModeCommand -> String
    show :: EmacsModeCommand -> String
    $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 -> String
    (Int -> InfectiveCoinfective -> ShowS)
    -> (InfectiveCoinfective -> String)
    -> ([InfectiveCoinfective] -> ShowS)
    -> Show InfectiveCoinfective
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> InfectiveCoinfective -> ShowS
    showsPrec :: Int -> InfectiveCoinfective -> ShowS
    $cshow :: InfectiveCoinfective -> String
    show :: InfectiveCoinfective -> String
    $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 PrintAgdaVersion
      = PrintAgdaVersion
          -- ^ Print Agda version information.
      | PrintAgdaNumericVersion
          -- ^ Print Agda version number.
      deriving (Int -> PrintAgdaVersion -> ShowS
    [PrintAgdaVersion] -> ShowS
    PrintAgdaVersion -> String
    (Int -> PrintAgdaVersion -> ShowS)
    -> (PrintAgdaVersion -> String)
    -> ([PrintAgdaVersion] -> ShowS)
    -> Show PrintAgdaVersion
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PrintAgdaVersion -> ShowS
    showsPrec :: Int -> PrintAgdaVersion -> ShowS
    $cshow :: PrintAgdaVersion -> String
    show :: PrintAgdaVersion -> String
    $cshowList :: [PrintAgdaVersion] -> ShowS
    showList :: [PrintAgdaVersion] -> ShowS
    Show, (forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x)
    -> (forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion)
    -> Generic PrintAgdaVersion
    forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion
    forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x
    from :: forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x
    $cto :: forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion
    to :: forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion
    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 -> Lens' a PragmaOptions -> PragmaOptions
    forall o i. o -> Lens' o i -> i
    ^. (PragmaOptions -> f PragmaOptions) -> a -> f a
    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 = Lens' a PragmaOptions -> (PragmaOptions -> PragmaOptions) -> a -> a
    forall o i. Lens' o i -> LensMap o i
    over (PragmaOptions -> f PragmaOptions) -> a -> f a
    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 ConfluenceCheck
    instance NFData DiagnosticsColours
    instance NFData EmacsModeCommand
    instance NFData InfectiveCoinfective
    instance NFData PrintAgdaVersion