    {-# LANGUAGE CPP       #-}
    {-# LANGUAGE DataKinds #-}

    module Agda.Interaction.Options.Base
        ( CommandLineOptions(..)
        , PragmaOptions(..)
        , OptionsPragma
        , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
        , Verbosity, VerboseKey, VerboseLevel
        , WarningMode(..)
        , ConfluenceCheck(..)
        , UnicodeOrAscii(..)
        , checkOpts
        , parsePragmaOptions
        , parsePluginOptions
        , stripRTS
        , defaultOptions
        , defaultInteractionOptions
        , defaultVerbosity
        , defaultCutOff
        , defaultPragmaOptions
        , standardOptions_
        , unsafePragmaOptions
        , restartOptions
        , infectiveOptions
        , coinfectiveOptions
        , safeFlag
        , mapFlag
        , usage
        -- Reused by PandocAgda
        , inputFlag
        , standardOptions, deadStandardOptions
        , getOptSimple
        ) where

    import Control.DeepSeq
    import Control.Monad ( when, void )
    import Control.Monad.Except ( Except, MonadError(throwError), runExcept )

    import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)
    import Data.Maybe
    import Data.Map                 ( Map )
    import qualified Data.Map as Map
    import Data.List                ( intercalate )
    import qualified Data.Set as Set

    import GHC.Generics (Generic)

    import System.Console.GetOpt    ( getOpt', usageInfo, ArgOrder(ReturnInOrder)
                                    , OptDescr(..), ArgDescr(..)
                                    )
    import Text.EditDistance
    import Text.Read                ( readMaybe )

    import Agda.Termination.CutOff  ( CutOff(..), defaultCutOff )

    import Agda.Interaction.Library ( ExeName, LibName )
    import Agda.Interaction.Options.Help
      ( Help(HelpFor, GeneralHelp)
      , string2HelpTopic
      , allHelpTopics
      , helpTopicUsage
      )
    import Agda.Interaction.Options.Warnings
    import Agda.Syntax.Concrete.Glyph ( unsafeSetUnicodeOrAscii, UnicodeOrAscii(..) )
    import Agda.Syntax.Common (Cubical(..))

    import Agda.Utils.FileName      ( AbsolutePath )
    import Agda.Utils.Functor       ( (<&>) )
    import Agda.Utils.Lens          ( Lens', over )
    import Agda.Utils.List          ( groupOn, initLast1, wordsBy )
    import Agda.Utils.Pretty        ( singPlural )
    import Agda.Utils.Trie          ( Trie )
    import qualified Agda.Utils.Trie as Trie
    import Agda.Utils.WithDefault

    import Agda.Version

    -- OptDescr is a Functor --------------------------------------------------

    type VerboseKey   = String
    type VerboseLevel = Int
    type Verbosity    = Trie VerboseKey VerboseLevel

    -- 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 -> [String]
    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 -> Map ExeName String
    optTrustedExecutables             :: Map ExeName FilePath
      -- ^ Map names of trusted executables to absolute paths
      , CommandLineOptions -> Bool
    optPrintAgdaDir          :: Bool
      , CommandLineOptions -> Bool
    optPrintVersion          :: Bool
      , CommandLineOptions -> Maybe Help
    optPrintHelp             :: Maybe Help
      , CommandLineOptions -> Bool
    optInteractive           :: Bool
          -- ^ Agda REPL (-I).
      , CommandLineOptions -> Bool
    optGHCiInteraction       :: Bool
      , CommandLineOptions -> Bool
    optJSONInteraction       :: Bool
      , CommandLineOptions -> Bool
    optOptimSmashing         :: Bool
      , 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 -> Bool
    optLocalInterfaces       :: Bool
      , CommandLineOptions -> PragmaOptions
    optPragmaOptions         :: PragmaOptions
      , CommandLineOptions -> Bool
    optOnlyScopeChecking     :: Bool
        -- ^ Should the top-level module only be scope-checked, and not
        --   type-checked?
      }
      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
    showList :: [CommandLineOptions] -> ShowS
    $cshowList :: [CommandLineOptions] -> ShowS
    show :: CommandLineOptions -> String
    $cshow :: CommandLineOptions -> String
    showsPrec :: Int -> CommandLineOptions -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep CommandLineOptions x -> CommandLineOptions
    $cfrom :: forall x. CommandLineOptions -> Rep CommandLineOptions x
    Generic)

    instance NFData CommandLineOptions

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

    data PragmaOptions = PragmaOptions
      { PragmaOptions -> Bool
    optShowImplicit              :: Bool
      , PragmaOptions -> Bool
    optShowIrrelevant            :: Bool
      , PragmaOptions -> UnicodeOrAscii
    optUseUnicode                :: UnicodeOrAscii
      , PragmaOptions -> Verbosity
    optVerbose                   :: Verbosity
      , PragmaOptions -> Bool
    optProp                      :: Bool
      , PragmaOptions -> WithDefault 'False
    optTwoLevel                  :: WithDefault 'False
      , PragmaOptions -> Bool
    optAllowUnsolved             :: Bool
      , PragmaOptions -> Bool
    optAllowIncompleteMatch      :: Bool
      , PragmaOptions -> Bool
    optDisablePositivity         :: Bool
      , PragmaOptions -> Bool
    optTerminationCheck          :: Bool
      , PragmaOptions -> CutOff
    optTerminationDepth          :: CutOff
        -- ^ Cut off structural order comparison at some depth in termination checker?
      , PragmaOptions -> Bool
    optCompletenessCheck         :: Bool
      , PragmaOptions -> Bool
    optUniverseCheck             :: Bool
      , PragmaOptions -> Bool
    optOmegaInOmega              :: Bool
      , PragmaOptions -> WithDefault 'False
    optSubtyping                 :: WithDefault 'False
      , PragmaOptions -> Bool
    optCumulativity              :: Bool
      , PragmaOptions -> WithDefault 'False
    optSizedTypes                :: WithDefault 'False
      , PragmaOptions -> WithDefault 'False
    optGuardedness               :: WithDefault 'False
      , PragmaOptions -> Bool
    optInjectiveTypeConstructors :: Bool
      , PragmaOptions -> Bool
    optUniversePolymorphism      :: Bool
      , PragmaOptions -> Bool
    optIrrelevantProjections     :: Bool
      , PragmaOptions -> Bool
    optExperimentalIrrelevance   :: Bool  -- ^ irrelevant levels, irrelevant data matching
      , PragmaOptions -> WithDefault 'False
    optWithoutK                  :: WithDefault 'False
      , PragmaOptions -> Bool
    optCopatterns                :: Bool  -- ^ Allow definitions by copattern matching?
      , PragmaOptions -> Bool
    optPatternMatching           :: Bool  -- ^ Is pattern matching allowed in the current file?
      , PragmaOptions -> Bool
    optExactSplit                :: Bool
      , PragmaOptions -> Bool
    optEta                       :: Bool
      , PragmaOptions -> Bool
    optForcing                   :: Bool  -- ^ Perform the forcing analysis on data constructors?
      , PragmaOptions -> Bool
    optProjectionLike            :: Bool  -- ^ Perform the projection-likeness analysis on functions?
      , PragmaOptions -> Bool
    optRewriting                 :: Bool  -- ^ Can rewrite rules be added and used?
      , PragmaOptions -> Maybe Cubical
    optCubical                   :: Maybe Cubical
      , PragmaOptions -> Bool
    optGuarded                   :: Bool
      , PragmaOptions -> Bool
    optFirstOrder                :: Bool  -- ^ Should we speculatively unify function applications as if they were injective?
      , PragmaOptions -> Bool
    optPostfixProjections        :: Bool
          -- ^ Should system generated projections 'ProjSystem' be printed
          --   postfix (True) or prefix (False).
      , PragmaOptions -> Bool
    optKeepPatternVariables      :: Bool
          -- ^ Should case splitting replace variables with dot patterns
          --   (False) or keep them as variables (True).
      , PragmaOptions -> Int
    optInstanceSearchDepth       :: Int
      , PragmaOptions -> Bool
    optOverlappingInstances      :: Bool
      , PragmaOptions -> Bool
    optQualifiedInstances        :: Bool  -- ^ Should instance search consider instances with qualified names?
      , PragmaOptions -> Int
    optInversionMaxDepth         :: Int
      , PragmaOptions -> Bool
    optSafe                      :: Bool
      , PragmaOptions -> Bool
    optDoubleCheck               :: Bool
      , PragmaOptions -> Bool
    optSyntacticEquality         :: Bool  -- ^ Should conversion checker use syntactic equality shortcut?
      , PragmaOptions -> WarningMode
    optWarningMode               :: WarningMode
      , PragmaOptions -> Bool
    optCompileNoMain             :: Bool
      , PragmaOptions -> Bool
    optCaching                   :: Bool
      , PragmaOptions -> Bool
    optCountClusters             :: Bool
        -- ^ Count extended grapheme clusters rather than code points when
        -- generating LaTeX.
      , PragmaOptions -> Bool
    optAutoInline                :: Bool
        -- ^ Automatic compile-time inlining for simple definitions (unless marked
        --   NOINLINE).
      , PragmaOptions -> Bool
    optPrintPatternSynonyms      :: Bool
      , PragmaOptions -> Bool
    optFastReduce                :: Bool
        -- ^ Use the Agda abstract machine (fastReduce)?
      , PragmaOptions -> Bool
    optCallByName                :: Bool
        -- ^ Use call-by-name instead of call-by-need
      , PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck           :: Maybe ConfluenceCheck
        -- ^ Check confluence of rewrite rules?
      , PragmaOptions -> Bool
    optFlatSplit                 :: Bool
         -- ^ Can we split on a (@flat x : A) argument?
      , PragmaOptions -> Bool
    optImportSorts               :: Bool
         -- ^ Should every top-level module start with an implicit statement
         --   @open import Agda.Primitive using (Set; Prop)@?
      , PragmaOptions -> Bool
    optAllowExec                 :: Bool
      , PragmaOptions -> Bool
    optShowIdentitySubstitutions :: Bool
        -- ^ Show identity substitutions when pretty-printing terms
        --   (i.e. always show all arguments of a metavariable)
      }
      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
    showList :: [PragmaOptions] -> ShowS
    $cshowList :: [PragmaOptions] -> ShowS
    show :: PragmaOptions -> String
    $cshow :: PragmaOptions -> String
    showsPrec :: Int -> PragmaOptions -> ShowS
    $cshowsPrec :: Int -> PragmaOptions -> ShowS
    Show, PragmaOptions -> PragmaOptions -> Bool
    (PragmaOptions -> PragmaOptions -> Bool)
    -> (PragmaOptions -> PragmaOptions -> Bool) -> Eq PragmaOptions
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: PragmaOptions -> PragmaOptions -> Bool
    $c/= :: PragmaOptions -> PragmaOptions -> Bool
    == :: PragmaOptions -> PragmaOptions -> Bool
    $c== :: 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
    $cto :: forall x. Rep PragmaOptions x -> PragmaOptions
    $cfrom :: forall x. PragmaOptions -> Rep PragmaOptions x
    Generic)

    instance NFData PragmaOptions

    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
    showList :: [ConfluenceCheck] -> ShowS
    $cshowList :: [ConfluenceCheck] -> ShowS
    show :: ConfluenceCheck -> String
    $cshow :: ConfluenceCheck -> String
    showsPrec :: Int -> ConfluenceCheck -> ShowS
    $cshowsPrec :: Int -> ConfluenceCheck -> ShowS
    Show, ConfluenceCheck -> ConfluenceCheck -> Bool
    (ConfluenceCheck -> ConfluenceCheck -> Bool)
    -> (ConfluenceCheck -> ConfluenceCheck -> Bool)
    -> Eq ConfluenceCheck
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: ConfluenceCheck -> ConfluenceCheck -> Bool
    $c/= :: ConfluenceCheck -> ConfluenceCheck -> Bool
    == :: ConfluenceCheck -> ConfluenceCheck -> Bool
    $c== :: 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
    $cto :: forall x. Rep ConfluenceCheck x -> ConfluenceCheck
    $cfrom :: forall x. ConfluenceCheck -> Rep ConfluenceCheck x
    Generic)

    instance NFData ConfluenceCheck

    -- | The options from an @OPTIONS@ pragma.
    --
    -- In the future it might be nice to switch to a more structured
    -- representation. Note that, currently, there is not a one-to-one
    -- correspondence between list elements and options.
    type OptionsPragma = [String]

    -- | Map a function over the long options. Also removes the short options.
    --   Will be used to add the plugin name to the plugin options.
    mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
    mapFlag :: forall a. ShowS -> OptDescr a -> OptDescr a
    mapFlag ShowS
    f (Option String
    _ [String]
    long ArgDescr a
    arg String
    descr) = String -> [String] -> ArgDescr a -> String -> OptDescr a
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] (ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ShowS
    f [String]
    long) ArgDescr a
    arg String
    descr

    defaultVerbosity :: Verbosity
    defaultVerbosity :: Verbosity
    defaultVerbosity = [String] -> Int -> Verbosity
    forall k v. [k] -> v -> Trie k v
    Trie.singleton [] Int
    1

    defaultInteractionOptions :: PragmaOptions
    defaultInteractionOptions :: PragmaOptions
    defaultInteractionOptions = PragmaOptions
    defaultPragmaOptions

    defaultOptions :: CommandLineOptions
    defaultOptions :: CommandLineOptions
    defaultOptions = Options :: String
    -> Maybe String
    -> [String]
    -> [AbsolutePath]
    -> [String]
    -> Maybe String
    -> Bool
    -> Bool
    -> Map ExeName String
    -> Bool
    -> Bool
    -> Maybe Help
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Maybe String
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> PragmaOptions
    -> Bool
    -> CommandLineOptions
    Options
      { optProgramName :: String
    optProgramName      = String
    "agda"
      , optInputFile :: Maybe String
    optInputFile             = Maybe String
    forall a. Maybe a
    Nothing
      , optIncludePaths :: [String]
    optIncludePaths          = []
      , optAbsoluteIncludePaths :: [AbsolutePath]
    optAbsoluteIncludePaths  = []
      , optLibraries :: [String]
    optLibraries             = []
      , optOverrideLibrariesFile :: Maybe String
    optOverrideLibrariesFile = Maybe String
    forall a. Maybe a
    Nothing
      , optDefaultLibs :: Bool
    optDefaultLibs           = Bool
    True
      , optUseLibs :: Bool
    optUseLibs               = Bool
    True
      , optTrustedExecutables :: Map ExeName String
    optTrustedExecutables    = Map ExeName String
    forall k a. Map k a
    Map.empty
      , optPrintAgdaDir :: Bool
    optPrintAgdaDir          = Bool
    False
      , optPrintVersion :: Bool
    optPrintVersion          = Bool
    False
      , optPrintHelp :: Maybe Help
    optPrintHelp             = Maybe Help
    forall a. Maybe a
    Nothing
      , optInteractive :: Bool
    optInteractive           = Bool
    False
      , optGHCiInteraction :: Bool
    optGHCiInteraction       = Bool
    False
      , optJSONInteraction :: Bool
    optJSONInteraction       = Bool
    False
      , optOptimSmashing :: Bool
    optOptimSmashing         = Bool
    True
      , optCompileDir :: Maybe String
    optCompileDir            = Maybe String
    forall a. Maybe a
    Nothing
      , optGenerateVimFile :: Bool
    optGenerateVimFile       = Bool
    False
      , optIgnoreInterfaces :: Bool
    optIgnoreInterfaces      = Bool
    False
      , optIgnoreAllInterfaces :: Bool
    optIgnoreAllInterfaces   = Bool
    False
      , optLocalInterfaces :: Bool
    optLocalInterfaces       = Bool
    False
      , optPragmaOptions :: PragmaOptions
    optPragmaOptions         = PragmaOptions
    defaultPragmaOptions
      , optOnlyScopeChecking :: Bool
    optOnlyScopeChecking     = Bool
    False
      }

    defaultPragmaOptions :: PragmaOptions
    defaultPragmaOptions :: PragmaOptions
    defaultPragmaOptions = PragmaOptions :: Bool
    -> Bool
    -> UnicodeOrAscii
    -> Verbosity
    -> Bool
    -> WithDefault 'False
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> CutOff
    -> Bool
    -> Bool
    -> Bool
    -> WithDefault 'False
    -> Bool
    -> WithDefault 'False
    -> WithDefault 'False
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> WithDefault 'False
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Maybe Cubical
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Int
    -> Bool
    -> Bool
    -> Int
    -> Bool
    -> Bool
    -> Bool
    -> WarningMode
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> Maybe ConfluenceCheck
    -> Bool
    -> Bool
    -> Bool
    -> Bool
    -> PragmaOptions
    PragmaOptions
      { optShowImplicit :: Bool
    optShowImplicit              = Bool
    False
      , optShowIrrelevant :: Bool
    optShowIrrelevant            = Bool
    False
      , optUseUnicode :: UnicodeOrAscii
    optUseUnicode                = UnicodeOrAscii
    UnicodeOk
      , optVerbose :: Verbosity
    optVerbose                   = Verbosity
    defaultVerbosity
      , optProp :: Bool
    optProp                      = Bool
    False
      , optTwoLevel :: WithDefault 'False
    optTwoLevel                  = WithDefault 'False
    forall (b :: Bool). WithDefault b
    Default
      , optExperimentalIrrelevance :: Bool
    optExperimentalIrrelevance   = Bool
    False
      , optIrrelevantProjections :: Bool
    optIrrelevantProjections     = Bool
    False -- off by default in > 2.5.4, see issue #2170
      , optAllowUnsolved :: Bool
    optAllowUnsolved             = Bool
    False
      , optAllowIncompleteMatch :: Bool
    optAllowIncompleteMatch      = Bool
    False
      , optDisablePositivity :: Bool
    optDisablePositivity         = Bool
    False
      , optTerminationCheck :: Bool
    optTerminationCheck          = Bool
    True
      , optTerminationDepth :: CutOff
    optTerminationDepth          = CutOff
    defaultCutOff
      , optCompletenessCheck :: Bool
    optCompletenessCheck         = Bool
    True
      , optUniverseCheck :: Bool
    optUniverseCheck             = Bool
    True
      , optOmegaInOmega :: Bool
    optOmegaInOmega              = Bool
    False
      , optSubtyping :: WithDefault 'False
    optSubtyping                 = WithDefault 'False
    forall (b :: Bool). WithDefault b
    Default
      , optCumulativity :: Bool
    optCumulativity              = Bool
    False
      , optSizedTypes :: WithDefault 'False
    optSizedTypes                = WithDefault 'False
    forall (b :: Bool). WithDefault b
    Default
      , optGuardedness :: WithDefault 'False
    optGuardedness               = WithDefault 'False
    forall (b :: Bool). WithDefault b
    Default
      , optInjectiveTypeConstructors :: Bool
    optInjectiveTypeConstructors = Bool
    False
      , optUniversePolymorphism :: Bool
    optUniversePolymorphism      = Bool
    True
      , optWithoutK :: WithDefault 'False
    optWithoutK                  = WithDefault 'False
    forall (b :: Bool). WithDefault b
    Default
      , optCopatterns :: Bool
    optCopatterns                = Bool
    True
      , optPatternMatching :: Bool
    optPatternMatching           = Bool
    True
      , optExactSplit :: Bool
    optExactSplit                = Bool
    False
      , optEta :: Bool
    optEta                       = Bool
    True
      , optForcing :: Bool
    optForcing                   = Bool
    True
      , optProjectionLike :: Bool
    optProjectionLike            = Bool
    True
      , optRewriting :: Bool
    optRewriting                 = Bool
    False
      , optCubical :: Maybe Cubical
    optCubical                   = Maybe Cubical
    forall a. Maybe a
    Nothing
      , optGuarded :: Bool
    optGuarded                   = Bool
    False
      , optFirstOrder :: Bool
    optFirstOrder                = Bool
    False
      , optPostfixProjections :: Bool
    optPostfixProjections        = Bool
    False
      , optKeepPatternVariables :: Bool
    optKeepPatternVariables      = Bool
    False
      , optInstanceSearchDepth :: Int
    optInstanceSearchDepth       = Int
    500
      , optOverlappingInstances :: Bool
    optOverlappingInstances      = Bool
    False
      , optQualifiedInstances :: Bool
    optQualifiedInstances        = Bool
    True
      , optInversionMaxDepth :: Int
    optInversionMaxDepth         = Int
    50
      , optSafe :: Bool
    optSafe                      = Bool
    False
      , optDoubleCheck :: Bool
    optDoubleCheck               = Bool
    False
      , optSyntacticEquality :: Bool
    optSyntacticEquality         = Bool
    True
      , optWarningMode :: WarningMode
    optWarningMode               = WarningMode
    defaultWarningMode
      , optCompileNoMain :: Bool
    optCompileNoMain             = Bool
    False
      , optCaching :: Bool
    optCaching                   = Bool
    True
      , optCountClusters :: Bool
    optCountClusters             = Bool
    False
      , optAutoInline :: Bool
    optAutoInline                = Bool
    False
      , optPrintPatternSynonyms :: Bool
    optPrintPatternSynonyms      = Bool
    True
      , optFastReduce :: Bool
    optFastReduce                = Bool
    True
      , optCallByName :: Bool
    optCallByName                = Bool
    False
      , optConfluenceCheck :: Maybe ConfluenceCheck
    optConfluenceCheck           = Maybe ConfluenceCheck
    forall a. Maybe a
    Nothing
      , optFlatSplit :: Bool
    optFlatSplit                 = Bool
    True
      , optImportSorts :: Bool
    optImportSorts               = Bool
    True
      , optAllowExec :: Bool
    optAllowExec                 = Bool
    False
      , optShowIdentitySubstitutions :: Bool
    optShowIdentitySubstitutions = Bool
    False
      }

    type OptM = Except String

    runOptM :: Monad m => OptM opts -> m (Either String opts)
    runOptM :: forall (m :: * -> *) opts.
    Monad m =>
    OptM opts -> m (Either String opts)
    runOptM = Either String opts -> m (Either String opts)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either String opts -> m (Either String opts))
    -> (Except String opts -> Either String opts)
    -> Except String opts
    -> m (Either String opts)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Except String opts -> Either String opts
    forall e a. Except e a -> Either e a
    runExcept

    {- | @f :: Flag opts@  is an action on the option record that results from
         parsing an option.  @f opts@ produces either an error message or an
         updated options record
    -}
    type Flag opts = opts -> OptM opts

    -- | Checks that the given options are consistent.

    checkOpts :: Flag CommandLineOptions
    checkOpts :: Flag CommandLineOptions
    checkOpts CommandLineOptions
    opts = do
      -- NOTE: This is a temporary hold-out until --vim can be converted into a backend or plugin,
      -- whose options compatibility currently is checked in `Agda.Compiler.Backend`.
      --
      -- Additionally, note that some options checking is performed in `Agda.Main`
      -- in which the top-level frontend and backend interactors are selected.
      --
      -- Those checks are not represented here, because:
      --   - They are used solely for selecting the initial executon mode; they
      --     don't need to be checked on a per-module etc basis.
      --   - I hope/expect that the presence of those specific flags will be eventually
      --     abstracted out (like the Backends' internal flags), so that they are invisible
      --     to the rest of the type-checking system.
      Bool -> ExceptT String Identity () -> ExceptT String Identity ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (CommandLineOptions -> Bool
    optGenerateVimFile CommandLineOptions
    opts Bool -> Bool -> Bool
    && CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts) (ExceptT String Identity () -> ExceptT String Identity ())
    -> ExceptT String Identity () -> ExceptT String Identity ()
    forall a b. (a -> b) -> a -> b
    $
        String -> ExceptT String Identity ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String Identity ())
    -> String -> ExceptT String Identity ()
    forall a b. (a -> b) -> a -> b
    $ String
    "The --only-scope-checking flag cannot be combined with --vim."
      Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    opts

    -- | Check for unsafe pragmas. Gives a list of used unsafe flags.

    unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
    unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
    unsafePragmaOptions CommandLineOptions
    clo PragmaOptions
    opts =
      [ String
    "--allow-unsolved-metas"                     | PragmaOptions -> Bool
    optAllowUnsolved PragmaOptions
    opts             ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--allow-incomplete-matches"                 | PragmaOptions -> Bool
    optAllowIncompleteMatch PragmaOptions
    opts      ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--no-positivity-check"                      | PragmaOptions -> Bool
    optDisablePositivity PragmaOptions
    opts         ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--no-termination-check"                     | Bool -> Bool
    not (PragmaOptions -> Bool
    optTerminationCheck PragmaOptions
    opts)    ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--type-in-type"                             | Bool -> Bool
    not (PragmaOptions -> Bool
    optUniverseCheck PragmaOptions
    opts)       ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--omega-in-omega"                           | PragmaOptions -> Bool
    optOmegaInOmega PragmaOptions
    opts              ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--sized-types"                              | WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (PragmaOptions -> WithDefault 'False
    optSizedTypes PragmaOptions
    opts) ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--injective-type-constructors"              | PragmaOptions -> Bool
    optInjectiveTypeConstructors PragmaOptions
    opts ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--irrelevant-projections"                   | PragmaOptions -> Bool
    optIrrelevantProjections PragmaOptions
    opts     ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--experimental-irrelevance"                 | PragmaOptions -> Bool
    optExperimentalIrrelevance PragmaOptions
    opts   ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--rewriting"                                | PragmaOptions -> Bool
    optRewriting PragmaOptions
    opts                 ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--cubical and --with-K"                     | PragmaOptions -> Maybe Cubical
    optCubical PragmaOptions
    opts Maybe Cubical -> Maybe Cubical -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    CFull
                                                     , Bool -> Bool
    not (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool) -> WithDefault 'False -> Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> WithDefault 'False
    optWithoutK PragmaOptions
    opts) ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--erased-cubical and --with-K"              | PragmaOptions -> Maybe Cubical
    optCubical PragmaOptions
    opts Maybe Cubical -> Maybe Cubical -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    CErased
                                                     , Bool -> Bool
    not (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool) -> WithDefault 'False -> Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> WithDefault 'False
    optWithoutK PragmaOptions
    opts) ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--cumulativity"                             | PragmaOptions -> Bool
    optCumulativity PragmaOptions
    opts              ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--allow-exec"                               | PragmaOptions -> Bool
    optAllowExec PragmaOptions
    opts                 ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      []

    -- | If any these options have changed, then the file will be
    --   rechecked. Boolean options are negated to mention non-default
    --   options, where possible.

    restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
    restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
    restartOptions =
      [ (CutOff -> RestartCodomain
    C (CutOff -> RestartCodomain)
    -> (PragmaOptions -> CutOff) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> CutOff
    optTerminationDepth, String
    "--termination-depth")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (UnicodeOrAscii -> UnicodeOrAscii -> Bool
    forall a. Eq a => a -> a -> Bool
    /= UnicodeOrAscii
    UnicodeOk) (UnicodeOrAscii -> Bool)
    -> (PragmaOptions -> UnicodeOrAscii) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> UnicodeOrAscii
    optUseUnicode, String
    "--no-unicode")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAllowUnsolved, String
    "--allow-unsolved-metas")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAllowIncompleteMatch, String
    "--allow-incomplete-matches")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optDisablePositivity, String
    "--no-positivity-check")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optTerminationCheck,  String
    "--no-termination-check")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optUniverseCheck, String
    "--type-in-type")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optOmegaInOmega, String
    "--omega-in-omega")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optSubtyping, String
    "--subtyping")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optCumulativity, String
    "--cumulativity")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optSizedTypes, String
    "--no-sized-types")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optGuardedness, String
    "--no-guardedness")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optInjectiveTypeConstructors, String
    "--injective-type-constructors")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optProp, String
    "--prop")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optTwoLevel, String
    "--two-level")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optUniversePolymorphism, String
    "--no-universe-polymorphism")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optIrrelevantProjections, String
    "--irrelevant-projections")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optExperimentalIrrelevance, String
    "--experimental-irrelevance")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optWithoutK, String
    "--without-K")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optExactSplit, String
    "--exact-split")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optEta, String
    "--no-eta-equality")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optRewriting, String
    "--rewriting")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Cubical -> Maybe Cubical -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    CFull) (Maybe Cubical -> Bool)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical, String
    "--cubical")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Cubical -> Maybe Cubical -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    CErased) (Maybe Cubical -> Bool)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical, String
    "--erased-cubical")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optGuarded, String
    "--guarded")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optOverlappingInstances, String
    "--overlapping-instances")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optQualifiedInstances, String
    "--qualified-instances")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optQualifiedInstances, String
    "--no-qualified-instances")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optSafe, String
    "--safe")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optDoubleCheck, String
    "--double-check")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optSyntacticEquality, String
    "--no-syntactic-equality")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAutoInline, String
    "--no-auto-inline")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optFastReduce, String
    "--no-fast-reduce")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optCallByName, String
    "--call-by-name")
      , (Int -> RestartCodomain
    I (Int -> RestartCodomain)
    -> (PragmaOptions -> Int) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Int
    optInstanceSearchDepth, String
    "--instance-search-depth")
      , (Int -> RestartCodomain
    I (Int -> RestartCodomain)
    -> (PragmaOptions -> Int) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Int
    optInversionMaxDepth, String
    "--inversion-max-depth")
      , (WarningMode -> RestartCodomain
    W (WarningMode -> RestartCodomain)
    -> (PragmaOptions -> WarningMode)
    -> PragmaOptions
    -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WarningMode
    optWarningMode, String
    "--warning")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe ConfluenceCheck -> Maybe ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck -> Maybe ConfluenceCheck
    forall a. a -> Maybe a
    Just ConfluenceCheck
    LocalConfluenceCheck) (Maybe ConfluenceCheck -> Bool)
    -> (PragmaOptions -> Maybe ConfluenceCheck)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck, String
    "--local-confluence-check")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe ConfluenceCheck -> Maybe ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck -> Maybe ConfluenceCheck
    forall a. a -> Maybe a
    Just ConfluenceCheck
    GlobalConfluenceCheck) (Maybe ConfluenceCheck -> Bool)
    -> (PragmaOptions -> Maybe ConfluenceCheck)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck, String
    "--confluence-check")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optImportSorts, String
    "--no-import-sorts")
      , (Bool -> RestartCodomain
    B (Bool -> RestartCodomain)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAllowExec, String
    "--allow-exec")
      ]

    -- to make all restart options have the same type
    data RestartCodomain = C CutOff | B Bool | I Int | W WarningMode
      deriving RestartCodomain -> RestartCodomain -> Bool
    (RestartCodomain -> RestartCodomain -> Bool)
    -> (RestartCodomain -> RestartCodomain -> Bool)
    -> Eq RestartCodomain
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: RestartCodomain -> RestartCodomain -> Bool
    $c/= :: RestartCodomain -> RestartCodomain -> Bool
    == :: RestartCodomain -> RestartCodomain -> Bool
    $c== :: RestartCodomain -> RestartCodomain -> Bool
    Eq

    -- | An infective option is an option that if used in one module, must
    --   be used in all modules that depend on this module.
    --
    -- Note that @--cubical@ and @--erased-cubical@ are \"jointly
    -- infective\": if one of them is used in one module, then one or the
    -- other must be used in all modules that depend on this module.

    infectiveOptions :: [(PragmaOptions -> Bool, String)]
    infectiveOptions :: [(PragmaOptions -> Bool, String)]
    infectiveOptions =
      [ (Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical, String
    "--cubical/--erased-cubical")
      , (PragmaOptions -> Bool
    optGuarded, String
    "--guarded")
      , (PragmaOptions -> Bool
    optProp, String
    "--prop")
      , (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optTwoLevel, String
    "--two-level")
      , (PragmaOptions -> Bool
    optRewriting, String
    "--rewriting")
      , (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optSizedTypes, String
    "--sized-types")
      , (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optGuardedness, String
    "--guardedness")
      ]

    -- | A coinfective option is an option that if used in one module, must
    --   be used in all modules that this module depends on.

    coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
    coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
    coinfectiveOptions =
      [ (PragmaOptions -> Bool
    optSafe, String
    "--safe")
      , (WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optWithoutK, String
    "--without-K")
      , (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optUniversePolymorphism, String
    "--no-universe-polymorphism")
      , (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optSubtyping, String
    "--no-subtyping")
      , (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optCumulativity, String
    "--no-cumulativity")
      ]

    inputFlag :: FilePath -> Flag CommandLineOptions
    inputFlag :: String -> Flag CommandLineOptions
    inputFlag String
    f CommandLineOptions
    o =
        case CommandLineOptions -> Maybe String
    optInputFile CommandLineOptions
    o of
            Maybe String
    Nothing  -> Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optInputFile :: Maybe String
    optInputFile = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    f }
            Just String
    _   -> String -> OptM CommandLineOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "only one input file allowed"

    printAgdaDirFlag :: Flag CommandLineOptions
    printAgdaDirFlag :: Flag CommandLineOptions
    printAgdaDirFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintAgdaDir :: Bool
    optPrintAgdaDir = Bool
    True }

    versionFlag :: Flag CommandLineOptions
    versionFlag :: Flag CommandLineOptions
    versionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintVersion :: Bool
    optPrintVersion = Bool
    True }

    helpFlag :: Maybe String -> Flag CommandLineOptions
    helpFlag :: Maybe String -> Flag CommandLineOptions
    helpFlag Maybe String
    Nothing    CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintHelp :: Maybe Help
    optPrintHelp = Help -> Maybe Help
    forall a. a -> Maybe a
    Just Help
    GeneralHelp }
    helpFlag (Just String
    str) CommandLineOptions
    o = case String -> Maybe HelpTopic
    string2HelpTopic String
    str of
      Just HelpTopic
    hpt -> Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintHelp :: Maybe Help
    optPrintHelp = Help -> Maybe Help
    forall a. a -> Maybe a
    Just (HelpTopic -> Help
    HelpFor HelpTopic
    hpt) }
      Maybe HelpTopic
    Nothing -> String -> OptM CommandLineOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM CommandLineOptions)
    -> String -> OptM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ String
    "unknown help topic " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    str String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " (available: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                               String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " (((String, HelpTopic) -> String)
    -> [(String, HelpTopic)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, HelpTopic) -> String
    forall a b. (a, b) -> a
    fst [(String, HelpTopic)]
    allHelpTopics) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    safeFlag :: Flag PragmaOptions
    safeFlag :: Flag PragmaOptions
    safeFlag PragmaOptions
    o = do
      let sizedTypes :: WithDefault 'False
    sizedTypes  = PragmaOptions -> WithDefault 'False
    optSizedTypes PragmaOptions
    o
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSafe :: Bool
    optSafe        = Bool
    True
                 , optSizedTypes :: WithDefault 'False
    optSizedTypes  = Bool -> WithDefault 'False -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
    setDefault Bool
    False WithDefault 'False
    sizedTypes
                 }

    flatSplitFlag :: Flag PragmaOptions
    flatSplitFlag :: Flag PragmaOptions
    flatSplitFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optFlatSplit :: Bool
    optFlatSplit = Bool
    True }

    noFlatSplitFlag :: Flag PragmaOptions
    noFlatSplitFlag :: Flag PragmaOptions
    noFlatSplitFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optFlatSplit :: Bool
    optFlatSplit = Bool
    False }

    doubleCheckFlag :: Bool -> Flag PragmaOptions
    doubleCheckFlag :: Bool -> Flag PragmaOptions
    doubleCheckFlag Bool
    b PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optDoubleCheck :: Bool
    optDoubleCheck = Bool
    b }

    noSyntacticEqualityFlag :: Flag PragmaOptions
    noSyntacticEqualityFlag :: Flag PragmaOptions
    noSyntacticEqualityFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSyntacticEquality :: Bool
    optSyntacticEquality = Bool
    False }

    noSortComparisonFlag :: Flag PragmaOptions
    noSortComparisonFlag :: Flag PragmaOptions
    noSortComparisonFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return PragmaOptions
    o

    sharingFlag :: Bool -> Flag CommandLineOptions
    sharingFlag :: Bool -> Flag CommandLineOptions
    sharingFlag Bool
    _ CommandLineOptions
    _ = String -> OptM CommandLineOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM CommandLineOptions)
    -> String -> OptM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $
      String
    "Feature --sharing has been removed (in favor of the Agda abstract machine)."

    cachingFlag :: Bool -> Flag PragmaOptions
    cachingFlag :: Bool -> Flag PragmaOptions
    cachingFlag Bool
    b PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCaching :: Bool
    optCaching = Bool
    b }

    propFlag :: Flag PragmaOptions
    propFlag :: Flag PragmaOptions
    propFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optProp :: Bool
    optProp = Bool
    True }

    noPropFlag :: Flag PragmaOptions
    noPropFlag :: Flag PragmaOptions
    noPropFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optProp :: Bool
    optProp = Bool
    False }

    twoLevelFlag :: Flag PragmaOptions
    twoLevelFlag :: Flag PragmaOptions
    twoLevelFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optTwoLevel :: WithDefault 'False
    optTwoLevel = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    True }

    experimentalIrrelevanceFlag :: Flag PragmaOptions
    experimentalIrrelevanceFlag :: Flag PragmaOptions
    experimentalIrrelevanceFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optExperimentalIrrelevance :: Bool
    optExperimentalIrrelevance = Bool
    True }

    irrelevantProjectionsFlag :: Flag PragmaOptions
    irrelevantProjectionsFlag :: Flag PragmaOptions
    irrelevantProjectionsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optIrrelevantProjections :: Bool
    optIrrelevantProjections = Bool
    True }

    noIrrelevantProjectionsFlag :: Flag PragmaOptions
    noIrrelevantProjectionsFlag :: Flag PragmaOptions
    noIrrelevantProjectionsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optIrrelevantProjections :: Bool
    optIrrelevantProjections = Bool
    False }

    ignoreInterfacesFlag :: Flag CommandLineOptions
    ignoreInterfacesFlag :: Flag CommandLineOptions
    ignoreInterfacesFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIgnoreInterfaces :: Bool
    optIgnoreInterfaces = Bool
    True }

    ignoreAllInterfacesFlag :: Flag CommandLineOptions
    ignoreAllInterfacesFlag :: Flag CommandLineOptions
    ignoreAllInterfacesFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIgnoreAllInterfaces :: Bool
    optIgnoreAllInterfaces = Bool
    True }

    localInterfacesFlag :: Flag CommandLineOptions
    localInterfacesFlag :: Flag CommandLineOptions
    localInterfacesFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optLocalInterfaces :: Bool
    optLocalInterfaces = Bool
    True }

    allowUnsolvedFlag :: Flag PragmaOptions
    allowUnsolvedFlag :: Flag PragmaOptions
    allowUnsolvedFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set WarningName
    unsolvedWarnings)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optAllowUnsolved :: Bool
    optAllowUnsolved = Bool
    True
                 , optWarningMode :: WarningMode
    optWarningMode   = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    allowIncompleteMatchFlag :: Flag PragmaOptions
    allowIncompleteMatchFlag :: Flag PragmaOptions
    allowIncompleteMatchFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set WarningName
    incompleteMatchWarnings)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optAllowIncompleteMatch :: Bool
    optAllowIncompleteMatch = Bool
    True
                 , optWarningMode :: WarningMode
    optWarningMode          = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    showImplicitFlag :: Flag PragmaOptions
    showImplicitFlag :: Flag PragmaOptions
    showImplicitFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optShowImplicit :: Bool
    optShowImplicit = Bool
    True }

    showIrrelevantFlag :: Flag PragmaOptions
    showIrrelevantFlag :: Flag PragmaOptions
    showIrrelevantFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optShowIrrelevant :: Bool
    optShowIrrelevant = Bool
    True }

    showIdentitySubstitutionsFlag :: Flag PragmaOptions
    showIdentitySubstitutionsFlag :: Flag PragmaOptions
    showIdentitySubstitutionsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optShowIdentitySubstitutions :: Bool
    optShowIdentitySubstitutions = Bool
    True }

    asciiOnlyFlag :: Flag PragmaOptions
    asciiOnlyFlag :: Flag PragmaOptions
    asciiOnlyFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ IO PragmaOptions -> PragmaOptions
    forall a. IO a -> a
    UNSAFE.unsafePerformIO (IO PragmaOptions -> PragmaOptions)
    -> IO PragmaOptions -> PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ do
      UnicodeOrAscii -> IO ()
    unsafeSetUnicodeOrAscii UnicodeOrAscii
    AsciiOnly
      PragmaOptions -> IO PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PragmaOptions -> IO PragmaOptions)
    -> PragmaOptions -> IO PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optUseUnicode :: UnicodeOrAscii
    optUseUnicode = UnicodeOrAscii
    AsciiOnly }

    ghciInteractionFlag :: Flag CommandLineOptions
    ghciInteractionFlag :: Flag CommandLineOptions
    ghciInteractionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optGHCiInteraction :: Bool
    optGHCiInteraction = Bool
    True }

    jsonInteractionFlag :: Flag CommandLineOptions
    jsonInteractionFlag :: Flag CommandLineOptions
    jsonInteractionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optJSONInteraction :: Bool
    optJSONInteraction = Bool
    True }

    vimFlag :: Flag CommandLineOptions
    vimFlag :: Flag CommandLineOptions
    vimFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optGenerateVimFile :: Bool
    optGenerateVimFile = Bool
    True }

    onlyScopeCheckingFlag :: Flag CommandLineOptions
    onlyScopeCheckingFlag :: Flag CommandLineOptions
    onlyScopeCheckingFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optOnlyScopeChecking :: Bool
    optOnlyScopeChecking = Bool
    True }

    countClustersFlag :: Flag PragmaOptions
    countClustersFlag :: Flag PragmaOptions
    countClustersFlag PragmaOptions
    o =
    #ifdef COUNT_CLUSTERS
      return $ o { optCountClusters = True }
    #else
      String -> OptM PragmaOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError
        String
    "Cluster counting has not been enabled in this build of Agda."
    #endif

    noAutoInlineFlag :: Flag PragmaOptions
    noAutoInlineFlag :: Flag PragmaOptions
    noAutoInlineFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optAutoInline :: Bool
    optAutoInline = Bool
    False }

    autoInlineFlag :: Flag PragmaOptions
    autoInlineFlag :: Flag PragmaOptions
    autoInlineFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optAutoInline :: Bool
    optAutoInline = Bool
    True }

    noPrintPatSynFlag :: Flag PragmaOptions
    noPrintPatSynFlag :: Flag PragmaOptions
    noPrintPatSynFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optPrintPatternSynonyms :: Bool
    optPrintPatternSynonyms = Bool
    False }

    noFastReduceFlag :: Flag PragmaOptions
    noFastReduceFlag :: Flag PragmaOptions
    noFastReduceFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optFastReduce :: Bool
    optFastReduce = Bool
    False }

    callByNameFlag :: Flag PragmaOptions
    callByNameFlag :: Flag PragmaOptions
    callByNameFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCallByName :: Bool
    optCallByName = Bool
    True }

    noPositivityFlag :: Flag PragmaOptions
    noPositivityFlag :: Flag PragmaOptions
    noPositivityFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete WarningName
    NotStrictlyPositive_)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optDisablePositivity :: Bool
    optDisablePositivity = Bool
    True
                 , optWarningMode :: WarningMode
    optWarningMode   = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    dontTerminationCheckFlag :: Flag PragmaOptions
    dontTerminationCheckFlag :: Flag PragmaOptions
    dontTerminationCheckFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete WarningName
    TerminationIssue_)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optTerminationCheck :: Bool
    optTerminationCheck = Bool
    False
                 , optWarningMode :: WarningMode
    optWarningMode   = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    -- The option was removed. See Issue 1918.
    dontCompletenessCheckFlag :: Flag PragmaOptions
    dontCompletenessCheckFlag :: Flag PragmaOptions
    dontCompletenessCheckFlag PragmaOptions
    _ =
      String -> OptM PragmaOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "The --no-coverage-check option has been removed."

    dontUniverseCheckFlag :: Flag PragmaOptions
    dontUniverseCheckFlag :: Flag PragmaOptions
    dontUniverseCheckFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optUniverseCheck :: Bool
    optUniverseCheck = Bool
    False }

    omegaInOmegaFlag :: Flag PragmaOptions
    omegaInOmegaFlag :: Flag PragmaOptions
    omegaInOmegaFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optOmegaInOmega :: Bool
    optOmegaInOmega = Bool
    True }

    subtypingFlag :: Flag PragmaOptions
    subtypingFlag :: Flag PragmaOptions
    subtypingFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSubtyping :: WithDefault 'False
    optSubtyping = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    True }

    noSubtypingFlag :: Flag PragmaOptions
    noSubtypingFlag :: Flag PragmaOptions
    noSubtypingFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSubtyping :: WithDefault 'False
    optSubtyping = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    False }

    cumulativityFlag :: Flag PragmaOptions
    cumulativityFlag :: Flag PragmaOptions
    cumulativityFlag PragmaOptions
    o =
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCumulativity :: Bool
    optCumulativity = Bool
    True
                 , optSubtyping :: WithDefault 'False
    optSubtyping    = Bool -> WithDefault 'False -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
    setDefault Bool
    True (WithDefault 'False -> WithDefault 'False)
    -> WithDefault 'False -> WithDefault 'False
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> WithDefault 'False
    optSubtyping PragmaOptions
    o
                 }

    noCumulativityFlag :: Flag PragmaOptions
    noCumulativityFlag :: Flag PragmaOptions
    noCumulativityFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCumulativity :: Bool
    optCumulativity = Bool
    False }

    --UNUSED Liang-Ting Chen 2019-07-16
    --etaFlag :: Flag PragmaOptions
    --etaFlag o = return $ o { optEta = True }

    noEtaFlag :: Flag PragmaOptions
    noEtaFlag :: Flag PragmaOptions
    noEtaFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optEta :: Bool
    optEta = Bool
    False }

    sizedTypes :: Flag PragmaOptions
    sizedTypes :: Flag PragmaOptions
    sizedTypes PragmaOptions
    o =
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSizedTypes :: WithDefault 'False
    optSizedTypes = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    True
                 --, optSubtyping  = setDefault True $ optSubtyping o
                 }

    noSizedTypes :: Flag PragmaOptions
    noSizedTypes :: Flag PragmaOptions
    noSizedTypes PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optSizedTypes :: WithDefault 'False
    optSizedTypes = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    False }

    guardedness :: Flag PragmaOptions
    guardedness :: Flag PragmaOptions
    guardedness PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optGuardedness :: WithDefault 'False
    optGuardedness = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    True }

    noGuardedness :: Flag PragmaOptions
    noGuardedness :: Flag PragmaOptions
    noGuardedness PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optGuardedness :: WithDefault 'False
    optGuardedness = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    False }

    injectiveTypeConstructorFlag :: Flag PragmaOptions
    injectiveTypeConstructorFlag :: Flag PragmaOptions
    injectiveTypeConstructorFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optInjectiveTypeConstructors :: Bool
    optInjectiveTypeConstructors = Bool
    True }

    guardingTypeConstructorFlag :: Flag PragmaOptions
    guardingTypeConstructorFlag :: Flag PragmaOptions
    guardingTypeConstructorFlag PragmaOptions
    _ = String -> OptM PragmaOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
    forall a b. (a -> b) -> a -> b
    $
      String
    "Experimental feature --guardedness-preserving-type-constructors has been removed."

    universePolymorphismFlag :: Flag PragmaOptions
    universePolymorphismFlag :: Flag PragmaOptions
    universePolymorphismFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optUniversePolymorphism :: Bool
    optUniversePolymorphism = Bool
    True }

    noUniversePolymorphismFlag :: Flag PragmaOptions
    noUniversePolymorphismFlag :: Flag PragmaOptions
    noUniversePolymorphismFlag  PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optUniversePolymorphism :: Bool
    optUniversePolymorphism = Bool
    False }

    noForcingFlag :: Flag PragmaOptions
    noForcingFlag :: Flag PragmaOptions
    noForcingFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optForcing :: Bool
    optForcing = Bool
    False }

    noProjectionLikeFlag :: Flag PragmaOptions
    noProjectionLikeFlag :: Flag PragmaOptions
    noProjectionLikeFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optProjectionLike :: Bool
    optProjectionLike = Bool
    False }

    withKFlag :: Flag PragmaOptions
    withKFlag :: Flag PragmaOptions
    withKFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optWithoutK :: WithDefault 'False
    optWithoutK = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    False }

    withoutKFlag :: Flag PragmaOptions
    withoutKFlag :: Flag PragmaOptions
    withoutKFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optWithoutK :: WithDefault 'False
    optWithoutK = Bool -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    True }

    copatternsFlag :: Flag PragmaOptions
    copatternsFlag :: Flag PragmaOptions
    copatternsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCopatterns :: Bool
    optCopatterns = Bool
    True }

    noCopatternsFlag :: Flag PragmaOptions
    noCopatternsFlag :: Flag PragmaOptions
    noCopatternsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCopatterns :: Bool
    optCopatterns = Bool
    False }

    noPatternMatchingFlag :: Flag PragmaOptions
    noPatternMatchingFlag :: Flag PragmaOptions
    noPatternMatchingFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optPatternMatching :: Bool
    optPatternMatching = Bool
    False }

    exactSplitFlag :: Flag PragmaOptions
    exactSplitFlag :: Flag PragmaOptions
    exactSplitFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert WarningName
    CoverageNoExactSplit_)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optExactSplit :: Bool
    optExactSplit = Bool
    True
                 , optWarningMode :: WarningMode
    optWarningMode   = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    noExactSplitFlag :: Flag PragmaOptions
    noExactSplitFlag :: Flag PragmaOptions
    noExactSplitFlag PragmaOptions
    o = do
      let upd :: WarningMode -> WarningMode
    upd = Lens' (Set WarningName) WarningMode
    -> LensMap (Set WarningName) WarningMode
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Set WarningName) WarningMode
    warningSet (WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete WarningName
    CoverageNoExactSplit_)
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optExactSplit :: Bool
    optExactSplit = Bool
    False
                 , optWarningMode :: WarningMode
    optWarningMode   = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o)
                 }

    rewritingFlag :: Flag PragmaOptions
    rewritingFlag :: Flag PragmaOptions
    rewritingFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optRewriting :: Bool
    optRewriting = Bool
    True }

    firstOrderFlag :: Flag PragmaOptions
    firstOrderFlag :: Flag PragmaOptions
    firstOrderFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optFirstOrder :: Bool
    optFirstOrder = Bool
    True }

    cubicalFlag
      :: Cubical  -- ^ Which variant of Cubical Agda?
      -> Flag PragmaOptions
    cubicalFlag :: Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    variant PragmaOptions
    o = do
      let withoutK :: WithDefault 'False
    withoutK = PragmaOptions -> WithDefault 'False
    optWithoutK PragmaOptions
    o
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCubical :: Maybe Cubical
    optCubical  = Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    variant
                 , optWithoutK :: WithDefault 'False
    optWithoutK = Bool -> WithDefault 'False -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
    setDefault Bool
    True WithDefault 'False
    withoutK
                 , optTwoLevel :: WithDefault 'False
    optTwoLevel = Bool -> WithDefault 'False -> WithDefault 'False
    forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
    setDefault Bool
    True (WithDefault 'False -> WithDefault 'False)
    -> WithDefault 'False -> WithDefault 'False
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> WithDefault 'False
    optTwoLevel PragmaOptions
    o
                 }

    guardedFlag :: Flag PragmaOptions
    guardedFlag :: Flag PragmaOptions
    guardedFlag PragmaOptions
    o = do
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optGuarded :: Bool
    optGuarded  = Bool
    True }

    postfixProjectionsFlag :: Flag PragmaOptions
    postfixProjectionsFlag :: Flag PragmaOptions
    postfixProjectionsFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optPostfixProjections :: Bool
    optPostfixProjections = Bool
    True }

    keepPatternVariablesFlag :: Flag PragmaOptions
    keepPatternVariablesFlag :: Flag PragmaOptions
    keepPatternVariablesFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optKeepPatternVariables :: Bool
    optKeepPatternVariables = Bool
    True }

    instanceDepthFlag :: String -> Flag PragmaOptions
    instanceDepthFlag :: String -> Flag PragmaOptions
    instanceDepthFlag String
    s PragmaOptions
    o = do
      Int
    d <- String -> String -> OptM Int
    integerArgument String
    "--instance-search-depth" String
    s
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optInstanceSearchDepth :: Int
    optInstanceSearchDepth = Int
    d }

    overlappingInstancesFlag :: Flag PragmaOptions
    overlappingInstancesFlag :: Flag PragmaOptions
    overlappingInstancesFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optOverlappingInstances :: Bool
    optOverlappingInstances = Bool
    True }

    noOverlappingInstancesFlag :: Flag PragmaOptions
    noOverlappingInstancesFlag :: Flag PragmaOptions
    noOverlappingInstancesFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optOverlappingInstances :: Bool
    optOverlappingInstances = Bool
    False }

    qualifiedInstancesFlag :: Flag PragmaOptions
    qualifiedInstancesFlag :: Flag PragmaOptions
    qualifiedInstancesFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optQualifiedInstances :: Bool
    optQualifiedInstances = Bool
    True }

    noQualifiedInstancesFlag :: Flag PragmaOptions
    noQualifiedInstancesFlag :: Flag PragmaOptions
    noQualifiedInstancesFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optQualifiedInstances :: Bool
    optQualifiedInstances = Bool
    False }

    inversionMaxDepthFlag :: String -> Flag PragmaOptions
    inversionMaxDepthFlag :: String -> Flag PragmaOptions
    inversionMaxDepthFlag String
    s PragmaOptions
    o = do
      Int
    d <- String -> String -> OptM Int
    integerArgument String
    "--inversion-max-depth" String
    s
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optInversionMaxDepth :: Int
    optInversionMaxDepth = Int
    d }

    interactiveFlag :: Flag CommandLineOptions
    interactiveFlag :: Flag CommandLineOptions
    interactiveFlag  CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optInteractive :: Bool
    optInteractive = Bool
    True }

    compileFlagNoMain :: Flag PragmaOptions
    compileFlagNoMain :: Flag PragmaOptions
    compileFlagNoMain PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optCompileNoMain :: Bool
    optCompileNoMain = Bool
    True }

    compileDirFlag :: FilePath -> Flag CommandLineOptions
    compileDirFlag :: String -> Flag CommandLineOptions
    compileDirFlag String
    f CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optCompileDir :: Maybe String
    optCompileDir = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    f }

    includeFlag :: FilePath -> Flag CommandLineOptions
    includeFlag :: String -> Flag CommandLineOptions
    includeFlag String
    d CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIncludePaths :: [String]
    optIncludePaths = String
    d String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : CommandLineOptions -> [String]
    optIncludePaths CommandLineOptions
    o }

    libraryFlag :: String -> Flag CommandLineOptions
    libraryFlag :: String -> Flag CommandLineOptions
    libraryFlag String
    s CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optLibraries :: [String]
    optLibraries = CommandLineOptions -> [String]
    optLibraries CommandLineOptions
    o [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    s] }

    overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
    overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
    overrideLibrariesFileFlag String
    s CommandLineOptions
    o =
      Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o
        { optOverrideLibrariesFile :: Maybe String
    optOverrideLibrariesFile = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    s
        , optUseLibs :: Bool
    optUseLibs = Bool
    True
        }

    noDefaultLibsFlag :: Flag CommandLineOptions
    noDefaultLibsFlag :: Flag CommandLineOptions
    noDefaultLibsFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optDefaultLibs :: Bool
    optDefaultLibs = Bool
    False }

    noLibsFlag :: Flag CommandLineOptions
    noLibsFlag :: Flag CommandLineOptions
    noLibsFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optUseLibs :: Bool
    optUseLibs = Bool
    False }

    verboseFlag :: String -> Flag PragmaOptions
    verboseFlag :: String -> Flag PragmaOptions
    verboseFlag String
    s PragmaOptions
    o =
        do  ([String]
    k,Int
    n) <- String -> OptM ([String], Int)
    parseVerbose String
    s
            Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optVerbose :: Verbosity
    optVerbose = [String] -> Int -> Verbosity -> Verbosity
    forall k v. Ord k => [k] -> v -> Trie k v -> Trie k v
    Trie.insert [String]
    k Int
    n (Verbosity -> Verbosity) -> Verbosity -> Verbosity
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Verbosity
    optVerbose PragmaOptions
    o }
      where
        parseVerbose :: String -> OptM ([VerboseKey], VerboseLevel)
        parseVerbose :: String -> OptM ([String], Int)
    parseVerbose String
    s = case (Char -> Bool) -> String -> [String]
    forall a. (a -> Bool) -> [a] -> [[a]]
    wordsBy (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` (String
    ":." :: String)) String
    s of
          []  -> OptM ([String], Int)
    forall {a}. ExceptT String Identity a
    usage
          String
    s0:[String]
    ss0 -> do
            let ([String]
    ss, String
    s) = String -> [String] -> ([String], String)
    forall a. a -> [a] -> ([a], a)
    initLast1 String
    s0 [String]
    ss0
            Int
    n <- OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    forall {a}. ExceptT String Identity a
    usage Int -> OptM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
            ([String], Int) -> OptM ([String], Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([String]
    ss, Int
    n)
        usage :: ExceptT String Identity a
    usage = String -> ExceptT String Identity a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "argument to verbose should be on the form x.y.z:N or N"

    warningModeFlag :: String -> Flag PragmaOptions
    warningModeFlag :: String -> Flag PragmaOptions
    warningModeFlag String
    s PragmaOptions
    o = case String -> Either WarningModeError (WarningMode -> WarningMode)
    warningModeUpdate String
    s of
      Right WarningMode -> WarningMode
    upd -> Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optWarningMode :: WarningMode
    optWarningMode = WarningMode -> WarningMode
    upd (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    o) }
      Left WarningModeError
    err  -> String -> OptM PragmaOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ WarningModeError -> String
    prettyWarningModeError WarningModeError
    err String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " See --help=warning."

    terminationDepthFlag :: String -> Flag PragmaOptions
    terminationDepthFlag :: String -> Flag PragmaOptions
    terminationDepthFlag String
    s PragmaOptions
    o =
        do Int
    k <- OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    forall {a}. ExceptT String Identity a
    usage Int -> OptM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
           Bool -> ExceptT String Identity () -> ExceptT String Identity ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    1) (ExceptT String Identity () -> ExceptT String Identity ())
    -> ExceptT String Identity () -> ExceptT String Identity ()
    forall a b. (a -> b) -> a -> b
    $ ExceptT String Identity ()
    forall {a}. ExceptT String Identity a
    usage -- or: turn termination checking off for 0
           Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optTerminationDepth :: CutOff
    optTerminationDepth = Int -> CutOff
    CutOff (Int -> CutOff) -> Int -> CutOff
    forall a b. (a -> b) -> a -> b
    $ Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1 }
        where usage :: ExceptT String Identity a
    usage = String -> ExceptT String Identity a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "argument to termination-depth should be >= 1"

    confluenceCheckFlag :: ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag :: ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    f PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optConfluenceCheck :: Maybe ConfluenceCheck
    optConfluenceCheck = ConfluenceCheck -> Maybe ConfluenceCheck
    forall a. a -> Maybe a
    Just ConfluenceCheck
    f }

    noConfluenceCheckFlag :: Flag PragmaOptions
    noConfluenceCheckFlag :: Flag PragmaOptions
    noConfluenceCheckFlag PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optConfluenceCheck :: Maybe ConfluenceCheck
    optConfluenceCheck = Maybe ConfluenceCheck
    forall a. Maybe a
    Nothing }

    noImportSorts :: Flag PragmaOptions
    noImportSorts :: Flag PragmaOptions
    noImportSorts PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optImportSorts :: Bool
    optImportSorts = Bool
    False }

    allowExec :: Flag PragmaOptions
    allowExec :: Flag PragmaOptions
    allowExec PragmaOptions
    o = Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { optAllowExec :: Bool
    optAllowExec = Bool
    True }

    integerArgument :: String -> String -> OptM Int
    integerArgument :: String -> String -> OptM Int
    integerArgument String
    flag String
    s = OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    usage Int -> OptM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
      where
      usage :: OptM Int
    usage = String -> OptM Int
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM Int) -> String -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String
    "option '" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    flag String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "' requires an integer argument"

    standardOptions :: [OptDescr (Flag CommandLineOptions)]
    standardOptions :: [OptDescr (Flag CommandLineOptions)]
    standardOptions =
        [ String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'V']  [String
    "version"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    versionFlag)
                        (String
    "print version number and exit")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    '?']  [String
    "help"]    ((Maybe String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (Maybe String -> a) -> String -> ArgDescr a
    OptArg Maybe String -> Flag CommandLineOptions
    helpFlag String
    "TOPIC") (String -> OptDescr (Flag CommandLineOptions))
    -> String -> OptDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
                        [ String
    "print help and exit; available "
                        , [(String, HelpTopic)] -> String -> ShowS
    forall a c. Sized a => a -> c -> c -> c
    singPlural [(String, HelpTopic)]
    allHelpTopics String
    "TOPIC" String
    "TOPICs"
                        , String
    ": "
                        , String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ ((String, HelpTopic) -> String)
    -> [(String, HelpTopic)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, HelpTopic) -> String
    forall a b. (a, b) -> a
    fst [(String, HelpTopic)]
    allHelpTopics
                        ]

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "print-agda-dir"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    printAgdaDirFlag)
                        (String
    "print $AGDA_DIR and exit")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'I']  [String
    "interactive"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    interactiveFlag)
                        String
    "start in interactive mode"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "interaction"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ghciInteractionFlag)
                        String
    "for use with the Emacs mode"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "interaction-json"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    jsonInteractionFlag)
                        String
    "for use with other editors such as Atom"

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "compile-dir"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    compileDirFlag String
    "DIR")
                        (String
    "directory for compiler output (default: the project root)")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "vim"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    vimFlag)
                        String
    "generate Vim highlighting files"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "ignore-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ignoreInterfacesFlag)
                        String
    "ignore interface files (re-type check everything)"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "local-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    localInterfacesFlag)
                        String
    "put interface files next to the Agda files they correspond to"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'i']  [String
    "include-path"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    includeFlag String
    "DIR")
                        String
    "look for imports in DIR"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'l']  [String
    "library"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    libraryFlag String
    "LIB")
                        String
    "use library LIB"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "library-file"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    overrideLibrariesFileFlag String
    "FILE")
                        String
    "use FILE instead of the standard libraries file"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    noLibsFlag)
                        String
    "don't use any library files"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-default-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    noDefaultLibsFlag)
                        String
    "don't use default libraries"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "only-scope-checking"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    onlyScopeCheckingFlag)
                        String
    "only scope-check the top-level module, do not type-check it"
        ] [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ (OptDescr (Flag PragmaOptions)
     -> OptDescr (Flag CommandLineOptions))
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Flag PragmaOptions -> Flag CommandLineOptions)
    -> OptDescr (Flag PragmaOptions)
    -> OptDescr (Flag CommandLineOptions)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Flag PragmaOptions -> Flag CommandLineOptions
    Lens' PragmaOptions CommandLineOptions
    lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
    pragmaOptions

    -- | Defined locally here since module ''Agda.Interaction.Options.Lenses''
    --   has cyclic dependency.
    lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
    lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
    lensPragmaOptions PragmaOptions -> f PragmaOptions
    f CommandLineOptions
    st = PragmaOptions -> f PragmaOptions
    f (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    st) f PragmaOptions
    -> (PragmaOptions -> CommandLineOptions) -> f CommandLineOptions
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ PragmaOptions
    opts -> CommandLineOptions
    st { optPragmaOptions :: PragmaOptions
    optPragmaOptions = PragmaOptions
    opts }

    -- | Command line options of previous versions of Agda.
    --   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
    deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
    deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
    deadStandardOptions =
        [ String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "sharing"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions))
    -> Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag CommandLineOptions
    sharingFlag Bool
    True)
                        String
    "DEPRECATED: does nothing"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-sharing"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions))
    -> Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag CommandLineOptions
    sharingFlag Bool
    False)
                        String
    "DEPRECATED: does nothing"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "ignore-all-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ignoreAllInterfacesFlag) -- not deprecated! Just hidden
                        String
    "ignore all interface files (re-type check everything, including builtin files)"
        ] [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ (OptDescr (Flag PragmaOptions)
     -> OptDescr (Flag CommandLineOptions))
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Flag PragmaOptions -> Flag CommandLineOptions)
    -> OptDescr (Flag PragmaOptions)
    -> OptDescr (Flag CommandLineOptions)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Flag PragmaOptions -> Flag CommandLineOptions
    Lens' PragmaOptions CommandLineOptions
    lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions

    pragmaOptions :: [OptDescr (Flag PragmaOptions)]
    pragmaOptions :: [OptDescr (Flag PragmaOptions)]
    pragmaOptions =
        [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "show-implicit"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    showImplicitFlag)
                        String
    "show implicit arguments when printing"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "show-irrelevant"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    showIrrelevantFlag)
                        String
    "show irrelevant arguments when printing"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "show-identity-substitutions"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    showIdentitySubstitutionsFlag)
                        String
    "show all arguments of metavariables when printing terms"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-unicode"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    asciiOnlyFlag)
                        String
    "don't use unicode characters when printing terms"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'v']  [String
    "verbose"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    verboseFlag String
    "N")
                        String
    "set verbosity level to N"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "allow-unsolved-metas"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    allowUnsolvedFlag)
                        String
    "succeed and create interface file regardless of unsolved meta variables"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "allow-incomplete-matches"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    allowIncompleteMatchFlag)
                        String
    "succeed and create interface file regardless of incomplete pattern matches"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-positivity-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noPositivityFlag)
                        String
    "do not warn about not strictly positive data types"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-termination-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    dontTerminationCheckFlag)
                        String
    "do not warn about possibly nonterminating code"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "termination-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    terminationDepthFlag String
    "N")
                        String
    "allow termination checker to count decrease/increase upto N (default N=1)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "type-in-type"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    dontUniverseCheckFlag)
                        String
    "ignore universe levels (this makes Agda inconsistent)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "omega-in-omega"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    omegaInOmegaFlag)
                        String
    "enable typing rule Setω : Setω (this makes Agda inconsistent)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    subtypingFlag)
                        String
    "enable subtyping rules in general (e.g. for irrelevance and erasure)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noSubtypingFlag)
                        String
    "disable subtyping rules in general (e.g. for irrelevance and erasure) (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    cumulativityFlag)
                        String
    "enable subtyping of universes (e.g. Set =< Set₁) (implies --subtyping)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noCumulativityFlag)
                        String
    "disable subtyping of universes (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    propFlag)
                        String
    "enable the use of the Prop universe"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noPropFlag)
                        String
    "disable the use of the Prop universe (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "two-level"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    twoLevelFlag)
                        String
    "enable the use of SSet* universes"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    sizedTypes)
                        String
    "enable sized types (default, inconsistent with --guardedness, implies --subtyping)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noSizedTypes)
                        String
    "disable sized types"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    flatSplitFlag)
                        String
    "allow split on (@flat x : A) arguments (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noFlatSplitFlag)
                        String
    "disable split on (@flat x : A) arguments"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    guardedness)
                        String
    "enable constructor-based guarded corecursion (default, inconsistent with --sized-types)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noGuardedness)
                        String
    "disable constructor-based guarded corecursion"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "injective-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    injectiveTypeConstructorFlag)
                        String
    "enable injective type constructors (makes Agda anti-classical and possibly inconsistent)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noUniversePolymorphismFlag)
                        String
    "disable universe polymorphism"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    universePolymorphismFlag)
                        String
    "enable universe polymorphism (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    irrelevantProjectionsFlag)
                        String
    "enable projection of irrelevant record fields and similar irrelevant definitions (inconsistent)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noIrrelevantProjectionsFlag)
                        String
    "disable projection of irrelevant record fields and similar irrelevant definitions (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "experimental-irrelevance"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    experimentalIrrelevanceFlag)
                        String
    "enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "with-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    withKFlag)
                        String
    "enable the K rule in pattern matching (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "without-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    withoutKFlag)
                        String
    "disable the K rule in pattern matching"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    copatternsFlag)
                        String
    "enable definitions by copattern matching (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noCopatternsFlag)
                        String
    "disable definitions by copattern matching"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-pattern-matching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noPatternMatchingFlag)
                        String
    "disable pattern matching completely"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    exactSplitFlag)
                        String
    "require all clauses in a definition to hold as definitional equalities (unless marked CATCHALL)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noExactSplitFlag)
                        String
    "do not require all clauses in a definition to hold as definitional equalities (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-eta-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noEtaFlag)
                        String
    "default records to no-eta-equality"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-forcing"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noForcingFlag)
                        String
    "disable the forcing analysis for data constructors (optimisation)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-projection-like"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noProjectionLikeFlag)
                        String
    "disable the analysis whether function signatures liken those of projections (optimisation)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "rewriting"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    rewritingFlag)
                        String
    "enable declaration and use of REWRITE rules"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "local-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    LocalConfluenceCheck)
                        String
    "enable checking of local confluence of REWRITE rules"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    GlobalConfluenceCheck)
                        String
    "enable global confluence checking of REWRITE rules (more restrictive than --local-confluence-check)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noConfluenceCheckFlag)
                        String
    "disable confluence checking of REWRITE rules (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    CFull)
                        String
    "enable cubical features (e.g. overloads lambdas for paths), implies --without-K"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "erased-cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    CErased)
                        String
    "enable cubical features (some only in erased settings), implies --without-K"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "guarded"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    guardedFlag)
                        String
    "enable @lock/@tick attributes"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "experimental-lossy-unification"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    firstOrderFlag)
                        String
    "enable heuristically unifying `f es = f es'` by unifying `es = es'`, even when it could lose solutions."
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "postfix-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    postfixProjectionsFlag)
                        String
    "make postfix projection notation the default"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "keep-pattern-variables"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    keepPatternVariablesFlag)
                        String
    "don't replace variables with dot patterns during case splitting"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "instance-search-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    instanceDepthFlag String
    "N")
                        String
    "set instance search depth to N (default: 500)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    overlappingInstancesFlag)
                        String
    "consider recursive instance arguments during pruning of instance candidates"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noOverlappingInstancesFlag)
                        String
    "don't consider recursive instance arguments during pruning of instance candidates (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "qualified-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    qualifiedInstancesFlag)
                        String
    "use instances with qualified names (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-qualified-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noQualifiedInstancesFlag)
                        String
    "don't use instances with qualified names"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "inversion-max-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    inversionMaxDepthFlag String
    "N")
                        String
    "set maximum depth for pattern match inversion to N (default: 50)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "safe"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    safeFlag)
                        String
    "disable postulates, unsafe OPTION pragmas and primEraseEquality, implies --no-sized-types"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "double-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Bool -> Flag PragmaOptions
    doubleCheckFlag Bool
    True))
                        String
    "enable double-checking of all terms using the internal typechecker"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-double-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Bool -> Flag PragmaOptions
    doubleCheckFlag Bool
    False))
                        String
    "disable double-checking of terms (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-syntactic-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noSyntacticEqualityFlag)
                        String
    "disable the syntactic equality shortcut in the conversion checker"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'W']  [String
    "warning"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    warningModeFlag String
    "FLAG")
                        (String
    "set warning flags. See --help=warning.")
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-main"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    compileFlagNoMain)
                        String
    "do not treat the requested module as the main module of a program when compiling"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "caching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag PragmaOptions
    cachingFlag Bool
    True)
                        String
    "enable caching of typechecking (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-caching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag PragmaOptions
    cachingFlag Bool
    False)
                        String
    "disable caching of typechecking"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "count-clusters"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    countClustersFlag)
                        (String
    "count extended grapheme clusters when " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                         String
    "generating LaTeX (note that this flag " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
    #ifdef COUNT_CLUSTERS
                         "is not enabled in all builds of Agda)"
    #else
                         String
    "has not been enabled in this build of Agda)"
    #endif
                        )
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "auto-inline"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    autoInlineFlag)
                        String
    "enable automatic compile-time inlining"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-auto-inline"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noAutoInlineFlag)
                        (String
    "disable automatic compile-time inlining (default), " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                         String
    "only definitions marked INLINE will be inlined")
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-print-pattern-synonyms"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noPrintPatSynFlag)
                        String
    "expand pattern synonyms when printing terms"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-fast-reduce"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noFastReduceFlag)
                        String
    "disable reduction using the Agda Abstract Machine"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "call-by-name"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    callByNameFlag)
                        String
    "use call-by-name evaluation instead of call-by-need"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-import-sorts"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noImportSorts)
                        String
    "disable the implicit import of Agda.Primitive using (Set; Prop) at the start of each top-level module"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "allow-exec"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    allowExec)
                        String
    "allow system calls to trusted executables with primExec"
        ]

    -- | Pragma options of previous versions of Agda.
    --   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
    deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions =
        [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "guardedness-preserving-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    guardingTypeConstructorFlag)
                        String
    "treat type constructors as inductive constructors when checking productivity"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-coverage-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    dontCompletenessCheckFlag)
                        String
    "the option has been removed"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-sort-comparison"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noSortComparisonFlag)
                        String
    "disable the comparison of sorts when checking conversion of types"
        ]

    -- | Used for printing usage info.
    --   Does not include the dead options.
    standardOptions_ :: [OptDescr ()]
    standardOptions_ :: [OptDescr ()]
    standardOptions_ = (OptDescr (Flag CommandLineOptions) -> OptDescr ())
    -> [OptDescr (Flag CommandLineOptions)] -> [OptDescr ()]
    forall a b. (a -> b) -> [a] -> [b]
    map OptDescr (Flag CommandLineOptions) -> OptDescr ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void [OptDescr (Flag CommandLineOptions)]
    standardOptions

    -- | Simple interface for System.Console.GetOpt
    --   Could be moved to Agda.Utils.Options (does not exist yet)
    getOptSimple
      :: [String]               -- ^ command line argument words
      -> [OptDescr (Flag opts)] -- ^ options handlers
      -> (String -> Flag opts)  -- ^ handler of non-options (only one is allowed)
      -> Flag opts              -- ^ combined opts data structure transformer
    getOptSimple :: forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple [String]
    argv [OptDescr (Flag opts)]
    opts String -> Flag opts
    fileArg = \ opts
    defaults ->
      case ArgOrder (Flag opts)
    -> [OptDescr (Flag opts)]
    -> [String]
    -> ([Flag opts], [String], [String], [String])
    forall a.
    ArgOrder a
    -> [OptDescr a] -> [String] -> ([a], [String], [String], [String])
    getOpt' ((String -> Flag opts) -> ArgOrder (Flag opts)
    forall a. (String -> a) -> ArgOrder a
    ReturnInOrder String -> Flag opts
    fileArg) [OptDescr (Flag opts)]
    opts [String]
    argv of
        ([Flag opts]
    o, [String]
    _, []          , [] )  -> (OptM opts -> Flag opts -> OptM opts)
    -> OptM opts -> [Flag opts] -> OptM opts
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl OptM opts -> Flag opts -> OptM opts
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    (>>=) (Flag opts
    forall (m :: * -> *) a. Monad m => a -> m a
    return opts
    defaults) [Flag opts]
    o
        ([Flag opts]
    _, [String]
    _, [String]
    unrecognized, [String]
    errs) -> String -> OptM opts
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM opts) -> String -> OptM opts
    forall a b. (a -> b) -> a -> b
    $ String
    umsg String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    emsg

          where
          ucap :: String
    ucap = String
    "Unrecognized " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> ShowS
    forall {a}. [a] -> ShowS
    plural [String]
    unrecognized String
    "option" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
          ecap :: String
    ecap = [String] -> ShowS
    forall {a}. [a] -> ShowS
    plural [String]
    errs String
    "Option error" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
          umsg :: String
    umsg = if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    unrecognized then String
    "" else [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
           String
    ucap String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ShowS
    suggest [String]
    unrecognized
          emsg :: String
    emsg = if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    errs then String
    "" else [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
           String
    ecap String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    errs
          plural :: [a] -> ShowS
    plural [a
    _] String
    x = String
    x
          plural [a]
    _   String
    x = String
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "s"

          -- Suggest alternatives that are at most 3 typos away

          longopts :: [String]
          longopts :: [String]
    longopts = ShowS -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "--" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (OptDescr (Flag opts) -> [String])
    -> [OptDescr (Flag opts)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\ (Option String
    _ [String]
    long ArgDescr (Flag opts)
    _ String
    _) -> [String]
    long) [OptDescr (Flag opts)]
    opts

          dist :: String -> String -> Int
          dist :: String -> String -> Int
    dist String
    s String
    t = EditCosts -> String -> String -> Int
    restrictedDamerauLevenshteinDistance EditCosts
    defaultEditCosts String
    s String
    t

          close :: String -> String -> Maybe (Int, String)
          close :: String -> String -> Maybe (Int, String)
    close String
    s String
    t = let d :: Int
    d = String -> String -> Int
    dist String
    s String
    t in if Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    3 then (Int, String) -> Maybe (Int, String)
    forall a. a -> Maybe a
    Just (Int
    d, String
    t) else Maybe (Int, String)
    forall a. Maybe a
    Nothing

          closeopts :: String -> [(Int, String)]
          closeopts :: String -> [(Int, String)]
    closeopts String
    s = (String -> Maybe (Int, String)) -> [String] -> [(Int, String)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (String -> String -> Maybe (Int, String)
    close String
    s) [String]
    longopts

          alts :: String -> [[String]]
          alts :: String -> [[String]]
    alts String
    s = ([(Int, String)] -> [String]) -> [[(Int, String)]] -> [[String]]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, String) -> String) -> [(Int, String)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, String) -> String
    forall a b. (a, b) -> b
    snd) ([[(Int, String)]] -> [[String]])
    -> [[(Int, String)]] -> [[String]]
    forall a b. (a -> b) -> a -> b
    $ ((Int, String) -> Int) -> [(Int, String)] -> [[(Int, String)]]
    forall b a. Ord b => (a -> b) -> [a] -> [[a]]
    groupOn (Int, String) -> Int
    forall a b. (a, b) -> a
    fst ([(Int, String)] -> [[(Int, String)]])
    -> [(Int, String)] -> [[(Int, String)]]
    forall a b. (a -> b) -> a -> b
    $ String -> [(Int, String)]
    closeopts String
    s

          suggest :: String -> String
          suggest :: ShowS
    suggest String
    s = case String -> [[String]]
    alts String
    s of
            []     -> String
    s
            [String]
    as : [[String]]
    _ -> String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " (did you mean " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    sugs [String]
    as String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " ?)"

          sugs :: [String] -> String
          sugs :: [String] -> String
    sugs [String
    a] = String
    a
          sugs [String]
    as  = String
    "any of " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords [String]
    as

    {- No longer used in favour of parseBackendOptions in Agda.Compiler.Backend
    -- | Parse the standard options.
    parseStandardOptions :: [String] -> OptM CommandLineOptions
    parseStandardOptions argv = parseStandardOptions' argv defaultOptions

    parseStandardOptions' :: [String] -> Flag CommandLineOptions
    parseStandardOptions' argv opts = do
      opts <- getOptSimple (stripRTS argv) (deadStandardOptions ++ standardOptions) inputFlag opts
      checkOpts opts
    -}

    -- | Parse options from an options pragma.
    parsePragmaOptions
      :: [String]
         -- ^ Pragma options.
      -> CommandLineOptions
         -- ^ Command-line options which should be updated.
      -> OptM PragmaOptions
    parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
    parsePragmaOptions [String]
    argv CommandLineOptions
    opts = do
      PragmaOptions
    ps <- [String]
    -> [OptDescr (Flag PragmaOptions)]
    -> (String -> Flag PragmaOptions)
    -> Flag PragmaOptions
    forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple [String]
    argv ([OptDescr (Flag PragmaOptions)]
    deadPragmaOptions [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag PragmaOptions)]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag PragmaOptions)]
    pragmaOptions)
              (\String
    s PragmaOptions
    _ -> String -> OptM PragmaOptions
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ String
    "Bad option in pragma: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s)
              (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts)
      CommandLineOptions
    _ <- Flag CommandLineOptions
    checkOpts (CommandLineOptions
    opts { optPragmaOptions :: PragmaOptions
    optPragmaOptions = PragmaOptions
    ps })
      Flag PragmaOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return PragmaOptions
    ps

    -- | Parse options for a plugin.
    parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
    parsePluginOptions :: forall opts. [String] -> [OptDescr (Flag opts)] -> Flag opts
    parsePluginOptions [String]
    argv [OptDescr (Flag opts)]
    opts =
      [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple [String]
    argv [OptDescr (Flag opts)]
    opts
        (\String
    s opts
    _ -> String -> ExceptT String Identity opts
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String Identity opts)
    -> String -> ExceptT String Identity opts
    forall a b. (a -> b) -> a -> b
    $
                   String
    "Internal error: Flag " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " passed to a plugin")

    -- | The usage info message. The argument is the program name (probably
    --   agda).
    usage :: [OptDescr ()] -> String -> Help -> String
    usage :: [OptDescr ()] -> String -> Help -> String
    usage [OptDescr ()]
    options String
    progName Help
    GeneralHelp = String -> [OptDescr ()] -> String
    forall a. String -> [OptDescr a] -> String
    usageInfo (ShowS
    header String
    progName) [OptDescr ()]
    options
        where
            header :: ShowS
    header String
    progName = [String] -> String
    unlines [ String
    "Agda version " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    version, String
    ""
                                      , String
    "Usage: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    progName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " [OPTIONS...] [FILE]" ]

    usage [OptDescr ()]
    options String
    progName (HelpFor HelpTopic
    topic) = HelpTopic -> String
    helpTopicUsage HelpTopic
    topic

    -- | Removes RTS options from a list of options.

    stripRTS :: [String] -> [String]
    stripRTS :: [String] -> [String]
    stripRTS [] = []
    stripRTS (String
    "--RTS" : [String]
    argv) = [String]
    argv
    stripRTS (String
    arg : [String]
    argv)
      | String -> String -> Bool
    is String
    "+RTS" String
    arg = [String] -> [String]
    stripRTS ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Bool -> Bool
    not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String -> Bool
    is String
    "-RTS") [String]
    argv
      | Bool
    otherwise     = String
    arg String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String] -> [String]
    stripRTS [String]
    argv
      where
        is :: String -> String -> Bool
    is String
    x String
    arg = [String
    x] [String] -> [String] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    take Int
    1 (String -> [String]
    words String
    arg)